Monotonic Reference-Free Refinement for Autoformalization
本文提出了一种无参考、迭代式单调细化框架，用于全定理自动形式化，该框架利用定理证明器与大语言模型评判者提供的互补反馈，同步优化形式有效性、逻辑保持性、数学一致性与形式质量，在无需真实标签数据或人工干预的情况下，于 miniF2F 和 ProofNet 基准测试中实现了最先进的性能。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正试图将一篇用随意、日常语言写成的复杂故事（比如一篇关于数学的博客文章）翻译成一种严格、计算机可读的语言（比如为机器人数学家编写的程序代码）。这个过程被称为自动形式化。
问题在于，虽然计算机非常擅长检查代码是否“语法正确”（是否有正确的标点符号？），但它们难以理解故事是否仍然通顺，或者逻辑是否成立。现有方法往往修正了语法却丢失了含义，或者搞对了含义但代码却无法运行。
本文介绍了一种名为单调无参考精炼的新方法。以下是其工作原理，辅以简单的类比：
1. 目标：完美的翻译
作者希望创造出在以下四个方面都完美的翻译：
- 形式有效性（“语法检查”）：代码必须无错误地运行。如果不行，机器人会立即拒绝它。
- 逻辑保持（“情节检查”）：翻译必须保留原始故事的逻辑。你不能仅仅因为更容易写就改变结局。
- 数学一致性（“事实检查”）：所有数字、变量和规则必须与原始故事完全匹配。
- 形式质量（“风格检查”）：代码应当简洁、清晰，便于人类日后阅读。
2. 问题：单一工具无法包揽一切
通常，研究人员使用一个 AI 模型来完成整个工作。但这就像要求一个人同时担任语法学家、逻辑学家、事实核查员和编辑。他们可能擅长语法，却在逻辑上表现糟糕。此外，如果第一次尝试出错，修正它通常需要一个“黄金标准”答案（即正确的代码）作为对比。作者希望找到一种无需答案键即可工作的方法。
3. 解决方案：专业化的流水线
作者构建了一个系统，它像一个专业工厂，拥有不同的工人，各自发挥所长。他们不需要答案键；只需不断改进草稿，直到其完美为止。
以下是他们工厂中三种类型的“工人”（AI 模型）：
- “初稿”撰写者（一次性生成器）：这些是专门的数学 AI，它们接收原始故事并编写代码的第一个版本。它们擅长构建正确的结构。
- “语法修复者”（FV 修复器）：如果初稿存在代码错误（被机器人拒绝），这些工人就会介入。它们是修复损坏代码以使其运行的专家，确保“形式有效性”得分提升。
- “精炼者”（循环生成器）：一旦代码能够运行，这些工人就会审视草稿并尝试使其更好。它们不仅修复错误，还改进逻辑、事实和风格。它们会从“评判者”（其他 AI）那里获得反馈，例如“这部分逻辑薄弱”或“这太啰嗦了”。
4. “单调”规则：绝不后退
该系统最重要的部分是接受策略。想象你在攀登一座山峰。
- 在许多 AI 系统中，你可能会向上迈一步，然后向下迈一步，再向上，希望能找到顶峰。
- 在这个系统中，规则是单调的：只有当新版本代码严格优于（或至少不差于）前一个版本时，才会被接受。
如果新草稿在逻辑上稍好但在风格上稍差，系统会检查一个“安全缓冲区”（一种称为下置信界的数学保证）。只有当系统确信整体质量有所提升时，才会接受该更改。这确保了过程永远不会陷入质量越来越差的循环。
5. 结果：自我改进的循环
该系统在一个循环中运行：
- 生成草稿。
- 检查其是否可运行（有效性）。如果不能，将其发送给语法修复者。
- 如果可以运行，将其发送给精炼者以改进逻辑和风格。
- 使用“安全缓冲区”将新版本与旧版本进行比较。
- 如果新版本被认证为更好，则保留它。否则，保留旧版本并尝试不同的方法。
结果：
作者在两个困难的数学基准测试（miniF2F 和 ProofNet）上测试了该方法。
- 在较简单的基准测试中，他们实现了100% 的有效性（代码始终可运行）和非常高的整体质量得分。
- 在较难的基准测试中，他们仍然实现了高有效性，并且整体得分显著优于之前的方法。
总结：
本文提出了一种将数学翻译为代码的“团队式”方法。它不依赖单一的超级 AI，而是利用一组专门的 AI 在循环中协同工作，并遵循严格的规则：每一步都必须是改进。这使得他们能够在无需预先看到正确答案的情况下，创建高质量、无错误的数学证明。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。