自然语言断言的忠实自动形式化

自然语言断言的忠实自动形式化（中文全译）

翻译说明：本文是 arXiv 论文 Faithful Autoformalization of Natural Language Assertions（arXiv:2607.13303）的中文全译，由智测团队翻译。原作者：Hongyi Liu、Madhusudan Parthasarathy、Adithya Murali。原文以 CC BY 4.0 许可发布。译文保留原文全部章节、数据与结论；参考文献列表从略。

arXiv:2607.13303v2 [cs.SE] 2026年7月16日

Hongyi Liu

单位：威斯康星大学麦迪逊分校（University of Wisconsin–Madison）

邮箱：{adithyamurali, hliu794}@cs.wisc.edu

Madhusudan Parthasarathy

单位：伊利诺伊大学厄巴纳-香槟分校（University of Illinois at Urbana–Champaign）

邮箱：madhu@illinois.edu

Adithya Murali

单位：威斯康星大学麦迪逊分校（University of Wisconsin–Madison）

邮箱：{adithyamurali, hliu794}@cs.wisc.edu

摘要

形式化契约对软件测试与验证至关重要，但编写它们仍然费力且容易出错。大语言模型（LLM）为自动形式化提供了一条有前景的路径：从自然语言规约综合出可执行断言，从而弥合开发者的非正式意图与形式化可执行规约之间的鸿沟。我们提出 Monty：一个面向断言的自动形式化框架，用以应对“对断言有效性的预期”以及自然语言歧义这两项挑战。我们的技术基于一种新颖的符合度分数（conformance score）来过滤形式化结果，并结合将代码对照已形式化断言进行测试所得到的有效性分数。我们在由 22 个类集合（collection-like）Java 类派生的 541 个断言生成任务上评估该方法，并表明：与朴素地使用 LLM 翻译断言相比，我们的技术能更可靠地产出真值（精确率平均最多提高 20 个百分点）。

1 引言

以契约或后置条件断言表达的模块化代码形式化规约，一直是实现稳健、有效软件开发的基石。作为运行时检查落地的形式化规约，使单元级测试、形式化验证成为可能，也使软件能够演化：模块可以被其他满足同一规约的模块替换。契约式设计（Design by Contract）范式（Meyer，1992a）把这一开发方法具体化；数十年来已发展出多种契约规约语言，包括 Eiffel（Meyer，1992b）、JML（Leavens 等，1999）、Spec#（Barnett 等，2004）以及微软的 Code Contracts（Logozzo，2013）。然而，尽管好处明确，我们始终难以让程序员编写形式化规约，主要原因是它被看作一种“负担”，会拖慢软件交付。

人工智能的出现开辟了两条路径，改变了“带契约写代码”的框架。第一，人工智能使自然语言规约成为可能，再将其自动形式化为形式化且可执行的契约（可执行逻辑）。这显著降低了编写形式化规约的负担，类似于人类软件开发者之间用于理解代码的现有文档。第二，基于人工智能的自动编码／编程近年来进展很大，程序员只需陈述编程任务的意图即可。但这在程序员意图与代码之间造成了巨大缺口（Lahiri，2026）。形式化规约有助于弥合这一缺口——开发者可以在模块层面编写自然语言规约，再用这些断言的自动形式化结果，通过测试检查人工智能所写的代码，甚至对照推导出的形式化规约形式化地证明代码正确。这一总体框架与使用人工智能的规约驱动开发相契合（Kiro，2025；GitHub，2025）：在人工智能编写代码的过程中，编写并维护结构化、人类可读的规约。

使上述两种应用得以成立的关键问题，是断言的可靠自动形式化。可靠性很重要——当工具成功时，我们需要能够信任这些形式化是自然语言规约的忠实翻译。更形式地说，除通常的准确率指标外，我们关心翻译框架的高精确率，也就是减少不正确翻译的数量。我们识别并处理自动形式化断言的两项关键挑战：（a）如何有效评估形式化的忠实性；（b）如何消解自然语言所写规约中固有的歧义？

前一个问题是自动形式化中的一般问题，后一个问题在翻译断言这一设定下有其独特之处。具体而言，自然语言断言中的歧义尤其麻烦：它们可能把一条有效断言解释成无效断言（产生假阳性，使人怀疑代码并不正确），或把无效断言解释成有效断言（导致断言并未检查用户意图，从而放行有缺陷的代码）。因此，在本工作中，我们提议同时返回自然语言断言最可能有效与最可能无效的形式化。此外，当合理可能的有效形式化与无效形式化同时存在时，我们提议用主动学习算法进一步询问用户，以消除断言的歧义。

与此相对，文献中若干关于规约自动形式化的现有工作，隐含地假定断言预期是有效的（Hahn 等，2022；Ma 等，2025；Wen 等，2024）。为了消除断言含义的歧义，作出这一假定固然诱人，但在并不预期断言有效的情境中，这些技术并不适用。例如，当程序员编写断言来测试代码时，有效性假定显然适得其反。同样，在用断言验证人工智能所写代码的情境中，至关重要的是不要假定该断言在那段代码上有效！

我们需要一种技术来检查断言是有效还是无效。本文的一个关键想法是分析代码，以审查自动形式化结果。更精确地说，我们在自动生成的测试输入上分析程序行为，以判定断言的有效性／无效性。

本文提出一个结合 LLM 与程序测试的自动形式化框架，它：（a）用一种称为子句覆盖（clausal coverage）的新技术，评估断言各种形式化的置信度；（b）利用包括子句覆盖度量在内的指标，同时生成最可能有效的形式化与最可能无效的形式化；（c）必要时，通过询问程序员的主动学习，在最可能有效与最可能无效的形式化之间消歧。

