Technical Summary: Teaching LLMs Program Semantics via Symbolic Execution Traces

Problem Statement

Large Language Models (LLMs) demonstrate high proficiency in understanding high-level code but struggle with low-level C code, particularly regarding memory safety, pointer arithmetic, and undefined behavior. While existing benchmarks for semantic code understanding exist, they often approach saturation or fail to isolate the specific reasoning required for C verification.

A critical gap identified in this work is the asymmetry in LLM performance: models are generally reliable at confirming that a property holds (e.g., "no overflow occurs"), but significantly weaker at detecting when a property is violated. This weakness is exacerbated by program length; violation detection accuracy degrades sharply as code length increases, often falling below 50% for programs of just 100–200 lines. Furthermore, this deficit does not correlate straightforwardly with model size or code specialization, suggesting that training data and objectives are more influential than scale alone.

Methodology

1. Evaluation Framework

The authors constructed a benchmark based on SV-COMP 2025 (Software Verification Competition), comprising 500 C verification tasks across five property types:

• Memory Safety
• Absence of Overflows
• Termination
• Reachability
• Absence of Data Races

The dataset was curated to be balanced (50% property holds, 50% violated) and varied in length (0–400 lines). Ground truth was established by formal verification tools. The framework evaluates 14 models across six families, measuring binary classification accuracy (holds vs. violated) without requiring witness generation.

2. Training Pipeline: Symbolic Execution Traces

To address the violation detection gap, the authors propose a training pipeline using formal verification artifacts rather than raw code or labeled bug reports.

• Data Source: The pipeline utilizes the CodeParrot dataset (14M C files), filtered to 1 million self-contained files.
• Symbolic Execution: The Soteria engine (an open-source symbolic execution tool for C and Rust) is run on these files. Unlike concrete execution, Soteria reasons over all possible inputs simultaneously, tracking memory states and branch conditions.
• Trace Curation: The authors filter the output to retain only manifest bug traces—cases where Soteria proves a violation occurs on all feasible inputs. This yielded approximately 3,208 high-quality traces.
• Training Strategy: The authors perform Continued Pretraining (CPT) on the Qwen3-8B model using these traces. They systematically ablate variables including:
  • Trace Content: Manifest bugs vs. latent bugs vs. no-violation traces.
  • Trace Format: Raw HTML output (preserving structural tags) vs. plain text vs. informalized natural language summaries.
  • Inference Mode: Standard decoding vs. Chain-of-Thought (CoT) "thinking" mode.

Key Contributions

1. Comprehensive Evaluation Framework: A benchmark of 500 C verification tasks revealing that violation detection is a distinct and harder capability than property confirmation, with performance dropping significantly for longer programs.
2. Automated Training Pipeline: A scalable, annotation-free method to generate training data by running symbolic execution on generic open-source code. The pipeline filters for manifest bugs to create a high-signal dataset.
3. Synergistic Training Strategy: The discovery that Continued Pretraining (CPT) on symbolic execution traces and Chain-of-Thought (CoT) reasoning at inference time are individually insufficient but superadditive in combination.
   • CPT alone improves violation detection by ~7.3 percentage points.
   • CoT alone provides no gain (and can degrade performance).
   • CPT + CoT yields a 17.9 percentage point improvement in violation detection.
4. Semantic vs. Volume: Evidence that the improvement stems from the semantic information in the traces (the logic of why a bug occurs) rather than simply increasing code exposure. Training on the underlying C source files without traces actually degraded performance.

Results

• Violation Detection: The best configuration (Qwen3-8B trained on 3,208 HTML-formatted manifest bug traces + CoT inference) improved violation detection from a baseline of 49.4% to 67.3%.
• Overall Accuracy: The trained model achieved 72.7% overall accuracy, approaching the performance of the Qwen3-32B base model (76.2%) while substantially outperforming it on violation detection (67.3% vs. 56.9%).
• Generalization: Improvements transferred to all five property types, including termination, data races, and reachability, even though the training traces (Soteria's built-in checks) primarily targeted memory safety and overflows. This suggests the model learned general verification reasoning patterns.
• Format Sensitivity: Preserving the structured HTML format of Soteria's output was critical. Converting traces to plain text or informal natural language summaries significantly degraded performance, particularly when combined with CoT.
• Ablation Findings:
  • Training on all traces (including non-bugs) hurt performance.
  • Training on latent bugs (not proven on all paths) hurt performance.
  • Training on the raw C code alone hurt performance.
  • Few-shot prompting with trace examples failed to replicate the gains of CPT.

Significance and Claims

The paper claims that formal verification artifacts serve as a potent, previously untapped resource for training LLMs on low-level code semantics. The primary significance lies in demonstrating that:

1. Scale is not the sole driver: A smaller model (8B) trained on specific semantic traces can outperform a much larger model (32B) on the specific task of bug detection.
2. Trace Semantics matter: The structured, logical reasoning embedded in symbolic execution traces (e.g., path conditions, memory state transitions) is more valuable for verification than raw code volume.
3. Superadditivity: The combination of internalizing verification logic via pretraining and utilizing extended reasoning (CoT) at inference creates a capability that neither component possesses alone.

The authors emphasize that their approach requires no manual annotation, relies on open-source tools and code, and produces models that generalize to unseen verification tasks (including those not explicitly checked by the training tool, such as data races). They conclude that while the approach improves reliability, it does not yet close the gap to formal verification tools, and future work should explore multi-file contexts and reinforcement learning loops.