代理程式迴圈超越客製化系統

資料來源#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• AutoGraphForge: Towards Automated Graph Theory Discovery
• OEIS Open: How many conjectures can language models turn into theorems?
• On the Navier–Stokes Millennium Prize Problem
• ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
• Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science

摘要#

DeepMind AI-Driven Formal Proof Search 論文的主要實證發現，也是跨領域印證苦澀教訓最明確的案例：基本代理程式——各自執行簡單「Ralph loop」生成、編輯、編譯循環的獨立證明子代理程式——解出了完整功能代理程式（演化式搜尋 + 客製化 AlphaProof RL 證明器）解出的全部 9 道 Erdős 問題，只是在最難的問題上成本較高。論文的結論是：「隨著 LLM 能力增強，正從專門訓練的系統轉向簡單的代理程式迴圈。」

作者所說的意外發現#

團隊根據完整功能代理程式（D）在競賽基準上的強勁表現，選擇它進行大規模探索——在規劃時，「較簡單的代理程式迴圈表現不佳」。事後分析已解出的 9 道 Erdős 問題，卻發現：

「令人驚訝的是，基本代理程式解出了全部 9 道問題，雖然較難的問題成本較高。」

他們將此歸因於兩件事：(1) 規劃與分析期間，LLM 生態「大幅轉變」（模型能力大幅躍進）；(2) 「編譯器回饋在讓 LLM 推理扎根方面的力量」——簡單迴圈之所以有效，是因為 Lean 驗證器讓每一步都經得起檢驗。

為何這是新領域中的苦澀教訓#

苦澀教訓：隨著時間推移，可擴展的一般方法勝過人工設計的架構。在這裡，「人工設計的架構」是客製化工具組——AlphaProof RL 定理證明器（專門訓練的系統）以及演化式族群／Elo 機制（演化式證明搜尋）。「可擴展的一般方法」則是搭配驗證器、在簡單迴圈中運作的前沿 LLM。隨著 LLM 改進，客製化鷹架在多數問題上的優勢縮減為成本差異，而非能力差異。這正是模型進步時的 Harness 縮減所描述的動態：彌補模型弱點的鷹架，會在模型變強後成為負擔；而這次觀察發生在形式數學，而非程式碼 harness。

剩餘優勢（及其到期日）#

客製化代理程式並非毫無用處——「目前在最難的問題上仍有優勢」，在兩道最難的 Erdős 問題（#125、#138）上節省了 2 到 5 倍成本。不過作者明確指出這項優勢的期限：**「隨著 LLM 能力提升，這項優勢可能會減弱。」**客製化系統仍然重要的前沿會逐漸後退：問題越難、模型越弱，專門架構就越有用——而每次模型發布後，這個適用區域都會縮小。（獨立 AlphaProof 樹搜尋和較小模型的基本代理程式都一無所獲——因此迴圈仍需要夠強的模型和驗證器；請見規模依賴的提示敏感度。）

反向測量（2026-09-21）——以及仍然成立的部分#

ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving（UVA + Meta AI，arXiv 2608.26334，empirical）是本資料集中第一個把客製化系統與迴圈的比較，設計成受控基準測試的來源，而非事後觀察客製化系統已解出的問題。每組使用相同基礎模型（Claude Opus 4.8，權重凍結）、相同 Lean 4 + Mathlib 環境、每個目標的預算相同、三次執行取平均，且所有基準都由作者重現。結果方向相反：

系統	Putnam	IMO-Lean	Combi	平均
Claude Opus 4.8，pass@16 抽樣	0.0	0.0	10.0	3.3
ReAct（簡單迴圈），Opus 4.8	35.0	15.0	27.0	25.7
Hilbert（遞迴分解 + 修復）	55.5	33.3	49.0	45.9
LEAP（AND-OR 證明 DAG，目標內）	64.7	36.7	50.0	50.5
ProofEvolve（演化 + 持續保存的綱要庫）	71.2	53.3	49.0	57.8

在模型和預算固定時，每增加一項客製化架構，解題率就單調提升。簡單迴圈落後最複雜系統 32 個百分點；沒有鷹架的模型在三個基準中的兩個完全一題也解不出來。

如何調和這個結果與 9/9 Erdős 的發現，而不是只讓它取而代之。兩份來源都是 empirical，也都未過時，因此要找出它們的差異軸——答案是預算，而不是驗證器品質（兩者都用 Lean），也不是模型強度（兩者都用 2026 年的前沿模型）。

• DeepMind 的發現是在寬裕預算下提出的能力主張：在完整功能代理程式已解出的九道問題中，基本代理程式也解出全部——「雖然較難的問題成本較高」，Erdős #125 和 #138 高出 2 到 5 倍。成本就是全部剩餘差異，沒有人設下上限。
• ProofEvolve 的發現是在嚴格上限下提出的預算效率主張：其 1× 設定每個目標允許 12 次模型呼叫、60 次 Lean 呼叫、400K 個 tokens 和 1,800 秒，每個系統都拿到相同額度。在硬性上限下，DeepMind 所稱的「成本較高」不再只是成本，而會變成失敗。
• 問題組合也不同。DeepMind 的九題是可解的研究問題；ProofEvolve 則用三個完整競賽基準計分，包含所有無人解出的題目。

