AI doesn't need to be perfectly trustworthy if its important outputs are independently verifiable.
Large language models are becoming increasingly capable at long-horizon reasoning.
They can explore mathematical problems, write complex software, construct scientific hypotheses, and operate as autonomous agents for extended periods of time.
But there is a fundamental engineering problem hiding underneath all of this progress:
How do we know when the model is wrong?
For a chatbot, an incorrect answer may be inconvenient.
For an autonomous research agent, an incorrect proof, unsafe code change, or false scientific conclusion can become a system-level failure.
The solution may not be another layer of prompting.
It may be a different architecture.
Reason → Formalize → Verify
A conventional LLM workflow looks like this:
Problem
↓
LLM
↓
Answer
↓
Human judgment
The problem is obvious.
The final verification step is often:
"Does this answer look convincing?"
That is not verification.
A stronger architecture separates generation from acceptance:
flowchart TD
A[Problem] --> B[LLM Reasoning]
B --> C[Candidate Solution]
C --> D[Human / AI Formalization]
D --> E[Formal Artifact]
E --> F[Machine Verification]
F --> G{Valid?}
G -->|Yes| H[Verified Artifact]
G -->|No| I[Failure / Repair]
I --> B
The model generates possibilities.
The formalization layer converts those possibilities into explicit artifacts.
The verifier decides whether the artifact survives formal checking.
That is a fundamentally different trust model.
The Astra Question
Recent reporting about OpenAI's next major model family, referred to as Astra, has drawn attention to mathematical results reportedly produced through a pipeline involving reasoning, human formalization, and machine-checked verification.
The important question for this article is not whether an independent implementation can reproduce Astra itself.
It cannot.
The model is unreleased, and reproducing its reported mathematical results would require access to the underlying system.
The interesting research object is the pipeline pattern.
The reported structure can be represented as:
┌──────────────────────┐
│ Reasoning │
│ LLM │
└──────────┬───────────┘
↓
┌──────────────────────┐
│ Formalization │
│ Human + AI │
└──────────┬───────────┘
↓
┌──────────────────────┐
│ Verification │
│ Lean 4 │
└──────────┬───────────┘
↓
Certificate
This distinction matters.
We are replicating the shape of the loop, not the model.
Why LLM Reasoning Is Not Enough
LLMs are probabilistic generators.
Even when a reasoning trace looks rigorous, the appearance of rigor is not itself evidence of correctness.
A model can:
- invent a lemma
- misuse a theorem
- skip a necessary assumption
- make an invalid algebraic transformation
- confuse correlation with causation
- produce code that looks correct but fails under edge cases
Increasing the model's reasoning budget may improve performance.
It does not eliminate the fundamental problem.
The model remains a generator.
So instead of demanding:
"Never make a mistake."
we can design:
"Mistakes must be detectable before acceptance."
That is a much more scalable engineering requirement.
A Small Verification-Loop Prototype
To explore this architecture, a small three-stage project can reproduce the pipeline structure using available models and Lean.
The prototype deliberately avoids claiming to reproduce Astra's capabilities.
Its purpose is to measure the engineering tradeoffs of the loop itself.
The architecture consists of:
stage1_reasoning.py
│
▼
Candidate trace
│
▼
stage2_formalize.md
│
▼
.lean proof
│
▼
stage3_verify.py
│
▼
PASS / FAIL / SKIPPED
│
▼
report.py
The project records both success and failure.
That is important.
A verification system that only records successful outcomes can easily become a success-reporting system rather than a verification system.
Stage 1 — Reasoning
The first stage asks an LLM to generate a candidate solution.
A minimal implementation can look like this:
from anthropic import Anthropic
client = Anthropic()
problem = """
Prove that the sum of the first n positive integers
is n(n+1)/2.
"""
response = client.messages.create(
model="YOUR_MODEL",
max_tokens=2000,
messages=[
{
"role": "user",
"content": problem
}
]
)
print(response.content[0].text)
This output is not yet a proof.
It is a hypothesis.
That distinction should be explicit in the system architecture.
The pipeline should treat it as:
LLM output = Candidate
not:
LLM output = Truth
Stage 2 — Formalization
The next step converts the informal reasoning into a formal artifact.
This is intentionally human-in-the-loop.
Why?
Because natural language is underspecified.
Consider the difference between:
"The sequence obviously follows by induction."
and a formal proof that explicitly defines:
- the proposition
- the base case
- the induction hypothesis
- the induction step
- the conclusion
Formalization forces hidden assumptions into the open.
The result might become a Lean theorem such as:
theorem sum_first_n (n : Nat) :
2 * (∑ k in Finset.range (n + 1), k) = n * (n + 1) := by
...
The exact proof is less important here than the architectural transition:
Natural-language argument
↓
Formal proposition
↓
Machine-checkable artifact
Stage 3 — Verification
Now the artifact reaches the trust boundary.
Lean is not being asked:
"Does this explanation sound reasonable?"
It is being asked to check a formal proof.
A simple verification wrapper can treat the result explicitly:
import subprocess
result = subprocess.run(
["lake", "env", "lean", "proof.lean"],
capture_output=True,
text=True
)
if result.returncode == 0:
print("PASS")
else:
print("FAIL")
print(result.stderr)
The important part is not the Python.
It is the state machine.
┌──────────┐
│ Candidate│
└────┬─────┘
↓
┌──────────┐
│ Formalize│
└────┬─────┘
↓
┌──────────┐
│ Verify │
└────┬─────┘
↓
┌──────────┴──────────┐
↓ ↓
PASS FAIL
↓ ↓
Certificate Repair
And there is a third state that is surprisingly important:
SKIPPED
If Lean is not installed, the system must not report:
VERIFIED
It should report:
SKIPPED_NO_LEAN_INSTALLED
Unknown is not success.
The Verification Boundary
This is the core design principle.
The LLM operates inside a probabilistic environment.
The verifier defines a boundary beyond which an artifact must satisfy explicit rules.
flowchart LR
subgraph P[Probabilistic Layer]
A[LLM]
B[Search]
C[Agent]
D[Reasoning]
end
subgraph V[Verification Boundary]
E[Formal Specification]
F[Lean / Compiler / Tests]
end
subgraph T[Trusted Output]
G[Verified Artifact]
end
A --> E
B --> E
C --> E
D --> E
E --> F
F --> G
This pattern can become much more powerful than simply increasing model intelligence.
The Pattern Generalizes Beyond Mathematics
The verifier does not have to be Lean.
The architecture can be domain-specific.
Software Engineering
LLM
↓
Code
↓
Compiler
↓
Static Analysis
↓
Tests
↓
Validated Build
Cybersecurity
AI
↓
Threat Hypothesis
↓
Formal Constraints
↓
Sandbox / Testing
↓
Security Decision
Scientific Research
AI
↓
Scientific Hypothesis
↓
Simulation
↓
Statistical Validation
↓
Experimental Confirmation
Autonomous Agents
Agent
↓
Plan
↓
Policy Constraints
↓
Execution
↓
Observed Outcome
↓
Validation
The implementation changes.
The principle does not.
Verification as an API Contract
There is another way to think about this architecture.
The verifier can be treated as an API contract.
The LLM is allowed to return:
{
"type": "candidate",
"artifact": "...",
"confidence": 0.87
}
But the system does not accept the candidate merely because confidence is high.
It must eventually produce something like:
{
"type": "verified_artifact",
"status": "PASS",
"verifier": "Lean",
"proof_hash": "..."
}
This creates a clean separation between:
model confidence
and
system acceptance.
Those are not the same thing.
A model can be 99% confident and still be wrong.
A verified artifact can be accepted without requiring the verifier to understand why the model was confident.
What Should We Measure?
If this architecture is going to become a serious research direction, benchmark accuracy alone is insufficient.
We need to measure the entire pipeline.
For every problem:
Inference tokens
API cost
Number of attempts
Formalization time
Human interventions
Verification time
Repair iterations
Proof size
Verification result
Failure category
A useful experiment table might look like:
| Problem | Attempts | Tokens | Human Time | Repairs | Lean | Cost |
|---|---|---|---|---|---|---|
| P1 | 3 | 8.2k | 12m | 1 | PASS | $X |
| P2 | 5 | 14.7k | 25m | 3 | PASS | $X |
| P3 | 4 | 11.1k | 19m | 2 | FAIL | $X |
Now we can ask much better questions.
Not simply:
"Which model is smarter?"
But:
"Which system produces verified artifacts most efficiently?"
The Real Cost of Verification
A reported API cost such as:
$200 / problem
is not sufficient to describe the economics of a verification pipeline.
The real cost should include:
Inference
+
Human formalization
+
Verification compute
+
Failed attempts
+
Repair iterations
A more meaningful metric is:
Total Verification Cost
────────────────────────
Successfully Verified Problems
This becomes particularly important when human intervention is substantial.
A system that costs $20 in inference but requires two hours of expert formalization may not actually be cheaper than a system that costs $100 in inference and requires five minutes of human intervention.
Failure Is Data
One of the strongest properties of this architecture is that failure becomes measurable.
Instead of:
AI failed.
we can distinguish:
GENERATION_FAILURE
FORMALIZATION_FAILURE
TYPE_ERROR
PROOF_FAILURE
MISSING_LEMMA
RESOURCE_LIMIT
VERIFIER_UNAVAILABLE
This gives us a much more informative research loop.
flowchart TD
A[Problem] --> B[Generate]
B --> C[Formalize]
C --> D[Verify]
D --> E{Result}
E -->|PASS| F[Verified]
E -->|Proof Failure| G[Repair]
E -->|Formalization Failure| H[Reformulate]
E -->|Generation Failure| I[Regenerate]
E -->|Verifier Unavailable| J[SKIPPED]
G --> B
H --> C
I --> B
The system becomes an experimental instrument rather than merely an AI wrapper.
What This Prototype Does Not Claim
Scientific restraint is important here.
The prototype does not claim:
- to reproduce Astra
- to reproduce Astra's model architecture
- to reproduce its reported mathematical results
- to match its inference capabilities
- to establish equivalent cost-performance
- to independently validate every external claim about Astra
It reproduces the verification-loop architecture.
That is a much narrower—and much more defensible—claim.
The Bigger Shift: From Model-Centric to Verification-Centric AI
For years, AI progress has largely been framed around:
Bigger model
↓
More compute
↓
More reasoning
↓
Better answer
A different paradigm is possible:
Better generator
↓
Better candidate artifacts
↓
Better verification
↓
Better repair loops
↓
More trustworthy systems
The model remains extremely important.
But it is no longer the entire system.
This changes the optimization target.
Instead of maximizing:
intelligence per parameter
we can start thinking about:
verified capability per unit of compute and human effort
That is a much more interesting systems problem.
The Long-Term Architecture
Imagine a future research agent.
It receives a scientific objective.
It generates hypotheses.
It writes simulations.
It proposes mathematical arguments.
It generates code.
It tests its own assumptions.
And every important artifact must cross a verification boundary before becoming part of the trusted state of the system.
flowchart TD
A[Research Objective] --> B[AI Research Agents]
B --> C[Hypotheses]
B --> D[Mathematical Arguments]
B --> E[Code]
B --> F[Simulations]
C --> G[Evidence / Validation]
D --> H[Formal Proof]
E --> I[Compiler + Tests]
F --> J[Statistical Validation]
G --> K[Trusted Research State]
H --> K
I --> K
J --> K
This is not a chatbot.
It is closer to a verification-oriented research operating system.
The Fundamental Principle
The central idea can be summarized in one sentence:
Do not make probabilistic systems responsible for being perfectly correct. Make them responsible for producing artifacts that can be independently checked.
This does not eliminate hallucinations.
It changes their consequences.
An incorrect hypothesis can be rejected.
A failed proof can be repaired.
Broken code can fail tests.
An invalid plan can be blocked by constraints.
The system becomes capable of saying:
"I don't know."
or, more importantly:
"I cannot verify this."
That may be one of the most important capabilities an autonomous AI system can have.
What Comes Next?
The next step is not another theoretical diagram.
It is experimentation.
A rigorous evaluation should:
- Select a controlled problem set.
- Generate multiple independent candidate solutions.
- Record exact token usage and cost.
- Measure human formalization effort.
- Convert candidates into formal artifacts.
- Run Lean verification.
- Record every failure mode.
- Measure repair iterations.
- Calculate total verification cost.
- Publish reproducible artifacts and results.
At that point, the verification loop becomes measurable.
And once it becomes measurable, we can start optimizing it.
Final Thought
The next generation of AI may not be defined only by how much a model can reason.
It may be defined by what happens after the model reasons.
The future architecture could be:
AI generates.
Human structures.
Machines verify.
Systems learn from failure.
That is a different vision of trustworthy AI.
Not an AI that never makes mistakes.
An AI system in which important mistakes are difficult to accept unnoticed.
And that may be a far more realistic path toward reliable long-horizon intelligence.
Technical Stack
The prototype described in this article is designed around:
- Python
- Anthropic API
- Lean 4
- Mathlib
- deterministic verification
- explicit failure states
- cost and token instrumentation
The implementation is intentionally provider-agnostic at the architectural level.
The model can change.
The verification boundary remains.
created by Seyed Alireza Alhosseini Almodarresieh
`
Top comments (0)