Elamur Research⌕
☰
home / papers / 2025 / CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

Paper · 2025 · Junqi Liu, Xiaohan Lin, Jonas Bayer et al.

Summary

Combining LLMs with formal proof assistants has produced strong results in competition algebra, geometry and number theory, but combinatorics lags behind. Existing formal benchmarks contain few combinatorial problems, Mathlib supports the area poorly, and translating informal statements into formal ones often requires custom definitions. The authors built CombiBench to fill this gap. It contains 100 manually formalized combinatorics problems in Lean 4, each paired with its natural-language statement. Difficulty spans a wide spectrum, starting at the middle-school level and extending up to IMO and university problems, and the topics follow Brualdi's textbook. The authors also present Fine-Eval, an evaluation framework that handles both proof problems and fill-in-the-blank problems. For fill-in-the-blank items, a model must supply an answer and prove it correct. If its answer differs from the reference, it can still pass by proving the two are equivalent. In tests with Kimina Lean Server as the backend, both general reasoning models and specialized provers solved very few problems. CombiBench therefore offers a demanding, standardized target for research on formal combinatorial reasoning.

Key points

  • The benchmark has 100 problems: 10 easy ones from Hackmath, 42 exercises from Brualdi's "Introductory Combinatorics", 36 IMO problems and 12 from other contests.
  • It includes every IMO combinatorics problem since 2000 except 2004 P3, which relies on an image.
  • Evaluation used pass@N with whole-proof generation, up to 16 samples, under "with solution" and "without solution" settings.
  • Kimina-Prover Preview (72B) performed best, solving 7/100 in both settings. Gemini-2.5-pro-preview reached 4 with the solution provided and 3 without. The smaller provers (Goedel-Prover, STP, Leanabell-Prover-GD-RL) solved none.
  • The dataset and code are released at github.com/MoonshotAI/CombiBench. The authors plan to upstream the new definitions to Mathlib.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓University of CambridgeCambridge · United Kingdom287 works · 125,174 citations🎓Sun Yat-sen UniversityGuangzhou · China80 works · 9,799 citations🎓Imperial College LondonLondon · United Kingdom56 works · 13,671 citations🎓University of Chinese Academy of SciencesBeijing · China196 works · 8,907 citations🎓Stockholm UniversityStockholm · Sweden22 works · 1,852 citations🔬Academy of Mathematics and Systems ScienceBeijing · China2 works · 35 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 worksComputational Theory and Mathematics · 496 works

Cite

Cite as 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 and Zhengying Liu. 2025. CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics. arXiv:2505.03171.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2505.03171 · arXiv 2505.03171

@misc{liu2025combibench,
  title = {{CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics}},
  author = {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 and Zhengying Liu},
  year = {2025},
  doi = {10.48550/arxiv.2505.03171},
  eprint = {2505.03171},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2505.03171}
}

References

