MA-ProofBench：面向数学分析中定理证明的LLM两层评估

大型语言模型（LLM）在自动定理证明方面取得了显着进展，但现有的正式基准在数学覆盖范围和难度方面仍然有限。大多数集中在更容易形式化的领域，例如代数和初等数论，并提供有限的需要更深入推理的子领域，包括数学分析。为了弥补这一差距，我们引入了 MA-ProofBench，据我们所知，这是第一个专门用于数学分析的正式定理证明基准。该基准包含 200 个形式化定理，涵盖 6 个核心主题和 27 个子类别，包括测度和积分理论、复分析和泛函分析。问题分为两个难度级别，本科级别（I级，100个问题）和博士级别。资格级别（II 级，100 个问题），用于评估大语言模型在不同数学深度的形式推理方面的表现。每个问题都是通过以人为主导、大语言模型协助的形式化流程构建的，随后进行独立专家审查，确保形式陈述忠实于原始数学。我们在 MA-ProofBench 上评估了一系列最新的通用推理模型和形式定理证明器。然而，大多数模型的表现都很差：即使是性能最好的模型 GPT-5.5，在 Level I 上也仅达到 16% Pass@8，在 Level II 上仅达到 5%，而大多数模型在 Level II 上仍接近 0%。进一步的分析将 Mathlib 幻觉和不完整证明确定为两种主要的失败模式，而对基准的自然语言版本的评估则暴露了非正式推理和正式推理之间的明显差距。 MA-ProofBench 旨在作为跟踪高级领域形式数学推理进展的可靠参考。