CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

Motivation

• Known: miniF2F, FIMO, PutnamBench, ProofNet 등 기존 formal mathematics benchmark들이 존재하며, 이들은 대수·기하·정수론 문제에서는 어느 정도 인간 수준의 성능을 보이는 neurosymbolic 접근(LLM+정형 증명기)의 발전을 뒷받침해왔다.
• Gap: 기존 벤치마크들은 combinatorics 문제를 거의 다루지 않거나(Lean 4 미지원, 소수 문제만 포함) Lean 3 기반이라 최신 도구와 호환되지 않으며, Mathlib의 combinatorics 관련 라이브러리 커버리지도 제한적이다. 또한 AlphaProof, Seed-Prover와 같은 최신 시스템들도 IMO에서 유독 combinatorics 문제를 풀지 못하는 공통된 병목을 보이는데, 이를 체계적으로 평가할 표준 방법론(특히 fill-in-the-blank 문제 평가)이 부재했다.
• Why: combinatorics는 비정형 진술과 정형 진술 간 격차가 다른 분야보다 크고 문제별 고유 정의가 필요한 경우가 많아, 이 영역에서 LLM의 정형 추론 능력을 정밀하게 측정하는 것이 AI의 수학적 추론 한계를 이해하고 개선하는 데 중요한 지표가 된다.
• Approach: 저자들은 중학교 수준부터 IMO, 대학 수준까지 걸친 10개 이상의 조합수학 주제를 포괄하는 100개의 문제를 Lean 4로 정형화하고, 서술형과 빈칸 채우기 문제를 모두 평가할 수 있는 Fine-Eval이라는 2단계/1단계 평가 파이프라인을 Kimina Lean Server 백엔드와 함께 제안한다.

Achievement

Figure 1. Code length distribution

1. CombiBench 구축: 2000년 이후 모든 IMO combinatorics 문제(이미지 포함된 IMO 2004 Problem 3 제외)를 포함해 100개의 Lean 4 정형화 문제와 대응 비정형 진술을 제작했다.
2. Lean 4 친화적 combinatorics 특화 벤치마크 최초 제공: 기존 벤치마크 대비(Table 1) combinatorics 문제 비율이 100%로, PutnamBench(4.4%)나 다른 벤치마크(0%)를 크게 상회한다.
3. Fine-Eval 프레임워크 제안: 서술형 증명뿐 아니라 fill-in-the-blank 문제의 해 생성과 검증을 모두 지원하는 최초의 표준화된 정형수학 평가 방법을 제시했다.
4. 최신 LLM 벤치마킹: state-of-the-art LLM들이 CombiBench 문제의 48%만 해결함을 보여, combinatorics 영역의 난이도와 평가 필요성을 입증했다.

How

Figure 2. Pipeline of the two-stage FINE-EVAL.

• 2000년 이후 IMO combinatorics 문제 전수 및 중학교~대학 수준의 다양한 문제를 선정해 Lean 4로 정형화하고 대응 비정형 진술을 페어링
• 10개 이상의 combinatorics 하위 주제(예: 그래프 이론, 조합 최적화 등으로 추정)를 포괄하도록 난이도와 주제를 다양화
• 서술형 문제와 fill-in-the-blank 문제를 모두 처리할 수 있도록 Fine-Eval을 2단계(two-stage) 파이프라인(Figure 2)과 1단계(one-stage) 파이프라인(Figure 3)으로 설계: 모델이 답을 생성한 뒤 Lean으로 정답 여부와 증명 유효성을 검증
• Kimina Lean Server를 백엔드로 사용해 실제 Lean 컴파일/검증을 자동화하고, 이를 통해 여러 LLM의 CombiBench 성능을 측정
• 문제 코드 길이 분포(Figure 1)를 분석하여 벤치마크의 복잡도 스펙트럼을 제시

Originality

• 기존에 다뤄지지 않았던 combinatorics 전용 Lean 4 벤치마크를 처음으로 제시
• fill-in-the-blank 유형의 정형 수학 문제에 대한 평가 방법론(Fine-Eval)을 세계 최초로 도입, 기존 방법들이 서술형 증명 평가에만 국한되어 있던 한계를 해결
• IMO 2000년 이후 combinatorics 문제 전수를 포함시켜 AlphaProof, Seed-Prover 등 최신 시스템들이 공통으로 실패한 영역을 직접 겨냥한 진단적 벤치마크 설계

Limitation & Further Study

• 문제 수가 100개로 상대적으로 적어 통계적 신뢰도나 다양한 세부 주제별 심층 분석에는 한계가 있을 수 있음
• combinatorics 특성상 문제별 고유 정의를 Lean으로 추가해야 하는 경우가 많아 정형화 과정의 일관성 및 확장성에 대한 논의가 더 필요함
• Mathlib의 combinatorics 라이브러리 자체가 아직 제한적이라는 근본 원인은 CombiBench만으로 해결되지 않으며, 후속 연구로 라이브러리 확장과 벤치마크 규모 확대가 필요
• 발췌된 부분만으로는 Fine-Eval의 정답 검증 알고리즘 세부 사항(특히 fill-in-the-blank 정답의 동치성 판별 방법)에 대한 기술적 엄밀성을 완전히 평가하기 어려움

Evaluation

총평: 조합수학이라는 formal theorem proving의 취약 영역을 정면으로 겨냥한 시의적절하고 실용적인 벤치마크이며, fill-in-the-blank 평가 프레임워크라는 방법론적 기여도 함께 제시하여 향후 LLM 기반 정형 수학 연구에 중요한 진단 도구가 될 것으로 기대된다.