因此調和後的主張比本頁原先所述更狹義，也更有用：**只要允許花費，搭配可靠驗證器的簡單迴圈就能達到客製化系統的結果；若預算受限，則會落後數十個百分點。**在可驗證的領域中，鷹架能提升樣本效率；當預算免費時，這恰好會表現成「沒有能力優勢」。前沿逐漸後退的說法仍然成立；不同之處是，前沿沿著預算軸後退，而不只是沿著模型能力軸後退；緊縮預算會讓前沿再次向外推進。

客製化代理程式在多數問題上的優勢已「縮減為成本差異，而非能力差異」 (2026-09-21 由 ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving 加上限定：預算不設上限時成立；預算相同時不成立——此時相同差異相當於解題率差了 32 個百分點。原文是 DeepMind 自己的說法，保留於此，因為它準確描述了該實驗。)

還有兩項細節值得一併記錄。ProofEvolve 的架構也不是訓練出的系統——所有權重都凍結，累積的知識則存放在明確且經 Lean 檢查的程式庫中——因此它不是苦澀教訓預測會被超越的那種系統；它是把學習成果存成文字、讓人能閱讀的鷹架。差距也因領域而異：ProofEvolve 領先 LEAP 的幅度，在 IMO-Lean（由多個引理組成的證明）上是 16.6 個百分點，在 CombiBench（依賴單一明確構造的證明）上則是 −1.0。若問題無法分解，複雜搜尋就不再有回報——這與原始發現形狀相同，只是下了一層。

同一模式向下一層：暴力查表勝過六種搜尋器（2026-09）#

一個小型且帶有許多保留條件的第三個資料點，來自搜尋，而非代理程式。 AutoGraphForge: Towards Automated Graph Theory Discovery（Pastorek，arXiv 2609.03478，empirical） 使用六種進階後端，執行數學發現迴圈中的反駁部分——尋找機器生成圖論猜想的反例：SMT 編碼、可變鄰域搜尋、線性交叉熵、MCTS、模擬退火，以及深度 RL 邊選取策略。與它們競爭的是最簡單的替代方法：到預先計算好的表格查詢猜想，表中有 348,207 張圖及其不變量。

表格勝出，差距約達兩個數量級。在單次基準中，1,249 個反駁中有 1,243 個來自靜態資料集和隨機模型；主動搜尋器只找到六個。在分成五個分區的 HPC 執行中，整套搜尋器每輪只貢獻 1 到 22 個反例，資料集則貢獻 500 到 790 個。預先計算表格的一次性成本（執行 1.22 CPU 年中有 0.85 年）遠高於迴圈本身——這正是苦澀教訓的模式：一次為規模付費，一般化的查詢就會勝過人工設計的搜尋。

有三個理由說明這只是資料點，不能當作證據。這是單次執行，搜尋器採用未調校的預設超參數；作者有明確說明，也拒絕將結果推廣。它不是代理程式迴圈——反駁過程完全沒有 LLM，因此它印證的是苦澀教訓，而非 harness 設計。比較也不像本頁其他數字那樣有相同預算：表格成本是預先支付，且排除在每輪帳目之外；正是 ProofEvolve 上述調和分析警告的無限支出假設。保留這個案例，是因為它是本資料集中唯一一個非代理程式搜尋呈現此模式的例子，也因為它與 9/9 Erdős 結果方向相同，而 ProofEvolve 對它的限定理由也相同。請見自動猜想生成。

雜訊驗證器案例終於獲得測量——結果兩面皆有（2026-09-21）#

上述兩個資料點都以 Lean 核心為基礎。Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science（Google Research + CMU，arXiv 2609.15983，empirical）是本資料集中第一個在驗證器由 LLM 組成的評議會之領域中，執行複雜客製化 harness 的來源：Stellar Colosseum 撰寫自然語言研究證明，其反駁者、章節審查者和全域驗證器全都是模型實例。架構請見多代理程式證明 Harness。

它的 TCS-Bench 基準欄最值得關注，因為它同時顯示兩個方向：

系統（TCS-Bench，300 道 FOCS/STOC/SODA 定理任務）	準確率
Gemini 3.1 Pro，直接單次呼叫	30.3%
Gemini 3.1 DeepThink，直接呼叫（模型端平行思考）	52.0%
Colosseum（客製化 harness），搭配 Gemini 3.1 Pro	54.0%
GPT-5.6 Pro（max），直接單次呼叫	68.0%
Colosseum 跨模型選取、執行兩次	71.0%

• 支持客製化架構的一面：相較於同一凍結模型的未加鷹架呼叫，harness 提升 23.7 個百分點。架構帶來的是能力，而非成本節省——方向與 ProofEvolve 在 Lean 中的發現相同。因此，雜訊驗證器不會抹煞鷹架的價值。
• **反映 harness 縮減的一面：同一模型系列的思考模式開關（DeepThink，52.0%）與整套 27 頁架構只差不到兩個百分點；而更強模型的普通單次呼叫（GPT-5.6 Pro max，68.0%）勝過整套 harness 14 個百分點。**只有跨模型、執行兩次的流程以 3.0 個百分點略勝；評分器是經過「>90% 準確率」驗證的模型，因此在約 30 道題的誤差範圍內，這 3.0 個百分點約等於 9 道題。這正是模型進步時的 Harness 縮減，出現在論文自己的基準表格中。

