CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

TL;DR

CombiBench addresses the need for rigorous benchmarking in combinatorial mathematics by providing 100 Lean 4 formalized problems with informal statements and a standardized Fine-Eval evaluation framework for both proof-based and fill-in-the-blank tasks. The approach exposes substantial gaps in current LLM and theorem-prover capabilities for combinatorics, even when leveraging Lean 4 backends, with the strongest model (Kimina-Prover Preview) solving 7 of 100 problems. Key contributions include the benchmark dataset, the Fine-Eval evaluation method, and the open-source release to support future development of combinatorics libraries and model improvements. The work highlights critical bottlenecks—limited combinatorial libraries in formal math environments and the informal-to-formal reasoning gap—driving plans to contribute new definitions to mathlib and build a dedicated combinatorics library.

Abstract

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/.

Figures (3)

• Figure 1: Code Length Distribution
• Figure 2: Pipeline of the two-stage Fine-Eval.
• Figure 3: Pipeline of the one-stage Fine-Eval.