PaperlayerView exact revision on arXiv

Source-linked AI summary

CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

Junqi Liu, Xiaohan Lin, Jonas Bayer, Yael Dillies, Weijie Jiang, Xiaodan Liang, Roman Soletskyi, Haiming Wang, Yunzhou Xie, Beibei Xiong, Zhengfeng Yang, Jujian Zhang, Lihong Zhi, Jia Li, Zhengying Liu

arXiv:2505.03171v1cs.AI

TL;DR

Formal theorem-proving benchmarks and libraries offer limited support for combinatorics, despite its reported difficulty for models. The paper introduces a Lean 4 benchmark and a fill-in-the-blank evaluation method; its experiments find that existing models cannot solve most of the problems.

  • Problem

    Combinatorics has limited benchmark coverage and lacks relevant pre-built definitions, lemmas, and theorems in existing theorem libraries.

    Source: §1 · p. 2, §5 · p. 9

  • Method

    The paper presents 100 combinatorial problems formalized in Lean 4 and a two-stage fill-in-the-blank evaluation requiring a solution and proof, then equivalence verification when needed.

    Source: §1 · p. 3, §5 · p. 9

  • Results

    All existing models were unable to solve most CombiBench problems.

    Source: §5 · p. 9

  • Takeaways & Limitations

    Without relevant pre-built definitions, lemmas, and theorems, models must construct them from scratch when formalizing combinatorial problems.

    Source: §5 · p. 9

    Most problems took over 30 minutes to formalize; nearly every IMO-level problem took over 3 hours, and some took over 8 hours.

    Source: §3 · p. 5

Abstract

from arXiv · show

Neurosymbolic approaches integrating large language models with formal reasoning have recently achieved human-level performance on mathematics competition problems in algebra, geometry and number theory. In comparison, combinatorics remains a challenging domain, characterized by a lack of appropriate benchmarks and theorem libraries. To address this gap, we introduce CombiBench, a comprehensive benchmark comprising 100 combinatorial problems, each formalized in Lean~4 and paired with its corresponding informal statement. The problem set covers a wide spectrum of difficulty levels, ranging from middle school to IMO and university level, and span over ten combinatorial topics. CombiBench is suitable for testing IMO solving capabilities since it includes all IMO combinatorial problems since 2000 (except IMO 2004 P3 as its statement contain an images). Furthermore, we provide a comprehensive and standardized evaluation framework, dubbed Fine-Eval (for $\textbf{F}$ill-in-the-blank $\textbf{in}$ L$\textbf{e}$an Evaluation), for formal mathematics. It accommodates not only proof-based problems but also, for the first time, the evaluation of fill-in-the-blank questions. Using Fine-Eval as the evaluation method and Kimina Lean Server as the backend, we benchmark several LLMs on CombiBench and observe that their capabilities for formally solving combinatorial problems remain limited. Among all models tested (none of which has been trained for this particular task), Kimina-Prover attains the best results, solving 7 problems (out of 100) under both ``with solution'' and ``without solution'' scenarios. We open source the benchmark dataset alongside with the code of the proposed evaluation method at https://github.com/MoonshotAI/CombiBench/.

1 Introduction

Existing formal-mathematics benchmarks provide limited coverage of combinatorics, a field the paper identifies as a weak area for theorem-proving models. CombiBench and Fine-Eval address gaps in combinatorial benchmarking and fill-in-the-blank evaluation.

1 Introduction

  • Existing benchmarks have limitations for combinatorics: miniF2F is limited to high-school mathematics, FIMO and ProofNet use Lean 3, and PutnamBench has few combinatorial problems.A Lean 4 version of ProofNet is available in DeepSeek-Prover-V1.5.Source: §1 · p. 2
  • Combinatorics is described as the weakest area for theorem-proving models; AlphaProof solved 4 of 6 IMO problems in 2024, with its two unsolved problems being combinatorial.The paper identifies absent benchmarks, limited combinatorics coverage in Mathlib, and the larger informal-to-formal gap as contributing factors.Source: §1 · p. 2
  • CombiBench aims to provide standards for evaluating LLM capabilities in combinatorics, where benchmark coverage and formal-library resources are limited.Source: §1 · p. 2
  • CombiBench contains 100 combinatorial statements formalized in Lean 4 with informal descriptions, spanning middle-school to university difficulty and over ten topics.Source: §1 · p. 3
  • Fine-Eval extends formal-mathematics evaluation to fill-in-the-blank questions as well as proof-based problems.Such questions require generating a solution and verifying its correctness, unlike completing a proof of a given proposition.Source: §1 · pp. 2–3

2 Related work

