The Reasoning Gap

The systems that work combine neural proposals with something that can check them. Reasoning becomes an architectural property.

Something interesting happened as we meander towards AGI: we are noticing that the most capable AI systems are not pure neural networks at all & we have sort of gone full circle back to hybrid architectures.

Consider two data points. First: Claude Sonnet 4 can now maintain focus on complex, multi-step coding tasks for over 30 hours, achieving 77.2% on SWE-bench Verified—solving real GitHub issues that would take human engineers days. Coding agents are shipping production features, passing code review, and operating autonomously across massive codebases. The practical utility is undeniable.

Second: on ARC-AGI-2 (December 2025), the latest benchmark designed to test genuine abstract reasoning, the best reasoning models score between 4% and 54%, depending on how much compute you throw at them. Claude Opus 4.5 with extended thinking reaches 37.6%. Gemini 3 Pro hits 31%. The top bespoke solution, built with refinement loops, reaches 54%. Humans? They average 60%, with 100% of tasks solvable by at least two people.

These aren't contradictory findings. They're the same finding, viewed from different angles.

The systems that work—really work, in production, for hours on end are not succeeding because LLMs have suddenly learned to reason. They're succeeding because they've been architected to avoid relying on LLM reasoning. Code execution. External verification. Symbolic critics. Test suites. Type checkers. The neural network proposes; something else disposes.

This is the central insight reshaping AI engineering in 2025: reasoning is a system-level property, not a model-level one.

Verification as Theory Building

In 1985, Peter Naur wrote a paper called "Programming as Theory Building" that is quietly influential in software engineering circles. His argument: the real output of programming isn't code; rather it's a theory about how the problem domain maps to the solution. Code is just a lossy representation of that theory. When the original developers leave, and only the code remains, we lose something essential. The program, in a meaningful sense, is a ghostly apparition that is slowly fading away. I also noticed this in my own research into software evolution.

Naur's insight applies directly to what we're seeing with AI systems today, but with a twist.

LLMs are extraordinary at generating plausible code. But plausible isn't the same as correct. And code isn't the same as theory. An LLM generating a solution doesn't understand the problem-domain mapping any more than a photocopier understands the document it's copying (though this is surprisingly contested & more for a later article). It produces artifacts that look like the output of theory building without having built any theory.

This is why self-verification fails. When Subbarao Kambhampati's team at Arizona State tested whether LLMs could verify their own plans, they found performance no better than random chance. The models can't distinguish good solutions from bad ones because distinguishing requires exactly the theory they don't have. Having an LLM critique its own output is like asking the photocopier to fact-check the document.

But here's where it gets interesting: external verification systems can build theory even when the generator can't.

When AlphaProof solves an International Math Olympiad (IMO) problem, it produces both an answer & a formal proof in Lean that can be mechanically verified. The Lean proof assistant doesn't care whether the proof was generated by a neural network, a human, or a random search. It checks each logical step against type-theoretic axioms, and either the proof holds or it doesn't. There's no ambiguity, no hallucination, no plausible-but-wrong.

This is verification as theory building. The verifier enforces the problem-domain constraints that the generator lacks. The formal proof is a kind of theory—a rigorous mapping between premises and conclusions that can be inspected, validated, and trusted.

The pattern generalizes beyond mathematics. A test suite that passes is a kind of theory about what the code should do. A type system that accepts a program is a kind of theory about its structure. A symbolic planner that validates a sequence of actions is a kind of theory about how the world changes. Each of these systems can hold knowledge that the LLM itself cannot.

The Lean Theorem Proving Revolution

The clearest demonstration of this architecture comes from formal mathematics, where the results are now impossible to dismiss.

AlphaProof, published in Nature in November 2025, achieved silver medal performance at the 2024 International Mathematical Olympiad by generating formal proofs in Lean. It solved three of six problems, including P6—the hardest problem of the contest, solved by only five of 609 human participants. Crucially, these weren't just answers. They were automatically verifiable proofs. Every logical step checked by Lean's trusted kernel.