子句覆盖技术是本工作的一项关键技术贡献。我们把形式化规约翻译回自然语言，然后询问 LLM：该自然语言规约中的每一条子句是否都被原始规约的某条子句匹配，反之亦然。我们要求 LLM 给出一个符合度分数，刻画子句匹配的好坏，并据此估计形式化有多稳健。

我们强调，本工作面向在模块／代码层面编写的断言的自动形式化。在人工智能所写代码的情境中，我们提出的工具帮助程序员编写模块级规约（在总体意图之外），再通过自动形式化与测试，对照代码加以审查。我们并不试图解决文献中若干密切相关的问题，例如：（a）把程序员更高层的应用级意图形式化（Lahiri，2026）；或（b）从自然语言文档中挖掘形式化规约（Zhong 等，2009；Pandita 等，2012）。我们的解决方案，尤其是子句覆盖技术与主动学习，依赖于这样一个事实：被形式化的是局部化的自然语言断言。

我们的目标是为一类丰富的面向对象代码规约／断言做形式化：这类代码封装数据并提供接口方法。这些方法既包括具有副作用的方法，也包括返回底层对象信息的纯观察者方法。我们的形式化规约基于书写涉及对象上丰富观察者方法的逻辑断言。所面向的逻辑具有表达力，包含布尔组合、有界量词以及多种类型（对象、整数等）。我们针对这类模块的现实规约。

基准、实现与评估

我们整理了若干基准套件，其中包含自然语言规约及对应的真值形式化规约。数据集既涵盖合成生成的自然语言规约，也涵盖人工撰写的规约，并且同时包含有效断言与无效断言。这些数据集合计包含 541 对（自然语言规约，形式化规约），分布在 22 个表示类集合数据结构的 Java 类上。我们在名为 Monty 的工具中实现了该方法，并评估不同的研究问题。

实验表明，Monty 能有效地对自然语言规约做自动形式化。特别是，我们的方法显著提高了自动形式化的精确率，而不只是简单地使用一个 LLM，也就是：生成的回答有多大可能是正确的？正如可以预期的那样，这一效应在较小模型上更为明显。Monty 与 Qwen2.5-Coder（一个 320 亿参数模型，相对而言较小）配合使用时，在一个数据集上把精确率从 75% 提高到 91.6%，在另一个数据集上从 64% 提高到 85%。我们还表明，精确率的提高是在仍然保持高召回率的同时获得的，这说明 Monty 提高了自动形式化的可靠性，而不影响从原始 LLM 翻译中获得正确回答的可用性。最后，我们还做了若干消融，涉及骨干模型的选择、我们所贡献的符合性检查方法以及主动学习。其中最有趣的观察是：子句覆盖方法似乎是符合性检查的最佳途径，优于与相关文献中类似的基线方法。

2 示例说明

我们用标准 ArrayList Java 类（Oracle，2023）中某个方法的一条断言来说明流水线。add(int index, E element) 方法在指定位置插入一个元素，把已有后缀右移，然后增加列表的大小。该方法的一条自然语言规约是：

“若索引有效，则插入之后该索引处的值将是被插入的元素。”

图 1 给出我们作为流水线输入提供的 ArrayList 类骨架。注意，骨架中还包含除 add 以外其他方法的桩。这些是观察者方法，即无副作用的函数，用作形式化规约词汇的原子（更形式的介绍见第 3 节）。本例中，观察者方法是 get（返回给定索引处的值）和 size（返回数组列表的大小）。骨架包含观察者方法的文档字符串与方法签名，以及目标方法的签名。标有 @@@ 的注释表示待形式化的自然语言断言。

尽管这条自然语言断言看起来直截了当，忠实的形式化必须避开许多陷阱，既涉及自然语言理解，也涉及为底层编程语言写出语义正确的断言。下面我们按解决方案架构的不同阶段逐步说明这些挑战。

class ArrayList<E> {

 /** Returns the element at the specified position. */

 E get(int index);

 /** Returns the number of elements in this list. */

 int size();

 /**
 * Inserts element at the specified position in this list.
 * Shifts the element currently at that position (if any)
 * and any subsequent elements to the right.
 *
 * @param index index at which element is inserted
 * @param element element to be inserted
 * @throws IndexOutOfBoundsException {@inheritDoc}
 */

 void add(int index, E element) {

 ...

 // @@@ If the index is valid, the value at the index after insertion will be the inserted element.

 }

 ...

}

图 1：ArrayList.add 的断言生成任务示例。

表 1：ArrayList.add 示例中有代表性的 LLM 生成断言。候选 #0 与真值等价。下划线文本标出与真值不同或导致验证失败的片段。（源文抽取中未保留下划线标记。）

用 LLM 生成候选形式化

给定上述自然语言规约与代码骨架，我们首先用 LLM 生成 JML（Java Modeling Language）中的候选形式化规约（Leavens 等，1999）。[^1] 设 LLM 产出表 1 所示的五条候选形式化。这些断言实际上代表了我们在实验中遇到的不同情形。

[^1]: 我们做了一些轻微的外观调整，以确保能够可靠地提示 LLM 写出语法正确的断言，并把生成的表达式解析为标准 JML。

这些候选可能遭受多种错误。最重要的是，如第 1 节所解释的，我们并不知道给定候选是否符合原始自然语言断言。其次，尽管本例中断言确实有效，我们的解决思路也不假定给定断言对该方法有效，因此不能简单地筛出有效的形式化（例如通过测试）。

选择可能且忠实的形式化

方法的第二阶段用两种互补信号对候选形式化排序并过滤。第一，我们用测试生成器计算有效性分数，刻画断言是否良构，以及相对于测试生成器生成的一组测试，该断言对给定方法是否有效。第二，我们计算符合度分数，估计候选形式化在多大程度上覆盖了原始自然语言规约的意图。

