可自动检测AI程序可靠性？科学家提出减少软件验证对先验知识依赖

在人工智能开始尝试编写核电站控制代码和自动驾驶系统代码的今天，我们面临一个关键安全问题：如何确保 AI 生成的程序绝对可靠？当前主流 AI 系统存在根本性隐患：它们依赖人类编写的测试用例进行验证，但这种方法存在两大致命缺陷。

首先，当代码复杂度增加时，所需的测试用例数量会呈指数级增长——即便是解决一道普通的 LeetCode 编程题，也需要数十个测试用例才能基本覆盖。更严峻的是，这些测试无法穷尽所有代码分支路径，尤其难以发现深藏的逻辑漏洞。

上海人工智能实验室青年科学家付杰团队（Veri-Code Team）对此进行了系统性研究，依托形式化语言（如 Dafny）直接生成可验证的代码，以此判断代码行为是否符合人类意图。团队在模型训练过程中使用强化学习，来减少大模型在可扩展形式化软件验证中对人类先验知识的依赖。

谈及应用落地的可能性，付杰对 DeepTech 表示，该方法适用于确保医疗、金融、自动驾驶和操作系统等安全关键领域的软件没有漏洞。“我们可以基于该方法开发一个类似 CodeRabbit 的插件，让大模型生成的代码自动验证其正确性。”

近日，相关论文以《Re：Form——减少可扩展形式化软件验证中的人类先验知识：在 Dafny 中的初步研究》（Re：Form—Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny）为题发表在预印本网站arXiv上 [1]。

目前，该团队已经将数据、代码和模型开源 [2,3]。上海人工智能实验室实习生、清华大学交叉信息研究院姚班（已直博）颜川皓是第一作者，付杰担任通讯作者。

验证危机在 AI 编程能力超越人类时，可能引发灾难性后果。正如最近一项研究所警示的那样 [4]：当前流行的长思维链（CoT，chain-ofthought）等非形式化推理方法，本质上是在模仿人类不完美的思维模式，这将成为制约 AI 发展的认知枷锁。

要真正解决安全问题，必须从“给 AI 打安全补丁”（make AI safe）转向“设计安全 AI”（make safe AI）——其中一个有效方法是建立数学定理级别的验证体系，而非依赖个案测试。

形式化定理验证器正是打开安全之门的“钥匙”。以 Lean/Dafny 为代表的验证框架，通过数学逻辑引擎生成“无错误声明”（error-free statements）。这种声明的可靠性达到数学定理级别，其真理性不因 AI 智能水平而变化——正如图灵奖得主约书亚·本吉奥（Yoshua Bengio）所言：“即使出现超级智能，定理依然为真。”

然而，现有方法陷入了依赖人类的困境：训练过程消耗海量人工标注的 CoT，监督信号易受主观判断干扰。当面对复杂编程任务时，这种模式已接近崩溃边缘——人类专家根本无法为每个任务提供足够可靠的监督信号。

例如，为 50 个初级程序编写形式化规范需要两名计算机科学家耗费 220 小时，而验证 SeL4 操作系统内核更是耗时 20 人年（注：相当于 20 个人工作一年的时间）。

在构建可验证 AI 系统的道路上，付杰与团队希望利用形式化定理验证器提供的保真的训练信号，以完全利用强化学习让模型自主学习以生成基于形式化语言的代码，从而实现可扩展性（scale-up）。

正如强化学习领域奠基人之一里奇·萨顿（Rich Sutton）在《苦涩教训》（The Bitter Lesson）[5] 中提出的经典观点：人工智能发展史反复证明，试图将人类思维模式硬编码到系统中——无论这种设计短期内多么有效，终将阻碍长期进步。而真正的突破性进展，永远来自基于搜索与学习的计算范式扩展。

这一洞见直指当前 AI 训练范式中人类先验的不可持续性这一缺陷：现有方法依赖人工标注的 CoT 和由人类提供的结果监督信号，本质上是在强迫 AI 模仿人类的非形式化推理过程。

这不仅消耗海量人力资源（为复杂编程任务标注可靠监督信号已接近不可能），更严重的是——当 AI 生成能力达到超人类水平时，人类提供的监督信号本身就可能包含错误或认知局限。这种模式完美复现了萨顿警示的困境：“研究者将自身知识植入智能体的做法，短期令人满意，长期却会扼杀进步”。

付杰在研究过程中一直在探索一个问题：如何找到一条可以拓展训练、减少人类非必要的先验对训练的影响的道路（不是移除全部人类先验），同时整个过程在数学意义上绝对可以被自动验证，以达到真正稳定 aligned 的 human-in-the-loop 人机共同进步（而不是强行把人类随意放在这个过程中，成为系统瓶颈）？

这让他想到美国 MIT 麦克斯·泰格马克（Max Tegmark）教授提出的“数学宇宙假说”：如果能够用数学描述一个结构，那么这个结构一定可以在某个多元宇宙中存在，即现实世界可以被数学很好地表达。“若基于这个假设，那么我们就可以用形式化语言来描述世界，同时在形式化空间做推理：把真实世界和数学紧密联系起来。”

从这个角度看，形式化定理验证器是个绝佳的奖励环境：通过客观数学逻辑验证确保反馈信号绝对准确，不受人类思维模式的影响。这是在形式化环境下进行训练的本征优势：是一条可能的可拓展训练的道路。

同时，付杰意识到，虽然泰格马克的假说描绘了用数学描述万物的宏伟图景，但在当前阶段，最具现实可行性和迫切价值的应用领域无疑是软件。软件系统天然具备高度的形式化特征，能够被精确地建模、用数学逻辑（如 Dafny 等工具所体现的）进行严格规范和验证。

