Generating Verifiable CoT from Execution-Traces

TL;DR

This work tackles the problem that language models struggle to reason about program behavior due to ungrounded, plausible-sounding CoT data. It introduces a complete three-stage data synthesis pipeline that grounds reasoning in actual execution traces, enabling step-by-step rationales that are verifiable by construction. A bi-directional CoT dataset (25k high-quality samples, 54k master set) is created using concept-first curriculum synthesis, execution-based verification with Dual Agreement, and trace-grounded CoT generation, and is evaluated across code-reasoning benchmarks and instruction-tuned models. Results show substantial improvements in output and input prediction, stronger reasoning consistency and information richness, and clear evidence that verification quality and bi-directional reasoning outperform plain CoT; the authors also release an open-source pipeline to enable reproducible, verified reasoning for code.

Abstract

Teaching language models to reason about code execution remains a fundamental challenge. While Chain-of-Thought (CoT) prompting has shown promise, current synthetic training data suffers from a critical weakness: the reasoning steps are often plausible-sounding explanations generated by teacher models, not verifiable accounts of what the code actually does. This creates a troubling failure mode where models learn to mimic superficially convincing but logically flawed reasoning patterns. We address this by grounding CoT generation directly in program execution traces. Our pipeline instruments code to capture its dynamic behavior, then narrates these verified execution traces into natural language rationales that are correct by construction. This execution-grounded approach ensures every reasoning step reflects what the program genuinely computes, eliminating logical hallucinations at the source. We evaluate our method on code reasoning tasks (forward reasoning on CruxEval and LiveCodeBench-Exec, backward reasoning on CruxEval-Input), as well as code generation and explanation tasks from HumanEval. Models trained on our bi-directional trace-grounded data achieve substantial improvements, with gains of up to 30 points on output prediction and 28 points on input prediction over base models, alongside improved explanation and code generation, demonstrating that verifiable reasoning fundamentally enhances model capabilities. https://github.ibm.com/IBM-Research-AI/Verified-Code-CoT

Figures (9)

• Figure 1: Comparison of hallucinated vs trace-grounded CoT. Our approach translates pysnooper execution trace (showing line numbers, variable states, state transitions) into natural language reasoning. Color mapping shows trace sections: yellow=init, blue=iterations, green=return. LLM hallucinates wrong comparison (arr[2] vs arr[1] instead of arr[3]) and wrong search direction.
• Figure 2: An overview of our three-stage data synthesis pipeline. Stage A (Concept Sourcing & Synthesis): Generates candidate concepts, code, and tests from raw documents. Stage B (Verification & Clustering): Uses our execution-based Dual Agreement algorithm to identify and rank the highest-quality solution-test pairs. Stage C (CoT Generation): Uses the verified artifacts and their execution traces to produce the final, bi-directional conversational data, complete with trace-grounded rationales and feedback.
• Figure 3: Bi-directional CoT data format examples. Blue tags denote prompt components (instruction, function, question); green regions show model's trace-grounded reasoning and prediction. Code appears in monospace, reasoning in normal text.
• Figure 4: Signature format templates with extracted metadata. Generated signatures specify function/class names, parameter names and types, and return variable names with types (e.g., tree: tuple, codes: dict). This metadata is stored to validate code/test consistency and prevent hallucinated names or type mismatches.
• Figure 5: Test format requirements. Correct format (left) enables clean I/O extraction for trace generation with direct function calls in assert statements, while prohibited format (right) complicates trace analysis with intermediate variable assignments.