有效性分数通过一系列检查计算：

• 语法检查：检查候选在语法与语义上是否良构，即形式化断言能否无错误地编译。
• 模糊测试安全性检查：用模糊测试器检查断言本身是否安全，即对断言求值不会引发运行时异常。
• 模糊测试语义检查：再次用模糊测试器检查候选对给定方法是测试有效还是测试无效。

注意，候选断言可以使用 \old(e) 算子表示表达式 $e$ 在方法前状态中的值。这些值只需通过记忆化前状态中的相应值来计算。

在本例中，有效性检查剔除了表 1 中的候选 #4，因为它多了一个括号，语法无效。此外，候选 #1 未通过模糊测试安全性检查，因为它没有使用空值安全的相等解释。

符合度分数提供互补信号。为确定该分数，我们请 LLM 用自然语言描述给定的形式化断言。然后请 LLM 把这一描述的子句结构与原始自然语言断言比较，并给出二者之间的符合度度量（1 为最佳可能分数）。在高层上，语义内容与原始自然语言断言重叠更好的候选得到更高分数，而缺失、无关或冲突内容的候选得到更低分数。这种用 LLM 提供数值分数的机制，在机器学习文献中称为 LLM 充当评判者（LLM-as-a-Judge）（Zheng 等，2023）。

在本例中，LLM 为候选 #1 给出如下自然语言描述：

“若索引至少为 0，且至多为插入前列表的大小，则在 add 操作之后，该索引处的元素等于被插入的元素。”

该句与原始规约做双向子句覆盖比较，即一方中的每一条实质性子句是否都在另一方中得到表示。本例中，LLM 评判者给出满分 1.0，因为它没有发现任何差异。

相比之下，候选 #3 的描述开头是：“若索引大于或等于 0，且小于插入前的列表大小……”。LLM 评判者随后正确地识别出，相对于原始自然语言断言，“小于该大小”漏掉了一个边界情形，因此给出更低的分数。

我们把评分过程重复若干次，并对 LLM 评判者的分数取平均。我们为平均符合度分数设定阈值，剔除未达到该阈值的候选。实验中我们将阈值设为 0.6，从而在本例中剔除候选 #3。

表 2：本例的有效性与符合度结果。

表 2 汇总了各候选的有效性与符合度结果。

自动形式化的关键挑战之一，是自然语言固有的歧义。歧义有多种来源，其中之一是：我们不知道原始自然语言断言是否意在对该方法有效。例如，在撰写形式化文档时，人们可能总希望选择有效的形式化；而在试图发现人类或人工智能所写代码中的缺陷时，更合适的选择可能是能揭示断言失败的那种形式化。

因此，在剩余候选中，我们从通过模糊测试检查的那些里选择符合度分数最高者，并同样从未能通过模糊测试检查的那些里选择一个。本例中，该决策返回候选 #0 与候选 #1，作为最可能且忠实的形式化。

用主动学习做最终消歧

流水线的最后阶段用主动学习，在可能且忠实的自动形式化之间消歧。其想法是：程序员可以查看两个候选之间的差别，并确定哪一个更好地形式化了意图中的规约。本工作采用主动学习的如下方式：我们产生一个能够区分两个候选形式化的具体赋值。用户（或自动预言机）随后判定意图中的规约是否会满足该赋值，我们再选取对应的形式化。

在本例中，候选 #0 与候选 #1 由“被插入元素为 null”这一情形区分。我们用测试生成器给出这一区分赋值。实验中，我们用一个获知真值的自动预言机模拟用户，并依据该真值作答。本例中，框架最终选择了候选 #0。

3 预备知识

本工作研究面向对象编程领域中规约的自动形式化。下面给出一些背景，以便形式化本文所用的词汇。

规约语言

我们的规约写在类中方法这一层级。我们为每个类确定一组观察者方法，它们本质上是无副作用的方法（数学函数），在给定状态下计算对象的有用属性。例如，在第 2 节的示例中，我们使用了 ArrayList 类中的观察者方法 size。观察者函数是面向对象程序规约语言中的标准特性，尤其是在受契约式设计启发的范式中（Meyer，1992a）。观察者函数是类中唯一可以在规约里使用的方法。当然，规约也可以表达方法输入参数及其返回值的性质。

在高层上，我们的断言语言本质上与 Java 建模语言（JML）相同（Leavens 等，1999）。给定一个函数，其输入变量为 $\overline{in}$，输出变量为 $\overline{out}$（表示为 $\mathit{\backslash result}$），我们的断言可以使用输入与输出变量、观察者方法、蕴涵、相等、布尔运算，以及所涉各种数据类型的某些基本运算，例如整型值的不等式与算术运算，或对象类型专用的 .equals 函数。我们把对象变量 $o$ 上观察者函数 $f(\mathit{args})$ 的值记为 $o.f(\mathit{args})$。特殊变量 $\mathit{this}$ 表示所考虑类的默认当前对象。

我们还允许断言中的有界量化，例如 $\forall i$，其范围是某个数组 $o$ 上的 $0 \leq i < o.\mathit{size}()$。最后，我们使用算子 $\mathit{\backslash old}(e)$：它接受表达式 $e$，并在方法的前状态中对其求值。例如，要说对象的大小相对于前状态增加了 1，我们会写

$$\mathit{this}.\mathit{size}() == \mathit{\backslash old}(\mathit{this}.\mathit{size}()) + 1.$$

测试生成器

本工作把测试生成器用作验证预言机，以判断方法上断言的有效性。测试生成器构造一批良构输入，并在给定资源预算内检查被测方法是否出现断言违反。特别是，它只构造有效且可达的程序状态：用构造函数和其他工厂方法构造有效对象，然后调用被测方法。实验中我们使用 Randoop（Pacheco 与 Ernst，2007）。

