REAL-Prover는 Lean 4를 위한 새로운 오픈소스 단계적 정리 증명기로, 고등 수학 및 경시 수준을 넘어 대학 수준의 수학 문제 해결을 목표로 한다. 미세 조정된 대규모 언어 모델 REAL-Prover-v1과 검색 시스템 Leansearch-PS를 통합하여 성능을 향상시켰다. 자연어 수학 문제를 공식적인 명제로 변환하는 데이터 추출 파이프라인 HERALD-AF와 합성 데이터 수집을 위한 Lean 4 대화형 환경 Jixia-interactive를 개발하여 REAL-Prover-v1을 훈련시켰다. ProofNet 데이터셋에서 23.7%의 성공률(Pass@64)을 달성했으며, 대수 문제에 집중한 새로운 벤치마크 FATE-M에서는 56.7%(Pass@64)의 최첨단 성공률을 기록했다.
시사점, 한계점
•
시사점:
◦
대학 수준의 수학 문제 해결에 도전하는 새로운 오픈소스 정리 증명기 REAL-Prover 제시.
◦
대규모 언어 모델과 검색 시스템 통합을 통한 성능 향상.
◦
새로운 데이터셋 생성 파이프라인 (HERALD-AF) 및 대화형 환경 (Jixia-interactive) 개발.
◦
ProofNet 및 새로운 벤치마크 FATE-M에서 경쟁력 있는 성능 달성.
◦
오픈소스 공개를 통한 학계의 발전 기여.
•
한계점:
◦
아직 대학 수준 수학 문제 해결 성공률이 완벽하지 않음 (ProofNet 23.7%, FATE-M 56.7%).
◦
FATE-M은 대수 문제에만 집중되어 있어, 다른 수학 분야로의 일반화 가능성에 대한 추가 연구 필요.
◦
HERALD-AF 및 Jixia-interactive의 성능 및 확장성에 대한 추가적인 평가 필요.
