CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

📄 arXiv: 2505.03171v1 📥 PDF

作者: 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

分类: cs.AI

发布日期: 2025-05-06

🔗 代码/项目: GITHUB

💡 一句话要点

提出CombiBench，用于评估LLM在组合数学问题上的推理能力

🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 组合数学 大语言模型 基准测试 形式化验证 神经符号推理 Lean 4 数学推理

📋 核心要点

  1. 现有方法在代数、几何和数论等数学问题上取得了进展，但组合数学领域缺乏合适的基准和定理库，成为一大挑战。
  2. CombiBench通过提供包含100个组合数学问题的数据集，并结合形式化语言Lean 4，为评估LLM的组合推理能力提供了基础。
  3. 实验结果表明，现有LLM在CombiBench上的表现有限，为未来的研究指明了方向，并开源了数据集和评估方法。

📝 摘要（中文）

本文提出了CombiBench，一个包含100个组合数学问题的综合基准，每个问题都以Lean 4形式化，并配有相应的非正式描述。问题难度范围广泛，从初中到IMO和大学级别，涵盖十多个组合主题。CombiBench适用于测试IMO解题能力，因为它包含了自2000年以来的所有IMO组合问题（除了IMO 2004 P3，因为它包含图像）。此外，本文还提供了一个全面的标准化评估框架Fine-Eval，用于形式化数学，它不仅适用于基于证明的问题，而且首次评估了填空题。使用Fine-Eval作为评估方法和Kimina Lean Server作为后端，对CombiBench上的几个LLM进行了基准测试，结果表明它们在形式化解决组合问题的能力仍然有限。在所有测试模型中（没有一个经过专门训练），Kimina-Prover取得了最好的结果，在“有解”和“无解”两种情况下都解决了7个问题（总共100个）。该基准数据集以及所提出的评估方法的代码已开源。

🔬 方法详解

问题定义：论文旨在解决缺乏针对组合数学领域的大语言模型（LLM）评估基准的问题。现有方法在代数、几何和数论等领域取得了显著进展，但组合数学由于其独特的复杂性和缺乏合适的资源，仍然是一个挑战。现有的数学基准测试通常不包含足够数量和多样性的组合问题，并且缺乏形式化的验证方法。

核心思路：论文的核心思路是构建一个高质量、多样化的组合数学问题集，并提供一个标准化的形式化评估框架。通过将问题形式化为Lean 4代码，可以实现对LLM生成答案的自动验证，从而更准确地评估其推理能力。同时，该框架也支持填空题的评估，扩展了评估的范围。

技术框架：CombiBench由两部分组成：问题集和评估框架Fine-Eval。问题集包含100个组合数学问题，涵盖不同难度级别和主题。Fine-Eval是一个基于Lean 4的形式化评估框架，它接收LLM生成的答案，并使用Kimina Lean Server进行验证。该框架支持两种类型的评估：证明题和填空题。对于证明题，Fine-Eval会检查LLM生成的证明是否正确。对于填空题，Fine-Eval会比较LLM填写的答案与正确答案是否一致。

关键创新：CombiBench的关键创新在于其综合性和形式化。它提供了一个包含大量多样化组合数学问题的基准，并且使用Lean 4进行形式化，从而可以实现自动化的、严格的评估。此外，Fine-Eval框架首次实现了对填空题的形式化评估，扩展了评估的范围。

关键设计：CombiBench的问题集涵盖了从初中到大学级别的各种难度，并包含了自2000年以来的所有IMO组合问题（除IMO 2004 P3）。Fine-Eval框架使用Kimina Lean Server作为后端，利用其强大的定理证明能力来验证LLM生成的答案。对于填空题，Fine-Eval使用模式匹配来比较LLM填写的答案与正确答案是否一致。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在CombiBench上，对多个LLM进行了基准测试，结果表明现有LLM在形式化解决组合问题的能力仍然有限。其中，Kimina-Prover取得了最好的结果，在“有解”和“无解”两种情况下都解决了7个问题（总共100个）。这表明组合数学对于当前的LLM来说仍然是一个具有挑战性的领域，CombiBench可以作为未来研究的基准。

🎯 应用场景

CombiBench可用于评估和提升LLM在组合数学领域的推理能力，推动神经符号推理的发展。该基准可以帮助研究人员开发更强大的数学问题求解器，并应用于教育、科研等领域，例如自动生成习题、辅助数学教学等。此外，形式化验证方法也为其他领域的AI系统提供了借鉴。

📄 摘要（原文）

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'' andwithout solution'' scenarios. We open source the benchmark dataset alongside with the code of the proposed evaluation method at https://github.com/MoonshotAI/CombiBench/.