柏克萊Vero基準：43個專案僅27個全解

柏克萊RDI實驗室釋出了一個叫Vero的新基準。它要求AI代理人在整個程式碼庫的規模上同時完成兩件事：把每個必要的API實作出來，並且證明每一條給定的規格都成立，同時讓程式碼、證明和建置三者從頭到尾保持一致。過去的形式化驗證基準大多停留在單一定理或單一函式的層級，儲存庫規模的還是頭一次出現。

題目是43個多模組Lean 4專案，從Python、Dafny、Verus和Coq的既有程式碼移植而來，總共涵蓋743個API與2705條形式化規格。評測跑兩種模式：純證明模式提供參考實作，代理人只需負責證明；實作與證明模式則要求代理人自己寫出實作，再證明它符合規格。

成績單

90分鐘預算下的完全解決數（滿分43）：

第一行和第三行之間的落差值得細看：同樣是GPT-5.5、同樣是Codex，光是把推理檔位從medium調到xhigh，實作與證明模式的成績就從2跳到27。在這類任務上，思考預算帶來的邊際效益遠遠還沒飽和。

難的不是單條證明

榜首那一行還藏著另一組數字。GPT-5.5（xhigh）在實作與證明模式下通過了87.3%的單條規格，純證明模式下則是85.8%，但一旦標準換成「整個實例完全做完」，就只剩27/43和25/43。研究人員的判斷很直接：證明每一條規格本身已經不算難點，難的是讓整個證明儲存庫維持一致。

這兩個數字之間的落差有明確的工程意涵。單條規格87%的通過率，換算到一個有幾十條規格的專案上，幾乎意味著每個專案都會剩下幾條卡住。而形式化驗證是全有全無的遊戲——只要有一條沒證出來，整個儲存庫就無法建置通過，前面證對的部分也拿不到任何部分分。這跟單元測試通過87%、專案照樣能上線，完全是兩碼事。

另一個值得留意的細節，是證明程式碼的組成。在那些完全解決的執行紀錄裡，輔助定理占了證明程式碼中位數的73.6%。也就是說，代理人寫出來的東西有四分之三只是為了撐住主證明而臨時搭的鷹架。這個比例暗示現在的模型走的是廣度優先的路線，靠堆疊引理硬推過關，而不是找出簡潔的證明結構。

自己挑演算法，五次幫上忙、十七次幫倒忙

實作與證明模式給了代理人一個額外的自由度：既然實作可以自己寫，那就能挑一個更好證的演算法。研究人員統計了這個自由度的淨效果，用配對比較的方式來看，5組因為換了演算法而做成，17組反而因此失敗。

這個5比17的數字挺說明問題。理論上，能自選實作應該只增不減——大不了照抄參考實作。但實際結果是，模型常常挑了一個自認為聰明、卻更難證明的寫法，然後在90分鐘裡卡住出不來。會寫程式碼和知道哪種寫法好證明，是兩種不同的能力，現在的代理人只具備前一種。

榜單最後還留了一筆：43個實例裡有10個，在所有組合、兩種模式下都沒有任何一次被解出來。這批題目構成了目前方法的硬上限，也是下一輪研究最該盯緊的地方。

對打造AI編程工具的人來說，Vero的參考價值不在排名，而在於它把「儲存庫規模的一致性」這個過去只能憑經驗感受的東西，拆解成了可以量測的指標。SWE-bench那類基準測的是能不能改對一個bug，Vero測的則是能不能扛住一整個工程專案的完整約束，兩者的難度根本不在同一個量級上。

參考來源：柏克萊RDI實驗室公開部落格、CocoLoop；基準規模、兩種模式的完全解決數、單條規格通過率、輔助定理占比與配對統計，均已按公開報告內容核對。