The Path Not Taken: Duality in Reasoning about Program Execution

1. Problem Statement

Large Language Models (LLMs) have demonstrated significant capabilities in coding tasks, yet their adoption in software engineering is hindered by a lack of true causal understanding of program execution. Current evaluation benchmarks primarily focus on single-path reasoning: predicting program outputs or properties (e.g., code coverage) for a specific input.

The authors identify two critical limitations in existing approaches:

1. Narrow View: Single-test evaluations only probe one execution path, failing to assess how models understand branching logic, state changes, and alternative flows.
2. Data Contamination: Benchmarks based on fixed input-output pairs are prone to memorization during training, leading to inflated performance metrics that do not reflect genuine reasoning capabilities.

The core problem is the absence of a framework that evaluates an LLM's ability to reason about the duality of program execution: understanding both what happens given an input and how to mutate that input to force a different execution path.

2. Methodology: The Duality Framework

The paper introduces the concept of Dual-Path Reasoning, which posits that understanding program execution requires evaluating two complementary tasks that share a common execution space but diverge at branching points.

A. The Two Reasoning Tasks

1. Forward Reasoning (Execution Reasoning):
   • Task: Given a program $P$ and an input $I_{exec}$, predict the observable behavior $\phi(\tau_{exec})$ (e.g., code coverage, output).
   • Goal: Assess the model's ability to simulate the program state forward from a given input.
2. Backward Reasoning (Counterfactual Reasoning):
   • Task: Given $P$, $I_{exec}$, and a desired behavioral objective $\phi^*$ (e.g., reaching an uncovered branch), infer the mutated input $I_{cf}$ required to achieve that objective.
   • Goal: Assess the model's ability to reason backward from a desired effect to the necessary causal conditions (input perturbations) to induce a counterfactual execution path $\pi_{cf}$.

B. The Benchmark: DEXBENCH

To operationalize this framework, the authors constructed DEXBENCH, a benchmark comprising 445 paired instances derived from three datasets: CruxEval, HumanEval, and PythonSaga.

• Construction: Programs are selected if they contain control flow (loops/conditionals) and yield partial code coverage under a specific test case.
• Task Definition:
  • Forward: Predict the set of executed lines (statement coverage) for the given input.
  • Backward: Generate a new input that forces the program to execute a specific, previously uncovered branch (maximizing coverage increase).
• Evaluation Metric: A Joint Success Indicator ($S_{dual}$) is used, requiring the model to simultaneously correctly predict the original coverage AND generate a valid counterfactual input. Success is defined as $S_{exec} \land S_{cf}$.

3. Key Contributions

1. Conceptual Framework: Formalizes "Duality in Reasoning," arguing that true program understanding requires causal reasoning across both forward execution and backward counterfactual mutation.
2. DEXBENCH Benchmark: Introduces a rigorous, dual-path benchmark that mitigates data contamination risks by requiring fine-grained reasoning over intermediate program states rather than simple input-output mapping.
3. Comprehensive Evaluation: Evaluates 13 LLMs (9 open-source, 4 closed-source) ranging from 3B to 72B parameters, including specialized reasoning models.

4. Key Results

The experiments reveal several counter-intuitive findings regarding LLM capabilities:

• Asymmetry of Performance: Strong performance in isolation (either forward or backward) does not guarantee success in joint evaluation. Many models succeed at predicting coverage but fail to mutate inputs correctly, or vice versa.
• Scaling Laws Do Not Guarantee Reasoning:
  • Small models (<10B) fail almost entirely at dual-path reasoning.
  • Mid-sized models (20B–30B) often outperform larger models. For instance, Qwen2.5-32B significantly outperforms Qwen2.5-72B in dual-path reasoning.
  • Reasoning-focused post-training does not consistently improve performance. Non-reasoning variants (e.g., Mistral Small 24B, Qwen2.5-32B) often outperform their reasoning-focused counterparts (e.g., Magistral Small, QwQ-32B) on this specific task.
• Closed-Source Dominance: Closed-source models (e.g., Claude Sonnet 4, Grok-4 Reasoning, GPT-5 Mini) generally achieve the highest scores, though they still struggle with complex control flow in the PythonSaga dataset.
• Error Analysis:
  • Forward errors are often due to prompt misreading or hallucination of code structure.
  • Backward errors frequently stem from semantic misunderstandings of API behavior (e.g., misinterpreting split() vs. splitlines()) or failure to maintain causal consistency in state transitions.

5. Significance and Implications

• Beyond Single-Path Evaluation: The paper demonstrates that single-path benchmarks are insufficient for assessing dynamic code understanding. Dual-path reasoning serves as a robust proxy for causal, state-aware reasoning.
• Redefining Model Capability: The results challenge the assumption that larger parameter counts or explicit "reasoning" post-training automatically lead to better program execution understanding. It suggests that current "reasoning" models may still rely on surface-level pattern matching rather than deep causal simulation.
• Future Directions: The framework is extensible to other dynamic behaviors (e.g., predicting intermediate states or specific outputs) and provides a systematic method for debugging and testing LLMs in software engineering contexts.

In conclusion, DEXBENCH establishes that true program execution reasoning is inherently dual. By requiring models to bridge the gap between observed behavior and counterfactual causality, it offers a more rigorous and discriminative evaluation of LLMs in software engineering than existing benchmarks.