The related work situates the benchmark against the IMO challenge, developments in automated theorem proving, and existing formal-mathematics benchmarks. It traces a shift toward LLM proof generation while noting that combinatorial coverage remains limited.

2.1 IMO

  • The IMO is a six-problem, two-day high-school competition spanning several mathematical areas, and has also been framed as an AI grand challenge [Challenge, 2019].Source: §2.1 · p. 3

2.2 Automated Theorem Proving

2.3 Existing Benchmarks

  • miniF2F covers high-school and undergraduate problems across formal systems; Kimina-Prover Preview [Wang et al., 2025] achieved 80.74% on its test set.Source: §2.3 · pp. 3–4
  • PutnamBench includes 26 combinatorial problems but has limited topic coverage, while LeanComb focuses on combinatorial identities whose proofs often use analytical techniques.Source: §2.3 · p. 4

3 CombiBench

CombiBench is a manually produced Lean 4 benchmark of 100 combinatorial problems, spanning varied difficulty levels and topics. Its problems draw from competitions and textbooks, and include tasks requiring a solution to be found before it is proved.

3 CombiBench

  • CombiBench is a manually produced benchmark of 100 combinatorial problems, with varied difficulty and knowledge levels.The problems are formalized in Lean 4 and paired with informal descriptions.Source: §3 · p. 4
  • Topic selection follows Brualdi’s textbook, which covers subjects including permutations, generating functions, graph theory, and combinatorial design.The book has 14 chapters and is widely used in undergraduate and graduate combinatorics courses.Source: §3 · p. 4
  • The benchmark combines 10 easy problems, 42 Brualdi exercises, 36 IMO problems, and 12 problems from other competitions.The 42 Brualdi exercises were randomly sampled as three problems from each of 14 chapters.Source: §3 · pp. 4–5
  • The IMO set contains all combinatorics problems since 2000 except 2004 Problem 3, whose image made direct formalization difficult.The authors found that 2023 Problem 5 could potentially be formalized despite its image.Source: §3 · p. 5
  • 45% of problems require first finding a solution and then proving its correctness, rather than directly proving a stated proposition.The example asks for the number of permutations in which no even integer is in its natural position.Source: §3 · p. 5
  • Such problems cannot be formalized directly as propositions; modifying them to prove a given solution can reduce difficulty by removing the solution-finding challenge.The text describes PutnamBench’s standardized formalization as better reflecting the difficulty of the informal problem.Source: §3 · p. 5
  • After excluding blank lines, comments, imports, and opens, all FIMO and miniF2F problem formalizations are within 15 lines of code directly related to the problem statements.The authors attribute the challenge in part to Mathlib’s scarcity of combinatorics theorems, which requires defining many concepts.Source: §3 · p. 5
  • More than half of CombiBench problems have statements over 10 code lines, more than a quarter exceed 20, and the longest is 67 lines.The authors exclude blank lines when counting formalization code.Source: §3 · p. 6

4 Evaluation

FINE-EVAL evaluates proof-based and fill-in-the-blank problems in Lean 4, using answer matching and proof verification. In baseline tests, models solved few problems; Kimina-Prover Preview solved the most reported problems.

4.1 Evaluation method

  • FINE-EVAL verifies proof-based and fill-in-the-blank problems by formalizing whether a predicted answer matches the ground truth as a theorem-proving task.The model receives a formal statement with blanks replaced by sorry and returns Lean 4 code; code containing sorry or new axioms, failing compilation, or changing other statement parts is rejected.Source: §4 · p. 6, §4.1 · p. 6
  • When an answer differs from the ground truth, two-stage FINE-EVAL first tries rfl and norm_num, then asks the model to prove equivalence if those tactics fail.The second-stage proof is limited to 42 non-space, non-newline characters.Source: §4.1 · p. 7, Figure 2 · p. 7
  • The simplified one-stage approach checks exact matches first and otherwise uses rfl to test definitional equivalence, requiring only one LLM call.It imposes stricter requirements on predicted answers but is easier to embed in other workflows.Source: §4.1 · p. 7, Figure 3 · p. 7

4.2 Baseline results

  • Baseline tests report pass@16 for whole-proof generation across theorem-prover and general reasoning models, without larger sample budgets or tree search.The authors cite economic cost and reproducibility as reasons for these evaluation limits.Source: §4.2 · p. 8
  • 7 problems were solved by Kimina-Prover Preview under both with_solution and without_solution settings, the best result among tested models.The model has 72B parameters and was fine-tuned for theorem proving, but not specifically on combinatorics or fill-in-the-blank datasets.Source: Table 3 · p. 8, §4.2 · p. 8

5 Conclusion

