AlphaEvolve:让模型去优化「有客观评分函数」的问题
Google DeepMind 的编码代理式进化搜索:Gemini Flash 出量、Gemini Pro 出质地提出候选,自动评估器打分,高分候选留进种群当下一轮上下文,本质是 LLM 当变异算子的进化搜索;它只做有自动评估器的优化问题,因此归到 math 与 agents 两域。进化出的调度启发式已在 Google 数据中心(Borg)生产运行超过一年,持续回收 Google 全球算力的 0.7%(口径是 Google 全球算力,不是全人类算力),卡片读数取自它:全部结果里唯一经长期生产验证的一条。另有 matmul kernel 特定规模提速 23%;数学侧在 50 多个开放问题上约 20% 给出改进,含 4x4 复矩阵乘法用 48 次标量乘改进 Strassen 1969 年的 49 次记录。可验证性与证明器不同:Lean 通过是数学意义上的对,「提速 23%」是特定硬件下的经验读数。可用性接近零:无公开权重、Early Access 只有登记表,前提是你写得出便宜、快速、可信的评估器。置信度 B(有争议):Borg 那条经一年生产验证,未复现任何一条。
0.7%Google 全球算力回收(生产验证)有争议 · 2025-05
AlphaEvolve:让模型去优化「有客观评分函数」的问题DeepSeek-Prover-V2:把「模型说它对」换成「Lean 说它对」
DeepSeek 的形式化定理证明模型:671B MoE 底座(与 DeepSeek-V3 同源)、目标语言 Lean 4,是在旗舰级底座上做形式化对齐。核心创新是冷启动的递归子目标分解:竞赛级命题一步证成功率极低、RL 几无正样本,于是先让 DeepSeek-V3 把命题拆成子目标串,再由 7B 小模型逐个证,合成的完整证明成了训练数据,即用可分解性换数据密度;RL 奖励二元,信号来自 Lean 内核。读数(厂商自报):MiniF2F-test 88.9%(pass@8192)、PutnamBench 49/658(约 7.4%)、自建 ProverBench 325 题。三个数一起读:MiniF2F 在该采样预算下已近饱和,换普特南立刻掉一个数量级;ProverBench 自家题自家跑要打折。公开仓库(约 1304 stars)含证法 ZIP,可直接在 Lean 里跑,可核验性比闭源高一档。边界:pass@8192 意味着八千多个候选再筛,与 pass@1 不可比。与 Kimina-Prover 的 92.2% 协议不可通约,并列收录,不排名。置信度 C(厂商宣称):未在自有 Lean 4 + mathlib 环境复算。
88.9%MiniF2F-test厂商宣称 · 2025-07
DeepSeek-Prover-V2:把「模型说它对」换成「Lean 说它对」Kimina-Prover:不挂搜索树,靠整证生成 RL 把 miniF2F 推到 92.2%
Moonshot AI 与 Numina 的 Lean 4 定理证明线,立场逆主流:训练与推理均无 prover 中间反馈,不用 MCTS、价值函数与过程奖励模型(arXiv:2504.11354),搜索内化成一次整证生成;Formal Reasoning Pattern 先写结构化自然语言草稿再落 Lean 代码,把稀疏二值奖励重述成语言问题。底座 Qwen2.5-72B、上下文 32K。两代分开读:Preview(2025-04)miniF2F-test 80.7%(pass@8192);72B(2025-07-10)加 TTRL 搜索与错误修复后 92.2%,是收录时最高公开读数,卡片取此数,同口径 pass@1 仅 63.9%。等预算 pass@1/32/1024 为 63.9/84.0/87.7,三档全领先 671B DeepSeek-Prover-V2(61.9/82.4/86.6)。打折:对照表由 Kimina 团队发布、DeepSeek 两行为其复跑;仓库未声明许可证;miniF2F 仅 244 题且已过 92%,区分度在衰减。该域无第三方榜,读数只读作方向。置信度 C(厂商宣称):未在固定 commit 复算。
92.2%miniF2F(TTRL 搜索后)厂商宣称 · 2025-07
研究Moonshot AI(Numina & Kimi)官网Repo Kimina-Prover:不挂搜索树,靠整证生成 RL 把 miniF2F 推到 92.2%
