Teaching LLMs Program Semantics via Symbolic Execution Traces

📄 arXiv: 2605.06184v1 📥 PDF

作者: Jonas Bayer, Stefan Zetzsche, Olivier Bouissou, Remi Delmas, Michael Tautschnig, Soonho Kong

分类: cs.SE, cs.LG, cs.PL

发布日期: 2026-05-07

💡 一句话要点

利用符号执行轨迹教导LLM理解程序语义，显著提升程序验证任务中的缺陷检测能力。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 程序验证 大语言模型 符号执行 程序语义 缺陷检测

📋 核心要点

  1. 现有LLM在程序验证任务中，虽然整体准确率较高，但在检测程序违规行为方面表现不足，尤其是在处理较长程序时。
  2. 论文提出利用符号执行生成的程序轨迹来训练LLM，使模型能够学习程序语义，从而提高违规检测能力。
  3. 实验表明，使用少量错误轨迹结合思维链推理，可以显著提升LLM在程序验证任务中的违规检测能力，甚至超越更大的模型。

📝 摘要（中文）

本文提出了一个包含500个C程序验证任务的评估框架，涵盖五种属性类型（内存安全、溢出、终止、可达性、数据竞争），基于SV-COMP 2025构建，并评估了六个系列的14个模型。研究发现，高整体准确率掩盖了一个关键弱点：虽然大多数模型能可靠地确认属性成立，但违规检测差异很大，并且随着程序长度的增加而急剧下降。为了弥补这一差距，本文利用形式验证工件进行训练：在通用开源C代码上运行Soteria符号执行引擎，并将生成的轨迹用于Qwen3-8B的持续预训练。仅使用约3,000个错误轨迹，结合推理时的思维链（chain-of-thought）推理，违规检测就提高了超过17个百分点，产生了评估模型中最平衡的准确率曲线之一。在违规检测方面，训练后的8B模型优于4倍大的Qwen3-32B（不使用思维链），并且在整体准确率上接近它。轨迹训练和思维链之间的交互是超加性的：单独使用都不能提供有意义的增益，但它们的组合可以。改进可以推广到所有五种属性类型，包括训练轨迹未针对的类型。28种配置证实了增益源于轨迹语义，而不是代码量，并且轨迹的策划和格式很重要。

🔬 方法详解

问题定义：现有的大语言模型（LLM）在程序验证任务中，虽然能够较好地确认程序属性的正确性，但在检测程序中存在的违规行为（例如内存安全问题、溢出等）时表现不佳。尤其当程序代码较长时，LLM的违规检测能力会显著下降。这限制了LLM在程序安全领域的应用。

核心思路：论文的核心思路是利用符号执行技术生成的程序执行轨迹来教导LLM理解程序语义。符号执行能够探索程序的不同执行路径，并生成包含程序状态信息的轨迹。通过在这些轨迹上训练LLM，可以使模型学习到程序中潜在的错误模式，从而提高违规检测能力。此外，结合思维链（Chain-of-Thought）推理，可以进一步提升LLM的推理能力。

技术框架：整体框架包括以下几个主要步骤：1) 使用Soteria符号执行引擎在开源C代码上生成程序执行轨迹，特别是包含错误信息的轨迹。2) 使用这些轨迹对Qwen3-8B模型进行持续预训练。3) 在包含500个C程序验证任务的评估框架上评估训练后的模型，并与其它模型进行比较。4) 在推理阶段，采用思维链（Chain-of-Thought）推理，引导模型逐步分析程序，提高推理的准确性。

关键创新：论文的关键创新在于将符号执行生成的程序轨迹作为训练数据，用于提升LLM的程序语义理解能力。与直接使用代码进行训练相比，程序轨迹包含了更丰富的程序状态信息，能够更有效地帮助LLM学习到程序中潜在的错误模式。此外，论文还发现轨迹训练和思维链推理之间存在超加性效应，即两者结合使用能够产生比单独使用更大的增益。

关键设计：论文的关键设计包括：1) 使用Soteria符号执行引擎生成高质量的程序轨迹，特别是包含错误信息的轨迹。2) 精心策划和格式化训练轨迹，以提高训练效果。3) 在推理阶段，采用思维链（Chain-of-Thought）推理，引导模型逐步分析程序，提高推理的准确性。4) 实验中使用了Qwen3-8B模型作为基础模型，并进行了持续预训练。训练数据量约为3000个错误轨迹。

📊 实验亮点

实验结果表明，使用约3,000个错误轨迹结合思维链推理，违规检测准确率提高了超过17个百分点。训练后的8B模型在违规检测方面优于4倍大的Qwen3-32B（不使用思维链），并且在整体准确率上接近它。这表明，通过学习程序语义，LLM可以在程序验证任务中取得显著的性能提升。

🎯 应用场景

该研究成果可应用于软件安全领域，帮助开发者更有效地检测程序中的漏洞和错误，提高软件的可靠性和安全性。此外，该方法还可以推广到其他程序分析任务中，例如程序调试、代码优化等。未来，可以将该方法应用于更复杂的程序和编程语言，并探索更有效的训练策略。

📄 摘要（原文）

We introduce an evaluation framework of 500 C verification tasks across five property types (memory safety, overflow, termination, reachability, data races) built on SV-COMP 2025, and evaluate 14 models across six families. We find that high overall accuracy masks a critical weakness: while most models reliably confirm properties hold, violation detection varies widely and degrades sharply with program length. To close this gap, we train on formal verification artifacts: running the Soteria symbolic execution engine on generic open-source C code and using the resulting traces for continued pretraining of Qwen3-8B. Just ${\sim}$3,000 bug traces combined with chain-of-thought reasoning at inference time improve violation detection by over 17 percentage points, producing one of the most balanced accuracy profiles among evaluated models. On violation detection, the trained 8B model outperforms the 4$\times$ larger Qwen3-32B without thinking and approaches it in overall accuracy. The interaction between trace training and chain-of-thought is superadditive: neither alone provides meaningful gains, but their combination does. Improvements transfer across all five property types, including ones the training traces do not target. Our 28 configurations confirm the gains stem from trace semantics, not code volume, and that trace curation and format matter.