多智能体证明自动形式化的高效测试时优化

中文摘要 AI 辅助

完全证明自动形式化将自然语言中的大量数学证明与形式化验证的推理联系起来，为提高可验证数学推理的上限提供了一条途径。与语句级形式化不同，证明自动形式化是一个长期挑战，需要协调许多证明步骤中的断言、上下文和依赖关系，但直到最近才受到集中研究。当前方法要么依赖昂贵的模型训练，要么在推理时进行过度的、无指导的修复。为此，我们引入了ToMap，这是一个多智能体框架，它将证明自动形式化构建为一个分解器-形式化器-证明器管道，并在形式验证和证明质量的语义标准的指导下进行高效的测试时优化。我们进行瓶颈分析，确定分解器是关键瓶颈，其原子的、自包含的证明单元的质量直接决定下游智能体能否成功形式化和证明每个步骤。因此，ToMap将形式化器和证明器视为下游执行器，并将测试时计算有效地集中在分解器的优化上。这种优化遵循受GEPA启发的循环，在候选分解上演变提示，并使用形式验证进展和语义证明标准来定义帕累托前沿，以指导下一次分解更新。在ProofFlowBench上的实验表明，ToMap在句法正确性和语义忠实性评估中比之前最好的方法提高了19.0%，同时需要更低的测试时成本。缩放分析表明，大多数收益在分解演变的几次迭代中出现，指导测试时预算选择。

英文摘要

Full-proof autoformalization bridges extensive mathematical proofs in natural language with formally validated reasoning, offering a pathway to elevate the ceiling of verifiable mathematical reasoning. Unlike statement-level formalization, proof autoformalization is a long-horizon challenge requiring coordination of claims, contexts, and dependencies across many proof steps, yet has only recently come under focused study. Current approaches either rely on costly model training or apply excessive, unguided repair at inference time. To this end, we introduce ToMap, a multi-agent framework that structures proof autoformalization as a Decomposer-Formalizer-Prover pipeline with efficient test-time optimization guided by formal verification and semantic rubrics for proof quality. Rather than distributing test-time compute across all agents, we perform bottleneck analysis and identify the Decomposer as the critical bottleneck: the quality of its atomic, self-contained proof units directly determines whether downstream agents can successfully formalize and prove each step. ToMap therefore treats the Formalizer and Prover as downstream executors and efficiently focuses test-time compute on Decomposer refinement. This refinement follows a loop inspired by GEPA, evolving prompts over candidate decompositions and using formal verification progress together with semantic proof rubrics to define a Pareto frontier that guides the next decomposition update. Experiments on ProofFlowBench show that ToMap improves over the best previous method by 19.0% when evaluated by both syntactic correctness and semantic faithfulness, while requiring lower test-time cost. Scaling analysis shows that most gains emerge within a few iterations of decomposition evolution, guiding test-time budget selection.

发表机构

• Polixir Technologies（波利希瑞技术公司）
• University of Science and Technology of China（中国科学技术大学）

机构由 AI 辅助整理，请以论文原文为准。