Agentic Code Reasoning

This paper introduces "semi-formal reasoning," a structured prompting methodology that enables LLM agents to accurately analyze code semantics and verify patches without execution, significantly improving performance across fault localization, patch equivalence, and code question answering tasks.

The Gist

Imagine you are a detective trying to solve a mystery in a massive, ancient library (the codebase). You have two different maps (patches) that claim to fix a broken door. Your job is to figure out: Do these two maps lead to the same destination, or will one of them get you stuck in a wall?

Usually, to know for sure, you would have to physically walk the path, try the door, and see what happens. In the world of software, this means running the code and testing it. But running tests is slow, expensive, and sometimes impossible (like trying to test a bridge before it's built).

This paper introduces a new way for AI detectives to solve these mysteries without ever leaving the library. They call this "Agentic Code Reasoning."

Here is the simple breakdown of how they did it and why it matters.

The Problem: The "Guessing Game"

Previously, AI agents tried to solve these puzzles using "Chain of Thought." Think of this as a detective talking to themselves: "Hmm, this looks like that, so it probably works."

The problem? The AI is too confident. It often guesses based on how things look rather than how they work.

• The Mistake: In the paper's example, the AI saw two code snippets that looked like they did the same math. It said, "Yes, they are the same!"
• The Reality: One snippet used a special tool from the library that only worked on "dates," while the other used a standard tool. The AI didn't check the tool's manual; it just guessed. The result? One map led to a dead end (a crash), and the other worked.

The Solution: The "Semi-Formal Certificate"

The authors realized that if they forced the AI to act like a lawyer instead of a guesser, it would get much smarter.

They introduced "Semi-Formal Reasoning." Instead of letting the AI ramble, they gave it a strict fill-in-the-blank template (a certificate). To win the case, the AI must provide:

1. Premises: "Here is exactly what this code changes."
2. The Trace: "I followed the path step-by-step. I saw that function A calls function B, which calls function C."
3. The Conclusion: "Therefore, the result is X."

The Analogy:

• Standard Reasoning is like a student saying, "I think the answer is 42 because it feels right."
• Semi-Formal Reasoning is like a student saying, "I know the answer is 42 because I showed my work: $10 \times 4 = 40$, plus$2 = 42$. Here is the calculator proof."

If the AI tries to skip a step or make a claim without evidence, the template forces it to stop and look again. It acts as a certificate of truth.

The Three Tests

The researchers tested this "Lawyer AI" on three different types of cases:

1. The Patch Equivalence Test (Are these fixes the same?):

   • The Challenge: Two developers fix the same bug. Are their solutions identical?
   • The Result: The "Lawyer AI" got it right 93% of the time, compared to 78% for the "Guesser AI." It caught subtle differences that the other AI missed.

2. The Fault Localization Test (Where is the broken part?):

   • The Challenge: A program crashes. Find the exact line of code causing it without running the program.
   • The Result: The structured approach helped the AI find the broken line much faster and more accurately, improving its success rate by about 12%.

3. The Code Question Test (What does this code do?):

   • The Challenge: Answer complex questions about how a specific piece of software behaves.
   • The Result: The AI became much better at answering correctly, jumping from 78% to 87% accuracy.

Why This Matters (The "So What?")

Imagine you are training a robot to be a software engineer. Usually, to teach the robot, you have to let it try a fix, run the tests, and see if it passes. This takes hours and requires powerful computers.

With this new method, the AI can simulate the test results in its head with high accuracy.

• Speed: It doesn't need to wait for the computer to run the tests.
• Cost: It saves money on computing power.
• Safety: It can verify code before it's even built, preventing disasters.

The Bottom Line

This paper shows that if you give an AI a structured checklist and force it to show its work like a lawyer, it stops guessing and starts truly understanding code. It's a way to make AI smarter, more reliable, and capable of doing deep analysis without needing to "run" the software first.

In short: Don't just ask the AI, "Is this right?" Ask it, "Show me the evidence, step-by-step, and then tell me." The answer will be much better.

Technical Summary

Here is a detailed technical summary of the paper "Agentic Code Reasoning" by Shubham Ugare and Satish Chandra (Meta).

1. Problem Statement

The paper addresses the challenge of enabling Large Language Model (LLM) agents to perform deep semantic code analysis without executing the code. Specifically, it investigates whether agents can:

• Navigate complex codebases.
• Trace execution paths and dependencies across multiple files.
• Determine semantic equivalence (e.g., do two patches produce the same test outcomes?) or locate faults.

The Core Challenge:
Current "unstructured" Chain-of-Thought (CoT) reasoning allows agents to make unsupported claims or skip critical edge cases, leading to hallucinations. Conversely, fully formal verification (e.g., using Lean or Coq) is impractical for arbitrary, multi-language repositories because translating real-world code into formal logic is too expensive and error-prone. The authors seek a middle ground: a method that enforces rigorous reasoning without requiring full formalization.

2. Methodology: Semi-Formal Reasoning

The authors introduce Semi-Formal Reasoning, a structured prompting methodology designed to act as a "certificate" of correctness. Unlike unstructured CoT, this approach requires the agent to fill in specific, structured templates that enforce a logical flow.

Key Components of the Method:

• Structured Templates: Agents must follow a task-specific template that mandates:
  1. Explicit Premises: Stating exactly what code is modified and what the tests check.
  2. Execution Tracing: For every claim, the agent must trace the specific execution path (e.g., function calls, variable flows) rather than guessing behavior.
  3. Formal Conclusions: Deriving a final answer based strictly on the gathered evidence.
• Agentic Exploration: The agents operate in a "static" mode (no code execution). They use tools (like grep, file reading) to explore the repository, trace dependencies, and gather context iteratively.
• Task-Specific Adaptation:
  • Patch Equivalence: Requires comparing test outcomes (Pass/Fail) for two patches, including handling "Fail-to-Pass" and "Pass-to-Pass" tests.
  • Fault Localization: Requires tracing from a failing test to the specific buggy code lines, distinguishing between the symptom (crash site) and the root cause.
  • Code Question Answering: Requires function trace tables, data flow analysis, and alternative hypothesis checks.

Motivating Example (Django):
In a patch equivalence task, standard reasoning assumed format() referred to Python's builtin, concluding two patches were equivalent. Semi-formal reasoning forced the agent to trace the actual definition of format in the Django module, discovering it was shadowed by a custom function expecting a datetime object. This revealed that Patch 1 would raise an AttributeError while Patch 2 would succeed, correctly identifying them as non-equivalent.

3. Key Contributions

1. Introduction of Semi-Formal Reasoning: A novel prompting strategy that bridges the gap between unstructured natural language reasoning and fully formal verification. It acts as a certificate, preventing agents from skipping cases.
2. Comprehensive Evaluation: The approach is evaluated across three distinct, high-stakes tasks:
   • Patch Equivalence Verification (SWE-bench context).
   • Fault Localization (Defects4J).
   • Code Question Answering (RubberDuckBench).
3. Execution-Free Verification: Demonstrates that high-accuracy verification is possible without running tests, which is critical for reducing the computational cost of Reinforcement Learning (RL) training pipelines for software agents.

4. Experimental Results

The authors evaluated their method using state-of-the-art models (Opus-4.5, Sonnet-4.5) against standard unstructured reasoning baselines.

• Patch Equivalence (Curated Dataset):
  • Accuracy improved from 78.2% (Standard) to 88.8% (Semi-formal).
  • On real-world agent-generated patches, accuracy reached 93.0% with semi-formal reasoning, significantly outperforming single-shot baselines (86%) and difflib similarity checks (73%).
• Code Question Answering (RubberDuckBench):
  • Opus-4.5 achieved 87.0% accuracy with semi-formal reasoning, a 9 percentage point gain over standard agentic reasoning (78.3%).
  • The structured format forced the agent to verify data flows, eliminating guesses based on function names.
• Fault Localization (Defects4J):
  • On a 100-bug sample, semi-formal reasoning improved Top-5 accuracy by 5 percentage points over standard reasoning.
  • In a smaller, context-fitting sample, the improvement was up to 12 percentage points.
  • The method successfully identified root causes (e.g., in Mockito_8) rather than just the crash sites, which standard reasoning often missed.

Trade-off: The semi-formal approach requires more computational steps (approx. 2.8x more steps in patch equivalence) to generate the detailed certificates, but the accuracy gains justify the cost for high-stakes verification.

5. Significance and Future Work

• RL Training Pipelines: The ability to verify patches with 93% accuracy without executing code offers a cheap, scalable reward signal for training software engineering agents via Reinforcement Learning, removing the bottleneck of sandbox execution.
• Alternative to Static Analysis: This approach offers a flexible alternative to classical static analysis tools. Instead of hard-coding analysis logic for specific languages, LLMs can be prompted with general reasoning templates that adapt to any framework.
• Limitations & Future Directions:
  • Failure Modes: Errors still occur due to incomplete tracing, unknown third-party library semantics, or dismissing subtle differences.
  • Future Work: The authors suggest fine-tuning models to internalize these templates (reducing prompt overhead), applying the method to security vulnerability detection, and creating hybrid systems that combine LLM reasoning with lightweight formal methods.

Conclusion:
The paper demonstrates that structured agentic reasoning enables LLMs to perform meaningful, deep semantic code analysis without execution. By enforcing a "semi-formal" certificate structure, agents can significantly reduce hallucinations and improve accuracy in complex software engineering tasks, paving the way for more reliable automated code review and verification systems.