它沒有解決的問題，也就是下方的開放問題仍未解答的原因：Colosseum 從未與簡單代理程式迴圈比較。所有比較對象都是直接呼叫——沒有 ReAct 系統、沒有預算相同的 best-of-N，也沒有在論文任何地方公布 token 或金額。作者自己也指出這個缺口（「要區分配置改善和單純使用更多推論，需要以相同運算量進行評估」）。因此，現在雜訊驗證器領域有的是客製化系統對上毫無架構的測量，並非本頁問題所問的客製化系統對上迴圈的測量。

本資料集中規模最大的客製化架構，卻完全沒有提出比較（2026-09）#

上述每個測量都會將某件事與另一件事比較。2026-09-08 的 OpenAI 公告 （Navier–Stokes AI 主張、On the Navier–Stokes Millennium Prize Problem、vendor-claim）值得在此記錄，正是因為它沒有進行比較，也因為它位於本頁追蹤的架構規模軸極端。

OpenAI 所描述的系統，依本頁所有標準都是客製化架構：約 10,000 個並行代理程式，分布在大小不一、彼此溝通的群組；不同問題變體分派給不同群組（A/B 負責證明、C/D 負責反證，同時執行）；取得額外訓練的檢查點後，執行途中更換模型；使用 Codex 在不同群組間交流洞見，OpenAI 表示找到解答的群組「是以某種方式受到引導」；Euler 結果出爐後，由人類決定將其他千禧年問題的資源調走；最後再以 Lean 驗證，據稱由 GPT‑6 Astra 執行，耗時 17 小時。公告揭露的預算為：此問題耗時 88 小時、代理程式之間傳送 270 萬則訊息、輸出約 1,300 億個 tokens。

**但完全沒有任何基準。**沒有單一代理程式系統、沒有簡單迴圈系統、沒有相同問題上的小型群組系統、也沒有消融實驗；貼文中最接近的配置是另一道問題（Euler 未施加限制，約 100 個代理程式、約 50 小時）。貼文未提出效率或架構主張，也沒有把自己定位成比較，因此這不是廠商漏報對照組；這是一則能力公告，而我們在此記錄它無法解答的問題。對本頁有三項啟示：

• 它對「迴圈超越客製化系統」這句話，無論哪個方向都沒有證據價值。來自歷來最複雜架構、又缺乏控制組的結果，無法告訴你較簡單的系統會如何表現——運算受控基準論點從預算面指出的同一個缺口；OpenAI 自己的多代理程式領先者也承認，填補此缺口負擔不起（Noam Brown：「我們還沒有做過那個實驗」）。
• 這是本資料集中最明確的完美驗證器情境，但沒有迴圈組——Lean 位於流程末端，仍然沒有比較對象。ProofEvolve 上述調和分析的關鍵是預算；此處預算已公布，卻沒有任何對照可比。
• 唯一值得推廣的架構細節是引導路徑：獲勝群組由另一個模型引導，該模型負責整合其他群組的中間結果。這是人工設計的跨群體資訊流，也就是增加而非減少鷹架——與同一研究室在本資料集其他地方描述的最小鷹架多代理程式設計方向相反，而且這只是主張，沒有測量。

以客製化系統自身的題目集再次測量（OEIS Open，2026-08）#

上一節將本頁主張重新限定為「只有預算不受限制時，迴圈才勝過客製化系統」，因為 ProofEvolve 在預算相同且緊縮的測試中反向落後 32 個百分點。OEIS Open: How many conjectures can language models turn into theorems? （OEIS OPEN，Tom Adamczewski，Epoch AI，arXiv 2608.11941，2026-08-12，empirical）是第三項測量，也是最有資格成為決定性比較的一項——因為它在客製化系統自己的基準上，以明確預算上限運行簡單迴圈，而且客製化系統自身的成本數據也是直接向作者取得。

實驗設定。492 個開放的 OEIS 猜想以 Lean 形式化——AlphaProof Nexus 建立並回報解出 44/492（9%）的那組題目。Epoch 的代理程式小到不能再小：Inspect 上的 ReAct 工具迴圈搭配三個工具（bash、文字編輯器，以及回報剩餘預算的 resources 工具）；執行環境包含 Lean+Mathlib、SageMath 和 Python；每個猜想的花費上限為 $50，除此之外別無其他。沒有演化、沒有族群、沒有 Elo，也沒有專門證明器。

系統	492 題中已解出	每題已解猜想的平均成本
Claude Opus 4.8，三工具 ReAct 迴圈	147（30%）	$10（最高 $47）
GPT-5.5，相同迴圈	26%（未回報數量）	$6
Gemini 3.5 Flash，相同迴圈	22%（未回報數量）	$9
AlphaProof Nexus（演化 + Elo 評分器 + AlphaProof 工具）	44（9%）	平均約 $10，最難的幾題最高約 $50

成本欄說明這項結果為何重要。ProofEvolve 上述調和分析的關鍵是預算：迴圈可在能夠花費時追上，預算不足時則落後。此處的迴圈以3.3 倍勝出，且每題解答成本相同；而這組題目原本是客製化系統的主場。論文自己的解讀逐字呼應苦澀教訓：「與其用問題專屬架構規定模型該如何推進，不如給模型簡單工具，讓它自行決定如何使用。」

