Do formal proof tools and neural networks fail in opposite places, so pairing them could cover both sets of gaps?
Do proof assistants and neural networks fail in complementary ways?
This explores whether the weaknesses of formal proof systems (rigid, exact, but hard to feed) and of neural networks (flexible and fluent, but loose with logic) line up so that each covers the other's blind spots.
This explores whether proof assistants and neural networks break in opposite places, so that pairing them could cover both sets of weaknesses. The corpus has no paper that tests this pairing head-on. It does describe each side's failures clearly, and when you put those descriptions next to each other, they look like mirror images. They are not a perfect fit, though.
Start with the neural side. Language models reason by meaning and association, not by manipulating symbols. Give them the correct logical rules but strip out familiar content, and their performance collapses Do large language models reason symbolically or semantically?. You can predict where they will stumble from the fact that they generate likely text: tasks whose correct answer is an unlikely string, like reciting the alphabet backwards, are harder even when the logic is trivial Can we predict where language models will fail?. Their reasoning traces may not mean what they appear to mean. Models trained on deliberately corrupted traces do about as well as models trained on correct ones Do reasoning traces need to be semantically correct?. A network can also pass every test while its internal structure is incoherent, and benchmarks can't tell the difference Can AI pass every test while understanding nothing?. A proof checker is built to catch exactly these failures. It doesn't care whether a step sounds plausible, only whether it follows from the rules.
The proof-assistant side fails in the other direction. Proof assistants are exact but hard to feed. Formalizing even one theorem means building a whole consistent set of definitions, axioms, and supporting lemmas. Systems that seem to translate single statements into formal language well are quietly relying on large existing libraries like Mathlib Can autoformalization work on individual statements alone?. That's the complementary story: neural networks are fluent and loose, and proof assistants are strict but need someone to do the tedious work of building that structure. This is why the obvious division of labor is to let the model draft and let the checker judge.
The less obvious point is that putting the two together doesn't add up to everything you want. The Leiden Declaration argues that a proof does two jobs: it makes a result certain, and it helps people understand why the result is true. Formal verification secures the first job but not the second Can AI-generated proofs ever replace human mathematical understanding?. So a model plus a checker can give you a correct proof that no one understands. That gap doesn't belong to either component. It appears only when you combine them. A related finding: many apparent reasoning collapses in models are really failures to carry out long procedures, and giving the model tools fixes them Are reasoning model collapses really failures of reasoning?. External formal machinery may help less by fixing the model's logic and more by handling the step-by-step work the model can't keep track of.
The history of self-improving systems shows the same trade-off. The original Gödel Machine idea required a formal proof that every self-modification was an improvement. That turned out to be unworkable. The Darwin Gödel Machine dropped the proofs and tested changes against benchmarks instead, and only then made real progress Can AI systems improve themselves through trial and error?. A milder version of formal checking also pays off in agents: checking intermediate steps instead of only final answers raised one agent's task success from 32% to 87% Where do reasoning agents actually fail during long traces?. The practical lesson is that the useful pairing often isn't full proof. It's lightweight checking applied at the points where the network's looseness causes real damage.
Sources 9 notes
When semantic content is decoupled from reasoning tasks, LLM performance collapses even with correct rules in context. Models rely on parametric commonsense and token associations rather than formal logical manipulation, constraining reasoning to training distribution semantics.
By framing LLMs as autoregressive probability machines, researchers predicted tasks with low-probability target responses would be systematically harder, even when logically simple. Experiments confirmed predictions like backwards alphabet and letter counting.
Models trained on systematically irrelevant traces maintain solution accuracy and sometimes improve out-of-distribution generalization, suggesting traces function as computational scaffolding rather than meaningful reasoning steps.
The Fractured Entangled Representation hypothesis shows that SGD-trained networks can produce identical outputs across all inputs while maintaining radically different internal representations. Standard benchmarks cannot detect this structural difference.
Real formalization requires theory-level work: even one theorem needs a coherent web of axioms, definitions, and lemmas. Statement-level approaches only succeed by borrowing from prebuilt libraries like Mathlib, hiding the actual complexity involved.
Show all 9 sources
The declaration requires mathematicians to disclose AI use and retain exclusive responsibility for correctness, grounding this duty in proof's dual role: establishing certainty and conveying understanding. Formal verification alone cannot secure both goods.
Models confined to text-only generation cannot execute multi-step procedures at scale, even when they know the underlying algorithm. Tool-enabled models solve problems beyond the supposed reasoning cliff, suggesting the bottleneck is procedural execution bandwidth.
DGM replaces formal proofs with empirical benchmarking and maintains an evolutionary archive of agent variants, achieving 2.5× improvement on SWE-bench and 2.2× on Polyglot by discovering capabilities like better code editing and context management.
Reliability for long-trace reasoning comes from checking intermediate states and policy compliance during generation, not from scoring final outputs. Adding intermediate verification raised task success from 32% to 87% because most failures are process violations, not wrong answers.
Papers this line draws on 8
The research behind the notes this line reads — ranked by how closely each paper relates.
- Beyond Accuracy: Evaluating the Reasoning Behavior of Large Language Models -- A Survey
- The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity
- Beyond Semantics: The Unreasonable Effectiveness of Reasonless Intermediate Tokens
- Large Language Model Reasoning Failures
- Stop Anthropomorphizing Intermediate Tokens as Reasoning/Thinking Traces!
- Local Coherence or Global Validity? Investigating RLVR Traces in Math Domains
- From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
- Sharpening Tax in Post-Training