REAL-Prover는 Lean 4를 위한 새로운 오픈소스 단계적 정리 증명기로, 고등학교 및 경시 수준의 수학 문제 해결에 있어 눈에 띄는 발전을 이룬 기존 형식적 정리 증명기의 한계를 뛰어넘고자 개발되었습니다. 대학 수준의 수학 문제 해결 성능을 향상시키기 위해 미세 조정된 대규모 언어 모델(REAL-Prover-v1)과 검색 시스템(Leansearch-PS)을 통합하였습니다. REAL-Prover-v1을 훈련하기 위해 자연어 수학 문제를 형식적 명제로 변환하는 데이터 추출 파이프라인인 HERALD-AF와 합성 데이터 수집을 용이하게 하는 새로운 오픈소스 Lean 4 대화형 환경인 Jixia-interactive를 개발했습니다. ProofNet 데이터셋에서 지도 학습 미세 조정만으로 최첨단 모델들과 비슷한 23.7%(Pass@64)의 성공률을 달성했습니다. 대수 문제에 중점을 둔 새로운 벤치마크인 FATE-M에서 56.7%(Pass@64)의 최첨단 성공률을 달성하여 성능을 추가적으로 평가했습니다.
시사점, 한계점
•
시사점:
◦
대학 수준 수학 문제 해결에 효과적인 새로운 오픈소스 정리 증명기 REAL-Prover 제시
◦
대규모 언어 모델과 검색 시스템 통합을 통한 성능 향상
◦
자연어 수학 문제를 형식적 명제로 변환하는 데이터 파이프라인 HERALD-AF 및 대화형 환경 Jixia-interactive 개발
◦
ProofNet 및 FATE-M 데이터셋에서 최첨단 성능 달성
•
한계점:
◦
현재는 대수 문제에 초점을 맞추고 있어 다른 수학 분야로의 일반화 가능성에 대한 추가 연구 필요
◦
FATE-M 데이터셋은 새롭게 제시된 것이므로, 다른 기존 벤치마크와의 비교 분석이 더 필요함
