Skip to content
RobotWorld
← Tags

#Tag (2)

WaterfallPagination
MathResearchTopC

Kimina-Prover: reaching 92.2% on miniF2F with whole-proof RL and no search tree

The Lean 4 theorem proving line from Moonshot AI with Numina, deliberately contrarian: no prover feedback in training or inference, no Monte Carlo tree search, value function or process reward model (arXiv:2504.11354), so search is internalised into a single whole-proof generation, and a custom Formal Reasoning Pattern writes a natural-language draft before Lean code, recasting a sparse binary reward as a language problem. The base is Qwen2.5-72B with up to 32K context. Keep two generations apart: Preview (2025-04) reached 80.7% on miniF2F-test at pass@8192, the first public result above 80%; the 72B model (2025-07-10) reached 92.2% after adding TTRL search and error repair, the highest public reading then and the number on our card, while pass@1 under the same protocol is only 63.9%. Equal-budget pass@1/32/1024 of 63.9/84.0/87.7 leads the 671B DeepSeek-Prover-V2 (61.9/82.4/86.6) at all three budgets. Discounts: that table is Kimina's own and its DeepSeek rows are their reruns, the repo declares no licence, and miniF2F holds 244 problems now past 92%, so its power to separate frontier models is decaying. No third-party board exists here, so read the numbers as direction. Graded C (vendor-stated): nothing recomputed on a pinned commit.

92.2%miniF2F(TTRL 搜索后)Vendor Claim · 2025-07
MathResearch
ResearchMoonshot AI(Numina & Kimi)SiteRepo
Kimina-Prover: reaching 92.2% on miniF2F with whole-proof RL and no search tree
MathResearchTopC

DeepSeek-Prover-V2: making the Lean kernel, not the model, the judge of correctness

DeepSeek's formal theorem proving model: a 671B MoE base shared with DeepSeek-V3 and Lean 4 as target language, so formal alignment on a flagship base. The core move is recursive subgoal decomposition at cold start: one-shot proofs of competition statements succeed so rarely that RL has almost no positive samples, so DeepSeek-V3 splits a statement into subgoals, a 7B model proves each, and the composed proofs become training data, trading decomposability for data density; the RL reward is binary and comes from the Lean kernel. Vendor-reported: MiniF2F-test 88.9% at pass@8192, PutnamBench 49/658 (about 7.4%), own ProverBench 325 problems. Read them together: MiniF2F is near saturation at that budget while hard Putnam problems drop an order of magnitude, and ProverBench is self-built and self-run. The public repo (about 1304 stars) ships a ZIP of proofs you can run through Lean, putting verifiability a tier above closed models. Limits: pass@8192 means eight thousand-plus candidates per problem, not comparable with pass@1. Not commensurable with Kimina-Prover's 92.2%, so we list both without ranking. Graded C (vendor-stated): nothing recomputed in our own Lean 4 + mathlib environment.

88.9%MiniF2F-testVendor Claim · 2025-07
MathResearch
ResearchDeepSeekSiteRepo
DeepSeek-Prover-V2: making the Lean kernel, not the model, the judge of correctness