QED-Nano: Small Models, Big Proof Energy

Cost is usually where AI miracles become accounting problems.

A frontier model can look brilliant when it is allowed to spend enormous inference compute, rely on undisclosed training data, and hide the machinery behind a clean demo. Very convenient. Also very hard to reproduce. For businesses, that matters because a capability that cannot be inspected, budgeted, or adapted is not really a capability. It is a vendor promise with a nice interface.

QED-Nano enters this story with a more useful provocation: a 4B open model, trained specifically for natural-language Olympiad proof writing, can outperform much larger open models and approach strong proprietary systems when paired with the right test-time scaffold.¹

That sentence is tempting to summarize as: small models can think longer and beat big models.

Tempting, but wrong.

The paper is not a fairy tale about tiny models suddenly becoming mathematical prodigies after being told to take a deep breath. The result depends on a sequence of mechanisms: curated proof data, generated grading rubrics, supervised fine-tuning from a much stronger proof model, reinforcement learning with rubric-based rewards, Reasoning Cache training, and then expensive test-time scaffolding such as RSA. The small model is not merely thinking longer. It has been trained to make longer thinking less useless. A subtle distinction, admittedly, but in AI engineering subtle distinctions are where the bill usually hides.

The useful question is not “Can 4B beat 120B?”

The obvious headline is parameter size. QED-Nano has 4B parameters. GPT-OSS-120B has 120B. DeepSeek-Math-V2 is described as a 685B model. Gemini 3 Pro is proprietary. QED-Nano, especially with the RSA scaffold, looks surprisingly competitive against these systems on proof benchmarks.

But parameter comparison alone gives the reader the wrong handle. It encourages a leaderboard story: tiny model defeats giant model, therefore small models are the future. That is too clean. Reality had the decency to be messier.

The better question is: what had to be engineered around the 4B model so that it could use inference-time compute productively?

Olympiad proof writing is not the same as answer extraction. A final answer can be checked mechanically in many math benchmarks. A proof must be coherent, rigorous, complete, and resistant to convenient hand-waving. It must connect intermediate claims across a long argument. It must not merely arrive at the right destination by falling downhill.

QED-Nano treats that problem as a process-control problem rather than a scale-only problem. The model is small, but the process around it is not casual.

First, the authors build a task that can actually be scored

The training pipeline starts with a curated corpus of about 5,000 Olympiad-style proof problems. The authors draw from public sources such as AoPS and olympiad datasets, then filter out problems that are ill-posed, too trivial, image-dependent, contaminated with evaluation benchmarks, or unsuitable for natural-language proof training.

That filtering stage is not glamorous. It is also not optional. If the data contains broken statements, incomplete reference solutions, or routine computation dressed up as proof, the training target becomes noise with a LaTeX accent.

The more important step is rubric construction. For each problem, the authors generate detailed grading schemes on a 0–7 scale. These rubrics include intermediate checkpoints, zero-credit failure modes, and deductions. The paper’s examples show rubrics that distinguish between proving a boundedness claim, invoking the pigeonhole principle, handling an isogonal geometry argument, or correctly applying a reflection-principle bijection.

This is the first mechanism worth taking seriously: the model is not trained against a vague notion of “good proof.” It is trained against a structured judgment surface.

The appendix grader experiments are easy to skip, but they are doing real work. The authors compare grader prompts and models against reference judgments, then choose GPT-OSS-20B with medium reasoning for training because it performs close to stronger alternatives while being cheaper and faster. This is not a second thesis about proof grading. It is an implementation constraint: RL needs many rewards, and reward latency becomes part of the training system.

Business translation: before a specialized model can improve, the organization needs a way to score intermediate quality. “The model should be better at legal reasoning” is not a reward function. “The model must identify governing clauses, test exceptions, cite evidence, and flag unresolved ambiguity” is closer. Less poetic, more useful. As usual.

SFT gives the model proof style, and also teaches it to ramble professionally

QED-Nano begins from Qwen3-4B-Thinking-2507 and receives supervised fine-tuning using proof traces distilled from DeepSeek-Math-V2. The authors generate 7,500 proof responses across about 4,300 distinct Olympiad-level problems. They keep structurally valid completions with reasoning blocks and proof sections, but do not filter out every low-scoring or incorrect proof because even imperfect traces may teach proof-writing structure.

