Joshua Ong Jun Leang, Haonan Li, Zheng Zhao, Xinyi Shang, Wenda Li, Zhengzhong Liu, Erix Xing, Shay Cohen, Eleonora Giunchiglia
9 pages, preprint
A training-free agentic pipeline that routes verification failures between informal re-derivation and local Lean repair solves 100% of AIME 2025, AIME 2026, and HMMT February 2026 problems, and with a 7B open-weight reasoner solves all six IMO 2026 problems.
End-to-end evaluation on AIME 2025, AIME 2026, HMMT February 2026, and IMO 2026 using four different prompted reasoners plus open-weight K2-Horizon-7B, with Lean 4 machine verification (SafeVerify), an LLM statement judge, and an error-attribution judge; ablations on statement adjudication, error attribution vs resampling, paraphrase robustness, and test-time budgets.
100% verified accuracy on all three olympiad benchmarks across four reasoners; all six IMO 2026 problems solved with the 7B open-weight reasoner, claimed as the smallest reported reasoner to do so, surpassing closed frontier models; the authors say this saturates the benchmarks under their setting.
The authors concede the final output is a soft certificate: Lean certifies only the generated statement, and semantic faithfulness rests on an LLM statement judge, not the kernel. Perfect scores invite contamination concerns, which they address only via paraphrase robustness and self-correction frequency, not a proven-clean evaluation set. Unstated: the pipeline's heavy test-time compute cost is not reported as a compute-normalized comparison, judges are themselves learned models that could share blind spots, and n is small (30 problems per AIME/HMMT, 6 IMO problems).
A skeptic would note tiny problem counts, prompts and model choices unpublished for independent replication, LLM judges doing the semantically load-bearing work (so the '100%' is only as trustworthy as a prompted classifier), saturation claims possibly reflecting benchmark leakage, and results bought with large inference-time budgets that make the small-model framing misleading.
Little or nothing yet for AI economics in the next 12 to 24 months. The nearest signal is that verification-guided pipelines let small open-weight models match frontier closed systems on narrow verifiable domains, which supports inference-cost compression and weakens capability-based moats, but only for olympiad-style math, not general economic work.
Technical Capability: Shows that orchestration around a formal verifier, not model scale, can be the binding constraint on reliability in verifiable domains, with a 7B model matching frontier systems on IMO 2026.
Market & Valuation: Weakens the claim that frontier scale is a durable barrier by demonstrating open-weight, small-parameter systems with training-free scaffolding reaching headline benchmark results.