Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs

Motivation

• Known: 기존에는 final-answer 형태의 olympiad 벤치마크(GSM8K, MATH 등)와 proof-based, formal(Lean) 벤치마크들이 개별적으로 존재했으며, LMArena, Artificial Analysis 등 일반적인 evaluation platform도 존재했다.
• Gap: 정적 벤치마크는 발표 후 유지보수가 되지 않아 빠르게 saturation되고, 단일 벤치마크로는 proof 생성, 연구 수준 문제, formal verification 등 다양한 수학적 능력을 포괄할 수 없으며, 기존 evaluation platform들은 수학 도메인에 특화되어 있지 않다는 한계가 있다.
• Why: LLM의 수학적 추론 능력이 빠르게 발전하는 상황에서 신뢰할 수 있는 최신 성능 지표가 없다면 연구자와 실무자는 모델 개발사의 자체 보고 수치나 소규모 비공식 테스트에 의존할 수밖에 없어, 지속적이고 투명한 평가 체계의 부재는 진행 상황 추적과 모델 비교에 심각한 문제를 야기한다.
• Approach: 저자들은 기존 MathArena 벤치마크를 proof-based 대회, arXiv 기반 research-level 문제(참/거짓 판별 포함), Lean 기반 formal proof generation을 포괄하는 evaluation platform으로 확장하고, 명확한 평가 프로토콜과 정기적인 벤치마크 추가·모델 평가 체계를 구축했다.

Achievement

Figure 2. Performance over time.

1. Evaluation platform 패러다임 제시: 벤치마크와 구분되는 evaluation platform의 설계 요구사항(지속적 유지, 다양성, 상세 분석 인터페이스, 벤치마크의 추가/제거/갱신)을 논의했다.
2. MathArena의 확장: 기존 final-answer olympiad 중심 벤치마크를 proof-based competitions, arXiv 기반 research-level 문제, false claim rejection, Lean 기반 정형 증명까지 포괄하도록 확장했다.
3. 최신 모델 성능 분석: GPT-5.5가 2026 USAMO에서 98%, research-level 문제에서 74%를 달성함을 보였고, DeepSeek-v4-Pro가 최강 오픈모델임을 확인했으며, 전체 평균 성능이 1년 만에 45%에서 84%로 상승했음을 정량화했다.
4. 다각적 강건성 분석: 비용 대비 성능(Fig 3), human-validated 점수와의 격차(Fig 4), leave-one-family-out을 이용한 순위 강건성(Fig 5), 신뢰구간 커버리지 검증(Fig 6) 등 플랫폼 신뢰성을 뒷받침하는 다양한 분석을 제공했다.

How

• 기존 MathArena의 final-answer 대회 문제 세트에 IMC 2025, Kangaroo 2025, Miklós Schweitzer 2025, Putnam 2025 등 proof-based 대회 벤치마크를 추가
• arXiv 논문에서 추출한 research-level 문제(ArXivMath)와 의도적으로 조작된 거짓 주장(BrokenArXiv)을 포함하는 벤치마크 도입
• Lean을 이용한 formal proof generation 벤치마크(ArXivLean) 구축
• 인간 채점(human grading)을 병행하여 LLM judge의 편향 문제를 보완
• 지연시간(latency), 비용(expected cost), API 안정성 등 실용적 지표를 함께 측정하는 GUI/인터페이스를 지속적으로 개선
• 신규 모델(GPT-5.5, DeepSeek-v4-Pro 등)을 정기적으로 평가에 추가하고 blog post를 통해 상세 분석 공개

Originality

• 단발성 벤치마크 논문이 아니라 지속적으로 운영되는 evaluation platform이라는 개념을 수학 추론 평가 영역에 명시적으로 도입
• final-answer, proof-based, formal(Lean), research-level(참/거짓 판별 포함) 등 이질적인 평가 유형을 하나의 플랫폼으로 통합
• 모든 모델 출력과 코드를 공개하는 완전 개방형 구조로 LMArena, Artificial Analysis 등 기존 범용 플랫폼과 차별화
• 인간 채점과 자동 채점을 병행하며 LLM judge의 self-preference 편향 문제를 완화하려는 시도

Limitation & Further Study

• Proof-based 벤치마크의 인간 채점은 확장성이 떨어져 지속적 유지에 비용이 크게 소요될 수 있음
• Lean 기반 정형 증명 벤치마크는 agentic 시스템 사용 시 문제당 $50 이상 소요되는 등 비용 문제가 여전히 존재
• LLM이 거짓 명제를 증명했다고 주장하는 경우가 빈번하다는 점은 research-level 평가의 신뢰성에 대한 근본적 도전 과제로 남아 있음
• 향후에는 채점 자동화의 신뢰성 제고, 비용 효율적인 Lean 평가 파이프라인 개발, 더 다양한 언어·분야로의 확장이 필요해 보임

Evaluation

총평: 정적 벤치마크의 한계를 명확히 지적하고 이를 지속 가능한 evaluation platform으로 전환한 실용적이고 시의적절한 연구로, 수학 추론 분야에서 LLM 발전 상황을 투명하게 추적하는 데 크게 기여할 것으로 평가된다.