研究とモデル 2026年10月22日

トレンド · プレプリント 10 月 19 日

Maestro、ハーネスで解答数が増加——問題集は小さい

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 問では数問で結論が変わる。ハーネスに開発リソースをかける価値があるかは、今の証拠ではまだ判断しにくい。本紙はそう見ている。ハーネスの形をそろえ、問題集を大きくした再測定があって初めて、伸びがハーネスから来るのか基礎モデルから来るのかを分けられる。