因此，他和团队将构建可验证的、高可靠性的软件系统确立为终极目标。这不仅是对数学宇宙假说在特定领域可行性的实践探索，更是利用形式化环境的本征优势——提供绝对客观、无歧义的验证信号，来突破当前依赖人类先验的 AI 训练范式，实现真正可扩展（scalable）的“制造安全 AI”路径的关键一步。

最近，随着 Manus 等工具的流行，也暴露出一个问题：生成代码很容易，但如何验证代码的正确性却是一个难题。随着代码规模和功能的不断增加，代码内部结构可能会变得极其复杂。这种复杂性可能会导致功能之间的相互影响，甚至限制代码功能的进一步扩展。

这不仅是一个安全问题，更是功能本身的瓶颈。因此，对生成代码进行形式化验证是必要的：用形式化验证器来确认代码是否符合用户意图，以判断代码的正确性。

付杰指出，“我希望能够对软件进行形式化验证。无论哪家公司生成的代码，都可以根据用户的需求判断代码是否与需求完全一致。这本质上是将验证过程转化为一个数学证明，确保其绝对正确。”

这一选择基于形式化语言如 Dafny 在软件工程场景，相比于其他场景具有独特的优势：

第一，搜索空间压缩。与数学证明工具 Lean 不同，Dafny 直接基于代码逻辑。在验证过程中，其搜索空间比数学定理验证缩减数个数量级。这意味着模型能更高效地探索解空间边界，加速能力进化

第二，难度线性可度量。在数学证明中，一行证明可能蕴含极其复杂的逻辑跃迁（例如，费马大定理的证明仅占半页纸但需要数年才能理解）。而 Dafny 代码行数与复杂度呈强线性关系——50 行代码的任务必然比 30 行更具挑战。这种特性可以像设计学校课程那样，精准实施渐进式训练（Curriculum Learning）：从单行断言验证到多模块组合，步步为营地突破能力边界。

第三，组合泛化试金石。Dafny 要求代码必须符合模块化结构（函数/类/接口分离），这天然成为评估智能体组合能力的理想考场。当模型学会将已验证的排序模块、搜索模块组合成新算法时，便展现出 Francois Chollet 在 ARC 竞赛中强调的核心智能指标——这种能力正是通向通用人工智能（AGI）的关键阶梯。

为了让模型生成可被验证的代码，Veri-Code 团队采取的方案是直接生成形式化语言（Dafny）编写的代码，和精准描述代码行为的规范（specification）并验证生成的规范是否等价于用户意图。为了大规模训练，团队大幅度减少人类先验对训练的干涉：摒弃人工标注的 CoT 与结果评判，并拒绝任何依赖人类主观判断的奖励机制。

团队发现，让模型直接输出结果而完全不使用 CoT 是可行的，至少在研究中任务未受到影响。目前，他们也在考虑较短代码和较局限的任务上是否可行。但需要了解的是，不使用 CoT 并不意味着对于更复杂的问题不需要 CoT。

在具体实现中，Veri-Code 团队目前关注第一步：给定代码实现（implementation），为该实现填写规范（specification）。基于目前现存关于 Dafny 代码的数据非常少，并考虑到目前大模型输出完整无误的 Dafny 代码的能力较差，他们通过对已有数据的利用清洗，设计了代码翻译的 pipeline。

从已有的 Python 源代码中翻译成可验证通过的 Dafny 代码，来获取训练数据，同时构造了测试模型组合泛化能力的 Benchmark，名为 DafnyComp。考虑到模型需要学会基本的 Dafny 语法，研究团队对 Qwen2.5-coder 进行了初步的监督微调（SFT，Supervised Fine-Tuning），当模型的语法正确率达到 80% 后进行强化学习训练。

在强化学习训练中，除了最基础的验证通过的 0/1 信号之外，为了提供更具信息量的奖励信号，同时为了防止模型通过输出简单语句进行奖励破解（reward hacking）, 研究团队基于 Dafny 等形式化语言的特性（每个语句都是可验证的数学命题），通过分析规范间的偏序关系，开发了新的验证技术。

并由此提出了规范优越率（SSR，specification superiority rate）的概念, 旨在衡量模型生成的规范（specification）是否比现有的 Ground Truth 更加优越（比如对函数输入的限制更少，对函数输出的描述更严格等）。

付杰指出，这一度量的引入有利于其测量模型现有的规范质量。同时将此度量作为奖励信号，训练后的模型显著提升了生成的规范质量。

在强化学习训练后，Re：Form 的全规模模型（0.5B-14B）在验证通过率和 SSR 上均超越了现有的 GPT-4o 和 Claude4 等闭源模型。而在 14B 模型在域内验证和已有的 DafnyBench，以及该团队提出的 DafnyComp 上均超越了现有闭源模型。

“现在已有相关研究证明，自回归的 Transformer 只有加上 CoT 才能模拟图灵机，在此基础上才有可能理解代码的运行过程。”付杰表示。

在接下来的研究阶段中，研究团队的重点是：一方面，探索是否能让模型自己学会 CoT，而非人类标注；另一方面，目前可对几百行代码进行验证，研究人员希望未来它能够支持更长的、达到上万行的代码。

参考资料：

1.https://arxiv.org/abs/2507.16331v2

2.Code: https://github.com/Veri-Code/ReForm

3.Models & Data: https://huggingface.co/Veri-Code

4.https://arxiv.org/abs/2502.09192

5.http://www.incompleteideas.net/IncIdeas/BitterLesson.html

运营/排版：何晨龙、刘雅坤