代理迴圈超越客製化系統

資料來源#

Advancing Mathematics Research with AI-Driven Formal Proof Search

摘要#

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 Shrinkage 所描述的動態——用來彌補模型弱點的腳手架，在模型變強後反而成為阻力——只是這次是在形式數學中觀察到，而非在程式碼 harness 中。

殘餘優勢（以及它的到期日）#

客製化代理並非毫無用處——它「目前在最困難的問題上仍保有優勢」，在兩道最棘手的 Erdős 問題（#125、#138）上節省了 2×–5× 的成本。但作者明確指出了這項優勢的期限：**「隨著 LLM 能力增長，這項優勢可能會減弱。」**這是一條逐漸退縮的前沿：客製化系統仍然重要的區域會隨著問題變難、模型變弱而增加，專門結構也就越能發揮價值——而這個區域在每次模型發布後都會縮小。（獨立的 AlphaProof 樹狀搜尋與較小模型的基本代理什麼都沒解出來——因此迴圈仍需要足夠強的模型 + 驗證器；請參見尺度依賴的提示敏感度。）

泛化#

可轉移的主張是：當某個領域擁有便宜且可靠的驗證器時，應偏好能利用它的最簡單代理迴圈，並在每次模型發布後重新評估客製化腳手架——它往往會從啟用能力的工具，轉變為僅僅節省成本的工具，最後成為阻力。驗證器（可驗證性論題）讓簡單迴圈得以運作；迴圈則讓系統便宜、容易建置與維護。客製化系統只有在逐漸退縮的困難前沿上才真正值得投入。

推導#

單一一般代理與多代理程式碼架構 — 9/9 Erdős 結果是本資料集最清楚的證據，顯示隨著模型改進，單一簡單迴圈會超越客製化多元件系統；這是回答單一代理是否勝過多代理的一半答案（另一半是：上下文／評估分離仍然存在）

開放問題#

客製化優勢被限定為「目前」。下一代模型會給出什麼判決——演化／AlphaProof 裝置是否能在任何問題上存續，還是完全縮減為一條成本線？
「簡單迴圈 + 驗證器勝過客製化系統」的結果，是否只在驗證器完美的地方（Lean）成立，還是在雜訊驗證器領域（測試、LLM 評審委員會）也成立？

資料來源#

Advancing Mathematics Research with AI-Driven Formal Proof Search

代理迴圈超越客製化系統

資料來源#

摘要#

作者筆下的意外結果#

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

殘餘優勢（以及它的到期日）#

泛化#

相關連結#

推導#

開放問題#

資料來源#