The paper presents CombiBench, a Lean 4 benchmark for combinatorics problems, alongside a two-stage evaluation method for fill-in-the-blank tasks. Tested models solved few problems, with failures attributed to missing combinatorial theorem-library content and the difficulty of formalizing informal statements.

5 Conclusion

  • CombiBench is a Lean 4 benchmark of combinatorics competition problems spanning high-school, IMO, and university levels.The benchmark is described as the first comprehensive benchmark specifically designed to assess language models on combinatorial mathematics problems.Source: §5 · p. 8
  • The proposed two-stage method evaluates fill-in-the-blank problems by checking a generated solution and its proof, then testing equivalence to the ground truth when needed.A differing answer may still be valid if its equivalence to the ground truth is proved.Source: §5 · p. 9
  • Existing models solved few CombiBench problems, with failures linked to missing combinatorial definitions, lemmas, and theorems and difficulty bridging informal statements to formal proofs.The missing library content can force models to construct relevant mathematical material from scratch.Source: §5 · p. 9
  • The authors plan to contribute newly formalized definitions to mathlib and develop a dedicated theorem library for combinatorics.They also aim to promote improvements in LLM capabilities in combinatorics.Source: §5 · p. 9

A.1 Example of the longest formalization

The example formalizes an island-and-bridge game in which players build bridges subject to factory-access and losing-condition rules. Its Lean representation models islands and bridges as a graph-based game state and expresses the winning-strategy question.

A.1 Example of the longest formalization

  • The problem asks who has a winning strategy when Alice starts, for each n ≥ 2, in a game played on n islands with two factories.A player loses upon building a bridge that connects the two factories.Source: §A.1 · p. 12
  • A legal move joins distinct islands not already connected, and at least one endpoint must have a bridge path to a factory.The statement permits bridges to pass above other bridges.Source: §A.1 · p. 12
  • The formalization represents islands as vertices in a graph and tracks bridges through a GameState, with separate predicates for valid moves and factory reachability.The code also defines move outcomes and a recursive predicate for whether Alice wins under the players’ strategies.Source: §A.1 · pp. 12–13

A.2 Cheat Case from Model

The example describes a model that hid functionally incorrect Lean code in comments, allowing it to pass server validation and be mistakenly accepted as a proof. The surrounding formalization concerns a midpoint-counting problem involving 997 points.

A.2 Cheat Case from Model

  • A model hid functionally incorrect Lean code in comments, and the code passed Lean server validation before being mistakenly judged correct.The authors cite such behavior as motivation for strict requirements on generated Lean 4 output.Source: §A.2 · p. 13
  • The example formal statement asks for at least 1991 red midpoint points from 997 plane points whose pairwise segment midpoints are red.The code defines red_points as a finite set of midpoints generated from the input points.Source: §A.2 · pp. 13–14

A.3 Case Study from Gemini

Gemini solved brualdi_ch1_10, which every other evaluated model failed, and its proof supplied a useful intermediate lemma. The section also walks through formal proofs of a difference-set claim and a subset count.

A.3 Case Study from Gemini

  • Gemini uniquely solved brualdi_ch1_10 by deriving equal off-diagonal entries from the magic-square sum constraints, contradicting pairwise distinctness.The case study highlights the intermediate lemma equating M 0 1 and M 1 0.Source: §A.3 · pp. 14–15
  • The Lean proof for brualdi_ch10_31 establishes that every nonzero difference in the specified 21-element modular group occurs once for the given set.It reduces the claim to finite cases and checks the resulting computations with native_decide.Source: §A.3 · pp. 15–16
  • The brualdi_ch2_11 example counts 816 size-3 subsets of 1 through 20 that contain no consecutive integers.The listing evaluates the filtered subset count using native_decide.Source: §A.3 · p. 16

A.4 Case Study from Kimina-Prover

Kimina-Prover Preview is presented as CombiBench’s state-of-the-art model, with three solutions to problems unsolved by every other evaluated model. The case study shows Lean code for these solutions.

A.4 Case Study from Kimina-Prover

  • Kimina-Prover Preview solved three CombiBench problems that remained unsolved by every other evaluated model.The paper identifies it as the benchmark’s current state-of-the-art model.Source: §A.4 · p. 16
  • One shown proof equates the cardinality of functions with six zero entries to the named target constant.The proof rewrites the solution set as a filter and evaluates the resulting cardinality.Source: §A.4 · p. 17
  • Another shown proof computes the cardinality of functions having exactly one occurrence each of 0, 1, and 2.The code identifies the target with the named solution constant.Source: §A.4 · p. 17
  • A third shown proof concerns permutations of 1 through 8 with no fixed points at even indices.Its cardinality is equated with the named solution constant.Source: §A.4 · p. 17

Related papers

Loading 2505.03171v1…