4 问题陈述与方法

问题陈述

我们首先陈述所研究的问题。我们固定一个逻辑 $\mathcal{L}$，框架以此为参数。在本工作中，逻辑 $\mathcal{L}$ 始终是“可执行的”，也就是说：给定一个方法以及 $\mathcal{L}$ 中的一个公式，可以求值该方法的某个给定行为（输入与输出）是否满足该公式。这类可执行逻辑的例子包括任意多种编程语言所支持的断言库或子语言。实验中，我们使用 JML 的一个可执行子语言（Leavens 等，1999）作为形式化规约的逻辑。

固定一个模块 $M$（我们互换使用类与模块这两个词），它由若干方法 $m$ 组成，每个方法都定义在一组输入变量 $\overline{in}$ 与输出变量 $\overline{out}$ 上。模块还可以可选地为每个方法 $m$ 包含文档字符串 $d_m$。如第 3 节所解释的，本工作考虑面向对象程序设定下的规约，因此我们还固定类 $M$ 的一个形式对象变量 $o$，表示调用对象。

定义 1（规约的忠实自动形式化）。

给定模块 $M$，以及 $M$ 中方法 $m(\overline{in}, \overline{out})$ 的一条自然语言规约 $s$，综合出 $\mathcal{L}$ 中的一条形式化规约 $\psi(o, \overline{in}, \overline{out})$，使得 $\psi$ 是 $s$ 的忠实形式翻译。

注意，求解上述问题的技术当然可以使用 $M$ 中的全部信息，包括任一方法的签名、文档与代码。上述定义刻画的是定义该问题所需的最小实体集合。

上述定义包含两处值得注意之处。第一，我们用“忠实”一词指自然语言规约之正确翻译这一直观概念。第二，我们并不要求那一个权威的忠实形式翻译，因为自然语言固有地有歧义。下面详细讨论这些挑战。我们在此指出，一般而言定义 1 中的问题是欠指定的，因此我们采用标准做法：在包含真值形式化断言的数据集上评估问题求解方案的性能。

图 2：用于断言忠实自动形式化的 Monty 架构。（源文仅给出图题，未附图像。）

挑战

本工作把 LLM 强大的形式化能力与模糊测试、主动学习等其他工具结合起来，构建自然语言断言的自动形式化技术。我们在这一过程中识别出两项关键技术挑战。

挑战 1：识别自然语言陈述与形式语言陈述之间的等价。 自然语言陈述与公式之间的“等价”概念，对熟悉表达形式逻辑的人来说是直观的。例如，$x > 0$ 是陈述“$x$ 为正”的忠实翻译，而 $x < 0$ 则不是。然而，由于断言的语义内容本身可能复杂，而表达公式又要处理错综的逻辑算子，LLM 有可能并不能忠实地翻译自然语言断言。它们可能遭受多种问题，包括误用规约语言、语义上过度延伸或过拟合常见情形；并且视模型而定，它们也可能干脆忘记把自然语言断言的某些部分形式化（Zhai 等，2020）。一种不必做后训练就能处理该问题的办法，是采用自然语言语句 $s$ 与公式 $\psi$ 之间可机械化的等价定义，使之尽可能逼近直观等价。然后可以从 LLM 采样许多输出，并滤除未通过等价检查的候选。本工作通过引入一种称为子句覆盖符合性检查的技术，来处理等价识别问题。

挑战 2：应对自然语言固有的歧义。 上述挑战关心的是追踪自然语言断言中明确出现的语义内容。然而自然语言固有地有歧义，并不总是能够识别出与一句自然语言对应的单一形式概念。例如，人们在非正式意义上使用“正”这个词时，既可能指严格为正，也可能指非负，取决于语境。先前关于人类对 LTL 理解的工作中记载的另一个例子（Greenman 等，2022）是诸如“红灯亮着，直到蓝灯亮起”这样的短语，它并未清楚说明：当蓝灯亮起时，红灯是继续亮着，还是会熄灭。注意，这两种翻译对原始语句都是忠实的，因此并不能由我们对挑战 1 的解决方案消解。

Monty 架构

现在描述 Monty，即我们用于规约忠实自动形式化的方法。总体流水线如图 2 所示。

我们首先用所考虑的模块与方法以及自然语言规约 $s$ 提示一个 LLM。提示中还提供目标逻辑的信息，以及少量上下文示例（完整提示见附录 B）。然后得到候选形式化 $\psi_1, \psi_2, \ldots, \psi_n$。架构的第一阶段对每个候选形式化 $\psi_i$ 调用：（a）一个测试生成器，评估 $\psi_i$ 对给定方法是否测试有效；（b）一个符合度测量模块，测量 $\psi_i$ 与原始自然语言断言 $s$ 之间语义内容的重叠。在此过程中，我们还剔除语法畸形的生成结果，或不能无错误编译的生成结果。

架构的第二阶段是一个决策矩阵：它接收测试生成器与符合性检查器对所有候选给出的分数，并返回其中最可能是忠实形式化的子集。本工作的关键洞见之一是：归纳偏置（例如有效性假定）可以用来对抗自然语言规约中的部分固有歧义。

系统的最后阶段是一个主动学习循环，在剩余候选之间消歧。下面详述架构中那些非平凡模块的构造。

子句覆盖符合性检查器。 本工作的关键贡献之一，是构造一个符合性检查器，以应对上面的挑战 1，即判断自然语言断言与形式化断言之间的语义等价。由于自然语言固有地有歧义，我们不希望符合性检查器去捕捉形式化断言中那些在自然语言断言里并未清楚规定的细节。这里的关键洞见是：固有歧义通常在形式化断言中局部显现，因此通过查看两条断言的大致结构，就有可能排除许多糟糕的形式化。

