🤖 AI

Faithful Autoformalization of Natural Language Assertions

该论文介绍了 Monty，这是一个自动形式化框架，通过利用新颖的一致性与有效性评分对大语言模型生成的输出进行过滤，提高了从自然语言合成可执行断言的精确度，相比于朴素的翻译方法，其平均精确度提升了高达 20 个百分点。

原作者： Hongyi Liu, Madhusudan Parthasarathy, Adithya Murali

发布于 2026-07-16

📖 1 分钟阅读☕ 轻松阅读

原作者： Hongyi Liu, Madhusudan Parthasarathy, Adithya Murali

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

翻译者的困境：当代码遇见人类语言

想象你正在建造一座宏大的数字城市。为了保持交通顺畅、建筑稳固，每一个街角和摩天大楼都需要一本规则手册。在软件世界中，这些规则手册被称为“形式化规范”（formal specifications）。它们是精确的、数学化的指令，告诉计算机一段代码应当做什么，以及绝对不能做什么。把它们想象成数字世界中不可打破的物理定律。问题在于，编写这些定律极其困难。它需要一种极高的精确度，这种精确度感觉像是说着一种完全不同的语言，大多数人类程序员会觉得这种语言既乏味又容易出错。

由此引出了“自动形式化”（Autoformalization）问题。这是一个追求将人类模糊的、自然语言的想法——比如“不要让列表变得太大”——自动转化为那种严格的、数学化代码的任务。多年来，科学家们一直尝试使用人工智能（AI），特别是大语言模型（LLMs），来充当这些翻译官。这些 AI 模型就像是博学多才的通晓多种语言的人，几乎读过人类写过的所有内容。它们非常擅长猜测一句话的意思。但问题在于：当你要求 AI 将一个模糊的人类想法翻译成一份严谨的法律合同文本时，它经常会产生“幻觉”。它可能会凭空捏造不存在的规则，可能会遗漏一个会导致整个系统崩溃的微小细节，或者会自信满满地将一个“可能”翻译成“肯定”。这篇论文探讨的核心问题是：当风险很高且人类指令很模糊时，我们如何信任一个 AI 翻译器？

认识 Monty：检查 AI 作业的侦探

这篇论文介绍了一个名为 Monty 的新框架，它是一个旨在成为 AI 生成代码规则的怀疑型、注重细节的编辑系统。来自威斯康星大学麦迪逊分校和伊利诺伊大学的研究人员意识到，仅仅要求 AI 将一句话翻译成代码是不够的。如果你要求 AI 翻译“列表应该是空的”，它可能会猜测这意味着“列表中的项目为零”或者“列表中完全没有任何项”。两者听起来都对，但在计算机代码中，它们的含义可能截然不同。

Monty 不仅仅信任 AI 给出的第一个答案。相反，它扮演着一个运行一系列测试的侦探角色。故事是这样展开的：

1. AI 生成一群嫌疑人
首先，Monty 要求大语言模型将一个自然语言断言（人类的一句话）翻译成形式化代码。AI 不仅仅给出一个答案；它会生成一整群“候选”翻译。其中一些可能是完美的，一些可能略有偏差，而另一些则可能完全错误。

2. “模糊测试”：破坏代码
接下来，Monty 会将这些候选翻译放入一个称为“模糊测试”（fuzzing）的压力测试中。想象一下，一个机器人向代码投掷随机且狂野的输入，以观察代码是否会崩溃或表现异常。

如果某个候选翻译导致计算机崩溃或抛出错误，Monty 会立即将其剔除。
如果翻译可以运行，但未能匹配原始人类句子的逻辑，它会得到低分。
至关重要的一点是，Monty 并不会假设人类的句子是正确的。有时，程序员写的规则本身就是错误的（即“有 Bug 的”规则）。Monty 足以识别出：一个“有效”的“有 Bug”规则的翻译，其本质仍然是一个 Bug。它会寻找最可能的正确翻译和最可能的错误翻译，以观察哪一个更符合语境。

3. “子句覆盖率”检查：反向翻译
这是 Monty 的秘密武器。为了检查 AI 的翻译是否真正忠实于原意，Monty 使用了一种被称为子句覆盖率（clausal coverage）的巧妙技巧。它获取 AI 的形式化代码，并要求 AI 将其反向翻译回白话英语。然后，它会将这个新的英语句子与原始的人类句子进行对比。

AI 是否遗漏了原始句子中的部分内容？
AI 是否添加了原本不存在的内容？
它是否改变了意思？
AI 充当评判者，根据两个句子的组成部分（子句）匹配程度给出评分。如果反向翻译丢失了关键细节，分数就会下降，该候选翻译也会被过滤掉。

