[Paper] 通过符号执行轨迹教授 LLMs 程序语义

Source: arXiv - 2605.06184v1

Overview

一项新研究表明，通过向大型语言模型（LLMs）展示符号执行轨迹——即程序行为的详细逐步表示——可以让模型学习理解 C 程序的语义。作者仅使用几千条此类轨迹，对一个规模为 80 亿参数的模型（Qwen‑3‑8B）进行微调，就显著提升了模型检测错误的能力，包括内存安全违规、溢出和数据竞争等问题，从而弥补了标准 LLM 在这些方面的巨大缺口。

关键贡献

• 500 任务基准，覆盖五种验证属性（内存安全、溢出、终止性、可达性、数据竞争），基于 SV‑COMP 2025 套件构建。
• 全面评估了来自六个家族的 14 种 LLM，揭示大多数模型在确认正确行为方面表现出色，但在检测违规，尤其是较长程序中的违规时表现不足。
• 基于轨迹的预训练：使用约 3 k 条符号执行错误轨迹（来自 Soteria 引擎）继续对 Qwen‑3‑8B 进行预训练。
• 推理时的链式思考 (CoT) 提示，结合轨迹训练模型，可实现 +17 pp 的违规检测准确率提升。
• 超加成效应：轨迹训练 和 CoT 同时使用的效果优于任一单独技术，即使训练轨迹仅针对五种属性中的一部分。
• 效率提升：8 B 轨迹训练模型的表现超过未进行轨迹训练的 32 B 基线，并在使用 CoT 时缩小了与更大模型的差距。
• 消融研究（28 种配置）证实收益来源于轨迹的语义内容，而不仅是额外的代码曝光，并且轨迹的格式/策划也很重要。

方法论

1. Benchmark construction – 作者从 SV‑COMP 2025 竞赛中挑选了 500 个 C 程序，并为每个程序标注了五种验证属性之一以及该属性是成立（安全）还是被违反（错误）。
2. Baseline evaluation – 对 14 种现成的大语言模型（包括 LLaMA、GPT‑NeoX 和 Qwen 系列）进行提示，让它们对每个任务回答“成立/违反”，分别在有无链式思考（CoT）推理的情况下进行。
3. Trace generation – 使用开源的 Soteria 符号执行引擎，对每个有缺陷的程序进行运行，并记录导致违规的 执行轨迹（变量状态、路径约束等）。共收集约 3 k 条不同的错误轨迹。
4. Continued pre‑training – 对 Qwen‑3‑8B 模型进行进一步训练，使用混合数据集：原始代码片段 + 符号轨迹，格式为 <code> → <trace>。
5. Inference with CoT – 在测试阶段，提示中加入“思考一步”的指令，鼓励模型在回答前通过轨迹进行推理。
6. Ablations – 变体包括 (a) 仅在原始代码上训练，(b) 在无 CoT 的情况下训练轨迹，(c) 不同的轨迹粒度，以及 (d) 扩大轨迹数量。

Source: …

结果与发现

• 平衡性能：经过 trace 训练的 8 B 模型实现了近乎对称的混淆矩阵——在检测漏洞和确认安全性方面同样可靠。
• 长度敏感性：对于代码行数 >200 LOC 的程序，普通模型的违规检测下降超过 20 pp；而 trace 训练模型的下降幅度小于 5 pp。
• 跨属性迁移：尽管训练时的 trace 仅覆盖了内存安全漏洞，但在溢出、终止和数据竞争任务上也观察到了检测性能的提升。
• 格式重要性：包含显式约束求解步骤的 trace（例如 “assert x ≤ MAX”）相比仅提供原始符号状态的 trace 能带来更高的增益。

实际意义

• 开发者工具：将具备追踪感知的 LLM 嵌入 IDE 中，可提供超越模式匹配检查器的语义错误提示，尤其针对难以检测的数据竞争等问题。
• 自动化代码审查：公司可以在自有代码库中精选的执行追踪上微调中等规模模型，从而在无需对每个 PR 进行完整符号执行的情况下，获得相当于验证级别的洞察。
• 成本效益验证：研究表明，当加入语义追踪后，体积小、成本低的模型（8 B）也能与更大模型竞争，从而降低持续集成流水线的计算预算。
• 教育与入职培训：基于追踪生成的交互式“思考过程”解释，可帮助初级开发者理解代码为何不安全，弥合静态分析报告与人类直觉之间的差距。

限制与未来工作

• Trace diversity: 训练集仅包含约 3 k 条来自开源项目的错误追踪；罕见或特定领域的错误仍可能被遗漏。
• Scalability to larger codebases: 虽然追踪训练缓解了与长度相关的性能下降，但该方法尚未在超过数千行的程序或多模块项目上进行测试。
• Property coverage: 仅研究了五种验证属性；将其扩展到安全相关属性（例如污点分析）仍有待探索。
• Model generality: 实验聚焦于 Qwen；在其他架构（如 LLaMA、Mistral）上复制这些收益仍需验证。
• Human‑in‑the‑loop: 未来工作可以探索开发者如何为专有代码提供自定义追踪，形成一个持续改进模型语义理解的反馈循环。

作者

• Jonas Bayer
• Stefan Zetzsche
• Olivier Bouissou
• Remi Delmas
• Michael Tautschnig
• Soonho Kong

论文信息

• arXiv ID: 2605.06184v1
• Categories: cs.SE, cs.LG, cs.PL
• Published: 2026年5月7日
• PDF: 下载 PDF