摘要
大型语言模型（LLMs）在自动定理证明方面取得了显著进展，但现有的正式基准在数学覆盖面和难度上仍然有限。大多数基准集中在更容易形式化的领域，如代数和初等数论，且对需要更深层推理的子领域（如数学分析）的覆盖不足。为此，我们推出了MA-ProofBench，这是我们所知的首个专门针对数学分析的正式定理证明基准。
该基准包含200个形式化定理，涵盖6个核心主题和27个子类，包括测度与积分理论、复分析和泛函分析。问题分为两个难度等级：本科生水平（等级I，100个问题）和博士资格水平（等级II，100个问题），以评估LLMs在不同数学深度下的正式推理表现。每个问题通过人类主导的、LLM辅助的形式化流程构建，随后由独立专家审查，确保形式陈述忠实于原始数学。
我们在MA-ProofBench上评估了一系列近期的通用推理模型和正式定理证明器。然而，大多数模型表现不佳：即使是表现最好的模型GPT-5.5，在等级I的通过率也仅为16%，在等级II则为5%，而大多数模型在等级II的通过率接近0%。进一步分析显示，Mathlib幻觉和不完整证明是两种主要失败模式，同时在基准的自然语言版本上评估暴露了非正式推理与正式推理之间的明显差距。MA-ProofBench旨在作为跟踪高级领域正式数学推理进展的可靠参考。
博主点评： MA-ProofBench的推出填补了数学分析领域定理证明的评估空白，尽管目前LLMs在该领域的表现不尽人意，但这一基准为未来的研究提供了重要的方向和参考，期待更多模型在此基础上进行优化与提升。