CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

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 spans more than ten combinatorial topics. CombiBench is suitable for testing IMO-solving capabilities since it includes all IMO combinatorics problems since 2000 (except IMO 2004 Problem 3, whose statement contains an image). Furthermore, we provide a comprehensive and standardized evaluation framework, dubbed \emph{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. State-of-the-art LLMs solve only 48% of CombiBench problems, highlighting its complexity and importance for LLM evaluation.