miniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

Motivation

• Known: Interactive theorem prover(ITP; Lean, Isabelle, Rocq 등)는 수학 정리 증명에서 지배적 패러다임이며 miniF2F, PutnamBench 등의 벤치마크로 LLM 성능이 평가되어 왔다. 반면 auto-active verifier(Dafny, Why3, F*, Verus 등)는 SMT 솔버 기반 자동화를 통해 소프트웨어 검증에 주로 활용되며 DafnyBench, VerifyThis 등으로 LLM 성능이 평가되어 왔다.
• Gap: ITP를 이용한 소프트웨어 검증(CLEVER, Verina)에 대한 LLM 평가는 이루어졌지만, 그 반대 방향인 auto-active verifier를 이용한 순수 수학 정리 증명에 대한 LLM 능력 평가는 전혀 탐구되지 않았다.
• Why: 암호학적 구현이나 확률적 보장을 갖는 프로그램처럼 깊은 수학적 추론과 소프트웨어 검증이 동시에 필요한 안전-critical 소프트웨어의 경우, ITP와 auto-active verifier 중 하나만 선택해야 하는 현재의 이분법적 구조가 큰 제약이 되므로, 두 패러다임을 잇는 실증적 토대를 마련하는 것이 중요하다.
• Approach: miniF2F 벤치마크를 Dafny로 최초 번역한 MINIF2F-DAFNY를 구축하고, Dafny의 자동화만으로 해결 가능한 문제 비율을 baseline으로 측정한 뒤, 8개의 기성(off-the-shelf) LLM이 SMT 자동화를 보조하는 증명 힌트(ghost code, assertion, lemma 등)를 생성하도록 하여 pass@4 성능을 평가한다.

Achievement

1. MINIF2F-DAFNY 벤치마크 구축: miniF2F를 auto-active verifier 언어인 Dafny로 최초 번역하여, ITP 중심이었던 수학 추론 평가를 auto-active 환경으로 확장했다.
2. Dafny 자동화 baseline 확립: 테스트셋의 38.9%(95/244), 검증셋의 43.4%(106/244) 문제가 빈 증명(empty proof)만으로 Dafny의 SMT 자동화에 의해 해결됨을 보였으며, 이는 Lean의 grind tactic(32.4%, 79/244)보다 높은 수치이다.
3. 상호보완적 자동화 프로파일 분석: Dafny와 grind가 함께 해결한 107개 문제 중 67개는 공통, 28개는 Dafny 전용(mathd_algebra, mathd_numbertheory에 집중), 12개는 grind 전용임을 밝혀 두 시스템의 증명 패턴 차이를 규명했다.
4. LLM 기반 증명 힌트 생성 평가: 8개 LLM을 평가하여 최고 성능 모델인 Claude Opus 4.6이 전체 테스트셋에서 62.7% 누적 pass@4를 달성, empty-proof baseline(38.9%) 대비 23.8%p 향상을 보였다.
5. 증명의 간결성·가독성 확인: 범용 모델과 제한된 컴퓨팅 자원, 최적화되지 않은 수학 라이브러리로도 Lean 대비 짧고 사람이 읽기 쉬운 증명을 생성함을 보였다.

How

• miniF2F의 문제들을 Dafny의 lemma/method 구문과 Hoare triple 스타일 requires/ensures 명세로 번역하여 정의 및 라이브러리 파일과 함께 구성
• Dafny 컴파일 파이프라인을 통해 Weakest Precondition calculus 기반으로 Boogie 중간표현을 생성하고 Verification Condition(VC)을 산출, Z3 SMT 솔버로 검증
• 빈 증명(empty proof) 상태로 자동화만으로 해결되는 문제 비율을 측정해 baseline 성능 산정
• Lean의 grind tactic과 문제별 해결 여부를 비교하여 두 자동화 방식의 중복 및 배타적 해결 문제 집합 분석
• 8개의 off-the-shelf LLM에게 문제 명세를 제공하고 ghost code(assertion, lemma, calculational proof 등) 형태의 증명 힌트를 생성하도록 요청, Dafny 검증기로 피드백을 받아 pass@4 지표로 누적 성공률 측정

Originality

• ITP 중심이었던 AI 수학 정리 증명 벤치마크 지형(Table 1)에서 auto-active verifier 방향의 빈 칸을 최초로 채운 벤치마크 제안
• 소프트웨어 검증 도구로 여겨지던 Dafny를 순수 수학(pure mathematics) 영역에 적용하여 SMT 자동화와 LLM 고수준 안내의 역할 분담이라는 새로운 실증적 프레임을 제시
• Dafny와 Lean grind의 baseline 자동화 능력을 직접 비교하여 두 패러다임의 상호보완성을 정량적으로 규명한 최초 분석

Limitation & Further Study

• Dafny로의 miniF2F 번역 과정에서 원본 정리의 수학적 표현이 완전히 동일하게 보존되는지, 번역 충실도(fidelity) 검증이 상세히 제시되지 않음
• 평가된 8개 LLM이 모두 범용 모델이며, ITP에 특화된 SeedProver나 Aristotle 같은 특수 목적 시스템/에이전틱 프레임워크와 직접적인 성능 비교가 제한적임
• pass@4라는 상대적으로 적은 샘플링 횟수와 모의 컴퓨팅 예산 하의 결과이므로, 대규모 agentic 파이프라인이나 반복적 상호작용을 적용했을 때의 성능 상한은 추가 연구가 필요함
• Dafny의 수학 라이브러리가 아직 최적화되지 않은 상태로 언급되어, 향후 라이브러리 고도화에 따른 성능 변화 가능성이 남아있음

Evaluation

총평: ITP 중심으로 편중되어 있던 AI 수학 정리 증명 연구에 auto-active verifier라는 새로운 실증적 축을 도입한 참신하고 시의적절한 벤치마크 논문으로, 향후 두 패러다임을 결합한 하이브리드 검증 연구의 토대를 제공할 것으로 기대된다.