LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics

Motivation

• Known: 기존 수학 벤치마크(GSM8K, MATH 등)는 학교~학부 수준 문제로 이미 포화 및 오염 문제가 있으며, FrontierMath, Soohak, First Proof, Leipzig Tier-4 등 전문가 큐레이션 기반 research-level 벤치마크는 비용이 크고 확장·갱신이 어렵다. RealMath, MathArena/ArxivMath, EternalMath 같은 arXiv 기반 live 벤치마크도 존재하지만 자동으로 검증 가능한 정답 형태의 문제로 한정된다.
• Gap: arXiv 원문의 lemma는 앞선 정의·가정에 강하게 의존하는 context-dependent 특성 때문에 그대로 벤치마크 문항으로 쓰기 어렵고, 기존 live 벤치마크들은 자동 채점 가능한 최종 답이 있는 문제로만 국한되어 자연어 증명 형태의 research-level lemma proving을 평가하지 못한다는 근본적 공백이 있다.
• Why: LLM이 실제 연구 수준 수학 증명을 얼마나 수행할 수 있는지를 오염 없이 지속적으로, 그리고 자연어 증명 형태로 측정할 수 있는 방법은 수학 연구에 LLM을 실제로 적용할 수 있는 시점을 가늠하는 데 중요하며, 특정 소수 연구자만 접근 가능한 특수 시스템이 아니라 일반 공개 LLM의 실질적 능력을 파악하는 데 실용적 의의가 있다.
• Approach: LiveCodeBench에서 영감을 받아, arXiv 최신 preprint에서 lemma를 추출하고 논문 내 다른 부분에서 필요한 가정과 정의를 자동으로 수집해 self-contained한 문항으로 재작성하는 파이프라인을 구축하고, 이를 통해 GPT-5, Gemini 2.5/3 Pro, Claude Opus 4.5, DeepSeek-R1 등 최신 LLM들을 pass@1 theorem proving 정확도로 평가한다.

Achievement

Figure 2. Evolution of proof quality of the best performing

1. Live 벤치마크 파이프라인 구축: arXiv에서 lemma를 자동 추출하고 self-contained 문항으로 변환하는 파이프라인을 제시해 주 단위로도 갱신 가능한 오염 방지 벤치마크를 실현했다.
2. 정확도 검증: 수동 검수를 통해 생성된 self-contained lemma 벤치마크가 수학적으로 정확하고 정밀함을 확인했다.
3. LLM 성능 추적: LLM-as-a-judge와 인간 전문가 검증을 결합해 신뢰도 있는 평가 체계를 마련하고, 최신 모델들이 지난 9개월간 이론 증명 정확도(pass@1)를 10-15%에서 40.8%까지 끌어올렸음을 정량적으로 보였다.
4. 재사용 가능한 데이터 자산화: 과거 데이터에도 동일 파이프라인을 적용해 대규모 고품질 학습 데이터셋 생성이 가능함을 보였고, 도메인별 세부 벤치마크 구성이 가능함을 제시했다.

How

Figure 1. Pipeline at a glance: the pipeline retrieves papers from

• arXiv 최신 preprint를 수집하여 lemma를 자동 추출
• 각 lemma가 의존하는 정의·가정·표기를 논문 내 다른 위치에서 자동으로 검색(retrieve)하여 self-contained statement로 재작성
• 학부 수준의 공통 배경 지식(실수/복소수체, 환, 가군, 연속성 등)은 이미 알려진 것으로 간주하고, 연구 특유의 개념만 명시적으로 포함
• 외부 prover(LLM)가 단계별로 증명을 시도하도록 하고, 결과 증명을 judge가 검사
• LLM-as-a-judge 평가와 함께 일부 증명 샘플에 대해 인간 전문가 수학자가 검증하여 judge의 신뢰도 점수를 산출
• GPT-5, Gemini 2.5 Pro, Gemini 3 Pro, Claude Opus 4.5, DeepSeek-R1을 baseline prover로 사용해 pass@1 정확도 비교

Originality

• 기존 arXiv 기반 live 벤치마크(RealMath, MathArena/ArxivMath, EternalMath)가 자동 검증 가능한 최종 답 문제로 국한된 것과 달리, 자연어 증명을 요구하는 research-level lemma proving을 목표로 삼은 최초의 접근
• context-dependent한 arXiv 정리를 self-contained 문항으로 자동 변환하는 파이프라인 자체가 참신하며, arXiv 데이터의 self-containedness 부족이라는 알려진 한계를 정면으로 다룸
• 과거 데이터에도 동일 파이프라인 적용이 가능해 평가용 벤치마크와 학습용 데이터셋 생성을 분리하지 않고 통합한 설계

Limitation & Further Study

• 자연어 증명 평가는 자동 채점이 어려워 LLM-as-a-judge에 의존하는데, 이 judge의 신뢰도 자체가 인간 검증 서브셋에 의해서만 부분적으로 보정되어 완전한 신뢰성 확보는 어려움
• self-contained 여부 판단 기준(학부 수준 배경지식 vs 연구 특유 개념)이 다소 주관적이며 도메인/난이도별 편차가 존재할 수 있음
• 발췌된 lemma가 원 논문 맥락에서 얼마나 대표성 있고 난이도가 고른지에 대한 체계적 분석이 제한적으로 보임
• 후속 연구로 judge의 정밀도 향상, 다양한 수학 하위분야에 대한 세분화된 평가, formal proof 검증과의 결합 등을 고려할 수 있음

Evaluation

총평: arXiv 기반의 자동화된 self-contained lemma 추출과 자연어 증명 평가를 결합한 live 벤치마크라는 아이디어는 참신하고 실용적 가치가 크며, 최신 LLM들의 급격한 성능 향상과 여전한 격차를 잘 보여준다. 다만 LLM-as-a-judge에 대한 의존도와 self-containedness 판정 기준의 주관성은 향후 보완이 필요한 지점이다.