MA-ProofBench는 수리해석학(Mathematical Analysis) 전용으로는 최초로 알려진 형식 정리증명 벤치마크로, 측도·적분론, 복소해석, 함수해석 등 6개 핵심 주제와 27개 하위범주를 아우르는 형식화된 정리 200개를 담는다. 문제는 학부 수준(레벨 I, 100개)과 박사 자격시험 수준(레벨 II, 100개)으로 나뉘며, 각 문제는 사람 주도·LLM 보조 형식화 파이프라인과 독립 전문가 검토를 거쳐 원래 수학에 충실하도록 구성됐다. 최신 추론 모델과 형식 증명기를 평가한 결과 대부분 저조했는데, 최고 성능 GPT-5.5조차 레벨 I에서 Pass@8 16%, 레벨 II에서 5%에 그쳤고 대부분 모델은 레벨 II에서 0%에 가까웠다. 주된 실패 원인은 Mathlib 환각과 미완성 증명이었으며, 고난도 영역의 형식 수학 추론 진전을 추적할 신뢰 기준으로 제시된다.

• •수리해석학 전용 최초의 형식 정리증명 벤치마크, 6개 주제·27개 하위범주의 형식화 정리 200개
• •학부(레벨 I)와 박사 자격시험(레벨 II) 두 난이도로 구성, 사람 주도·전문가 검토 파이프라인
• •최고 성능 GPT-5.5도 레벨 I Pass@8 16%, 레벨 II 5%에 그쳐 대부분 모델이 고난이도에서 사실상 실패
• •주요 실패 원인은 Mathlib 환각과 미완성 증명
• •자연어 버전 평가에서 비형식 추론과 형식 추론 사이의 명확한 격차 드러남