AWS 研究：用符号执行轨迹训练小模型，代码缺陷检测反超四倍体量对手

Amazon Web Services（AWS）的研究团队最近发表了一项独立工作：他们借助 Soteria 产出的符号执行轨迹，对一个 80 亿参数的语言模型做继续预训练（continued pretraining），使其在 C 代码缺陷检测任务上的表现优于体量约四倍的大型模型。这是把符号执行从验证技术转化为 AI 训练数据的一次典型探索，对 AI 辅助软件验证方向具有参考意义。

现有 AI 编码助手的局限

现代大模型在写代码方面已经相当出色：给定一段提示，它们能生成完整函数、实现复杂 API，甚至产出可运行的系统。但这些模型存在一个根本短板——它们擅长写出「看起来对」的代码，却未必能判断代码是否真正正确。

人类程序员通过调试、执行轨迹、测试失败和程序状态检视来理解程序行为，习得的是语义层面的认知。相比之下，大模型主要从海量源代码语料中学习，更接近「语法模仿」而非「语义理解」。这一差距在前沿模型（文中提到的 Mythos 等）以及更大模型上依然存在，而且训练和部署成本极高。如果能让更小、更高效的模型具备同等甚至更强的程序推理能力，将大幅降低高质量 AI 软件验证的门槛。

量化「理解差距」

为了让这一差距可被衡量，AWS 研究者构建了一套评测集，包含 500 个来自 SV-COMP 2025 的 C 语言验证任务，覆盖内存安全、溢出、终止性、可达性和数据竞争五类问题，每道题只要求模型回答「性质成立」或「被违反」二选一。

他们测试了 6 个模型家族、共 14 个模型，结果呈现出一致规律：

• 在「确认性质成立」上，多数模型得分高于 90%；
• 在「检出性质被违反」上能力明显更弱，14 个模型中有 4 个的真实缺陷召回率不足 50%；
• 随着程序长度增加，准确率断崖式下跌：部分模型在 100–200 行的程序上准确率跌破 10%。

研究者在文中给出了一个典型反例：仅 11 行的 C 代码中包含一个 while (x != 0) x = x - 2 循环，当 x 为无符号奇数时减法会绕过 0 导致死循环。某 6750 亿参数的模型虽然识别出了无符号环绕，却仍错误地断定循环会终止。这说明对 AI 而言，推理「代码如何执行」远比理解语法困难。

Soteria：把符号执行变成训练数据

Soteria 是一款符号执行工具，能在多条可能的执行路径上系统性地推理程序行为，并把过程中产生的程序状态、符号值、路径条件、分支决策与性质被违反的精确条件一并记录下来，输出为机器可读的 JSON 或可交互的 HTML 轨迹。换言之，它不仅判断「是否有 bug」，还记录下「bug 为什么发生」。

AWS 研究者将 Soteria 跑在从开源数据集 CodeParrot 筛选出的 C 代码上，收集了数千条这样的轨迹作为训练数据。关键在于：训练数据来自任意开源代码，并非评测集本身，因此任何提升反映的是模型泛化能力，而非对答案的记忆。

训练方法与结果

他们选用的基座模型是开源权重的 Qwen3-8B，使用上述轨迹进行继续预训练。结果显示，经过这类语义化训练数据继续预训练后，模型在「检测性质违反」这一更难的子任务上提升显著，并最终在 SV-COMP 2025 的整体验证任务中，击败了体量约为其四倍的大型模型。

这项工作的核心启示在于：符号执行积累的程序运行语义信息，是远比纯源代码更高效的学习信号。它把「验证工具」改造成了「训练数据工厂」，为小模型补齐程序推理能力提供了一条可扩展的路径，也为前沿模型在程序分析方向上的进一步增强打开了新的数据通道。