Leanabell-Prover: Posttraining Scaling in Formal Reasoning
Created by
Haebom
저자
Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, Kun Gai
개요
본 논문은 최근 대규모 언어 모델(LLM)을 활용한 자동 정리 증명(ATP) 분야의 발전에도 불구하고, OpenAI O1/O3 및 DeepSeek R1과 같은 사후 훈련 확장이 ATP에 혁명적인 변화를 가져오지 못했다는 점을 지적합니다. 따라서 기존 ATP 모델을 다양한 명제-증명 쌍과 인간 추론 및 가설 개선을 모방하는 추가 데이터로 구성된 혼합 데이터셋을 사용하여 지속적으로 훈련하는 방법을 제시합니다. 또한 Lean 4 컴파일러의 결과 보상을 활용한 강화 학습을 통해 DeepSeek-Prover-v1.5 및 Goedel-Prover와 같은 기존 형식적 증명기를 개선하여 MiniF2F에서 59.8%의 통과율(pass@32)을 달성하는 등 최첨단 성능을 달성했습니다. 본 연구는 진행 중이며, 지속적인 결과 업데이트와 데이터 및 훈련 세부 정보 공개를 약속합니다.
시사점, 한계점
•
시사점:
◦
LLM 기반 ATP 모델의 사후 훈련을 통해 기존 형식적 증명기의 성능을 향상시킬 수 있음을 보여줌.
