# Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

arXiv: https://arxiv.org/abs/2607.01223 · HTML: https://mlsanity.com/paper/2607.01223/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 17 of its 29 references that are in the map.
- First posted on arXiv 1 Jul 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 17 of 17)

- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [GPQA: A Graduate-Level Google-Proof Q&A Benchmark](https://mlsanity.com/paper/2311.12022/) (2023)
- [A Survey on LLM-as-a-Judge](https://mlsanity.com/paper/2411.15594/) (2024)
- [Math-Shepherd: Verify and Reinforce LLMs Step-by-step without Human Annotations](https://mlsanity.com/paper/2312.08935/) (2023)
- [Reinforced Self-Training (ReST) for Language Modeling](https://mlsanity.com/paper/2308.08998/) (2023)
- [ReST-MCTS*: LLM Self-Training via Process Reward Guided Tree Search](https://mlsanity.com/paper/2406.03816/) (2024)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Free Process Rewards without Process Labels](https://mlsanity.com/paper/2412.01981/) (2024)
- [Deductive Verification of Chain-of-Thought Reasoning](https://mlsanity.com/paper/2306.03872/) (2023)
- [Prover-Verifier Games improve legibility of LLM outputs](https://mlsanity.com/paper/2407.13692/) (2024)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://mlsanity.com/paper/2605.22763/) (2026)
- [HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam](https://mlsanity.com/paper/2602.13964/) (2026)
- [Graph of Verification: Structured Verification of LLM Reasoning with Directed Acyclic Graphs](https://mlsanity.com/paper/2506.12509/) (2025)
- [Verify Before You Commit: Towards Faithful Reasoning in LLM Agents via Self-Auditing](https://mlsanity.com/paper/2604.08401/) (2026)
- [Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving](https://mlsanity.com/paper/2505.20869/) (2025)

## Abstract (arXiv)

When should an AI system's answer be trusted? Formal proof assistants offer certainty but cannot reach most of the problem distribution; scalar LLM judges offer coverage but produce opaque scores that cannot be audited after the fact and are subject to the same coherence issues as any LLM. We present Theoria, a verification architecture that closes this gap. A candidate solution is rewritten into a sequence of typed state transitions, each licensed by an explicit justification, whether that be a citation, computation, or problem-given fact, and every transition is independently auditable. The foundational invariant is completeness of change: every difference between consecutive proof states must be accounted for, so hidden premises surface as unlicensed mutations rather than passing silently. On HLE-Verified Gold (185 text-only expert problems), Theoria certifies 105 at 91.4% strict precision (Wilson 95% CI [84.5%, 95.4%]). Every certification produces a human readable proof trace in which each step can be independently challenged. Holistic LLM judges achieve comparable precision at matched coverage but fail on different problems (Jaccard 0.14-0.36), making the approaches complementary. On 95 adversarial poisoned proofs across 15 domains, structured judges catch 94.7% versus 83.2% for holistic judging (p= 0.0017). The overall 11.5 pp gap concentrates in hidden premises (90.6% vs. 62.5%, a 28 pp difference) and fabricated citations (100% vs. 90%), the error classes where the formal analysis predicts an advantage; performance is identical on arithmetic and theorem-misapplication errors, where no advantage is predicted. On GPQA Diamond (n= 65), certified precision is 97.1% (Wilson CI [85.1%, 99.5%]).