Verified Steps, Not Faster Guesses

Abstract

Large language models are changing mathematics and reasoning in two uncomfortable ways at once. First, they can produce fluent, confident mathematical argument faster than the community's slow, adversarial verification process can check it, risking a flood of plausible-looking but unverified claims. Second, their own way of "thinking" is structurally unlike deliberate human reasoning: a single forward pass with no persistent working memory, no built-in self-doubt, and no mechanism to notice and correct a wrong step before committing to it.

We argue these are related problems with a shared fix. Rather than trying to make a model "think like a human" in general — which is not yet a well-posed engineering goal — we propose a scoped program: force mathematical reasoning into discrete, checkable steps; verify each step with an external symbolic or numerical check rather than the model's own confidence; backtrack on failure instead of rationalizing forward; and, when a step produces an identity not already known to the system, verify it independently before storing it or reporting it to the user. This is a design document and a validation plan. Nothing in this paper has been trained or evaluated on a real model.

1. Introduction

The Verification Gap in Mathematics

Mathematical knowledge has historically advanced through a slow, adversarial checking process: a claimed proof is scrutinized, often for years, before the community trusts it. This slowness is not incidental — it is the mechanism that catches errors. Language models can now produce fluent mathematical prose, including proof-shaped text, far faster than that process can absorb it. The risk is not that mathematics stops being true; it is that confidently-stated, subtly-wrong material accumulates faster than experts can review it.

The Reasoning-Mode Gap

Current language models reason in a way that is structurally unlike deliberate human thought. Human cognition is commonly described as having a fast, automatic mode and a slow, effortful, correctable mode. A standard Transformer's forward pass is closer to the fast mode: pattern completion, with no persistent internal state that updates as reasoning proceeds, no explicit mechanism to notice "this step looks wrong," and no calibrated sense of its own uncertainty. Chain-of-thought prompting and process-level training push toward the slow mode, but a gap remains between "writes text that looks like steps" and "verifies each step before trusting it."

2. Background

Calibration. A standard way to score calibration is the Brier score — the mean squared error between a stated probability p̂ and the true outcome y over N predictions:

A lower score indicates better-calibrated confidence; a model that is always 100% confident and always right scores 0, while overconfidence on wrong answers is heavily penalized.

3. Verified Step-by-Step Mathematical Reasoning

3.1 Design

The mechanism has four parts:

1. Discrete steps. The model produces one reasoning step at a time — a stated sub-goal, a method choice, or a single derivation — rather than one uninterrupted stream. Each step is a separate, addressable unit the system can check and, if necessary, discard.
2. External verification per step, not self-report. Where a step makes an algebraic or arithmetic claim, it is checked with a computer algebra system. An identity claim f = g is checked either by symbolic simplification of f − g to zero, or by evaluating both sides at many random values and requiring agreement to numerical precision.
3. Backtracking on failure. A step that fails verification is not pushed through. The system returns to the last verified step and proposes a different method. This is the main way this design departs from a single forward pass.
4. Process-level training signal. Training rewards correct intermediate steps, not only a correct final answer. For a solution of m steps:

3.2 Numerical Verification

For a claimed identity over a domain D, the symbolic check tests whether the difference simplifies to zero:

When symbolic simplification does not terminate, the fallback is repeated random-value testing. If a false identity would fail at any single randomly drawn point with probability at least p, then the probability that T independent random trials all pass by chance is bounded:

4. Discovering and Remembering New Identities

While solving a problem, a model may produce a simplification or identity not in its training data or a known formula table. We treat this as a candidate, not a discovery, until it passes the same two-part verification. Only a verified candidate is stored in a small persistent memory keyed by the identity and its derivation, and only then reported to the user — stated as verified and accompanied by the derivation that produced it.

The persistent store for verified identities is a natural fit for the chunk memory in the Vitasta architecture, extended with the exact-match retrieval channel described in that architecture's report.

5. Roadmap

#	Addition	What it addresses	Status
1	Reasoning scratchpad	Fast-only pattern completion	Standard practice
2	Calibrated confidence output	Overconfidence; no self-knowledge	Partially solved
3	Self-verification pass	No self-correction loop	Feasible now
4	Trained abstention	Confident guessing on uncertain claims	Feasible
5	Formal-checker-in-the-loop	The verification gap	This paper
6	Multi-timescale memory	No persistent working memory	Designed in Vitasta; untested
7	Persistent memory across sessions	No memory beyond one context	Common in products
8	Iterative self-correction loop	Single forward pass, no revision	Feasible wrapper
9	Reasoning-trace training	Rewards outcome, not process	This paper
10	User-instruction tracking	No model of what the user has stated	Engineering task

6. Validation Plan

1. Symbolic verifier correctness. Confirm the checks correctly accept known true identities and reject known false ones on a curated benchmark, before any model-facing use.
2. Step-level accuracy. Measure how often a model's proposed step passes external verification, with and without backtracking enabled, on a benchmark of multi-step algebra and calculus problems.
3. Final-answer accuracy with and without the loop. Compare accuracy and rate of confidently-stated wrong answers for the same base model with the verification loop on vs off.
4. Calibration. Compare stated confidence against realized accuracy before and after training toward calibration.
5. Discovery-mechanism false-positive rate. On a benchmark with known, exhaustively catalogued identities, measure how often the mechanism flags something as new that is already known, and how often it stores an unverified identity (target: zero by construction, but must be checked empirically).

7. Limitations and Risks

1. Symbolic and numerical verification cover checkable claims only. Inequalities, existence claims, or statements involving infinite structures are not reducible to a simplify-to-zero or random-sampling check.
2. Self-verification by the same model has known blind spots; the design relies on an external, independent check to avoid this, but any step type not covered by the external checker falls back to weaker model-internal review.
3. The discovery mechanism will mostly surface known results. Framing outputs as "verified and new to this conversation" rather than "a mathematical discovery" is a communication requirement, not only a technical one.
4. Per-step external verification adds real computational and latency cost proportional to the number of steps; this cost has not been measured.
5. The verification-gap problem in mathematics is partly social and institutional — journal review norms, publication incentives, education practice — and no tooling change fully addresses that part.

References

1. Kahneman, D. Thinking, Fast and Slow. Farrar, Straus and Giroux, 2011.
2. Wei et al. Chain-of-thought prompting elicits reasoning in large language models. NeurIPS, 2022.
3. Lightman et al. Let's verify step by step. arXiv:2305.20050, 2023.
4. Trinh et al. Solving olympiad geometry without human demonstrations. Nature, 2024.
5. DeepMind. AlphaProof. DeepMind blog, 2024.
6. Kadavath et al. Language models (mostly) know what they know. arXiv:2207.05221, 2022.
7. Lin et al. Teaching models to express their uncertainty in words. arXiv:2205.14334, 2022.
8. Wang et al. Self-consistency improves chain of thought reasoning. ICLR, 2023.
9. Madaan et al. Self-Refine. NeurIPS, 2023.
10. Baddeley, A. Working memory. Science, 1992.
11. Schaeffer et al. Are emergent abilities of large language models a mirage? NeurIPS, 2023.
12. Lakoff & Johnson. Philosophy in the Flesh. Basic Books, 1999.
13. Damasio, A. Descartes' Error. Putnam, 1994.