4. 最终对决：主动学习
有时，AI 会生成两个看起来都非常完美且通过了所有测试的候选方案，但它们的含义略有不同。这就是人类语言的“歧义性”在作祟。在这种罕见的情况下，Monty 不会瞎猜。它会寻找一个特定的场景（一个“区分性赋值”），在这个场景下，两个候选方案的行为会有所不同。然后，它会询问人类（或模拟的神谕/Oracle）一个简单的问题：“在这种特定情况下，你实际指的是哪条规则？”人类选出胜者，随后 Monty 锁定正确的翻译。

Monty 的发现

研究人员在涉及 Java 代码（一种流行的编程语言）的 541 个不同任务上对 Monty 进行了测试。他们使用的数据集既包括完美编写的规则，也包括故意写错的规则，以观察 Monty 能否处理现实生活的混乱情况。

结果令人振奋。当他们让 AI 在没有 Monty 帮助的情况下进行自然翻译时，准确率虽然尚可，但远非完美。例如，使用名为 Qwen2.5-Coder 的特定模型，在其中一个数据集上，原始 AI 的翻译正确率约为 75%。但当 Monty 介入进行过滤和检查后，准确率跃升至 91.6%。在另一个数据集上，准确率从 64% 提升到了 85%。

论文指出，Monty 在解决“精确度”问题方面表现尤为出色。这意味着，当 Monty 说“这就是正确的规则”时，你比单纯询问 AI 并接受其第一个答案时要能信任它得多。它在保持高“召回率”（即没有丢弃太多正确答案）的同时实现了这一点。

Monty 不做什么

了解这篇论文并非在声称什么同样重要。Monty 并不是一个能解决所有编程问题的魔杖。

它并不试图理解整个软件项目的宏观“意图”（例如“帮我做一个社交媒体应用”）。它专注于严格翻译单个代码片段的具体、局部规则。
它并不声称已经永久解决了歧义问题。有时，人类的输入过于模糊，以至于即使是 Monty 也需要人类介入进行澄清。
作者明确反对“我们应该假设程序员写的每一条规则都是正确”的观点。许多旧工具假设如果写了规则，它就一定是正确的。Monty 拒绝这种做法，它表明有时目标是找到那条失败的规则，从而证明代码是有 Bug 的。

总结

归根结底，Monty 表明，编程的未来不仅仅是要求 AI 去完成工作。它应该是构建一个系统，让 AI 生成想法，但由一个聪明且严谨的过程来对照现实进行检查。通过将 AI 的创造力与测试的怀疑精神以及“反向翻译”的精确性相结合，Monty 展示了一条让软件更安全、更可靠的路径，将人类开发者混乱、模糊的想法转化为干净、不可撼动的数字世界法则。论文表明，虽然我们尚未完全到达终点，但这种“检查作业”的方法是让 AI 成为软件开发中值得信赖的伙伴的重要一步。

技术摘要：自然语言断言的忠实自动形式化

问题陈述

本文探讨了可靠自动形式化（autoformalization）的挑战：即从自然语言（NL）规范中合成可执行的形式化断言（例如，Java Modeling Language, JML）。虽然大语言模型（LLM）为弥合非正式开发者意图与形式化规范之间的鸿沟提供了路径，但现有方法存在两个关键问题：

不忠实性（Unfaithfulness）： LLM 生成的形式化内容往往无法准确反映原始自然语言断言的语义内容。
歧义性（Ambiguity）： 自然语言本质上具有歧义。现有工作通常隐含地假设自然语言断言描述的是代码的一个有效属性。然而，在诸如寻找 Bug 或测试 AI 生成的代码等场景中，断言可能是旨在表达无效（即揭示失败）的。假设其有效性可能会导致系统过滤掉正确的形式化结果（如果代码本身有 Bug），或者接受了一个未能检查用户真实意图的形式化结果。

目标是生成一个对自然语言规范保持忠实的形式化结果，无论该结果相对于代码实现是有效的还是无效的。

方法论：Monty 框架

作者提出了 Monty，这是一个结合了 LLM 生成、程序测试和主动学习的框架，旨在解决歧义并确保忠实度。该流水线由四个阶段组成：

1. 候选生成

给定一个代码模块（类）、方法签名、文档以及一个自然语言规范，通过提示词引导 LLM 生成多个候选形式化规范 ( $\psi_1, \dots, \psi_n$ )，采用可执行逻辑（JML）编写。

2. 过滤与评分

使用两种互补的信号对候选结果进行评估：