混淆因素是論文自己指出的，本頁也必須保留。兩組用的模型並不相同。AlphaProof Nexus 的證明子代理程式採用 Gemini 3.1 Pro（2026 年 2 月 19 日發布）；GPT-5.5 和 Claude Opus 4.8 晚了約兩到三個月發布（4 月 23 日和 5 月 28 日）。因此，對 3.3 倍結果的誠實表述不是「在預算相同時，迴圈勝過客製化架構」，而是「在預算相同時，使用新兩代模型的迴圈勝過客製化架構」；這支持本頁的harness 縮減主張，而不是迴圈勝過客製化系統主張，過去本頁曾把兩者混為一談。仍然沒有人做過的比較一如以往：讓客製化架構改用較新的模型重新執行。

使用相同模型的消融實驗，是更清楚的資料點#

附錄 A.2 深藏著一項實驗，可排除上述混淆因素——相同模型、相同驗證器、相同 $200 上限、相同 100 題 LITE 子集，只改變 harness。DeepAgent 系統以 Inspect 的 deepagent 取代 ReAct 迴圈：子代理程式委派、持續記憶、待辦清單工具，以及更長且立場明確的系統提示詞。****文獻系統則為基礎迴圈提供離線快照，其中收錄 476,000 篇純數學 arXiv 論文。

模型	基礎迴圈	DeepAgent	+ 文獻
Claude Opus 4.8	39%	39%	39%
GPT-5.5	36%	41%	37%
Gemini 3.5 Flash	29%	29%	28%

「代理程式變體沒有影響。」Opus 在三種配置下的結果精確到個位數都相同；GPT-5.5 的 +5 位於 n=100 時互相重疊的誤差範圍內，也未能重現。這是同模型、同預算、可靠驗證器下的架構消融實驗，結果是零——正是本頁原先主張、而 ProofEvolve 看似推翻的模式。

**因此，三項測量的差異取決於加入的是哪一種架構，而非只有預算不同。**ProofEvolve 加入的是搜尋機制——AND-OR 證明 DAG、依據核心回饋的適合度，以及持續保存的已驗證子證明程式庫；也就是會改變搜尋如何分配呼叫次數的機制。DeepAgent 加入的是代理程式功能——記憶、子代理程式、待辦事項、更好的提示詞；也就是改變模型組織自身方式的機制。預算受限時，前者帶來 32 個百分點，後者毫無作用。更精確的規則是：在每一步都有可靠驗證器的領域，工程心力應花在搜尋，而不是代理程式。

再次測量搜尋機制；這次達到帕累托優勢（2026-08）#

本頁前文歸納出的差異——搜尋機制在預算上限下有價值，代理程式功能則沒有——在機制這一側又多了一項測量，而且是三者中最乾淨的一項。Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing（Vamshi 和 Yang，University of Maryland，arXiv 2608.28639，empirical）執行三種角色的 MCTS——生成器、分解器、評論者，全都使用同一個凍結的 7–8B 檢查點——並與整份證明的平坦抽樣比較，證明嘗試預算完全相同（N×K×S，成功時不提前終止），涵蓋三種證明器、四個基準和五個隨機種子。AI-Driven Formal Proof Search 提供詳細說明；此處有三點值得補充。

**它在各種預算下都勝出，而且差距沒有縮小。**Goedel-Prover-V2-8B 在 MiniF2F 上執行 32 次嘗試時，達到 84.2%，高於對照組的 82.4%；執行 256 次時，達到 87.1%，高於對照組的 84.7%。PutnamBench 在 32 次嘗試時為 26/659，高於對照組的 18/659。三個模型方向都相同。相較於上文 ProofEvolve 的調和結果，這是 Lean 中第二個互不相關的預算相同實驗，證明客製化搜尋架構勝出。

完整的預算相同結果表（由 AI-Driven Formal Proof Search 移至此處，2026-09-29）：總嘗試次數精確為 N × K × S，其中 N = 4 次 MCTS 迭代、K = 4 個子節點固定，S 則改變（PAB@32 到 PAB@256）；每種系統（整份證明抽樣、兩種消融搜尋基準、Prover Agent 重現版本和本方法）都使用相同檢查點、提示模板、解碼設定和固定環境，且成功時均不提前終止；結果為五個隨機種子的平均值 ± 標準差。MiniF2F、Goedel-Prover-V2-8B：PAB@32 時為 84.2 ± 0.5%，對照組 82.4 ± 0.6%；到 PAB@256 時單調上升至 87.1 ± 0.2%，對照組 84.7 ± 0.1%；DeepSeek 從 77.1 → 82.6，對照組從 75.2 → 78.2；Kimina 從 64.3 → 66.9，對照組從 62.8 → 65.1。PutnamBench（已稽核，Goedel）：PAB@32 時為 26/659，對照組 18/659；PAB@128 時為 36/659，對照組 22/659。物理題在 PAB@16 時：搭配 PhysLib 程式庫作為上下文，在 PhysLeandata 上高出 1.9 到 2.4 個百分點，在 LeanPhysBench 上高出 1.5 到 2.0 個百分點；不搭配 PhysLib 的本方法，接近搭配 PhysLib 的整份證明抽樣，因此結構化搜尋部分取代了缺少領域程式庫上下文的影響。論文指出最大單一架構因素是分解器的溫度衰減（τ_d 依深度與迭代次數退火，從 τ₀ = 0.7 開始）：移除它會讓每個模型的成績下降 1.8 到 2.5 個百分點。

