中国实验室如何破解AI数学证明的瓶颈

形式化数学证明, , 那种由机器而非人类验证的证明, , 是严谨性的黄金标准。但将数学家以自然语言撰写的非形式证明翻译成Lean等形式化语言，仍是一个顽固的长期挑战。南京大学和波利克斯技术公司的团队现在表示，他们已经破解了该流程中的一个关键瓶颈。

他们提出的框架名为ToMap（测试时优化多智能体证明自动形式化），将完整证明形式化并非视为单一翻译任务，而是看作一个三阶段多智能体系统：一个将证明拆解为原子单元的分解器，一个将每个单元渲染为Lean语法的形式化器，以及一个生成策略以完成每个目标的证明器。这项发表在预印本中的惊人发现是，最薄弱的环节是第一阶段，而将算力集中用于改进分解环节能带来超乎比例的巨大收益。

瓶颈分析

为了确定测试时算力最佳投向，研究人员进行了一项对照干预实验。在相同的Lean错误追踪和固定更正预算条件下，他们只允许三个智能体中的一个修改其输出，同时冻结其他两个。分解器干预在184样本的ProofFlowBench上经过五次迭代后，始终实现最高的完整证明准确率：51.1%，而形式化器为45.1%，证明器为33.7%。

研究人员写道：“分解器设定了所有下游任务困难程度。”一种能产生具有显式依赖关系的原子化、自包含证明单元的分解，可将形式化和证明简化为下游智能体能够处理的局部任务。而范围不当的单元则会留给执行器模糊或不完整的目标。

ToMap的工作原理

ToMap并非将测试时算力分配到所有三个智能体上，而是将其集中到分解器上。它维护一个候选自然语言分解池，根据三维评估标准（语义忠实度、可证明性和Lean友好性）对每个分解进行评分，并利用由此产生的Pareto前沿来引导分解提示的迭代进化, , 这一技术灵感来自用于反思性提示优化的GEPA算法。

一个提交门控将昂贵的下游形式化器-证明器-Lean验证循环保留给在三个评估维度上均满足最低阈值的候选分解。研究人员解释说：“评估反馈成本低廉且信息密集，主导了大部分搜索过程，而Lean验证提供了忠实但昂贵的真实信号，仅保留给有希望的候选。”

结果与比较

在ProofFlowBench上，由Gemini3-Pro驱动的ToMap实现了40.22%的联合句法正确率和语义忠实度得分，比此前最佳方法Codex End2End（21.20%）提升了19.0个百分点。在包含高中水平竞赛问题的miniF2F数据集中，ToMap达到55.74%，提升了8.2%。该系统还优于ProofBridge等基于训练的方法, , 后者需要检索模型和微调的翻译器, , 同时保持较低的纯推理成本。

消融研究揭示了清晰的时间-性能权衡：大多数增益出现在3-5次进化迭代内，之后收益递减。这为在延迟或成本约束下选择迭代预算提供了实用指导。

研究人员指出：“生成单一整体Lean证明的方法可以达到相对较高的句法正确率，但在忠实翻译自然语言证明的各个步骤方面存在困难。逐步证明形式化通过明确对齐形式化过程与中间证明步骤，更好地保留了语义忠实度。”

局限性与未来工作

评估仅限于基准规模的证明，而非长篇研究级数学。该系统还假设输入证明是正确的；处理错误或不完整的非形式证明仍是一个开放问题。将框架扩展到检测和修复有缺陷的推理被列为未来工作。

南京团队的贡献与其说是形式推理能力上的突破，不如说是证明了：通过受系统瓶颈分析指导的巧妙算力分配，可以从现有模型中提取比简单扩展整体方法更多的价值。对于致力于弥合非形式数学与形式数学之间鸿沟的日益壮大的社区而言，这一见解可能与基准测试本身同样宝贵。