This stage gives the small model an initial proof-writing habit. That matters because raw reasoning ability is not enough. Natural-language proofs need a recognizable form: definitions introduced at the right time, lemmas stated before use, algebraic steps expanded, edge cases closed. A model that only knows how to guess answers is not suddenly going to write a clean proof because the prompt said “be rigorous.” Prompts are not fairy dust.

But the paper is refreshingly explicit about the cost of SFT. The SFT checkpoint develops a length pathology. Even though the training data caps sequences at 45k tokens, the fine-tuned model can produce outputs extending to hundreds of thousands of tokens, especially on incorrect attempts. The authors describe this as superficial imitation of long proofs rather than structured long-form reasoning.

This matters because it corrects a common misconception. Long output is not long reasoning. Sometimes it is just expensive wandering.

The authors report that early RL from an overly verbose SFT checkpoint suffers from high overflow rates, often around 60%, which weakens credit assignment. If a rollout is truncated before the proof reaches a useful conclusion, the reward signal becomes messy. The model is punished or rewarded through fog.

So SFT is not “the solution.” It is a starting condition with side effects.

That table is the paper in miniature. The model does not improve because one technique is magic. It improves because each stage repairs a weakness introduced or exposed by the previous one.

Rubric RL changes the target from answer-getting to proof-quality improvement

After SFT, the authors apply GRPO with rubric-based rewards. The reward comes from a grader using the problem-specific marking scheme. The authors also filter the prompt set: very easy problems are removed, and so are problems where no rollouts succeed. This is practical RL hygiene. Training on problems that are always solved or never solved is a fine way to burn compute while pretending to do science.

The important shift is that the reward is not merely final-answer correctness. ProofBench and IMO-ProofBench require proof quality. The model must assemble a coherent argument and earn partial credit against a grading scheme.

This places QED-Nano in a different category from many math-reasoning systems optimized around verifiable final answers. A final answer benchmark can reward a shortcut. A proof benchmark is supposed to punish unsupported leaps. Supposed to, anyway; we will return to the grading boundary later, because LLM judges remain charmingly imperfect.

The reported result of the basic RL stage is meaningful but not the full story. In Table 1, QED-Nano without the RSA scaffold reaches 40.0 on IMO-ProofBench, 44.9 on ProofBench, and 67.5 on IMO-AnswerBench. The SFT-only model scores 39.5, 33.3, and 57.5 respectively. So the largest gains from RL appear on ProofBench and IMO-AnswerBench, while IMO-ProofBench changes little from SFT-only in the reported table.

That pattern is worth reading carefully. RL does not simply add a uniform “reasoning boost.” It improves some evaluation settings more than others. This is why a mechanism-first article is better than a victory-lap summary: the result is not “RL fixes math.” The result is “rubric rewards improve proof-oriented behavior, but the interaction with benchmark, initialization, and scaffold matters.”

Reasoning Cache trains the model for the loop it will use later

The paper’s most business-relevant mechanism is Reasoning Cache training.

The naive way to scale test-time reasoning is to let the model generate a very long proof. That runs directly into high-variance training and the already noted problem of length explosion. QED-Nano instead uses an iterative process: generate a partial reasoning segment, summarize progress into a compact textual state, then condition the next generation on the original problem plus that summary.

This is not just a decoding trick. The authors train with this structure. The model learns to improve under summary-conditioned generation, not merely to emit one giant proof and hope the ending arrives before the context window gives up.

The distinction is central. If inference will happen through a loop, training should prepare the model for the loop. Otherwise, the scaffold becomes a fancy wrapper around a model that has no idea how to use it.

The paper reports that standard RL and RC-trained checkpoints can perform similarly within a single decoding turn, but the RC-trained model improves more when run with the RC scaffold. The largest gap appears within the first three turns, matching the training setup. That is a clean mechanism-evidence connection: the training format predicts where the test-time gains appear.

For business readers, this is the part to underline. A deployment workflow is not only about choosing a model. It is about choosing the interaction protocol the model is trained to exploit.

A customer-support model trained on single-turn answers may not benefit from a multi-step investigation scaffold. A compliance model trained only on final labels may not use a review-and-revise loop well. A financial research model trained to write fluent memos may not know how to update its thesis after a contradiction is found. The loop must be part of the learning problem, not a decorative flowchart pasted onto the product deck.

