Teaching LLMs Program Semantics via Symbolic Execution Traces

• URL: http://arxiv.org/abs/2605.06184v1
• Date: Thu, 07 May 2026 13:01:06 GMT
• Title: Teaching LLMs Program Semantics via Symbolic Execution Traces
• Abstract summary: We introduce an evaluation framework of 500 C verification tasks built on SV-COMP 2025.<n>We evaluate 14 models across six families and find high overall accuracy masks a critical weakness.<n>Just $sim$3,000 bug traces combined with chain-of-thought reasoning at inference time improve violation detection by over 17 percentage points.
• Score: 0.7046782561282057
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Verification-Aware Training for Speculative Decoding [57.84976863792784]
  We introduce Verification-Aware Training (VAT), a plug-in framework that simulates verification at every training step and turns the resulting accept and reject patterns into supervision.<n>VAT modifies only the training objective, so it can be layered on top of existing methods without changing the draft architecture, the target model, or the inference procedure.<n>VAT improves average acceptance length by up to 11.4% and wall-clock speedup by up to 8.7%, with consistent gains across math, code, and chat benchmarks.
  arXiv  Detail & Related papers  (2026-08-31T01:42:10Z)
• Cybersecurity Detection Classification with Reasoning-enabled Language Models [50.72675435043546]
  A major issue in Security Operations Centers (SOCs) is alert fatigue.<n>Prior work prompts or fine-tunes large language models (LLMs) to emit a triage label directly, but does not train them to reason about whether a detection is a genuine threat.<n>We train a chain-of-thought (CoT) reasoning-enabled triage classifier on real, human-labeled Windows endpoint detections.
  arXiv  Detail & Related papers  (2026-07-30T16:22:13Z)
• Fantastic Adaptive Taxonomies and How to Use Them [100.20614173157708]
  AdaMAST converts execution traces into a compact, evidence-grounded failure taxonomy.<n>No code is hand-authored, no trace human-annotated.<n>In agent-system search, taxonomy-coded diagnoses of failed candidates outperform free-form.
  arXiv  Detail & Related papers  (2026-07-17T17:41:16Z)
• Silent Failures in Quantized LLM Reasoning: A Taxonomy-Based Analysis of Hollow Convergence and Failure Mode Shifts [0.0]
  We show that post-training quantization can silently alter how large language models reason even when task accuracy is preserved.<n>We classify 30,000 chain-of-thought outputs from five instruction-tuned LLMs across three quantization precisions.<n>We find that while accuracy is robust across precisions, Hollow Convergence shows a significant size-dependent shift under NF4.
  arXiv  Detail & Related papers  (2026-07-10T21:55:05Z)
• Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
  Large Language Models produce structured outputs such as travel plans or code solutions.<n>Individual reasoning steps may appear correct while the output as a whole violates budgets, fails test cases, or contradicts earlier deductions.<n>We propose a learned quality scorer with deterministic analytical constraint penalties for verifying structured LLM outputs.
  arXiv  Detail & Related papers  (2026-05-15T17:08:27Z)
• KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code [15.778121969330476]
  We present KVerus, a retrieval-augmented system for Verus-based Rust verification.<n> KVerus constructs a dynamic knowledge base of code metadata, lemma semantics, and toolchain specifics.<n>It can navigate intricate cross-file dependencies to synthesize proofs and automatically repair proofs when faced with common evolutionary changes.
  arXiv  Detail & Related papers  (2026-05-05T14:50:24Z)
• Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
  SPECA is an audit framework that derives explicit, categorized security properties from natural-language specifications and reuses them across implementations.<n>On the RepoAudit benchmark, SPECA reaches 88.9% precision at 100% recall (F1=0.94) and surfaces 12 author-validated bugs beyond ground truth.<n>On the Sherlock Fusaka Audit Contest (10 targets, 366 submissions), SPECA recovers all 15 vulnerabilities expert-augmented and surfaces 4 fix-confirmed bugs.
  arXiv  Detail & Related papers  (2026-04-29T09:57:07Z)
• Claw-Eval: Toward Trustworthy Evaluation of Autonomous Agents [66.97968363332465]
  We introduce Claw-Eval, an end-to-end evaluation suite addressing all three gaps in agent benchmarks.<n>Claw-Eval comprises 300 human-verified tasks spanning 9 categories across three groups.<n>Every agent action is recorded through three independent evidence channels.
  arXiv  Detail & Related papers  (2026-04-07T17:43:18Z)
• TraPO: A Semi-Supervised Reinforcement Learning Framework for Boosting LLM Reasoning [33.47825979936341]
  Reinforcement learning with verifiable rewards (RLVR) has proven effective in training large reasoning models (LRMs)<n>We propose an effective policy optimization algorithm, TraPO, that identifies reliable unlabeled samples by matching their learning trajectory similarity to labeled ones.<n>With only 1K labeled and 3K unlabeled samples, TraPO reaches 42.6% average accuracy, surpassing the best unsupervised method trained on 45K unlabeled samples (38.3%)
  arXiv  Detail & Related papers  (2025-12-15T09:03:45Z)
• LYNX: Learning Dynamic Exits for Confidence-Controlled Reasoning [15.597220136913258]
  LYNX is an online early-exit mechanism that turns a model's own hidden-state awareness into confidence-controlled stopping decisions.<n>We train and calibrate this probe once on a generic mathematical corpus and reuse it unchanged across benchmarks, decoding temperatures, and even non-mathematical tasks.
  arXiv  Detail & Related papers  (2025-12-05T00:04:42Z)
• Explainable Vulnerability Detection in C/C++ Using Edge-Aware Graph Attention Networks [0.2499907423888049]
  This paper presents ExplainVulD, a graph-based framework for vulnerability detection in C/C++ code.<n>It achieves a mean accuracy of 88.25 percent and an F1 score of 48.23 percent across 30 independent runs on the ReVeal dataset.
  arXiv  Detail & Related papers  (2025-07-22T12:49:14Z)
• SEAL: Steerable Reasoning Calibration of Large Language Models for Free [58.931194824519935]
  Large Language Models (LLMs) have demonstrated compelling capabilities for complex reasoning tasks via the extended chain-of-thought (CoT) reasoning mechanism.<n>Recent studies reveal substantial redundancy in the CoT reasoning traces, which negatively impacts model performance.<n>We introduce SEAL, a training-free approach that seamlessly calibrates the CoT process, improving accuracy while demonstrating significant efficiency gains.
  arXiv  Detail & Related papers  (2025-04-07T02:42:07Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• Masked Thought: Simply Masking Partial Reasoning Steps Can Improve Mathematical Reasoning Learning of Language Models [102.72940700598055]
  In reasoning tasks, even a minor error can cascade into inaccurate results. We develop a method that avoids introducing external resources, relying instead on perturbations to the input. Our training approach randomly masks certain tokens within the chain of thought, a technique we found to be particularly effective for reasoning tasks.
  arXiv  Detail & Related papers  (2024-03-04T16:21:54Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.