The architecture is explicitly hybrid: a neural language model fine-tuned on Lean generates proof candidates. The Lean proof assistant verifies or rejects them. Reinforcement learning trains the generator based on verification feedback. The loop continues, with the model learning to generate proofs that survive the verifier's scrutiny.

Harmonic AI's Aristotle takes this further, achieving gold-medal performance on IMO 2025 problems—with formal proofs. Not natural language solutions that look right, but that are right by construction. The company raised $100 million in 2025 specifically to build "hallucination-free" AI using formal verification as its backbone.

The Lean ecosystem has exploded: mathlib now contains over 210,000 formalized theorems. Terence Tao has released a Lean companion to his analysis textbook. DeepSeek, Google DeepMind, and OpenAI are all investing heavily in formal verification. Lean won the 2025 ACM SIGPLAN Programming Languages Software Award.

What makes this work isn't that the neural networks have learned to reason. It's that the architecture routes around the need for the neural network to reason correctly. The LLM's job is to propose candidate proofs—to use its pattern-matching capabilities to suggest plausible next steps. Lean's job is to verify. The system reasons correctly because verification is externalized to a component designed for exactness.

Code Agents: The Same Pattern at Scale

The same architectural insight is now driving the most capable coding agents in production.

When Anthropic reports that Claude Sonnet 4.5 can work for 30+ hours on complex tasks, they're not describing a model that's learned to maintain long-term coherence through some emergent property. They're describing an architecture: the Claude Agent SDK with checkpoints, progress files, git commits as save points, browser automation for end-to-end testing, and explicit prompts for incremental progress.

The engineering post on effective harnesses for long-running agents is revealing:

"Out of the box, even a frontier coding model like Opus 4.5 running on the Claude Agent SDK in a loop across multiple context windows will fall short of building a production-quality web app if it's only given a high-level prompt."

The solution? An initializer agent that sets up environment scaffolding. Progress files that persist across context windows. Git history as a form of memory. Browser automation tools for verification. In other words: external systems that hold the theory the model can't.

ARC Prize's 2025 analysis identifies the same pattern: the top approaches all use refinement loops—evolutionary search harnesses that generate candidates, verify them against training examples, and iterate. Jeremy Berman's approach evolves solutions in natural language. Eric Pang's approach evolves them in Python, building a dynamic library of program abstractions. Both achieve scores far above what single-shot LLM inference can reach.

The central theme driving AGI progress in 2025, according to ARC Prize, is refinement loops: "iteratively transforming one program into another, where the objective is to incrementally optimize a program towards a goal based on a feedback signal."

This isn't reasoning as traditionally conceived. It's search guided by neural intuition and constrained by symbolic verification.

The Kambhampati Framework

Subbarao Kambhampati's "LLM-Modulo" framework, presented at ICML 2024, provides the conceptual vocabulary for what's happening:

"Auto-regressive LLMs cannot, by themselves, do planning or self-verification (which is after all a form of reasoning)... LLMs should be viewed as universal approximate knowledge sources that have much more meaningful roles to play in planning/reasoning tasks beyond simple front-end/back-end format translators."

The framework pairs LLMs with external model-based verifiers in a "generate-test-critique" loop. The LLM generates candidate plans. External critics—symbolic planners, constraint checkers, domain validators—evaluate them against hard constraints. Feedback flows back to the LLM for refinement.

On travel planning benchmarks, this framework achieved 6x better performance than baseline LLM approaches. On blocks world planning, performance jumped to 82% within 15 feedback rounds with a model-based verifier. The LLM's autonomous planning success rate? About 12%.

The key point: the framework doesn't try to make LLMs into something they're not. It positions them where they're strong—as "approximate knowledge sources" trained on humanity's collective output—while routing verification to systems designed for correctness.

Kambhampati frames LLMs as a kind of "pseudo System 1" in Kahneman's terms: fast, intuitive, pattern-matching. The deliberate, logical System 2 capabilities required for genuine planning must come from somewhere else.

The Manifold Problem (or: Why This Is Hard)

