通过符号执行跟踪教授 LLM 程序语义

我们引入了基于 SV-COMP 2025 构建的跨五种属性类型（内存安全、溢出、终止、可达性、数据竞争）的 500 个 C 验证任务的评估框架，并评估了 6 个系列的 14 个模型。我们发现，较高的整体准确率掩盖了一个关键弱点：虽然大多数模型可靠地确认属性成立，但违规检测变化很大，并且随着程序长度的增加而急剧下降。为了弥补这一差距，我们对形式验证工件进行训练：在通用开源 C 代码上运行 Soteria 符号执行引擎，并使用生成的跟踪来继续对 Qwen3-8B 进行预训练。仅 ${\sim}$3,000 的错误跟踪与推理时的思想链推理相结合，就将违规检测提高了 17 个百分点以上，从而产生了评估模型中最平衡的准确度概况之一。在违规检测方面，经过训练的 8B 模型在不加思考的情况下胜过大 4 倍的 Qwen3-32B，并且在整体精度上接近它。痕迹训练和思维链之间的相互作用是超加性的：两者都不能单独提供有意义的收益，但它们的组合可以提供有意义的收益。改进转移到所有五种属性类型，包括训练跟踪不针对的属性类型。我们的 28 个配置证实了收益源于跟踪语义，而不是代码量，并且跟踪管理和格式很重要。