而且它成本較低，這是本頁此前所有資料點都沒有的結果。本頁一直把各種架構效果視為以運算量換品質的取捨，而運算成本的比較也各有爭論。這次在嘗試預算完全相同時，推論 tokens 總數少 32.8%，輸出 tokens 少 35.8%；因為分解器和評論者呼叫很短（最多輸出 1,024 和 3 個 tokens），而生成器收到明確分解後能寫出更短的證明（32.84% 是三個模型在單一基準執行中、相同 PAB 下，相較整份證明抽樣的累計用量平均；分解器和評論者呼叫每個模型增加約 7k 個 tokens，生成器輸出則減少約 114k）。這種更好且更便宜的架構，超出本頁一直討論的框架；其機制值得指出：加入架構不是為了進行更多搜尋，而是藉由告訴生成器要證明什麼，讓它生成更短內容。

**但必須留意輸家究竟是誰。**整份證明抽樣並非代理程式迴圈——它是沒有任何回饋的 best-of-N，因此勝過它並不是本頁關心的比較。論文唯一真正的迴圈系統是重現 Prover Agent；它做的正是本頁原始發現的關鍵：把編譯器的錯誤文字放進下一輪上下文。在相近預算下（260 次，相較 PAB@256），Prover Agent 在 MiniF2F 上達到 86.2 ± 0.1%，MCTS 架構則是 87.1 ± 0.2%。**差九十分之一個百分點。**因此，以本頁關注的軸線解讀這個來源，應採取較狹義的結論：複雜搜尋明顯勝過平坦抽樣，僅微幅勝過編譯器回饋迴圈；測試僅用一個基準，由獲勝一方重現，而且每個系統都使用 7–8B 模型。

**它在迴圈對客製化系統軸線上的位置：**偏向搜尋機制，但位於成本較低的一端。整套系統中沒有任何訓練元件——沒有價值網路、沒有 RL、沒有微調；只有三種提示模板和一個圍繞凍結檢查點運作的 UCB 公式。論文刻意排除會重新訓練證明器的比較對象（BFS-Prover、HunyuanProver），理由是更換檢查點會把搜尋提升和模型提升混在一起。作者把這項原則用在自身有利的一方，正是本頁反覆要求的嚴謹做法；這也讓本系統明確歸入 ProofEvolve，而非 AlphaProof 的類別：沒有專門訓練系統的架構，恰好是苦澀教訓最難撼動的那半邊「客製化系統」。

保真度分級任務中，裸迴圈墊底（ProofLoom，2026-09）#

ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization（empirical）以一個模型和 48 小時上限，對七種系統處理 15 個隨機最佳化演算法的形式化成果進行比較，評分項目是來源忠實度，而不只是核心驗證通過與否。裸 Codex 迴圈及其 Goals 變體，在人類評分中分別得到 2.8 和 3.0 分（滿分 7 分）；採用角色結構的 harness（OpenGauss、LeanMarathon、Trellis、Archon、ProofLoom）在教科書任務上則得 3.5 到 6.3 分。這與本頁的主要發現方向相反，而本頁對驗證器的限定條件正好可以說明原因：在有廉價可靠驗證器的情況下，迴圈勝出；但此處目標還包括「這是否為來源論文中的定理」，編譯器無法判斷這件事，因此沒有審查者的迴圈無從取得回饋（而且如核心層級證明稽核所述，它會偏離原始陳述）。限制條件也和往常一樣：作者在自家轉接器上執行每個基準；基準系統的 tokens 數量未公開；而且這裡沒有跨模型世代的比較，因此無法檢驗上文的「到期日」主張。

推廣#

可轉移的主張是：當某個領域有廉價且可靠的驗證器時，應採用能利用它的最簡單代理程式迴圈，並在每次模型發布時重新評估客製化鷹架——它往往會從促成能力，轉變為只節省成本，最後成為負擔。驗證器（可驗證性論點）讓簡單迴圈得以運作；迴圈則讓系統建置和維護成本低廉。客製化系統只有在逐漸後退的困難前沿上才值得投入。

加上預算限定後（2026-09-21）：……若每次額外呼叫都夠便宜，讓你永遠不必設上限，就採用最簡單的迴圈。只要單一任務的預算受到限制——延遲 SLO、token 上限、付費 API、需要數秒 CPU 的驗證器呼叫——排序就會翻轉，而 Lean 中測得的翻轉差距達 32 個百分點。「省成本而非提升能力」只有在暗中假設可無限支出的情況下，才代表降級；同一套節省成本的架構，在預算受限時就是能力。這是Large-Scale Test-Time Compute核心觀點在形式數學上的表述：不說明預算就討論系統能力，問題本身便不成立；此處將其應用在 harness 設計，而非模型評估。

相關文章#

