教导AI推理软件
AWS团队通过训练小型语言模型于Soteria的符号执行轨迹上，使其在C语言错误检测上超过了四倍大的模型。本文探讨了这一方法及其对AI辅助软件工程的影响。
亚马逊云服务（AWS）的一个团队近期发布了一项研究，利用Soteria的符号执行轨迹来训练AI模型，使其能够推理代码。研究结果引人注目：通过仅用少量Soteria生成的符号执行轨迹对80亿参数模型进行持续训练，该模型在C语言错误检测方面的表现超过了比它大四倍的模型。
现代AI编码助手正在改变软件开发的方式，但它们有一个根本局限性：能够生成看似正确的代码，却难以理解代码是否真正正确。大型语言模型从海量源代码中学习，但软件工程不仅仅是生成语法正确的代码。人类软件工程师通过观察程序运行来理解其行为，而调试、执行轨迹和测试失败提供了更深的语义理解。
AWS的研究人员直接测量了这一差距。他们构建了包含500个C语言验证任务的评估集，涵盖内存安全、溢出、终止、可达性和数据竞争。结果显示，模型在确认属性成立方面表现良好（多数超过90%），但在检测违规时表现不佳。14个模型中有4个捕获了不到一半的真实错误，且随着程序长度增加，准确率急剧下降。
这正是Soteria发挥作用的地方。Soteria是一款符号执行工具，能够深入语义层推理软件行为。它记录程序状态、符号值、路径条件和分支决策，精确捕获错误发生的条件。这些轨迹可以导出为机器可读的JSON或交互式HTML，从而将符号执行从验证技术转变为训练数据的来源。
研究人员将Soteria在开源C代码上运行，收集轨迹，然后用这些轨迹对Qwen3-8B模型进行持续预训练。结果显示，训练后模型在软件验证任务上表现显著提升。最佳组合是使用Soteria的错误轨迹训练，并在推理时让模型逐步推理，这使违规检测提高了17.9个百分点。训练后的8B模型检测违规的可靠性（67%）超过了未训练的32B模型（57%）。
更重要的是，训练泛化到了所有五种属性类型，表明模型学习了通用推理模式，而非记忆特定错误形状。这意味着下一代AI不仅可以从源代码学习，还可以从程序语义——即代码实际如何执行——中学习。
Soteria团队认为，这将在AI和验证之间创建强大的良性循环：AI生成代码，Soteria分析代码生成语义轨迹，轨迹帮助训练更好的AI模型，再生成更高质量的代码。长期目标是让Soteria在crates.io（Rust包注册表）上运行，生成Rust代码有史以来最大的语义数据集。
未来的软件工程将由AI和形式验证的交互塑造。最强大的系统将结合语言模型的创造力和规模与形式推理的严谨性和精确性。Soteria正是为此而建。