# Teaching LLMs Program Semantics via Symbolic Execution Traces

arXiv: https://arxiv.org/abs/2605.06184 · HTML: https://mlsanity.com/paper/2605.06184/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 25 of its 38 references that are in the map.
- First posted on arXiv 7 May 2026.

## Builds on (most cited first, 25 of 25)

- [CRUXEval: A Benchmark for Code Reasoning, Understanding and Execution](https://mlsanity.com/paper/2401.03065/) (2024)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [CWM: An Open-Weights LLM for Research on Code Generation with World Models](https://mlsanity.com/paper/2510.02387/) (2025)
- [NExT: Teaching Large Language Models to Reason about Code Execution](https://mlsanity.com/paper/2404.14662/) (2024)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [Code Execution with Pre-trained Language Models](https://mlsanity.com/paper/2305.05383/) (2023)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [CoRe: Benchmarking LLMs Code Reasoning Capabilities through Static Analysis Tasks](https://mlsanity.com/paper/2507.05269/) (2025)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (2025)
- [Everything You Wanted to Know About LLM-based Vulnerability Detection But Were Afraid to Ask](https://mlsanity.com/paper/2504.13474/) (2025)
- [What I cannot execute, I do not understand: Training and Evaluating LLMs on Program Execution Traces](https://mlsanity.com/paper/2503.05703/) (2025)
- [LoCoBench: A Benchmark for Long-Context Large Language Models in Complex Software Engineering](https://mlsanity.com/paper/2509.09614/) (2025)
- [CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detection](https://mlsanity.com/paper/2503.09433/) (2025)
- [Agentic Property-Based Testing: Finding Bugs Across the Python Ecosystem](https://mlsanity.com/paper/2510.09907/) (2025)
- [Trace Gadgets: Minimizing Code Context for Machine Learning-Based Vulnerability Prediction](https://mlsanity.com/paper/2504.13676/) (2025)
- [SkipAnalyzer: A Tool for Static Code Analysis with Large Language Models](https://mlsanity.com/paper/2310.18532/) (2023)
- [Chain of Execution Supervision Promotes General Reasoning in Large Language Models](https://mlsanity.com/paper/2510.23629/) (2025)
- [ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis](https://mlsanity.com/paper/2512.10173/) (2025)
- [Integrating Symbolic Execution into the Fine-Tuning of Code-Generating LLMs](https://mlsanity.com/paper/2504.15210/) (2025)
- [Soteria: Efficient Symbolic Execution as a Functional Library](https://mlsanity.com/paper/2511.08729/) (2025)

## Abstract (arXiv)

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 ~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× 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.