The benchmark table is strong, but the scaffold bill is not small

The paper’s main comparison is impressive. QED-Nano with RSA reaches 56.9 on IMO-ProofBench, 62.6 on ProofBench, and 76.5 on IMO-AnswerBench. That places it above GPT-OSS-120B on the three reported metrics and close to DeepSeek-Math-V2 on the proof benchmarks and IMO-AnswerBench. It also approaches Gemini 3 Pro on IMO-ProofBench, though Gemini remains higher on ProofBench and clearly higher on IMO-AnswerBench.

For the proof benchmarks, the table reports avg@3 grade as a percentage. IMO-AnswerBench is a final-answer benchmark, so it is not measuring exactly the same capability. This distinction matters because proof performance and answer performance can move differently.

Now the cost side.

The strongest QED-Nano result uses RSA, a recursive self-aggregation scaffold. In the paper’s scaffold comparison on IMO-ProofBench, single-turn QED-Nano uses about 93,690 tokens and scores 40.0. RSA uses about 2,045,764 tokens and scores 56.9. That is 21.84× the single-turn token count.

So yes, a small model can compete. No, the best result is not “cheap” in the ordinary sense. It is cheaper relative to running much larger models, and the authors state that QED-Nano Agent is at least 3× cheaper than Gemini 3 Pro on IMO-ProofBench. But internally, QED-Nano’s best scaffold still spends roughly twenty-two times the tokens of its single-turn version.

This is the correct business framing: small-model specialization shifts the cost frontier. It does not delete cost from the universe. Very rude of physics, but there we are.

The appendix tests robustness; it does not license a generic agent strategy

The paper’s appendix is especially useful because it prevents over-reading the main result.

The Reasoning Cache turn-scaling result shows that more RC turns can improve ProofBench performance: 3 turns score 40.0, 5 turns score 42.4, and 7 turns score 54.0, with token use rising from about 261k to 579k. This is evidence that iterative refinement can scale performance in that setting. It is not evidence that every agent loop improves every model on every task.

The DSM scaffold result is even more revealing. DSM is designed for proof-based problems, but on IMO-AnswerBench it lowers QED-Nano’s performance from 66.3% to 58.3%, despite higher cost. For GPT-OSS-20B, DSM improves answer performance from 61.5% to 69.8%.

That is not a contradiction. It is a warning label. A scaffold changes the behavior of a model in task-specific ways. A proof-oriented scaffold may reject concise answer-oriented reasoning because the prompt prefers rigorous proofs. That can help in one evaluation and hurt in another.

In business terms, the scaffold is not a universal “make model smarter” button. It is a workflow intervention. Workflow interventions have side effects. Ask anyone who has ever installed an enterprise resource planning system and then spent six months discovering new ways to enter the same invoice.

Human evaluation makes the result more credible, and also more bounded

The authors manually inspect a subset of QED-Nano proofs to check proof quality and possible reward hacking. Their qualitative summary is sensible: QED-Nano tends to produce structured, explicit, easy-to-follow proofs compared with weaker small models. The scaffolded version often improves by correcting substantial but fixable mistakes rather than changing the overall proof style.

They also report no clear evidence of reward hacking against the Gemini 3 Pro grader. That is useful because rubric-based RL can, in principle, teach the model to exploit grader preferences rather than produce better mathematics.

But the appendix examples also show why the boundary matters. Human annotations find cases where the LLM judge is too generous. In one IMO 2025 Q2 example, the scaffolded QED-Nano solution receives a favorable automated judgment but the human evaluator identifies serious algebraic and definitional errors and grades it as incorrect. Other examples show computation-heavy proofs, hallucinated theorem references, skipped algebra, or flawed advanced techniques.

This does not invalidate the paper. It improves it. The authors are not pretending natural-language proof grading has been solved. They are showing that a small model can be substantially improved under a practical, imperfect grading pipeline.

The business analogue is straightforward. In domains where mistakes are costly, automated graders and review loops can increase throughput, but they cannot be treated as final authority without calibration. A model can learn the house style of the evaluator. Sometimes that is exactly what you want. Sometimes it is how errors acquire excellent formatting.

What the paper directly shows

Here is the cleanest reading of the evidence.

