正确代码与已验证程序之间的鸿沟

LLM能写出可以编译甚至通过cargo test的Rust代码。但它们目前还无法可靠地写出形式化证明，来证实代码对所有可能的输入都是正确的。

问题不在Rust语法。形式化验证要求你明确陈述要证明什么，找到能让证明成立的不变量，并用验证器接受的语言来表达这两者。LLM训练的是源代码，而不是证明行为本身。它们见过定理，却很少见过成功证明之前那二十次失败的尝试。

如果你把递归二分查找贴给GPT-4，让它”证明这段代码正确”，你会得到一份看起来像证明的东西。它会提到循环不变量和前置条件。但它也很可能混用Dafny语法、引用不存在的引理、断言弱到不足以导出后置条件的不变量。在你尝试验证之前，它看起来完全正确。

Rust形式化验证实际长什么样

Rust有多种验证工具。Kani是一个模型检查器，它会穷尽探索函数在某一界限内的所有可能状态。Prusti和Creusot是演绎验证器，它们将Rust转换为逻辑表达式，再让SMT求解器来证明性质。每种工具都要求使用特定语法的注解。

下面是一个简单函数，以及Creusot中真实演绎证明的样子：

// Requires creusot-contracts crate
use creusot_contracts::*;

#[requires(a.len() > 0)]
#[ensures(result == a[0])]
pub fn first<T>(a: &[T]) -> &T {
    &a[0]
}

Creusot验证前置条件a.len() > 0能保证后置条件result == a[0]。这很平凡，因为逻辑很简单。现在加大难度：

use creusot_contracts::*;

#[requires(n <= 1000)]
#[ensures(result == n * (n + 1) / 2)]
pub fn sum_to(n: u32) -> u32 {
    let mut i = 0;
    let mut s = 0;
    #[invariant(i <= n)]
    #[invariant(s == i * (i + 1) / 2)]
    while i < n {
        i += 1;
        s += i;
    }
    s
}

不变量才是难点。人通过思考每次迭代中什么保持为真来写出不变量。LLM可能因为训练数据中有这个模式就猜测s == i * (i - 1) / 2，也可能干脆省略不变量让求解器失败。

当你让LLM写证明时会发生什么

我用多个模型测试过这一点。提示词是：“用Creusot写一个经过验证的Rust函数，计算n的阶乘，包含完整的前置条件、后置条件和循环不变量。”

回答分成了三类。

第一类，有些模型输出了看起来像样但语法错误的注解。它们把#[requires(...)]写成了#[precondition(...)]，或者把Prusti语法和Creusot语法混用。代码连解析都过不了。

第二类，有些模型输出了语法正确但不变量太弱的注解。阶乘函数需要类似res == fact(i)的不变量。模型经常写成res >= i，这虽然为真，但对证明后置条件毫无帮助。Creusot会报告无法建立目标，而LLM没有机制来修复它。

第三类，少数回答猜对了不变量，但幻觉出了一个辅助引理。它们引用了Creusot标准库中并不存在的math::fact函数。这个逻辑定义必须你自己构建，证明才能成立。

没有一个模型能在第一次尝试就输出能通过验证的证明。

LLM在验证工作流中真正有用的地方

这并不意味着LLM对形式化验证毫无用处。它意味着你必须把它们用在正确的任务上。

它们擅长生成样板代码。给定一个函数签名，LLM通常能生成捕获明显契约的#[requires]和#[ensures]子句。对于函数fn divide(a: i32, b: i32) -> i32，它会正确建议#[requires(b != 0)]和#[ensures(result * b == a)]。这些不算深刻洞见，但能省不少按键。

它们解释验证器错误的能力也还可以。如果Creusot报告”cannot prove loop invariant”，把错误信息贴给LLM，往往能得到关于这个不变量应该做什么的有用解释。它不会给出你需要的精确不变量，但能缩小搜索范围。

它们对翻译验证语言也有帮助。如果你有一个Dafny证明想移植到Prusti，LLM可以处理大部分语法映射。底层逻辑是一样的。这正是LLM擅长的模式匹配任务。

根本限制：证明是搜索，不是补全

写证明和写Web服务器不一样。写Web服务器时，正确答案有很多个。写证明时，正确答案只有一个，或只有一小族，其余全错。

LLM是下一个词预测器。它们根据上下文生成最可能的后续。证明步骤不是最可能的后续。它是关闭证明义务的那一步，可能是第二十个或第二千个最可能的选项。

想想证明排序函数返回输入的排列。关键洞见通常是定义多重集或统计出现次数。LLM可能建议比较长度，这有必要但不充分。需要人来认识到长度相等不意味着排列，并引入计数不变量。

用Kani做模型检查可以避开部分问题，因为它不需要不变量。LLM能更可靠地生成kani::proof测试架，因为它们看起来像单元测试。但Kani只适用于有界验证。如果你需要无界证明，仍然离不开人。

一个能同时利用两者的实用工作流

如果你想在今天验证Rust，这里有一个确实有效的工作流。

先正常写代码。运行cargo test。然后添加契约。用LLM从函数签名生成#[requires]和#[ensures]子句。仔细审查。模型会把简单的做对，把难的微妙地做 wrong。

运行验证器。它至少会在一个循环上失败。拿到错误信息后让LLM解释缺少哪个不变量。把它的解释当作起点，而不是答案。自己写不变量。

迭代。验证器会告诉你不变量够不够强。LLM不会。把模型当作一个懂语法但从未完成过证明的结对编程伙伴。

对这个问题的诚实回答

LLM能为Rust写形式化证明吗？不能。还不能。没有懂逻辑的人在场就不行。

它们能搭脚手架、解释错误、在工具之间翻译。但找到让证明成立的不变量、引理或归纳假设，仍然是人的能力。

如果你在找一种工具，让你跳过学习分离逻辑或霍尔三元组，LLM不是。如果你在找一种工具，通过替你处理语法和样板代码来让学习曲线更平缓，让你专注于逻辑，LLM值得一试。

如果你想做不需要不变量的有界检查，从Kani开始。当你需要无界证明时，转向Creusot或Prusti。用LLM来把语法写对，但证明得自己写。

常见问题

Rust中的形式化验证是什么？

形式化验证使用数理逻辑来证明程序对所有可能的输入都满足规约。在Rust中，Kani、Prusti和Creusot等工具为函数添加注解，描述前置条件、后置条件和不变量。然后由验证器检查这些性质是否成立。

ChatGPT能为Kani写证明吗？

ChatGPT能写Kani证明测试架，它们看起来像带有#[kani::proof]属性的单元测试。这些测试架比演绎证明更容易生成，因为它们不需要循环不变量。但包含假设和断言的复杂测试架仍然需要人工审查。

Kani和Creusot有什么区别？

Kani是一个有界模型检查器。它在一定界限内探索所有可能的执行路径，检查panic或断言失败。Creusot是一个演绎验证器。它将Rust转换为逻辑公式，用SMT求解器证明对所有输入都成立的性质，包括无界循环，但需要用户提供不变量。

为什么LLM在循环不变量上表现不佳？

循环不变量需要推理每次迭代中什么保持为真，这是一种归纳推理。LLM训练的是预测可能的文本延续，而不是搜索能关闭证明义务的精确逻辑陈述。正确的不变量往往不是最可能的下一个词。