Verify the Contract Before You Verify the Work

TL;DR for operators

A deterministic verifier can tell you whether an artifact satisfies a formal specification. It cannot tell you whether that specification faithfully represents what the user originally asked for.

Magenta makes this distinction explicit. The system first converts a natural-language mathematics problem and proposed answer into a Lean statement, then uses a learned judge to check whether that statement preserves the intended problem before attempting a machine-checked proof. When proof verification fails, another judge classifies the failure as mathematical or formal-implementation related and sends the next correction to the corresponding component.¹

The strongest evidence for this architecture is not the paper’s eventual 100% scores. It is what happens when the semantic check is removed. On AIME 2026, verified-correct performance falls from 63.3% to 20.0%, while the false certification rate rises from 0.0% to 45.5%. The verifier is still working; the system is sometimes proving the wrong statement.

For high-assurance business agents, the transferable design principle is to separate specification validation from execution verification, then diagnose which stage failed before spending more inference on recovery. That can make retries more targeted and may let smaller models trade additional verification-time computation for capability. The paper does not establish that this architecture generalizes unchanged beyond competition mathematics, and its semantic bridge still relies on a learned judge.

A valid result can still answer the wrong request

Consider an agent that converts a user’s request into something a machine can check: code plus tests, a compliance rule, a database query, or a mathematical specification.

Suppose the checker reports success. That establishes something useful, but narrower than it may appear. The output satisfies the representation that entered the checker. If the agent misunderstood the request while constructing that representation, a flawless verifier can certify the wrong task.

This is the reliability problem Magenta addresses.

The paper studies natural-language competition mathematics. Before Lean can verify anything, the original problem must be translated into a precise Lean theorem. This conversion is autoformalisation. A generated statement can compile perfectly and still change a condition, encode the wrong answer, or otherwise fail to preserve the intended problem.

Magenta therefore inserts a separate semantic check before proof generation. The paper calls this statement adjudication: a learned judge assesses whether the generated Lean statement still represents the natural-language problem and proposed answer.

The distinction is not cosmetic. In the paper’s AIME 2026 audit, 66.55% of generated statements successfully elaborated in Lean. Yet among the statements reaching the semantic judge, 67.08% were rejected. Passing the formal-language interface was therefore a poor substitute for checking whether the specification meant the right thing.

Magenta turns verification into a feedback loop

Magenta is not a newly trained theorem prover. It is a training-free pipeline coordinating several existing model roles with deterministic Lean verification.

The workflow is roughly:

1. A reasoner generates an informal derivation and candidate answer.
2. A formaliser converts the problem and answer into a Lean statement.
3. Lean checks whether the statement is well formed.
4. A statement judge checks whether that formal statement preserves the intended problem.
5. A prover attempts a Lean proof.
6. Lean and SafeVerify check the proof.
7. If verification fails, an error judge decides where the failure belongs.

That last step changes what happens after an error.

If the failure is attributed to Lean implementation, Magenta keeps the mathematics and accepted statement fixed and asks the prover to repair the proof using Lean diagnostics. If the failure is mathematical, control returns to the reasoner for a revised derivation and answer.

In compact form, the paper describes the routing rule as:

The architecture treats a failed verification not as a generic reason to “try again,” but as evidence about which component deserves the next unit of computation.

The statement-judge ablation exposes the real reliability gain

Magenta ultimately reaches 100% accuracy on the combined 93 AIME 2025, AIME 2026, and HMMT February 2026 problems with each of four tested reasoners. With K2-Horizon-7B, overall accuracy rises from 74.19% standalone to 100% inside the pipeline.

Those endpoint results demonstrate what the system can reach under the evaluated budgets. The component ablations are more informative about why it works.

On AIME 2026, the paper compares the pipeline with and without statement adjudication while using the Goedel formaliser:

Without the semantic judge, some returned proofs remain formally valid while certifying answers that do not match the reference solution. Lean has not failed. It has proved what it was asked to prove.

For agent architecture, that is the more general result: execution verification inherits the quality of the specification entering it.

Different failures deserve different retries

Magenta also tests whether diagnostic-directed correction is better than simply generating more independent attempts.