The paper directly shows that an open 4B model can be post-trained into a strong natural-language theorem prover. It also shows that test-time scaffolds can lift that model substantially. It does not show that small models will generally replace large models, that proof grading is solved, or that longer reasoning automatically produces better reasoning.

That last point deserves emphasis because it is the misconception most readers will bring to the paper. The result is not “let the model think longer.” The result is “train the model so that structured, repeated reasoning has somewhere useful to go.”

What Cognaptus infers for business use

The practical pathway is not to copy QED-Nano’s math pipeline directly. Most companies are not training Olympiad proof models, and if they are, one hopes they have more than a slide deck and ambition.

The transferable pattern is more general:

1. Define a narrow, high-value reasoning task.
2. Build or curate task examples where quality can be judged.
3. Convert expert judgment into rubrics with partial-credit checkpoints.
4. Use a strong model or human experts to provide initial behavior traces.
5. Fine-tune a smaller model for domain style and structure.
6. Apply RL or preference optimization against rubric-based evaluation.
7. Train and deploy the model with the same iterative workflow it will use in production.
8. Reserve expensive test-time scaffolds for cases where marginal accuracy is worth the marginal cost.

This pattern is most plausible in domains where outputs are long, structured, and reviewable: compliance analysis, contract clause checking, technical report verification, claims adjudication, financial research memos, scientific literature screening, and complex customer escalations.

It is less plausible where the task lacks stable evaluation criteria, where latency is critical, where one-shot factual retrieval is enough, or where the model must invent genuinely novel strategies rather than refine known reasoning patterns.

The ROI story is therefore not “small models are cheap.” The better ROI story is: small specialized models may make high-quality reasoning loops affordable enough to use selectively.

Selective is doing a lot of work. A two-million-token scaffold for every customer question would be an exciting way to turn support automation into a controlled fire. But for a small subset of high-value, high-risk decisions, an iterative reasoning scaffold can be rational.

The remaining boundary: QED-Nano is strong, not magical

Several limitations materially affect interpretation.

First, QED-Nano operates in natural language and does not rely on Lean or external formal tools. That makes the pipeline more flexible and readable, but the proofs are not formally verified. Natural-language proof quality remains partly dependent on graders and human review.

Second, the evaluation pipeline uses LLM judges. The paper’s grader work is thoughtful, and the qualitative checks are valuable, but the appendix examples show occasional generosity and missed errors. For business adoption, this means the evaluator must be monitored as seriously as the generator. A weak judge turns RL into theater.

Third, the best reported performance depends on heavy test-time scaffolding. RSA is powerful, but the token multiple is large. The small model is cheap relative to some frontier alternatives, not free in absolute deployment terms.

Fourth, the recipe still depends on strong upstream systems. SFT uses traces from DeepSeek-Math-V2, and the grading/rubric pipeline uses powerful LLMs. QED-Nano is open and small at inference time, but the development process is not a weekend hobby project unless your weekend includes clusters and a suspicious amount of caffeine.

Fifth, the model’s qualitative style remains computation-heavy. The authors explicitly note that QED-Nano often refines computational paths rather than discovering elegant “aha” insights. This is important. Many business reasoning tasks reward systematic verification; some require creative reframing. QED-Nano is stronger evidence for the former than the latter.

The real lesson is process advantage

QED-Nano is not a declaration that small models beat large models. It is a demonstration that model size is only one part of the reasoning system.

The deeper lesson is that reasoning performance can be engineered through task-specific data, reward design, training-inference alignment, and selective test-time compute. Parameter count still matters. But it is no longer the only lever, and in specialized domains it may not be the best first lever.

For AI strategy, this shifts the question from “Which biggest model should we buy?” to “Which reasoning process should we build, score, and improve?” That is less glamorous. It is also more controllable.

QED-Nano’s small-model story is powerful precisely because it is not a small-process story. The model is tiny compared with frontier systems, but the pipeline around it is disciplined: clean data, explicit rubrics, strong initialization, experiential learning, scaffold-aware training, and expensive inference only when the result justifies the spend.

That is the part businesses should copy. Not the math contest branding. Not the leaderboard screenshot. The process.

Because in deployed AI, “thinking longer” is not a strategy. Training the system so that longer thinking becomes measurable improvement is.

Cognaptus: Automate the Present, Incubate the Future.