我们把所得技术称为子句覆盖。我们首先请 LLM 用自然语言描述给定的形式化。然后提示 LLM 识别原始自然语言断言以及该描述中的全部实质性子句，并询问该描述是否同时满足：（a）可靠（Sound）：描述包含自然语言断言中的全部子句；（b）完备（Complete）：描述不包含自然语言断言各子句所给出信息之外的任何信息。我们要求 LLM 在区间 $[-1, 1]$ 上给出分数，并附如下评分标准：正分表示原始断言中的子句被覆盖，$+1$ 表示完美符合。负分表示形式化的某些部分与原始断言冲突，负分的绝对值越大，表示两条断言之间的矛盾越严重。零分是中性判断，涵盖多种情形，例如形式化中存在无关内容，或未能清楚检测出符合或矛盾。这种把 LLM 用作评分函数的方法，在机器学习文献中称为 LLM 充当评判者（Zheng 等，2023）。我们把这一评估重复多次并取分数的平均，仅当形式化超过某一阈值时才接受其为忠实。实验中我们将检查重复 8 次，并把阈值设为 0.6。符合性检查所用提示见附录 B。

尽管上述技术很直观，据我们所知，我们是第一个把这一途径用于符合性检查的。事实上，在架构的初始版本中，我们使用了基于自然语言推断（NLI）的符合性检查方法（Bowman 等，2015），类似于当代提及符合性检查的工作中的建议（Fazelnia 等，2024）。这些当代技术也建议做“反向翻译”，并询问它是否与原始输入等价。然而，我们发现这只会放大固有歧义问题，而且 LLM 对措辞差异过于敏感。我们在第 6 节评估符合性检查技术的消融。

决策矩阵与归纳偏置。 本工作的第二项洞见是：自然语言固有的歧义，可以部分地通过纳入特定于应用领域的归纳偏置来应对。例如，若陈述“$x$ 为正”同时产生 $x > 0$ 与 $x \geq 0$ 这两条忠实候选形式化，而其中只有一条对给定方法是测试有效的，那么如果我们假定应用要求编写自然语言规约的用户预设断言有效，我们也许就能选出有效的那一条。代码文档中常常如此，而其他相关的规约挖掘工作也把这作为默认（见第 7 节）。相反，若用户编写断言是为了识别边界情形并发现缺陷，我们实际上可能希望选择对给定方法并非测试有效的形式化，并返回引发断言违反的输入。

本工作假定一个更一般的设定，对断言的有效性不作预设。相反，我们把生成的断言分为测试有效与测试无效两类，并从每一类中选择符合度分数最高的候选。当然，符合度分数低于可接受阈值的候选我们一概不选。该方法背后的直觉是：最好的测试有效形式化与测试无效形式化合在一起，刻画了原始自然语言断言中的歧义范围。这类似于学习理论传统工作中由一般假设与特殊假设所界定的版本空间（Mitchell，1977）。

主动学习循环。 流水线的最后阶段利用主动学习，在忠实的候选形式化之间消歧。其直觉是：这一阶段剩余的候选是可能且忠实的形式化，并标示出原始自然语言断言中固有歧义或欠指定的范围。本工作使用如下主动学习范式：有一位教师（通常是用户）能够说明某个给定数据点是否满足意图中的断言。这里的数据点是断言所涉实体／变量上的一个赋值。因此，例如，若原始断言是“若被插入元素为正，则数组大小增加 1”，则赋值会给出被插入元素的值，以及数组对象大小的前状态值与后状态值。

本工作中，主动学习只区分决策矩阵返回的那两个候选。我们用测试生成器比较它们，以产生一个区分它们的赋值（图 2 中的 $\overline{v}$）。在第 2 节中，该赋值是把被插入元素设为 null。特别是，我们确保该赋值是可实现的，即确实能由该方法的变换产生。例如，若赋值同时涉及对象的旧大小与新大小，我们只让测试生成器搜索旧大小的取值，并执行程序以得到后状态中的大小。然后我们询问用户，以收集意图中的形式化断言是否满足该区分点，并选取相应候选。实验中，我们使用带有真值形式化断言的数据集，通过在区分赋值上执行真值断言来模拟用户。

当然，也可能决策矩阵只产生一个超过符合度阈值的候选，此时我们直接返回该候选。一个有趣的情形是：有两个以上候选的符合度分数足够高。此时可以考虑用主动学习区分它们。本工作不处理这一情形，但只需做足够多次成对比较（要么所有对，要么或许按顺序），并像目前这样寻找区分输入，就可以简单地做到。我们也可以考虑最小化区分点的数量以减少用户参与，最近已有一些工作研究这一问题（Barnaby 等，2026）。

5 基准构建

我们从现有数据集整理出一套基准，以评估我们的方法。特别是，如第 7 节所讨论的，现有基准与我们“形式化断言”这一任务并不精确对齐，因此需要一些改编／整理。就此而言，我们开发的数据集是本工作的贡献之一。

我们的数据集都围绕 Zhai 等人先前工作 C2S 中的形式化断言（Zhai 等，2020）。该工作发布的数据集包含一组 Java 集合风格的类，以及这些类中方法的形式化规约。我们改编了该数据集，手工解决了部分形式化断言中的错误，并增补了更多集合风格的类与形式化规约。

C2S 增强合成数据集。 我们开发的第一套基准，其自然语言规约是从上面描述的增强 C2S 套件中的形式化断言合成生成的。我们提示 Claude-Sonnet-4.6，用简洁、听起来自然的英语陈述来描述这些形式化规约。由此得到一套共 416 对（自然语言规约，真值形式化规约），分布在 19 个类上。

