测试大模型在不等式证明中的组合推理能力，发现其远逊于人类直觉。
Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities
- 构建包含变量复制、代数变换的不等式组合基准测试
- 多数模型在组合问题上表现差，最大性能下降20%（pass@32）
- 即使给出子步骤证明，模型仍无法正确推理，适合研究数学推理局限性
基于大语言模型的正式证明助手（如Lean）在自动化数学发现方面潜力巨大。但它们是否真正理解数学结构，如同人类一样？我们聚焦于不等式证明，考察其识别问题可通过已知不等式（如AM/GM）简化的能力，尤其在需多步组合应用的场景下。为此，我们构建了Ineq-Comp基准，通过系统性变换（如变量复制、代数重写、多步组合）生成基础不等式。尽管这些问题对人类仍简单，但多数证明器——包括Goedel、STP和Kimina-7B——表现显著不佳。DeepSeek-Prover-V2-7B相对稳健，但仍出现20%性能下降（pass@32）。即使对于671B参数的DeepSeek-Prover-V2-671B，组合变体与原始问题之间仍存在差距，说明单纯扩大模型规模无法解决组合推理缺陷。更令人震惊的是，即便在上下文中提供子部分的形式化证明，所有模型表现依然欠佳，表明根本问题在于组合推理能力。结果揭示当前AI证明器在泛化行为上与人类数学直觉之间存在持续差距。所有数据与评估代码见https://github.com/haoyuzhao123/LeanIneqComp。
原文摘要 · Abstract (English)
LLM-based formal proof assistants (e.g., in Lean) hold great promise for automating mathematical discovery. But beyond syntactic correctness, do these systems truly understand mathematical structure as humans do? We investigate this question in context of mathematical inequalities -- specifically the prover's ability to recognize that the given problem simplifies by applying a known inequality such as AM/GM. Specifically, we are interested in their ability to do this in a compositional setting where multiple inequalities must be applied as part of a solution. We introduce Ineq-Comp, a benchmark built from elementary inequalities through systematic transformations, including variable duplication, algebraic rewriting, and multi-step composition. Although these problems remain easy for humans, we find that most provers -- including Goedel, STP, and Kimina-7B -- struggle significantly. DeepSeek-Prover-V2-7B shows relative robustness, but still suffers a 20% performance drop (pass@32). Even for DeepSeek-Prover-V2-671B model, the gap between compositional variants and seed problems exists, implying that simply scaling up the model size alone does not fully solve the compositional weakness. Strikingly, performance remains poor for all models even when formal proofs of the constituent parts are provided in context, revealing that the source of weakness is indeed in compositional reasoning. Our results expose a persisting gap between the generalization behavior of current AI provers and human mathematical intuition. All data and evaluation code can be found at https://github.com/haoyuzhao123/LeanIneqComp.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。