研究與模型 2026年10月22日

趨勢 · 預印本 10 月 19 日

Maestro 稱換外框多解 Lean 證明題。題庫很小

兩篇預印本對「Lean 定理證明的增益來自外框還是基礎模型」結論方向不同：Maestro 說同一基礎模型換協調外框，48 題解出 34 題、原生代理解 19 題，mini-Lean 說通用程式代理加最小外框就夠。 Lean 是數學證明的形式化語言。外框是包在模型外面、負責調度的程式。Maestro 是一套協調多個代理的外框，arXivLean 是一套 Lean 題庫。Maestro 自量 arXivLean 2026 年 6 月版 48 題中解 34 題，原生代理 Claude Code 或 Codex 解 19 題，作者單位原文未提供（arXiv 2610.25920，2026-10-19）。Maestro 寫兩邊用的是同一個基礎模型。10 月 12 日普林斯頓 Sanjeev Arora 等的 mini-Lean 寫「a generic coding agent with a minimal harness can already achieve strong performance on Lean benchmarks」，自量 Putnam 2025 共 12 題，Gemini 3.8 Flash 解 7 題、對手 AxProverBase 解 4 題（arXiv 2610.17331，2026-10-12）。兩篇的外框形態與題庫不同，不是同題反駁。兩篇的題庫都很小，12 題與 48 題差幾題就會改變結論。本報的讀法：現有證據還不足以判斷外框值不值得投入開發資源。外框形態相同、題庫更大的重測，才分得出增益來自外框還是基礎模型。