缺陷数据集。 增强 C2S 套件中的规约是有效断言。因此我们构造一个缺陷断言数据集，以评估当规约不正确或程序上下文不一致时，对自然语言规约的翻译。该数据集派生自上述 19 个类的一个子集。我们创建两个变体：缺陷代码变体，其中扰动了目标方法的代码；以及缺陷断言变体，其中把规约扰动为不正确或误导性的断言。我们再次使用 Claude Sonnet 4.6，为缺陷断言生成自然语言规约。

人工自然语言规约数据集。 我们还创建一个较小的数据集，其中自然语言规约由人工撰写。我们选择了上述集合之外的另外三个 Java 类及其形式化规约。然后请作者之一撰写规约，唯一的指示是：他们可以查看代码与文档，并且需要写出一条本质上能刻画给定形式化规约的自然语言规约。该作者并未参与这三个额外类或形式化规约的确定，也没有看过上述数据集中任何合成生成的自然语言规约。不过，该作者了解论文中的解决方法。该数据集包含 39 对（自然语言，形式化）规约。

数据集统计的详细说明见附录 A。

6 评估

表 3：决策矩阵在各数据集上、以 GPT-oss 与 Qwen2.5-Coder 为骨干模型时，对候选选择的影响。计数显示在括号中。

我们遵循附录 D 所述的常规实验设置，并在 Monty 的实现上评估下列研究问题：

• RQ1：我们的方法在自动形式化自然语言规约方面有多有效？
• RQ2：相对于纯粹调用 LLM 来求解该任务，我们的方法提供了哪些改进（如果有）？
• RQ3：我们的方法在人工撰写的自然语言规约上效果如何？
• RQ4：骨干 LLM 的选择如何影响自动形式化性能？
• RQ5：符合性检查在提高形式化忠实性方面有多有效？我们的方法与基线相比如何？
• RQ6：主动学习在该架构中有多有效？

我们在整个评估中使用下列任务级指标（例如见表 3）。Any-Equiv 衡量骨干 LLM 的生成潜力：它报告候选池中是否至少包含一条与真值等价的断言。这本质上是 Pass@5 指标。Oneshot 是 Pass@1 指标：它衡量 LLM 生成的第一个候选是否与真值断言等价。这提供了朴素调用 LLM 来求解手头任务的基线比较。Monty-Acc 衡量我们方法的端到端准确率：完整流水线选出的最终断言（因而通过符合度阈值 0.6）在逻辑上等价于真值。Monty-Prec 衡量 Monty 输出的可靠性：在 Monty 返回一条高符合度（$\geq 0.6$）最终断言的全部任务中，它报告最终断言等价的比例。这是该工具的精确率指标。换言之，当 Monty 返回一条形式化断言时，它有多大可能是正确的？这是最重要的指标之一，因为它衡量工具在报告一条形式化时有多准确。最后，Monty-Rec 衡量召回率，即当存在一条正确断言时，Monty 有多经常恢复出它：在候选池至少包含一条等价断言的任务中，它报告 Monty 选出一条逻辑等价的高符合度（分数 $\geq 0.6$）最终断言的比例。

我们在此指出，第 7 节讨论了若干关于用 LLM 从自然语言文档挖掘形式化规约这一相关问题的工作。据我们所知，这些工作要么（a）朴素地使用一个 LLM，要么（b）用 LLM 生成形式化断言，然后用一组固定测试／测试生成器以及正确性假定剔除无效者。我们的实验本质上用 Oneshot 指标刻画（a），并通过消融符合性检查的评估来刻画（b）（但仅在具有有效断言的基准上）。文献中的另一项技术是用 LLM “修复”测试无效的断言。我们不采用它，因为我们没有有效性假定。

RQ1：我们的方法在自动形式化自然语言规约方面有多有效？

表 3 汇总了 Monty 在各数据集与开源骨干模型上的总体有效性。结果呈现出两种互补效应。第一，LLM 常常能够生成至少一条合适的候选形式化，这反映在 Any-Equiv 指标上。第二，给定生成的候选池，我们的决策矩阵与主动学习消解器能够以高精确率和高召回率有效地选出最终候选。在主要的 C2S 增强数据集上，GPT-oss 达到 89.7% 的总体成功率，而 Qwen2.5-Coder 达到 75.7%。

同样的趋势在其余数据集上成立。在缺陷代码上，Monty 对两个模型都保持高召回率。在缺陷断言上性能较低，对 Qwen2.5-Coder 尤其如此，这反映了形式化误导性或不正确规约的困难。这也表明，LLM 有一种明显的偏向，倾向于产出看起来有效的断言或规约，因此如果要用它们来做例如缺陷发现，就更难从自然语言描述综合出有意无效的断言。总体而言，这些结果表明 Monty 在所评估的数据集上是有效的。

我们还在上述数据集的一个变体上评估了流水线，其中自然语言规约由 GPT-5 生成，我们发现结果与表 3 所呈现的结果实质上并无不同。

RQ2：相对于纯粹调用 LLM 来求解该任务，我们的方法提供了哪些改进（如果有）？

这是本文的主要研究问题。对于任何增强 LLM 的方法，比较的主要基线是朴素用户会诉诸的那种：简单地用任务描述调用一个 LLM，并选择第一个回答。虽然我们并不使用朴素提示，但我们用 Oneshot 指标刻画这一做法。

表 3 表明，我们的方法（Monty-Acc）总体上优于 Oneshot 指标。在主要的 C2S 增强数据集上，GPT-oss 从 Oneshot 准确率 85.3% 提高到 Monty-Acc 准确率 89.7%，而 Qwen2.5-Coder 从 75.0% 略提高到 75.7%。改进在其他数据集上是一致的，尤其是缺陷代码，其中 GPT-oss 从 60.0% 提高到 70.0%。