None of this is surprising if you understand the underlying math.

Gradient descent works beautifully when the problem space is smooth. Vision, speech, perception—these domains align well with the manifold hypothesis. Small changes in input produce small, learnable changes in output.

But abstract reasoning lives in discrete spaces. These landscapes are riddled with cliffs, dead ends, and sparse rewards. A single wrong inference doesn't give you a gentle gradient—it just fails. There's no partial credit for almost-correct logic.

This explains the ARC-AGI-2 results. The benchmark is specifically designed to resist memorization. Each puzzle requires recognizing a pattern from a few examples and applying it to a new situation. The o3 model that achieved 75.7% on ARC-AGI-1 with massive compute? It scores around 4% on ARC-AGI-2. The architectures haven't changed. The test got harder—harder in ways that expose what was always true about these models.

In-context learning helps on smooth surfaces. It doesn't solve discrete cliffs.

What This Means for AI Engineering

The practical implications are becoming clear:

Build verification into your architecture, not your prompts. Chain-of-thought prompting, self-critique, and reflection don't reliably improve correctness. External verification does. Use test suites, type systems, linters, symbolic planners, and formal provers as your critics.

Treat code generation as the happy path. When an LLM generates Python instead of reasoning in natural language, you gain access to an entire ecosystem of verification: the interpreter catches syntax errors, the type checker catches structural errors, the test suite catches behavioral errors. Code is a forcing function for rigor.

Design for refinement loops. The best-performing systems on hard reasoning tasks aren't single-shot. They're evolutionary—generating many candidates, filtering through verification, iterating. Budget for multiple attempts. Build harnesses that support search.

Invest in verification infrastructure. The systems winning right now—AlphaProof with Lean, coding agents with test suites, ARC solutions with program synthesis—all share massive investment in verification. Your verifiers are as important as your generators. Maybe more.

Accept that reasoning is a system property. Stop asking whether LLMs "really reason." The question is malformed. Ask instead: does your system reason? Does it produce correct outputs reliably? The model is one component. The architecture is what matters.

The Road Ahead

We're at an inflection point.

On one side: pure scaling. The hope that with enough parameters, enough data, enough compute, reasoning will emerge. This path has produced extraordinary systems—but the ARC-AGI-2 results suggest fundamental limits remain.

On the other side: hybrid architectures. The recognition that different cognitive tasks may require different mechanisms, and that the right composition of neural generators with symbolic verifiers can achieve what neither achieves alone.

The evidence increasingly favors the hybrid path. AlphaProof's Lean proofs. AlphaGeometry's symbolic deduction engine. Code agents with test suites and type checkers. Refinement loops that search over solution spaces.

From an engineering perspective, this is good news. It means we don't have to wait for AGI to build useful systems. We can build them now, by composing the pieces we have: LLMs for generation, external systems for verification, architectures that route around the weaknesses of each component.

Peter Naur's insight of "programming is theory building" is spot-on. The LLMs can't build the theory. But with the right architecture & with verification systems that enforce constraints, with formal provers that check each step, with test suites that validate behavior ... we can build systems that act as if they had the theory, even when no single component does.

That's the insight driving the most capable AI systems of 2025. And it's the insight that will likely drive the next generation.

The gap between neural intuition and logical rigor isn't a bug to be fixed. It's a design constraint to be respected.

This brings me to a set of other ideas that have to be further explored (i) verification as a theory building process, (ii) how to make sense as a team when we have deep asymmetries introduced by AI, and (iii) how we go about binding agents/components that have varying level of cognition as we engineer the next generation of systems of intelligence.

Further reading:

ARC Prize, "ARC Prize 2025 Results and Analysis" (arcprize.org/blog)
Kambhampati et al., "LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworks" (ICML 2024)
Schrittwieser et al., "AlphaProof" (Nature, November 2025)
Naur, "Programming as Theory Building" (1985)
Anthropic, "Effective Harnesses for Long-Running Agents" (anthropic.com/engineering)
Lean FRO, "Lean Programming Language" (lean-lang.org)