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과 같은 사후 훈련 확장(post-training scaling)이 ATP 분야에 혁신을 가져오지 못한 점을 지적합니다. 따라서 기존 ATP 모델들을 지속적인 학습(continual training)과 강화 학습(reinforcement learning)을 통해 개선하고자 합니다. 구체적으로, 명제-증명 쌍 데이터와 인간 추론 및 가설 개선을 모방하는 추가 데이터를 사용한 혼합 데이터셋으로 기존 ATP 모델을 지속적으로 학습시키고, Lean 4 컴파일러의 결과 보상을 활용한 강화 학습을 수행합니다. 그 결과 DeepSeek-Prover-v1.5와 Goedel-Prover를 포함한 기존의 형식적 증명기를 개선하여 전체 증명 생성 분야에서 최첨단 성능을 달성하였으며, MiniF2F에서 59.8%의 통과율(pass@32)을 기록하였습니다. 본 연구는 진행 중이며, 지속적으로 결과를 업데이트하고 데이터 및 훈련 세부 정보를 공개할 예정입니다.
시사점, 한계점
•
시사점:
◦
LLM 기반 ATP 모델의 성능 향상을 위한 지속적 학습 및 강화 학습 기법의 효과성을 보여줌.