33 references, 20 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Anthropic. Claude 3.7 sonnet, 2025. claude-3-7-sonnet. find
  2. URL — ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics https://www.anthropic.com/news/Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023. ↗
  3. W. Bibel. Automated theorem proving. Springer Science & Business Media, 2013. find
  4. R. A. Brualdi. Introductory combinatorics. Pearson Education India, 2004. find
  5. I. G. Challenge. IMO Grand Challenge — imo-grand-challenge.github.io. imo-grand-challenge.github.io/, 2019. [Accessed 01-06-2024]. https:// find
  6. S.-C. Chou, X.-S. Gao, and J.-Z. Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 25(3):219–246, 2000. find
  7. L. de Moura, S. Kong, J. Avigad, F. Van Doorn, and J. von Raumer. The Lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. find
  8. K. Dong and T. Ma. Stp: Self-play llm theorem provers with iterative conjecturing and proving. arXiv e-prints, pages arXiv–2502, 2025.
  9. Google. Gemini 2.5: Our most intelligent ai model, 2025. URL https://blog.google/ technology/google-deepmind/gemini-model-thinking-updates-march-2025/ \#gemini-2-5-thinking. ↗
  10. D. Guo, D. Yang, H. Zhang, J. Song, R. Zhang, R. Xu, Q. Zhu, S. Ma, P. Wang, X. Bi, et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025.
  11. A. Jaech, A. Kalai, A. Lerer, A. Richardson, A. El-Kishky, A. Low, A. Helyar, A. Madry, A. Beutel, A. Carney, et al. Openai o1 system card. arXiv preprint arXiv:2412.16720, 2024.
  12. A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y. Wu, and G. Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022.
  13. Y. Lin, S. Tang, B. Lyu, J. Wu, H. Lin, K. Yang, J. Li, M. Xia, D. Chen, S. Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025.
  14. C. Liu, J. Shen, H. Xin, Z. Liu, Y. Yuan, H. Wang, W. Ju, C. Zheng, Y. Yin, L. Li, M. Zhang, and Q. Liu. Fimo: A challenge formal dataset for automated theorem proving, 2023.
  15. T. mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20. ACM, Jan. 2020. doi: 10.1145/3372885.3373824. URL http://dx.doi.org/10.1145/3372885.3373824. ↗
  16. L. d. Moura and S. Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635.
  17. OpenAI. Openai o3-mini, 2025. URL https://openai.com/index/openai-o3-mini/. ↗
  18. S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  19. Prize. AIMO Prize — aimoprize.com. https://aimoprize.com/, 2023. [Accessed 01-06-2024]. ↗
  20. T. Qwen. Qwq-32b: Embracing the power of reinforcement learning, March 2025. URL https://qwenlm.github.io/blog/qwq-32b/. ↗
  21. S. Schulz. E–a brainiac theorem prover. Ai Communications, 15(2-3):111–126, 2002. find
  22. The Coq Development Team. The Coq Proof Assistant, Sept. 2023. find
  23. G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. arXiv preprint arXiv:2407.11214, 2024.
  24. H. Wang, H. Xin, C. Zheng, L. Li, Z. Liu, Q. Cao, Y. Huang, J. Xiong, H. Shi, E. Xie, J. Yin, Z. Li, H. Liao, and X. Liang. Lego-prover: Neural theorem proving with growing libraries, 2023a.
  25. H. Wang, Y. Yuan, Z. Liu, J. Shen, Y. Yin, J. Xiong, E. Xie, H. Shi, Y. Li, L. Li, et al. Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long P…
  26. H. Wang, M. Unsal, X. Lin, M. Baksys, J. Liu, M. D. Santos, F. Sung, M. Vinyes, Z. Ying, Z. Zhu, J. Lu, H. de Saxcé, B. Bailey, C. Song, C. Xiao, D. Zhang, E. Zhang, F. Pu, H. Zhu, J. Liu, J. Bayer, J. Michel, L. Yu, L. Dreyfus-Schmidt, L. Tunstall, L. Pagani, M. Machado, P. Bourigault, R. Wang, S.… — Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
  27. M. Wenzel, L. C. Paulson, and T. Nipkow. The isabelle framework. In Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings 21, pages 33–38.
  28. H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data, 2024a.
  29. H. Xin, Z. Z. Ren, J. Song, Z. Shao, W. Zhao, H. Wang, B. Liu, L. Zhang, X. Lu, Q. Du, W. Gao, Q. Zhu, D. Yang, Z. Gou, Z. F. Wu, F. Luo, and C. Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search, 2024b. URL https://arxiv.org/abs/24… ↗
  30. R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y. Sun, S. Zheng, and K. Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025.
  31. B. Xiong, H. Lv, H. Shan, J. Wang, Z. Yang, and L. Zhi. A combinatorial identities benchmark for theorem proving via automated theorem generation. arXiv preprint arXiv:2502.17840, 2025. — [arXiv:2502.17840](https://arxiv.org/abs/2502.17840) find
  32. J. Zhang, Q. Wang, X. Ji, Y. Liu, Y. Yue, F. Zhang, D. Zhang, G. Zhou, and K. Gai. Leanabell-prover: Posttraining scaling in formal reasoning. arXiv preprint arXiv:2504.06122, 2025.
  33. K. Zheng, J. M. Han, and S. Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/liu-2025-combibench-benchmarking-llm-capability-combinatorial/