본 논문은 Lean 4 환경을 위한 새로운 오픈 소스 단계별 정리 증명 시스템인 REAL-Prover를 제시한다. 이는 고등학교 및 경쟁 수학 문제를 넘어 보다 진보된 수학 문제 해결을 목표로 한다. REAL-Prover는 fine-tuned large language model (REAL-Prover-v1)과 retrieval system (Leansearch-PS)을 통합하여 대학 수준의 수학 문제 해결 능력을 향상시켰다. REAL-Prover-v1의 학습을 위해, 자연어 수학 문제를 형식적 진술로 변환하는 데이터 추출 파이프라인 HERALD-AF와 데이터 수집을 용이하게 하는 Lean 4 interactive environment Jixia-interactive를 개발했다. Supervised fine-tuning만 사용하여 ProofNet 데이터셋에서 23.7%의 성공률 (Pass@64)을 달성하여 최첨단 모델과 경쟁력 있는 결과를 보였다. 또한, 대수 문제를 중심으로 하는 새로운 벤치마크 FATE-M에서 56.7%의 성공률 (Pass@64)로 SOTA를 달성했다.
시사점, 한계점
•
시사점:
◦
대학 수준의 수학 문제 해결 능력을 향상시킨 새로운 정리 증명 시스템 제시
◦
새로운 데이터 추출 파이프라인 HERALD-AF 및 Lean 4 interactive environment Jixia-interactive 개발
