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 컴파일러의 결과 보상을 활용한 강화 학습을 통해 ATP 성능 향상을 시도합니다. DeepSeek-Prover-v1.5 및 Goedel-Prover와 같은 기존 형식 증명기를 개선하여 MiniF2F에서 59.8%의 통과율(pass@32)을 달성하는 등 최첨단 성능을 달성했습니다. 본 연구는 진행 중이며, 지속적인 업데이트와 데이터 및 훈련 세부 정보 공개를 약속합니다.
시사점, 한계점
•
시사점:
◦
LLM 기반 ATP 모델의 성능 향상을 위한 지속적 학습 및 강화 학습 기법의 효과를 실증적으로 보여줍니다.
◦
하이브리드 데이터셋을 활용하여 인간 추론 과정을 모방함으로써 ATP 모델의 성능 향상 가능성을 제시합니다.
◦
MiniF2F 데이터셋에서 state-of-the-art 성능 달성을 통해 연구의 유효성을 입증합니다.
