LLM(대규모 언어 모델)의 수학적 해석학 분야 형식 정리 증명 능력을 평가하는 벤치마크 MA-ProofBench가 2026년 6월 11일 arXiv(2606.13782)에 공개됐다. 기존 형식 벤치마크들이 형식화하기 쉬운 대수학과 초등 정수론에 집중해 깊은 추론이 필요한 하위 분야, 특히 수학적 해석학의 커버리지가 제한적이라는 문제를 보완하기 위해 개발됐다. 연구팀은 MA-ProofBench가 수학적 해석학에 특화된 최초의 형식 정리 증명 벤치마크라고 밝혔다.
이 벤치마크에는 측도 및 적분론, 복소해석학, 함수해석학을 포함한 6개 핵심 주제와 27개 하위 범주를 아우르는 200개의 형식화된 정리가 수록됐다. 문제는 학부 수준(Level I, 100문제)과 박사 자격시험 수준(Level II, 100문제)의 두 난이도로 구분된다. 각 문제는 사람 주도·LLM 보조 형식화 파이프라인을 거쳐 전문가 독립 검토를 통해 원래 수학적 내용에 충실함을 확인했다.
최근 범용 추론 모델과 형식 정리 증명기들을 평가한 결과는 LLM의 형식 수학 추론 능력이 여전히 크게 부족함을 드러낸다. 가장 높은 성능을 보인 GPT-5.5도 Level I에서 Pass@8 기준 16%, Level II에서 5%에 그쳤으며, 대부분의 모델은 Level II에서 0%에 가까운 결과를 보였다. 주요 실패 원인으로는 Mathlib 환각과 불완전한 증명이 지목됐다. 연구팀은 자연어 버전 평가에서 비형식·형식 추론 간 뚜렷한 격차가 드러났다며, MA-ProofBench가 고급 영역 형식 수학 추론 발전을 추적하는 신뢰할 수 있는 참조 기준이 되기를 기대한다고 밝혔다.