更有趣的结果在于 Monty-Prec 分数。注意，由于 LLM 总会给出回答，Oneshot 指标也就等同于朴素使用 LLM 时的精确率指标。表 3 表明，我们的方法显著提高了精确率。该效应在较小模型上更为明显：对 Qwen2.5-Coder，精确率在 C2S-Aug 上从 75% 提高到 91.6%，在人工规约数据集上从 64.1% 提高到 85.2%。即便在更大的模型 GPT-oss 上，精确率平均也从 80% 提高到 88%。这是显著的差异，也是有前景的观察，因为实际采用通常要求精确率超过 90%（许多情形下超过 95%）。

表 3 还表明，精确率的提高并未损害召回率。在 C2S 增强数据集上，GPT-oss 的精确率达到 92.8%、Qwen2.5-Coder 达到 91.6% 的同时，召回率分别达到 97.6% 与 93.2%。召回率刻画与精确率互补的性质：当候选池包含一条正确形式化时，高召回率表明过滤过程通常保留它，而不是丢弃它。合在一起，这些结果表明决策矩阵提高了可靠性，而没有实质性地降低有用输出的可用性。

RQ3：我们的方法在人工撰写的自然语言规约上效果如何？

机器生成的自然语言规约，与真实开发者撰写的人类规约相比，可能更规则、更模板化。这引起一种担忧：若自动形式化模型利用了机器生成的措辞模式，在这类数据上的评估可能高估性能。为应对这一担忧，我们在人工自然语言规约数据集上评估 Monty，其中自然语言规约由人工撰写。如表 3 所示，我们的工具在这些规约上仍然取得有意义的端到端性能：GPT-oss 获得 84.6% 的准确率，而 Qwen2.5-Coder 获得 59.0%。这表明 Monty 的性能或许可以推广到有人类用户的真实使用情形。

精确率与召回率结果进一步澄清了 Monty 在这一设定下的行为。对 GPT-oss，所报告输出的精确率为 86.8%，并且在存在等价候选的情形中，该工具还恢复了 97.1%。Qwen2.5-Coder 在该数据集上较弱，但其报告的输出仍有相对较高的精确率 85.2%，召回率为 85.2%。

RQ4：骨干 LLM 的选择如何影响自动形式化性能？

表 4：RQ4：在 C2S-Aug. 数据集的一个子集上比较骨干模型。计数显示在括号中。

表 4 在 C2S 增强数据集的一个随机选取子集上比较不同骨干模型。由于资源限制，我们选择一个子集。除两个主要开源模型外，我们还评估三个更强的骨干：Qwen3-235B-A22B-Instruct-2507（Team，2025）、GPT-5.5（OpenAI，2026）以及 Claude-Opus-4.8（Anthropic，2026）。Qwen3-235B 是 Qwen 家族中更大的模型，而 GPT-5.5 与 Claude-Opus-4.8 代表闭源前沿模型。对 GPT-5.5，我们使用中等力度（medium effort）。

结果表明，骨干质量对候选生成有明显影响。较小的 Qwen2.5-Coder 模型获得 81.2% 的 Any-Equiv 分数，而更大或更强的模型都超过 90%，表明它们更有可能在候选池中生成至少一条等价形式化。Oneshot 结果的差异甚至更大：Claude-Opus-4.8 与 GPT-5.5 取得最强的首候选准确率，分别为 90.6% 与 88.5%，而 GPT-oss 与 Qwen 模型较低。与此同时，所有模型的精确率都保持较高，表明即便第一个生成的候选并不始终正确，决策矩阵仍能选出可靠输出。总体而言，更强的骨干提高了原始生成质量，而 Monty 则提高了跨模型家族所报告的最终形式化的可靠性。

RQ5：符合性检查在提高形式化忠实性方面有多有效？我们的方法与基线相比如何？

表 5：各主要数据集上符合度阈值分类器的性能与主动学习准确率。符合性分类器在全部生成候选上以阈值 0.6 评估。主动学习准确率仅在符合条件的歧义情形上评估。

图 3：以 GPT-oss 为骨干模型时，C2S-Aug. 数据集中全部生成候选上符合度阈值分类器的 ROC 曲线。（源文仅给出图题，未附图像。）

为分离符合性检查的效应，我们把它作为一个分类器来评估：当候选的符合度分数至少为 $\tau$ 时预测为正确，标签则是在逻辑上等价于真值规约。图 3 给出扫描符合度阈值 $\tau$ 得到的 ROC 曲线；基于这一权衡，我们设定 $\tau = 0.6$，因为它偏向高召回率，同时仍然过滤低符合度候选。

表 5 报告该阈值下的性能。在 C2S 增强数据集上，符合性检查为 GPT-oss 与 Qwen2.5-Coder 取得较强的 F1 分数，分别为 93.3% 与 85.4%。召回率始终较高，表明该过滤器很少移除正确候选。精确率较低，证实符合性并不是正确性预言机，但仍为排序与过滤提供了有用信号。Qwen2.5-Coder 在缺陷断言上表现较差，表明当许多候选看起来有效但并不匹配意图规约时，较小模型会遇到困难。

表 6 用 AUC 比较符合性检查的实现。详细解释与可视化见附录 E。我们的完整方法取得最佳的汇总 AUC，为 0.659，优于其他方法。Ours 与 Ours-noCtx 之间的差距表明，上下文信息提高了排序质量。尽管 NLI 在人工 NL 上表现良好，其总体 AUC 与固定阈值行为较弱。这些结果支持使用带上下文、基于往返的双向子句符合性检查。

