摘要
全证明自动形式化将自然语言中的广泛数学证明与正式验证的推理相结合，为可验证的数学推理提升了上限。与语句级形式化不同，证明自动形式化是一个长周期挑战，需要协调多个证明步骤中的主张、上下文和依赖关系，然而这一领域的研究直到最近才受到关注。目前的方法要么依赖于昂贵的模型训练，要么在推理时应用过度且无指导的修复。
为此，我们引入了 ToMap，一个将证明自动形式化结构化为分解器-形式化器-证明者管道的多智能体框架，并通过形式验证和语义标准对证明质量进行高效的测试时间优化。与其将测试时间计算分布在所有智能体上，我们进行瓶颈分析，识别出分解器作为关键瓶颈：其原子、自包含的证明单元的质量直接决定了下游智能体是否能够成功形式化和证明每一步。因此，ToMap 将形式化器和证明者视为下游执行者，并高效地将测试时间计算集中在分解器的优化上。
这种优化遵循一个受 GEPA 启发的循环，通过候选分解的演变更新提示，并结合形式验证进展与语义证明标准定义一个 Pareto 前沿，以指导下一个分解更新。在 ProofFlowBench 上的实验表明，ToMap 在语法正确性和语义忠实性评估中比最佳前方法提高了 19.0%，同时降低了测试时间成本。扩展分析显示，大部分收益在几次分解演变迭代内产生，从而指导测试时间预算的选择。
博主点评： 该研究通过引入高效的多智能体框架 ToMap，深入探讨了证明自动形式化的瓶颈问题，强调了分解器在整个过程中关键的作用。这种方法不仅提升了证明的质量，还为未来的数学验证提供了新的思路，展示了形式化推理在复杂任务中的巨大潜力。