본 논문은 대규모 언어 모델(LLM) 기반의 정형 정리 증명 능력을 평가하기 위해, 기존 수학 경시대회 벤치마크의 한계를 넘어선 새로운 벤치마크 FATE (Formal Algebra Theorem Evaluation)를 제시한다. FATE는 추상 대수학과 가환 대수학 분야의 200개 문제를 포함하며, 학부 수준부터 박사 학위 예비 시험 수준을 넘어서는 난이도를 가진다. 특히, FATE-X는 박사 수준의 난이도를 넘어서고 Mathlib 라이브러리의 범위를 초과하는 최초의 정형 벤치마크이다. 최첨단 LLM 증명자를 FATE에서 평가한 결과, 경시대회 수학에 비해 현저히 낮은 성능을 보였으며, 자연어 추론 능력보다 형식화 능력에서 더 큰 어려움을 겪는 것으로 나타났다.
시사점, 한계점
•
시사점:
◦
FATE는 연구 수준의 정형 수학적 추론을 향한 중요한 이정표를 제시하는 강력하고 도전적인 벤치마크이다.