表 6：以 GPT-oss 为骨干 LLM 时，各符合性方法在全部生成候选上的 AUC 比较。RT 表示往返（roundtrip），Bi 表示双向（bidirectional），Ctx 表示上下文（context）。

RQ6：主动学习在该架构中有多有效？

我们跨数据集评估主动学习的有效性。仅当决策矩阵同时识别出一个有效候选与一个无效候选时，才调用学习器。我们发现，在实验中主动学习只适用于数据集中的少数情形。在表 5 中，情形数（Cases）统计符合条件的主动学习任务：学习器被调用，且两个竞争候选中至少有一个等价于真值的任务。准确率衡量学习器在这些符合条件的情形中是否选择了等价候选。尽管在实践中，让主动学习交互尽量少对于防止用户疲劳是有用的，但我们认为可能需要更大规模的研究，才能更完整地展现需要主动学习的情形有多普遍。

7 相关工作

传统规约挖掘与契约推断

传统规约挖掘与契约推断旨在自动恢复程序性质。早期的被动技术从观察到的执行与踪迹推断不变量或 API 协议，例如 Daikon 风格的动态不变量检测以及基于踪迹的协议挖掘（Ernst 等，2001；Ernst 等，2007；Ammons 等，2002；Whaley 等，2002；Xie 等，2006；Alur 等，2005）。这些方法以程序行为为根据，但只能推断被观察执行所暴露的性质，一般并不直接捕捉开发者意图。

后续工作把动态分析与测试、符号推理、谓词综合以及学习结合起来。例如，Sankaranarayanan 等人（Sankaranarayanan 等，2008）结合动态与符号技术做不变量推断，Padhi 等人（Padhi 等，2016）从执行数据综合前置条件，Astorga 等人（Astorga 等，2019；Astorga 等，2021）学习有状态与面向对象的契约，其保证是相对于测试生成器定义的。更新近的工作也从自然语言 API 文档与注释中挖掘规约（Pandita 等，2012；Zhai 等，2020）。我们的工作是互补的：我们从一条自然语言断言出发，研究 LLM 能否在保持意图的同时把它自动形式化为可执行断言。与先前的挖掘方法不同，Monty 沿两个维度显式评估生成的候选：它们在执行层面的有效性，以及它们与用户意图规约的语义对齐。

基于 LLM 的规约生成与自动形式化

基于 LLM 的规约生成沿两个主要方向出现。第一个方向把自然语言需求、文档或非正式描述翻译为形式化工件，例如正则表达式、一阶逻辑、时序逻辑、契约以及硬件断言（Hahn 等，2022；Cosler 等，2023；Yan 等，2025；Xia 等，2026；Richter 与 Wehrheim，2025）。这些系统表明，学习得到的模型能够从自然语言中恢复有用的语义结构，常常借助文法、模板、交互或精化来提高语法有效性并减少歧义。

第二个方向直接从代码或程序上下文生成规约。SpecGen（Ma 等，2025）用 LLM 综合形式化规约，并通过基于变异的精化与验证引导的选择来改进它们。SpecSyn（Ma 等，2026）面向真实世界的程序验证，通过分解程序并基于语义强度精化所生成的规约。SLD-Spec（Chen 等，2026）聚焦复杂循环函数，使用程序切片与基于 LLM 的逻辑删除，以去除无关或不正确的规约。AutoReSpec（Ayon 与 Ahmed，2026）进一步探索由验证器引导的协作式 LLM 生成，以改进可验证的规约。最近的工作也使用基于 LLM 的库规约抽取来证明客户端正确（Uppar 等，2026）。

我们的工作与之不同之处在于：它面向模块级代码上下文，并显式地从自然语言规约出发，目标是在保持用户意图含义的同时，把它们形式化为可执行断言。

面向规约与验证的往返技术

往返技术把工件翻译回原始表示，以暴露信息损失或语义不匹配。在从自然语言到形式化规约的设定中，先前系统使用回译或子公式到文本的映射，以检查、调试或精化所生成的规约（Cosler 等，2023）。Clover 通过重构测试检查代码、文档字符串与形式化标注之间的一致性（Sun 等，2024），而 Claimcheck 回译已验证的 Dafny 引理，以检测证明与意图的不匹配（Graciolli 与 Amin，2026）。往返翻译已被用于机器翻译与软件可追溯性中的质量控制，但它并不总是前向翻译正确性的可靠代理（Somers，2005）。

我们的符合性检查把这一想法适配到断言自动形式化。它并不只是提示 LLM 判断等价，而是在相关代码上下文中评估双向的子句级覆盖，上下文包括方法签名、参数、返回值与文档。

8 结论

我们提出 Monty，一条把自然语言规约自动形式化为可执行断言的流水线：它把基于 LLM 的候选生成，与基于执行层有效性和语义层符合度的决策矩阵结合起来，并配以用于消歧的主动学习循环。Monty 并不依赖单次原始 LLM 输出，而是生成多个候选形式化，检查它们的可执行行为，估计它们与意图规约的对齐程度，并在可能时选出一条可靠的最终形式化。跨多个数据集与骨干模型，我们的结果表明 Monty 提高了它所报告的形式化的可靠性。消融研究进一步表明，带上下文、基于往返的双向子句覆盖，为候选选择提供了有效的符合性信号。

源文本止于第 8 节。正文引用的附录 A、B、D、E 未出现在源文件中，未另作补写。

署名与许可

本文翻译自 arXiv 论文 Faithful Autoformalization of Natural Language Assertions，原文以 CC BY 4.0 许可发布。

译者： 智测团队

原文链接： https://arxiv.org/abs/2607.13303

许可： CC BY 4.0