• AI-Driven Formal Proof Search — 問題背景；本文整理其核心架構發現
• 苦澀教訓 — 本研究在形式數學中以實證確認的原則
• 模型進步時的 Harness 縮減 — 同樣呈現「模型進步後，鷹架會成為負擔」的動態，此處案例是證明搜尋 harness
• Harness Build-vs-Buy — 從另一條路徑得到同樣不應打造客製化系統的結論：流失的不是能力，而是維護經濟效益；即使沒有失去任何能力，一個分支每年仍會少掉 866 個上游錯誤修正
• Agent Loop Pattern — 「Ralph loop」基本代理程式是以迴圈為基礎元件的實例
• 演化式證明搜尋 — 簡單迴圈所比肩的客製化鷹架（族群 + Elo）；現在也收錄 ProofEvolve 以核心為基礎的變體，也就是在預算設上限後以 32 個百分點勝過簡單迴圈的系統
• 多代理程式證明 Harness — 同一比較中的雜訊驗證器分支：以模型評議會評分的客製化多代理程式 harness，比相同模型的裸呼叫高出 23.7 個百分點，卻比更強模型的裸呼叫低 14 個百分點
• Navier–Stokes AI 主張 — 架構規模軸的極端，且比較軸為零：約 10,000 個代理程式、各群組採用不同問題變體、執行途中更換模型、透過 Codex 交流洞見，再以 Lean 驗證；完全沒有基準，證據等級為 vendor-claim
• 自動猜想生成 — 同一模式的非代理程式案例：預先計算的 348,207 張圖查詢表，在駁斥能力上以兩個數量級勝過六種隨機式和神經網路搜尋後端
• OEIS Open Benchmark — 本頁最接近決定性比較的一項，也是最乾淨的無差異結果：三工具 ReAct 迴圈在客製化系統自己的題目集上，以相同解題成本解出 147/492 題，而 AlphaProof Nexus 解出 44/492 題（但受到兩代模型差異混淆）；同模型、同預算的 DeepAgent 系統——子代理程式、持續記憶、待辦清單——則讓成績完全不變
• 核心層級證明稽核 — 同一來源的第二部分，也是理解本頁任何比較的前提：如果 harness 只回報「已編譯，沒有 sorry」，卻不詢問核心宣告依賴哪些內容，那麼某證明器在 PutnamBench 的成功案例中有 31–44% 並非證明；而且搜尋程序產生這類結果的數量多於平坦抽樣，卻沒有引入漏洞
• AlphaProof Nexus — 涵蓋從基本（A）到完整功能（D）代理程式的架構
• 可驗證性論點 — 驗證器讓簡單迴圈得以運作
• Client-Side Agent Optimization — 「以較低成本達到同等能力」是 AgentOpt 形式化處理的成本／品質最佳化；此處由低成本配置勝出
• 規模依賴的提示敏感度 — 迴圈需要足夠強的模型：較小的 Gemini 變體一題也解不出來
• Recursive Self-Improvement — 這是 RSI 最明確的既有領域替代案例：隨著模型改進，簡單迴圈追上客製化訓練系統；若將這種動態用於 AI 開發本身，就能形成閉環
• AI Accelerating AI Development — 同樣呈現簡單迴圈超越客製化系統的模式，但觀察對象是 Anthropic 內部 AI 研發吞吐量，而非形式數學
• 對代理程式軌跡進行樹搜尋（LATS） — 上文引用的 reward-oracle MCTS 預算相同比較表，從樹搜尋的角度來看，它的價值函數第二項是編譯器接受次數；加上狀態可免費回溯，並藉由分配測試說明增益來自反向傳播，而非呼叫預算

衍生主張#

• 單一通用代理程式與多代理程式程式碼架構的比較 — 9/9 Erdős 結果是本資料集中最有力的證據，說明模型進步後，單一簡單迴圈能勝過多元件客製化系統；這是單一代理程式是否勝過多代理程式的答案之一（另一半是：上下文／評估分離依然重要）

開放問題#

