다중 모드 검증기를 이용한 인증된 프로그램 합성

Certified Program Synthesis with a Multi-Modal Verifier

인증된 프로그램 합성(또는 베리코딩)은 자연어 설명을 기반으로 프로그램을 자동으로 생성하고, 해당 프로그램의 형식적인 명세와 함께 기계가 검증할 수 있는 증명을 생성하는 과정입니다. 베리코딩을 어렵게 만드는 두 가지 과제가 있습니다. 첫째, 자연어로부터 합성된 명세는 종종 의미가 없거나 너무 약하거나, 또는 구현 불가능하게 너무 강한 경우가 있는데, 기존 방법들은 이러한 결함을 체계적으로 탐지하는 수단이 부족합니다. 둘째, 프로그램 검증 도구의 환경은 단편화되어 있습니다. 각 도구는 특정 추론 모드(예: 자동 모드 - Dafny, Verus 또는 대화형 모드 - Coq, Lean)를 지원하며, 각 모드는 자동화와 표현력 간의 고유한 균형을 가지고 있습니다. 이는 모든 합성 방법론이 단일 검증 패러다임에 맞춰야 하므로, 효과적으로 처리할 수 있는 작업의 범위를 제한합니다. 저희는 다중 모드 검증기라는 단일 도구를 중심으로 인증된 합성 워크플로우를 구성함으로써 이러한 두 가지 과제를 모두 해결합니다. 이 도구는 동적 검증, 자동 증명, 그리고 대화형 증명 스크립팅을 하나의 기본 프레임워크로 결합합니다. 저희는 이 아이디어를 LeetProof라는 에이전트 기반 파이프라인에 구현했습니다. LeetProof는 Lean에 내장된 다중 모드 검증기인 Velvet를 기반으로 구축되었습니다. 다중 모드 기능은 LeetProof가 코드를 합성하기 전에 무작위 속성 기반 테스트를 통해 생성된 명세를 검증하고, 검증 조건을 기반으로 합성 작업을 하위 문제로 분해하며, Lean에 특화된 최첨단 AI 증명기를 사용하여 남은 증명 의무를 처리할 수 있도록 합니다. 저희는 LeetProof를 기존 인증된 합성 연구에서 파생된 벤치마크를 사용하여 평가했습니다. 저희의 명세 검증은 기존의 참고 벤치마크에서 결함을 발견했으며, LeetProof의 단계별 파이프라인은 동일한 예산 내에서 단일 모드 기반 모델보다 훨씬 높은 비율의 완전한 인증 솔루션을 달성했습니다. 이는 두 개의 최첨단 LLM 백엔드에서 일관되게 나타났습니다.

Certified program synthesis (aka vericoding) is the process of automatically generating a program, its formal specification, and a machine-checkable proof of their alignment from a natural-language description. Two challenges make vericoding difficult. First, specifications synthesised from natural language are often either too weak to be meaningful or too strong to be implementable, yet existing approaches lack systematic means to detect such defects. Second, the landscape of program verifiers is fragmented: each tool supports a particular reasoning mode -- auto-active (e.g., Dafny, Verus) or interactive (e.g., Coq, Lean) -- with its own trade-off between automation and expressivity. This forces every synthesis methodology to be tailored to a single verification paradigm, limiting the class of tasks it can handle effectively. We overcome both challenges by structuring the certified synthesis workflow around a multi-modal verifier -- a single tool combining dynamic validation, automated proofs, and interactive proof scripting in one foundational framework. We realise this idea in LeetProof, an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean. Multi-modality enables LeetProof to validate generated specifications via randomised property-based testing before any code is synthesised, decompose the synthesis task into sub-problems guided by verification conditions, and delegate residual proof obligations to frontier AI provers specialised for Lean. We evaluate LeetProof on benchmarks derived from prior work on certified synthesis. Our specification validation uncovers defects in existing reference benchmarks, and LeetProof's staged pipeline achieves a significantly higher rate of fully certified solutions than a single-mode baseline at the same budget -- consistently across two frontier LLM backends.