괴델 코드 프로버: 개방형 최첨단 코드 검증을 위한 계층적 증명 탐색

Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

대규모 언어 모델(LLM)은 그럴듯한 코드를 생성할 수 있지만, 정확성에 대한 제한적인 보장을 제공합니다. 구현이 명세사항을 만족하는지 형식적으로 검증하려면 기계가 확인할 수 있는 증명을 구성해야 하는데, 이는 현재 자동화 수준으로는 어려운 작업입니다. 우리는 Lean 4에서 자동 코드 검증을 위한 계층적 증명 탐색 프레임워크를 제안하며, 이 프레임워크는 전술 수준의 증명을 시도하기 전에 복잡한 검증 목표를 구조적으로 더 간단한 하위 목표로 분해합니다. 우리의 접근 방식의 핵심은 구성적인 정당성과 구조적 효율성을 결합하는 원칙적인 분해 점수이며, 이 점수는 학습 보상과 추론 시간 순위 기준 모두로 사용되어 최적화와 배포를 일치시킵니다. 우리는 지도 초기화 후 하이브리드 강화 학습을 통해 분해 및 완성 작업을 모두 처리하는 단일 통합 정책인 Goedel Code Prover를 훈련합니다. 여기서 연속적인 분해 보상은 계획 탐색을 지원하고, 지도 재학습은 증명 생성을 안정화시킵니다. Lean 기반의 세 가지 코드 검증 벤치마크에서 총 427개의 작업으로 구성된 데이터셋에서, 80억 개의 파라미터를 가진 우리의 모델은 62.0%의 성공률을 달성했으며, 이는 보고된 추론 설정 하에서 가장 강력한 기준 모델보다 2.6% 향상된 수치입니다. 또한, 우리는 일관된 추론 시간 스케일링을 관찰했습니다. 성공률은 탐색 반복 및 샘플링 예산 증가에 따라 꾸준히 개선되는 반면, 전체 증명 기반 모델은 평가된 예산 내에서 성능이 정체됩니다.

Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness. Formally verifying that implementations satisfy specifications requires constructing machine-checkable proofs, a task that remains beyond current automation. We propose a hierarchical proof search framework for automated code verification in Lean~4 that decomposes complex verification goals into structurally simpler subgoals before attempting tactic-level proving. Central to our approach is a principled decomposition score that combines constructive justification with structural effectiveness. The same score serves as both the training reward and the inference-time ranking criterion, aligning optimization and deployment. We train Goedel Code Prover, a single unified policy for both decomposition and completion, through supervised initialization followed by hybrid reinforcement learning, where a continuous decomposition reward supports planning exploration while supervised replay stabilizes proof generation. On three Lean-based code verification benchmarks comprising 427 tasks, our 8B-parameter model achieves a 62.0% prove success rate, a 2.6 improvement over the strongest baseline under the reported inference settings. We further observe consistent inference-time scaling: success rates improve monotonically with search iterations and sampling budget, while whole-proof baselines plateau within the evaluated budgets.