On AIME 2026 with K2-Horizon-7B, both approaches perform strongly: diagnostic-conditioned correction solves 30 of 30 problems, compared with 29 of 30 under independent resampling. On the six IMO 2026 problems, however, the gap becomes much larger: targeted self-correction verifies 6 of 6, while independent resampling verifies 1 of 6.

The likely mechanism is straightforward. Resampling repeats computation near the stage currently being sampled. It cannot reliably repair a mathematical answer that has already been frozen into the formal statement. Magenta can move control upstream when its error judge attributes the failure to the mathematics.

This matters for multi-stage agents because restarting an entire workflow is rarely the only recovery strategy. A failed database query, malformed API call, incorrect analytical assumption, and misinterpreted user request are different failure classes. Treating them as interchangeable retries spends compute without using the information produced by the failure.

Smaller models can spend compute instead of owning all capability upfront

The paper also shows a test-time trade-off between model scale and iterative verification.

K2-Horizon-7B starts substantially below K2-Horizon-375B as a standalone reasoner, yet both ultimately reach the evaluated benchmark ceiling inside Magenta. The smaller model needs more refinement: on HMMT 2026, for example, K2-Horizon-7B averages three rounds and reaches a maximum of ten, while the 375B model averages one round with a maximum of two.

This does not show that the 7B model has the same one-shot mathematical capability as the 375B model. It shows that, within this verifiable workflow, additional structured test-time computation can compensate for some differences in the base reasoner.

Cognaptus inference: for enterprise systems with strong external verification signals, model size, verification quality, and recovery budget can be treated as partially substitutable design resources. A cheaper model plus targeted verification may sometimes be preferable to paying for the strongest model on every step.

The relevant metric is therefore not endpoint accuracy alone. The paper’s budget-dependent pass-rate formulation measures how much of the benchmark has been verified by a given computation budget:

Two systems that eventually solve everything can still have very different operating costs.

For enterprise agents, verify meaning before execution

The direct evidence concerns mathematical reasoning, not enterprise software. The business interpretation is architectural.

A high-assurance workflow can be separated into three questions:

This structure is applicable wherever an agent first translates an informal instruction into something more formal: code generation, compliance automation, quantitative analysis, workflow configuration, or structured data operations.

The design goal is not to add more judges indiscriminately. It is to place verification at distinct failure boundaries. Semantic misunderstanding and execution failure carry different information and should trigger different repairs.

The certificate is still soft

Magenta does not eliminate the semantic gap. It manages it with another learned model.

Lean can deterministically establish that a proof proves the generated Lean statement. The statement judge cannot provide the same kind of formal guarantee that the Lean statement perfectly preserves the natural-language problem. The authors therefore characterize the result as a soft certificate relative to the original natural-language task.

The empirical scope is also narrow. The reported perfect scores come from competition mathematics and substantial test-time budgets: the experimental limits allow up to 32 reasoner attempts, 512 formalisation samples per candidate answer, and 4,096 proof attempts per accepted statement.

The paraphrase experiment is useful as a robustness check—standalone K2-Horizon models lose between 3.3 and 10 percentage points on answer-preserving AIME 2026 paraphrases while the corresponding Magenta configurations remain at 100%—but the paper explicitly notes that this is not a sufficient contamination test because quantities and reference answers remain unchanged.

So the transferable claim should remain architectural rather than universal: layered semantic checking, deterministic execution verification, and failure-directed repair provide a stronger reliability structure than attaching a verifier to the end of an otherwise unchanged agent.

Verification starts one step earlier than it looks

A formal verifier answers a precise question: did this artifact satisfy this specification?

An agent system still has to answer the preceding question: was this the right specification?

Magenta’s strongest contribution is to make those two decisions separate, observable, and repairable. Once they are separated, verification stops being a terminal quality gate and becomes part of a control loop. Failures generate information about where computation should go next.

For operators designing high-assurance agents, that changes the deployment question from “Do we have a verifier?” to “What exactly does each verifier establish, and where does the system send the failure when it does not?”

Cognaptus: Automate the Present, Incubate the Future.