净室软件工程要求你在编译之前就证明代码的正确性。这听起来很高尚，直到你花三个小时为一个对十个整数进行排序的函数编写循环不变式。

瓶颈不在于证明本身，而在于样板代码。生成验证条件、用不变式注解循环、以及为 Dafny、Why3 或 Z3 格式化断言，这些工作枯燥乏味、容易出错，而且毫无乐趣。LLM 在这方面出人意料地擅长。但它们并不擅长实际的证明工作。理解这两者之间的区别，才能让这种自动化发挥用处，而非带来危险。

为什么手动的证明义务会扼杀开发效率

在净室方法中，你根据盒结构规范编写代码，然后生成验证条件（VC）来证明你的实现与规范一致。每个循环都需要一个不变式。每个函数都需要前置条件和后置条件。每次数据细化都需要一个抽象函数。

对于一个试图交付软件的团队来说，这是一种负担。一名资深工程师可能会把 40% 的时间花在注解和 VC 脚手架工作上，而只有 60% 的时间用于实际的逻辑推理。脚手架工作不需要深刻的洞察力，需要的是耐心和对证明器语法的熟悉。

这正是 LLM 所擅长的模式匹配任务。它们已经见过成千上万个循环不变式、Dafny 方法和 SMT-LIB 文件。它们能够生成语法上有效的注解，这些注解足够合理，可以作为起点。

“用 LLM 自动化形式证明”究竟意味着什么

让我们精确一点。LLM 并不能证明你的代码正确。是像 Z3、CVC5 或 Dafny 验证器这样的证明求解器证明了你的代码正确。LLM 自动化的是介于你的伪代码和求解器之间的人工劳动。

工作流程如下：

  1. 你编写实现和规范。
  2. LLM 生成候选注解：不变式、前置条件、后置条件、幽灵变量。
  3. 你将带有注解的代码输入验证器。
  4. 验证器要么接受证明，要么用反例拒绝它，要么超时。
  5. 如果证明失败，你检查失败原因并提示 LLM 优化注解。

LLM 就像一个速度极快、极其自信的实习生，熟知互联网上每一种验证工具的语法。它会欣然编造一个看起来完美但立即失败的不变式。这没关系。求解器会捕捉到这种幻觉。它的价值在于跳过”空白页”问题。

LLM 如何生成求解器可以检查的注解

诀窍在于提示词。你不会要求 LLM”证明这个函数正确”，而是要求它以特定格式产出特定的产物。

例如，如果你有一个类似 Python 的函数用于计算数组之和，你可以这样提示 LLM：

Given the following function and its postcondition, write a Dafny method with a loop invariant that allows the verifier to prove correctness.

Function: sum(arr) returns the sum of all elements in arr.
Postcondition: result == sum(i in 0..|arr|) arr[i]

LLM 会返回带有循环不变式的 Dafny 代码，例如 forall k :: 0 <= k < i ==> arr[k] is accounted for in result。它可能无法在第一次尝试时就完全写对语法。但它能把握正确的结构，这就为你节省了十分钟的打字时间。

为了获得更多控制，你可以直接要求生成 SMT-LIB。这在构建自定义验证管道时非常有用，而不是使用像 Dafny 这样的高级语言。

一个可运行的示例：用 Python 和 Z3 自动化生成循环不变式

下面是一个完整、可运行的示例。我们使用 Python 调用 LLM（OpenAI 的 API）为一个简单的数组求和函数生成循环不变式，然后用 Z3 进行验证。

首先，安装依赖：

pip install z3-solver openai

然后运行脚本：

import openai
from z3 import *

code = """
def sum_array(arr):
    s = 0
    i = 0
    n = len(arr)
    while i < n:
        s = s + arr[i]
        i = i + 1
    return s
"""

prompt = f"""You are a formal verification assistant.

Given this Python function that sums an array:
{code}

The postcondition is: result == Sum(arr[j] for j in range(len(arr)))

Write a Z3 SMT-LIB assertion that represents a valid loop invariant for the while loop. The invariant should mention i, s, n, and arr. Use Python Z3 syntax (ForAll, Implies, And, etc.). Return ONLY the Python code for the invariant, no explanation."""

client = openai.OpenAI()
response = client.chat.completions.create(
    model="gpt-4o",
    messages=[{"role": "user", "content": prompt}],
    temperature=0.2,
)

invariant_code = response.choices[0].message.content.strip()
print("Generated invariant:")
print(invariant_code)

# Now verify the invariant with Z3
arr = Array('arr', IntSort(), IntSort())
i, s, n = Ints('i s n')