• 客製化系統的優勢被限定為「目前如此」。下一代模型會如何改變結果——演化式／AlphaProof 架構在任何問題上都能維持優勢嗎？還是會完全縮減成成本差異？2026-09-21 有類比性的部分答案，但不是直接答案——Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science 沒有測試演化式／AlphaProof 架構，也沒有在 Lean 中執行，因此無法為此定論。它提供的是預測中的縮減第一次發生在同一篇論文自己的基準欄中的案例，而且模型世代只差一代：使用 Gemini 3.1 Pro 的 27 頁客製化多代理程式 harness，在研究級 TCS 證明任務上達到 54.0%；同系列的模型端思考模式不需 harness 就達到 52.0%；而更強模型的普通單次呼叫（GPT-5.6 Pro max）達到 68.0%，比 harness 高 14 個百分點。作用機制符合此處的預測，但有一項值得記下的轉折：吸收這項能力的不是更好的迴圈，而是測試時運算移入模型內部，本頁原先未預料到這條路徑。由於架構不同、驗證器不同（模型評議會，而非核心），且比較來自不同廠商，而非在新模型上重跑同一系統，因此仍標記為 #oq/wait。觸發條件仍然不變——使用新一代 LLM，在相同九道 Erdős 問題上重新執行 AlphaProof／演化式系統。**2026-09-21 由 On the Navier–Stokes Millennium Prize Problem 延伸此問題；這項延伸是警訊，而非資料點。**新一代模型已經問世，而掌握它的研究室為它打造的是更多架構，而非更少：約 10,000 個並行代理程式、互通群組、各群組各自負責的問題變體、執行途中更換模型、另一個模型整合群組間的洞見，以及末尾的 Lean 驗證。因此，新一代前沿模型搭配客製化架構的首個觀察，方向與此問題的預期相反——不過它無法計分，因為公告沒有基準、消融實驗或任何比較，而且它是針對未發布模型的 vendor-claim。兩種解讀仍都成立，而此來源將它們區分開來：在能力前沿上，架構可能仍能提升能力；或者，在沒有人測量效率時，它可能只是花掉一個週末運算額度最簡單的方式。觸發條件不變，另外多出一個值得關注的情況——任何研究室公布最新模型搭配多代理程式架構，與單一長時間執行代理程式在相同問題上的比較。**2026-09-23 由 OEIS Open: How many conjectures can language models turn into theorems? 從比較的另一側提供部分答案。**沒有人以更新模型重跑該架構；而是第三方以較新的模型，在架構自身的 492 個 OEIS 猜想題目上、設下 $50 上限，執行一個三工具迴圈；架構的 44/492 成為另一篇論文圖表中的門檻，迴圈則達到 147/492——在每題平均解答成本相同時差距為 3.3 倍（兩者都約 $10，資料來自架構作者自己的往來信件）。從此問題的角度來看，這正是它預期的縮減：只差一個世代，而且涵蓋 492 道題，而非九道。此問題仍標記為 #oq/wait，因為架構本身從未重新執行：Gemini 3.1 Pro 與 Opus 4.8、GPT-5.5 相差兩到三個月，因此無法判斷是「架構不再帶來效益」，還是「新模型也能讓架構更有效」。觸發條件仍然不變。
• 「簡單迴圈 + 驗證器勝過客製化系統」的結果，是否只適用於驗證器完美的場景（Lean），還是也適用於驗證器有雜訊的領域（測試、LLM 評審團）？2026-09-21 有部分答案——而答案來自意想不到的方向。ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving 沒有討論雜訊驗證器，所有實驗都是以 Lean 核心為驗證器。它所推翻的，是完美驗證器情境下這個問題的前提：使用相同且緊縮的目標預算，固定基礎模型進行比較時，簡單 ReAct 迴圈的平均成績為 25.7%，客製化演化式系統則為 57.8%，中間系統的成績依架構增加而單調提升。因此，即使驗證器完美，結果也不會無條件成立——只有在驗證器完美，而且預算實際上不受限制時才成立。雜訊驗證器的部分仍未解答，現在問題也更精確：在驗證器為測試套件或評審團的領域中，以相同預算測試迴圈和客製化架構，藉此區分「架構提升樣本效率」與「架構讓系統更能抵禦會說謊的驗證器」。**同日，Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science 延伸了這項問題；它帶來雜訊驗證器領域，卻仍沒有迴圈組。**Stellar Colosseum 是一套客製化多代理程式 harness，所有正確性訊號都由模型生成——包括對抗式反駁者、逐節審查者和全域驗證器；其數學系統完全沒有形式化檢查——因此終於排除了「驗證器完美」這項前提。結果：與相同凍結模型的未加鷹架單次呼叫相比，複雜架構高出 23.7 個百分點（300 道研究級 FOCS/STOC/SODA 定理任務中，從 30.3% 提升至 54.0%）。因此，雜訊驗證器本身不會破壞客製化架構的價值；ProofEvolve 所示方向也出現在 Lean 以外的領域。但兩點使它仍只是部分答案，標籤也仍是 #oq/source。第一，完全沒有迴圈組——論文中的所有比較對象都是直接呼叫模型，沒有 ReAct 類型迴圈、沒有 best-of-N 控制，也沒有公布任何 token 數、呼叫次數、執行時間或金額，因此無法定位上述調和分析所倚賴的預算軸。作者在未來工作中也承認：「需要以相同運算量進行評估，才能區分配置改善和單純使用更多推論。」第二，反方向的同一張表顯示，更強模型的普通單次呼叫（68.0%）勝過整套 harness（54.0%）；這是 harness 縮減的資料，而非迴圈勝過客製化系統的資料，不能取代後者。現在的問題已精確化：用相同模型和相同且明確列出的呼叫預算，搭配評審團驗證器，比較簡單迴圈和客製化 harness。**2026-09-21 又有第三個來源提供預算，但仍缺少同一個系統組（On the Navier–Stokes Millennium Prize Problem，vendor-claim）：**一套運作 88 小時、傳送 270 萬則代理程式間訊息並輸出約 1,300 億個 tokens 的 10,000 代理程式架構，最後以 Lean 驗證——因此驗證器再次回到完美，預算也完整公開，但依然沒有迴圈組、單代理程式組或消融實驗。值得記錄，因為這似乎是整個領域的現象，而非單篇論文的問題：一個月內、三個來源、兩種驗證器情境、兩個研究室，沒有人執行過對照組；而被直接問到的其中一方也表示尚未做過這項實驗。2026-09-23 有部分答案——有人做了對照，在完美驗證器情境中，結果沒有差異。OEIS Open: How many conjectures can language models turn into theorems? 在相同模型、相同 100 題 LITE 子集、相同 Lean/SafeVerify 閘門及相同 $200 上限下，比較基礎 ReAct 和 Inspect 的 deepagent（子代理程式委派、持續記憶、待辦清單工具、更長的系統提示詞）；Claude Opus 4.8、GPT-5.5 和 Gemini 3.5 Flash 的結果分別是 39/39、36/41、29/29。收錄 476,000 篇論文的 arXiv 文獻系統也同樣沒有影響（39/37/28）。因此，在預算相同且驗證器可靠時，客製化的代理程式功能毫無作用；這與 ProofEvolve 中客製化的搜尋機制在預算相同時帶來相反的結果，而兩類架構之間的差異才是此處的重要發現。此問題仍標記為 #oq/source，原因有二：驗證器仍然完美，因此雜訊驗證器部分仍未觸及；各系統比較的是相同金額，而不是相同呼叫次數或 tokens，因此 DeepAgent 可能把 $200 花在子代理程式的額外負擔，而非證明嘗試上，無從判斷是功能本身沒有幫助，還是預算配置方式造成結果。

