MathConstruct: Challenging LLM Reasoning with Constructive Proofs

📄 arXiv: 2502.10197v2 📥 PDF

作者: Mislav Balunović, Jasper Dekoninck, Nikola Jovanović, Ivo Petrov, Martin Vechev

分类: cs.AI

发布日期: 2025-02-14 (更新: 2025-09-30)

💡 一句话要点

MathConstruct：提出构造性证明数学基准，挑战LLM推理能力

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 数学推理 构造性证明 基准测试 自动验证

📋 核心要点

  1. 现有数学基准测试存在问题简单、易于猜测或记忆等局限性，无法全面评估LLM的数学能力。
  2. MathConstruct基准专注于构造性证明，要求LLM构建满足特定属性的数学对象，更具挑战性且易于验证。
  3. 实验表明，即使是最先进的LLM在MathConstruct上的表现也远未达到完美，突显了该基准的价值。

📝 摘要（中文）

大型语言模型(LLM)在数学方面表现出令人印象深刻的性能，但现有的数学基准存在重大局限性。许多基准侧重于具有固定标准答案的问题，并且由于问题简单或猜测/记忆的可行性而经常饱和。至关重要的是，它们仅捕获了相关数学问题的一个狭窄子集。为了解决这一研究空白，我们引入了MathConstruct，这是一个新的基准，包含来自各种数学竞赛的121个具有挑战性的问题，目标是构造性证明，这是一种广泛遇到的问题类型，需要构造具有特定属性的数学对象。这些证明特别适合LLM评估，因为可以轻松验证解决方案的正确性。我们的自动验证器还使MathConstruct能够生成问题变体，用于评估鲁棒性。最先进的LLM仅解决了MathConstruct问题的60％，突显了其复杂性和对LLM评估的重要性。

🔬 方法详解

问题定义：现有数学基准测试在评估LLM的数学推理能力方面存在局限性。它们通常侧重于具有固定答案的问题，容易被LLM通过记忆或简单推理解决，无法有效评估LLM在构造性证明方面的能力。构造性证明需要LLM构建满足特定属性的数学对象，更具挑战性，也更贴近实际数学研究的需求。

核心思路：MathConstruct的核心思路是创建一个包含大量构造性证明问题的基准测试，这些问题来源于各种数学竞赛，难度适中，并且可以通过自动验证器进行验证。通过评估LLM在这些问题上的表现，可以更全面地了解LLM的数学推理能力，并推动LLM在数学领域的进一步发展。

技术框架：MathConstruct基准测试包含121个问题，这些问题涵盖了数论、代数、几何等多个数学领域。每个问题都配有详细的描述和自动验证器，可以自动判断LLM生成的答案是否正确。此外，MathConstruct还提供了问题变体生成功能，可以根据原始问题生成新的问题，用于评估LLM的鲁棒性。

关键创新：MathConstruct的关键创新在于它专注于构造性证明问题，并提供了自动验证器和问题变体生成功能。这使得MathConstruct成为一个更加全面、可靠和灵活的LLM数学推理能力评估基准。与现有基准相比，MathConstruct更能反映LLM在实际数学研究中的应用潜力。

关键设计：MathConstruct的问题来源于各种数学竞赛，难度经过精心挑选，既具有挑战性，又不会过于困难。自动验证器采用符号计算和逻辑推理等技术，可以准确判断LLM生成的答案是否正确。问题变体生成功能通过改变问题的参数或条件，生成新的问题，用于评估LLM的鲁棒性。

🖼️ 关键图片

img_0

📊 实验亮点

实验结果表明，即使是最先进的LLM在MathConstruct上的表现也远未达到完美，平均正确率仅为60%。这表明MathConstruct对LLM来说是一个具有挑战性的基准，可以有效地评估LLM的数学推理能力，并推动LLM在数学领域的进一步发展。

🎯 应用场景

MathConstruct可用于评估和提升LLM在数学领域的推理能力，尤其是在需要构造性证明的场景中。例如，可应用于自动定理证明、数学建模、算法设计等领域，帮助LLM更好地解决实际数学问题，并促进数学研究的自动化。

📄 摘要（原文）

While Large Language Models (LLMs) demonstrate impressive performance in mathematics, existing math benchmarks come with significant limitations. Many focus on problems with fixed ground-truth answers, and are often saturated due to problem simplicity or the viability of guessing or memorization. Crucially, they capture only a narrow subset of relevant math problems. To address this research gap, we introduce MathConstruct, a new benchmark of 121 challenging problems sourced from various math competitions, which targets constructive proofs, a widely encountered problem type requiring the construction of mathematical objects with specific properties. These proofs are particularly suitable for LLM evaluation, as solution correctness can be easily verified. Our automated verifiers also enable MathConstruct to generate problem variations, used to evaluate robustness. State-of-the-art LLMs solve only 60% of MathConstruct problems, highlighting its complexity and importance for LLM evaluation.