← 返回 PaperDaily 大模型与智能体

TOMAP让Lean证明更省算力：分解环节一优化，语义忠实度涨19%

这篇论文盯住了自动形式化里最容易“翻车”的一环：证明分解。不是一味堆算力，而是把测试时预算花在最值钱的地方，结果更准、也更省。

龙哥读论文 阅读 4 查看原文
#大语言模型 #Agent #人工智能 #AI应用
TOMAP让Lean证明更省算力：分解环节一优化，语义忠实度涨19%
🐉 龙哥读论文知识星球来了！
公众号每日8篇拆解不够看？星球无上限更AI领域论文、资讯、招聘、招博、开源代码，一站式干货，每日2分钟刷完即赚！
👇扫码加入「龙哥读论文」知识星球，前沿干货、实用资源一站式拿捏～ xingqiu_header

龙哥导读：
这篇论文盯住了自动形式化里最容易“翻车”的一环：证明分解。不是一味堆算力，而是把测试时预算花在最值钱的地方，结果更准、也更省。


原论文信息如下：
论文标题:
Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization 发表日期:
2026年07月 发表单位:
南京大学；中国科学技术大学；Polixir Technologies 原文链接:
https://arxiv.org/pdf/2607.11307v1.pdf

引言

数学证明自动形式化，难点不在最后几行代码，而在证明单元怎么切、上下文怎么带、依赖怎么接。一旦切错，下游再强也只能硬修烂摊子。
图1
图1：完整证明自动形式化的多智能体流水线。
TOMAP 思路很直接：预算有限就别平均撒，先找出最拖后腿的环节集中砸算力。结论也很干脆——瓶颈不是证明器，而是分解器。

数学证明的“最后一公里”：从自然语言到机器验证的鸿沟

完整证明自动形式化要处理整条推理链：每一步结论、依赖、局部假设都得对得上。不是把中文翻成 Lean，而是把“证明过程”翻成机器可验的结构。

痛点直击：为何之前的“暴力”优化不奏效？

很多方法通病是“哪里坏了就整套重来”，训练成本高，测试时反复试错烧穿预算。问题在于，验证失败并不告诉你该改谁：是分解切错，还是形式化没写对？上游错了，下游修得再勤也只是跑偏。
TOMAP 的关键判断：真正值钱的反馈不该平均分给所有环节。先做弱链接分析，找出最易修复且影响最大的层，集中投预算。

TOMAP的破局之道：锁定“分解”环节这一关键瓶颈

论文把流水线拆成三个角色：分解器切证明单元，形式化器翻成 Lean，证明器完成局部证明，最后由 Lean verifier 验收。
图3
图3：TOMAP 的 GEPA 风格测试时优化流程。
它先用四个维度准则打分：语义忠实、原子性、自包含、依赖一致性。便宜反馈拉正方向，昂贵验证只留给少数“有戏”的候选。

高效的“两段式”优化：先让廉价准则“带路”，再让昂贵验证“定稿”

TOMAP 优化分两步：先生成多个候选分解，由 LLM 裁判按规则打分，取帕累托前沿；再从前沿挑父节点做反思式改写，直到通过门控阈值才送正式验证。
这很像筛矿石：便宜筛子先筛掉石头，高概率样本再精炼。它把大模型擅长的生成、批判、重写放在前面，最贵的 Lean 调用留到最后。
核心不是让模型“更努力”，而是在更合适的地方努力。

实验结果大胜：不仅语法正确性领先，语义忠实度更是质的飞跃

实验结论明确：TOMAP 在 PROOFFLOWBENCH 和 miniF2F 上综合表现更好，尤其是语义忠实度和联合指标更突出。模型不只是“能跑通”，而且更像原始证明。
图2
图2：不同接口干预下，五轮修正后的准确率变化。修正分解器收益最大。
论文明确给出代价：多数收益在少数几轮内出现，边际收益递减。这对实际部署很重要。
它的价值不是“又一个更大模型”，而是先诊断瓶颈，再决定算力怎么花。

龙迷三问

下面是龙哥对于大家可能的一些问题的解答：

为什么要先优化分解器，而不是直接优化证明器？因为证明器和形式化器再强，也只能在上游结构里做文章。分解切清楚，下游难度明显下降；上游切歪了，下游只是在错误约束里做精细活。

这套方法是不是只是把测试时算力换了个花样花掉？不是。它把廉价 rubric 反馈放前面，昂贵 Lean 验证放后面，减少无效调用。核心是“把算力花在更可能成功的候选上”。

这项工作对普通做大模型工程的人有什么启发？先找瓶颈，再谈优化。很多系统不是整体都弱，而是某一层特别拖后腿；不先定位弱链接，后面的优化通常只是在烧预算。

如果你还有哪些想要了解的，欢迎在评论区留言或者讨论~

龙哥点评

论文创新性分数：★★★★☆把测试时优化火力集中到“分解器”，思路准且工程化。

实验合理度：★★★★☆弱链接干预、统一预算和语义评估设计扎实，避免只看编译通过的假繁荣。

学术研究价值：★★★★☆对自动形式化和多智能体流水线有直接启发，解决“预算该投给谁”的核心问题。

稳定性：★★★☆☆收益存在，但与优化轮次和底座模型能力有关，非一招通吃。

适应性以及泛化能力：★★★☆☆主要在数学证明基准上验证，离更复杂的研究级证明还有距离。

硬件需求及成本：★★★★☆比无脑反复跑完整链路更省 Lean 调用，成本控制是加分项。

复现难度：★★★☆☆系统组件多，复现门槛不低，但流程清楚。

产品化成熟度：★★★☆☆离可交付工具还有距离，但作为内部提效模块已有价值。

可能的问题：论文假设输入的非形式化证明本身正确，现实未必成立；GEPA 迭代依赖高质量裁判模型，裁判偏了搜索方向也会歪。


主要参考文献

L. A. Agrawal, S. Tan, D. Soylu, N. Ziems, R. Khare, K. Opsahl-Ong, A. Singhvi, H. Shandilya, M. J. Ryan, M. Jiang, et al. Gepa: Reflective prompt evolution can outperform reinforcement learning. arXiv preprint arXiv:2507.19457, 2025.
K. Baba, C. Liu, S. Kurita, and A. Sannai. Prover agent: An agent-based framework for formal mathematical proofs. arXiv preprint arXiv:2506.19923, 2025.
R. Cabral, T. M. Do, X. Yu, W. M. Tai, Z. Feng, and X. Shen. Proofflow: A dependency graph approach to faithful proof autoformalization. arXiv preprint arXiv:2510.15981, 2025.
G. Chen, W. Jing, X. Chen, X. Zhao, R. Song, C. Li, K. Fan, D. Liu, and M. Liao. Reform: Reflective autoformalization with prospective bounded sequence optimization. International Conference on Learning Representations, 2026.
A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y. Wu, and G. Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022.
Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025.
Y. Wu, A. Q. Jiang, N. Baek, et al. Autoformalization with large language models. In Advances in Neural Information Processing Systems, 2022.

想看更多这类测试时优化、多智能体、自动形式化干货，欢迎加入龙哥读论文粉丝群，扫码或者加微信一起拆论文、聊落地、抠细节。备注：研究方向+地点+学校/公司+昵称，方便快速通过～

转发文章 微博 X LinkedIn Facebook
龙哥读论文 · PaperDaily

本文基于龙哥读论文 PaperDaily 数据库整理，结合论文原文与工程视角进行解读。