Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
Created by
Haebom
저자
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, Chi Jin
개요
Goedel-Prover-V2는 자동 정리 증명 분야에서 새로운 최첨단 기술을 제시하는 일련의 오픈소스 언어 모델입니다. 표준 전문가 반복 및 강화 학습 파이프라인을 기반으로 하며, 점진적으로 어려워지는 합성 과제를 생성하여 모델이 점점 더 복잡한 정리를 숙달하도록 훈련하는 'Scaffolding data synthesis', Lean 컴파일러의 피드백을 활용하여 모델이 증명을 반복적으로 수정할 수 있도록 하는 'Verifier-guided self-correction', 훈련 후반부의 모델 출력 다양성 감소를 완화하기 위해 모델 체크포인트를 병합하는 'Model averaging'의 세 가지 핵심 혁신을 통합합니다. 소형 모델인 Goedel-Prover-V2-8B는 MiniF2F에서 84.6% pass@32를 달성하여 DeepSeek-Prover-V2-671B를 능가하며, 주력 모델인 Goedel-Prover-V2-32B는 표준 모드에서 88.1%, 자가 수정 모드에서 90.4%의 pass@32를 달성하여 기존 최고 성능을 크게 능가합니다. 또한 PutnamBench에서 86개의 문제를 해결하여 오픈소스 모델 중 1위를 차지하며, DeepSeek-Prover-V2-671B의 기록을 능가합니다. 2025년 7월-8월 출시 당시 모든 오픈소스 정리 증명기 중 가장 강력한 성능을 달성했으며, 제한된 테스트 시간 컴퓨팅 예산 하에서도 최고 성능 모델 중 하나로 자리매김했습니다. 모델, 코드 및 데이터는 https://github.com/Goedel-LM/Goedel-Prover-V2에서 공개됩니다.
시사점, 한계점
•
시사점:
◦
자동 정리 증명 분야에서 새로운 최첨단 기술을 제시.
◦
오픈소스로 공개되어 접근성과 연구 확장성 증대.
◦
소형 모델에서도 기존 대규모 모델을 능가하는 성능 달성.
◦
'Scaffolding data synthesis', 'Verifier-guided self-correction', 'Model averaging' 기법의 효과 입증.
◦
제한된 컴퓨팅 자원에서도 우수한 성능 발휘.
•
한계점:
◦
논문에서 명시적으로 언급된 한계점은 없음. 추가적인 실험 및 분석을 통해 한계점을 밝힐 필요가 있음.
