mathematical-reasoning formal-verification qwen3-4b proof-verification ai-generated-proofs lean-proof-assistant verification-benchmarks lean-prm
Abstract
AI systems now write long and difficult mathematical proofs, and checking their step-by-step validity is becoming a bottleneck. A learned verifier could check proofs cheaply, but training one requires a correctness label on every step, and such labels are hard to obtain for open-ended proofs. Existing methods take them from human annotators, which is costly, or derive them from final answers, which proofs do not have, and formalizing each proof in Lean requires expert effort. We introduce LeanPRM, a framework that uses the Lean proof assistant to create step-level labels for natural-language proofs. A model writes a natural-language proof together with a paired formal proof, without feedback from Lean. Lean then labels every step, and a second model discards failures caused only by the formal syntax, so that the negative labels mark errors in the mathematics. LeanPRM contains 10,634 proofs with 152K labeled steps and no human annotation. A Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy on a held-out set of 200 proofs (LeanPRM-Bench) from 48.2 to 74.7, as opposed to 60.3 when the same base model is trained on PRM800K. It also selects better proofs in best-of-N selection on IMO-level problems, and outperforms the PRM800K-trained verifier on three of four external verification benchmarks. Training on LeanPRM improves verifiers at every size from 0.6B to 8B parameters on LeanPRM-Bench, Hard2Verify and IMO-GradingBench. Given the labels need no human annotation, LeanPRM can grow with the supply of formal statements, offering a path to step-level feedback on AI-generated proofs that are hard for humans to check.
한국어 요약
한 줄 요약
LeanPRM은 Lean 프로빙 어시스턴트를 활용해 자연어 증명의 단계별 정확도를 라벨링하는 프레임워크로, Qwen3-4B 모델로 74.7%의 정확도를 달성했다.
핵심 기여도
- LeanPRM: 10,634개의 자연어 증명에 152,005개의 단계 라벨을 포함한 데이터셋.
- LeanPRM-Bench: 200개의 자연어 증명을 포함한 평가 벤치마크.
- Qwen3-4B 모델로 LeanPRM-Bench에서 정확도 74.7% 달성 (기존 PRM800K 기반 모델 대비 +14.4% 향상).
- 0.6B~8B 파라미터 모델 모두에서 LeanPRM-Bench, Hard2Verify, IMO-GradingBench에서 성능 향상.
핵심 아이디어
LeanPRM은 자연어 증명의 단계별 정확도를 라벨링하기 위해 Lean 프로빙 어시스턴트를 활용하는 새로운 프레임워크이다. 기존 방법은 인간 라벨러나 최종 답변 기반의 라벨링을 사용했지만, 이는 비용이 높거나 증명 구조에 맞지 않았다. LeanPRM은 모델이 자연어 증명과 함께 형식적 증명을 생성하고, Lean이 단계별로 검증하여 라벨을 생성한다. 이후, 두 번째 모델이 형식적 문법 오류만 제거하여 수학적 오류만 남긴다. 이 방식은 인간 라벨 없이도 정확한 단계 라벨을 생성할 수 있으며, AI 생성 증명의 검증을 자동화할 수 있는 기반을 제공한다.
기술적 접근법
- **LeanPRM 데이터셋 생성**: 모델이 자연어 증명과 형식적 증명을 생성하고, Lean이 단계별로 검증.
- **라벨링 과정**: 첫 번째 실패 단계 이후 모든 단계는 부정확으로 라벨링. 형식적 문법 오류는 별도 모델로 제거.
- **학습 알고리즘**: Qwen3-0.6B, 4B, 8B 모델을 사용. Group Relative Policy Optimization (GRPO)로 학습.
- **하이퍼파라미터**: 학습률 1e-6, KL 페널티 계수 1e-3, importance ratio 클리핑 [0.8, 1.26].
- **평가 지표**: R_c (정확한 단계 정확도), R_i (오류 단계 정확도), R_step (단계 정확도), r (종합 점수).
주요 결과
- **LeanPRM-Bench**: Qwen3-4B 모델로 정확도 74.7% 달성 (기존 PRM800K 기반 모델 대비 +14.4%).
- **Hard2Verify**: +9.7% 향상.
- **IMO-GradingBench**: +9.4% 향상.
- **모델 규모별 성능**: 0.6B, 4B, 8B 모델 모두에서 LeanPRM-Bench, Hard2Verify, IMO-GradingBench에서 향상.
- **Best-of-N 선택**: 16개 증명 중 35.9% 정확도 달성 (랜덤 선택 대비 +3.5%).
의의 및 한계
LeanPRM은 인간 라벨 없이도 자연어 증명의 단계별 정확도를 생성할 수 있는 첫 번째 프레임워크로, AI 증명 검증의 신뢰성을 높이는 데 기여한다. 특히, LeanPRM-Bench와 같은 평가 벤치마크를 제공하여 연구자들이 모델 성능을 비교할 수 있도록 지원한다. 그러나, 형식적 증명 생성에 오류가 발생할 경우, 일부 수학적 오류가 누락될 수 있으며, 이는 라벨링 정확도에 영향을 줄 수 있다. 또한, 모델이 생성한 증명의 형식적 구조가 불완전할 경우, Lean 검증이 실패할 수 있어 추가적인 개선이 필요하다.
실용적 활용
LeanPRM은 수학, 논리, 알고리즘 등 복잡한 증명이 필요한 연구 분야에서 AI 증명 검증을 자동화하는 데 활용될 수 있다. 특히, 대규모 수학 문제 해결, 자동화된 교육 피드백, 수학적 추론 모델 개발 등에 적용 가능하다.