有效性评分（执行层面）： 使用测试生成器（Randoop）创建测试输入来检查候选结果。
- 语法检查： 确保代码可以编译。
- 模糊安全性检查（Fuzz-Safety Check）： 确保断言不会抛出运行时异常。
- 模糊语义检查（Fuzz-Semantic Check）： 确定断言对于给定方法是测试有效（test-valid）还是测试无效（test-invalid）的。
- 注：框架不会仅仅因为断言在测试中无效就将其丢弃；它会保留这些候选，以处理用户意图在于发现 Bug 的情况。
一致性评分（语义层面）： 使用一种称为**子句覆盖率（Clausal Coverage）**的新型指标。
- 将形式化候选结果通过 LLM 翻译回自然语言。
- 第二个 LLM（充当评判者）将生成的自然语言描述与原始自然语言断言进行对比。
- 它会检查完备性（Soundness）（描述是否涵盖了原始语句的所有子句？）以及完整性（Completeness）（是否包含了额外或冲突的信息？）。
- 系统分配一个 $[-1, 1]$ 之间的分数，其中 $+1$ 表示完美的符合度。低于阈值（例如 0.6）的候选将被丢弃。

3. 决策矩阵

系统通过根据有效性检查将候选结果分为两类，从而选择“最可能的忠实”形式化结果：

在所有测试有效的候选中，选择一致性评分最高的那个。
在所有测试无效的候选中，选择一致性评分最高的那个。
这种方法承认了“正确”的形式化取决于用户的意图（是文档说明还是找 Bug），并避免了预设有效性的偏差。

4. 主动学习消歧

如果同时存在一个有效候选和一个无效候选（且两者都具有高一致性评分），系统会识别一个区分性赋值（一个特定的输入状态），在该状态下两者存在差异。

系统向用户（或评估中的 Oracle）查询，以确定哪一个候选满足该特定赋值下的预期规范。
然后，系统选择对应的形式化结果。

核心贡献

忠实自动形式化框架： 一个能够生成既可能是有效的也可能是无效的形式化结果的流水线，解决了以往工作假设断言必须有效的局限性。
子句覆盖一致性检查： 一种利用 LLM-as-a-Judge 技术，通过往返翻译和子句级覆盖分析来评估自然语言与形式化断言之间语义重叠的新技术。论文声称该方法优于标准的自然语言推理（NLI）基准。
用于消歧的主动学习： 一种通过生成特定的测试用例来区分不同忠实候选结果的机制，从而解决自然语言固有的歧义问题。
新的基准测试集： 作者策划了包含 541 个断言生成任务的数据集，涵盖 22 个 Java 集合类。这些数据集包括：
- C2S-增强数据集： 从形式化断言通过合成方式生成的自然语言规范。
- 缺陷数据集（Buggy Datasets）： 包含有 Bug 的代码或故意错误/误导性的断言。
- 人工编写的自然语言规范： 用于测试泛化能力的真人编写规范。

实验结果

作者在 541 个任务上使用多种骨干 LLM（包括 GPT-oss、Qwen2.5-Coder 及更大的模型）对 Monty 进行了评估。

精确度提升： 与朴素的“单次提示”（Oneshot）LLM 使用相比，Monty 显著提高了自动形式化的精确度。
- 在 C2S-增强数据集上，Qwen2.5-Coder (32B) 将精确度从 75% 提升至 91.6%。
- 在人工自然语言数据集上，精确度从 64.1% 提升至 85.2%。
召回率维持： 过滤过程保持了高召回率（例如 GPT-oss 在 C2S-Aug 上为 97.6%），表明正确的候选结果很少被丢弃。
对歧义的鲁棒性： 该框架成功处理了“缺陷”数据集，即断言旨在表达无效的情况，而在这种场景下，朴素的 LLM 通常会失败或产生幻觉（生成有效的断言）。
消融研究：
- 子句覆盖法在 AUC 指标上优于基准方法（包括 NLI 和简单的往返检查）。
- 上下文信息（代码签名、文档）被证明对排序质量至关重要。
- 主动学习在极少数情况下被调用（即有效和无效候选均通过了一致性检查），但在符合条件的案例中证明了其有效性（GPT-oss 的准确率为 100%）。

意义与主张

论文声称，Monty 通过明确应对自然语言的歧义性和断言有效性的不确定性，为自动形式化提供了一条更可靠的路径。

可信度： 通过针对一致性进行过滤并分离有效/无效候选，该工具生成的形式化结果更可能忠实地翻译开发者的意图。
实用性： 该方法不需要对模型进行微调；它依赖于提示词、测试和决策矩阵，因此适用于现有的 LLM。
局限性： 作者指出，该方法依赖于局部化的自然语言断言（模块级），并不尝试形式化高层应用意图，也不尝试从没有特定目标方法的非结构化文档中挖掘规范。主动学习组件需要用户交互，尽管系统通过仅在必要时进行查询来尽量减少这种需求。

这项工作将自身定位为迈向由 AI 驱动的规范驱动开发的一步，在这种模式下，人类编写可读的规范，然后通过自动形式化和测试对其进行严格验证。