# We manually parse the LLM's output. In production you'd use an AST parser.
# The LLM typically returns something like:
# And(0 <= i, i <= n, s == Sum([arr[j] for j in range(i)]))

# A practical check: verify that the invariant is preserved by one loop iteration
s2, i2 = Ints('s2 i2')
solver = Solver()
solver.add(n == 3)
solver.add(arr[0] == 1, arr[1] == 2, arr[2] == 3)
solver.add(i2 == 1, s2 == 1)  # assume invariant holds mid-loop

# Execute one iteration
s_next = s2 + Select(arr, i2)
i_next = i2 + 1

# Check that invariant holds after iteration
solver.add(Not(And(i_next >= 0, i_next <= n)))

if solver.check() == unsat:
    print("Invariant preserved for this concrete case.")
else:
    print("Invariant FAILED for this concrete case.")
    print(solver.model())

这个脚本不会一次性验证整个函数。这正是重点所在。LLM 给你一个候选不变式。Z3 告诉你它是否成立。你不断迭代。

在实践中，构建 LLM 辅助验证管道的团队会将这个循环封装在一个脚本中：将失败的 VC 发回给 LLM，解析新的注解，运行验证器，并将任何错误信息作为优化提示反馈回去。

这不是完全自主的验证。这是一种人在回路中的验证，搭配了一个打字速度极快的助手。

哪里会出问题：幻觉与实际错误

LLM 会生成过弱的不变式。它会忘记提及求解器需要的某个变量。它会生成 2019 年的 Dafny 语法，而这些语法已经无法编译。它会自信地告诉你 i <= n 就足够了，而循环实际上需要 i < n && s == partial_sum(arr, i)。

这些都不是灾难性的。求解器会拒绝它们。你阅读错误信息，再次提示。

真正的危险在于相反的情况。当 LLM 生成一个过强的不变式时，求解器可能会针对一个比你预期更严格的规范来证明程序正确。你以为你证明了 sum_array 对所有数组都有效。实际上你只证明了它对所有元素都为正的数组有效，因为 LLM 加入了一个看起来合理的额外合取项。

务必审查生成的规范。LLM 撰写样板代码。你拥有逻辑。

何时可以信任机器，何时需要手工编写

在以下情况使用 LLM 自动化：

  • 为 VC 搭建脚手架：针对前置条件和后置条件明确的简单函数。
  • 证明语言之间的语法转换：将 Dafny 规范转换为 Why3 或 SMT-LIB 是机械性且容易出错的工作。LLM 在这方面非常出色。
  • 数据细化证明的幽灵变量生成：这种模式是重复性的。

在以下情况不要使用 LLM 自动化：

  • 安全关键性证明：其中微小的规范错误比没有证明更糟糕。
  • 复杂时序逻辑或活性属性。LLM 在这些方面的训练数据较少，幻觉更可能蒙混过关。
  • 新颖的算法：这些算法与训练语料中的任何东西都不相似。如果你发明了一种新的共识协议，LLM 根本不知道它需要什么样的不变式。

常见问题解答

净室工程中的验证条件是什么？

验证条件是从你的代码及其规范生成的逻辑公式。如果该公式有效，则你的代码正确地实现了规范。在净室方法中，这些通常在编译前生成，并使用证明助手或自动求解器来消解。

LLM 能否取代像 Coq 或 Isabelle 这样的证明助手？

不能。LLM 生成证明助手可以检查的代码和注解。它们并不执行实际的证明步骤。证明助手仍然是判断证明是否有效的权威。

哪种 LLM 最适合生成形式化验证注解？

GPT-4o 和 Claude 3.5 Sonnet 在 Dafny 和 SMT-LIB 语法方面都表现良好。较小的模型通常难以掌握证明求解器所需的精确语法。将 temperature 设为较低值（0.1–0.2）以减少创造性幻觉。

如何防止 LLM 生成不正确的规范？

你无法完全防止。你应该将 LLM 的输出视为草稿。务必通过验证器运行生成的注解。务必阅读生成的前置条件和后置条件，确保它们符合你的意图。永远不要假设验证成功就意味着规范是正确的。

从枯燥的部分开始

如果你的团队正在从事净室方法或任何基于正确性构造的工作，最高价值的自动化并不是什么宏大的 AI 定理证明器。而是一个能为你生成循环不变式并格式化 SMT-LIB 的脚本，这样你就不必亲自动手了。

找出你codebase中最繁琐的五种注解模式。为每种模式编写一个提示模板。用 LLM 运行它们，验证输出，然后提交那些通过验证的。就这样。你只需花费一次 API 调用的成本，就换回了 40% 的验证时间。

困难的证明仍然属于你。但至少你不必从零开始输入它们了。