언어 모델(LM)은 신뢰할 수 있고 안전한 소프트웨어 구축을 위한 형식 검증(formal verification) 적용 장벽을 크게 낮추었습니다. 기존 접근 방식들은 일반적으로 verifier-in-the-loop 패러다임을 따르지만, verifier는 종종 증명이 어떻게 복구되어야 하는지에 대한 실행 가능한 신호가 거의 없는 거칠고 이진적인 합격/불합격 피드백만을 제공합니다. 최근 연구에 따르면 반례(counterexamples)는 증명 실패를 구체적인 프로그램 상태에 근거하여 제시함으로써 더 실행 가능한 피드백을 제공하지만, 추론 시간(inference time)에 유용한 반례를 생성하는 것은 비용이 많이 드는 반복적 정제 과정을 필요로 합니다. 우리는 Verus 증명 복구를 위한 LM 기반 프레임워크인 TopoVerus를 소개합니다. 이는 반례 안내 진단(counterexample-guided diagnosis)을 모델 역량으로 내재화하여 단일 패스에서 유용한 반례를 생성합니다. 우리의 핵심 통찰력은 반례 생성을 독립적인 검증 작업이 아니라 데이터 기반의 진단 목표로 훈련하는 것입니다. 즉, 어떤 조건 하에 반례가 주어질 때 모델이 안전하고 verifier를 통과하는 증명을 생성하도록 도움을 줄 수 있다면 그 반례는 유용합니다.
실패한 Verus 증명과 verifier 오류가 주어졌을 때, TopoVerus는 단일 궤적(trajectory) 내에서 구조화된 소스 레벨의 반례, 복구 근거(repair rationale), 그리고 복구된 증명을 생성하며, 이는 Verus 피드백과 증명-코드 안전 게이트를 이용한 강화학습(reinforcement learning, RL)으로 최적화됩니다. 불변성(invariant) 복구 순서를 안내하기 위해 TopoVerus는 귀납성 테스트(inductiveness tests)에서 파생된 불변성 의존성을 기반으로 하는 위상 그래프 보상(topological graph reward)을 가진 커리큘럼을 도입하여, 반례 생성이 동일한 위상적 순서를 따르도록 장려합니다.
471개의 문제에 대한 7개 Verus 벤치마크 전반에 걸쳐 TopoVerus는 가중 평균 Safe-Pass@1/Safe-Pass@3에서 각각 61.6%/72.2%를 달성하며, 가장 강력한 기준선인 Claude Sonnet 4.5보다 5.7/6.3 포인트 앞섰습니다. 또한 TopoVerus의 학습된 반례가 기존 LM 기반 증명 복구 접근 방식의 추론을 직접적으로 보강하여, 사슬 사고(chain-of-thought) 진단 대비 성공률을 64.3% 향상시킬 수 있음을 보여줍니다.