資料來源#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving — arXiv 2608.26334，UVA + Meta AI，2026-08-26，27 頁，empirical。此處的表 1 由 pdftotext -layout 重新讀取，並與 §5.2 的文字說明核對後才撰寫上方表格。**每個數字都必須一併保留以下限制：**五種代理程式基準（ReAct、Aristotle、AxProver、Hilbert、LEAP）都是 ProofEvolve 作者自行重現——「保留其搜尋策略，並在相同預算下執行」——而非原始作者公布的數字。若重現實驗未充分調校競爭方法，就會放大差距；目前也沒有第三方重現
• AutoGraphForge: Towards Automated Graph Theory Discovery — arXiv 2609.03478，Ján Pastorek（Comenius University in Bratislava），2026-09-03，17 頁，ITAT 2026 投稿，empirical。此處只引用 §4.1 中依據文字敘述、歸因於資料集與主動搜尋的結果。單一作者、工作坊投稿、單次執行、明確未最佳化搜尋器超參數——本頁證據最薄弱的一項，因此本文特別保留限定說明。完整來源分析見自動猜想生成
• On the Navier–Stokes Millennium Prize Problem — OpenAI（無署名），openai.com，2026-09-08 發布，2026-09-10 更新，約 1,900 字，vendor-claim。此處只引用架構描述（群組結構、各群組負責的問題變體、執行途中更新模型、透過 Codex 交流洞見，以及獲勝群組受到引導），以及公布的預算。本文沒有任何比較，因此其中沒有任何測量可用於本頁目的——在此將它記錄為架構規模軸的極端案例，也用來說明目前沒有人執行對照組。第一手資料，涉及未發布模型，優先權有爭議，尚未驗證。完整分析見Navier–Stokes AI 主張
• Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science — arXiv 2609.15983，Lin、Woodruff、Deng、Mao、Zuo 和 Mirrokni（Google Research；Woodruff 也任職 CMU），v2，2026-09-15，27 頁，empirical。此處引用表 2 的基準與 Colosseum 系統結果，使用前已與 pdftotext -layout 核對；另引用 §8.1 文字中對運算量配對問題的承認。所有數字都須搭配三項限制：評分者本身是模型（以參考資料輔助，在 100 個專家標註上「>90% 準確率」，但沒有一致性統計），因此它與 GPT-5.6 Pro 之間的 3.0 個百分點差距仍在誤差範圍內；論文沒有回報呼叫次數、token 數、執行時間或成本，因此無法依本頁調和分析所需的預算軸定位；這是 Google 對 Gemini 的第一方評估，六位作者中有三人也撰寫了基準。完整來源分析見多代理程式證明 Harness
• OEIS Open: How many conjectures can language models turn into theorems? — Tom Adamczewski（Epoch AI），「OEIS Open: How many conjectures can language models turn into theorems?」，arXiv 2608.11941，2026-08-12，27 頁，empirical。此處引用 147/492 對 44/492 的比較及成本欄、造成混淆的模型發布日期（論文自己的註腳 10），以及附錄 A.2 的代理程式變體消融實驗。3.3 倍的主要結果並非同模型比較，本頁不可把它寫成同模型比較；同模型的資料點是 DeepAgent／文獻系統沒有差異的結果。上文所有數字都來自內文、圖說或圖像（已檢視圖 1 和圖 3）；論文唯一的表格已透過 pdftotext -layout 核對，但本頁未引用該表。完整分析見OEIS Open Benchmark
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing — Vamshi 和 Yang（University of Maryland），arXiv 2608.28639，2026-08-11，14 頁，empirical。此處引用其對整份證明抽樣的 PAB 相同比較、以 260 次預算重現 Prover Agent、token 效率數字，以及排除重新訓練比較對象的論文理由。所有基準都是作者自行重現，包含僅領先 0.9 個百分點的 Prover Agent 系統——本頁對 ProofEvolve 已保留相同限制。三種證明器都是 7–8B 的開放權重檢查點，因此本研究結果無法推廣到前沿規模模型。完整分析見AI-Driven Formal Proof Search和核心層級證明稽核
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization — Wang、Li 和 Yuan，arXiv 2609.34960，2026-09-28，empirical。此處僅引用七種系統的人類評分比較；完整分析見多代理程式證明 Harness。