讓 AI 寫出精準的 Rust 驗證規格：Verus-SpecGym 自動化形式化評測環境

本研究開發了 Verus-SpecGym 環境與 Verus-SpecBench 基準測試，專注於評估 LLM 將自然語言描述轉化為 Rust 正式規格的能力，並透過可執行規格驗證大幅提升了評測準確度。

Problem

雖然 AI 代理能產出程式碼，但確保其符合使用者意圖仍具挑戰。形式化驗證雖能保證正確性，但手寫正式規格極其困難且容易出錯，且傳統評測方法（如 LLM 裁判）難以偵測規格中的細微邏輯謬誤。

團隊推出 Verus-SpecBench 基準測試（包含 581 個任務）與代理環境 Verus-SpecGym。核心技術包含擴充 Verus 的 exec_spec 機制，讓產出的規格能轉化為可執行 Rust 程式碼，並結合 Codeforces 的測試資料與對抗性案例進行精準的自動化檢核。

最強大的模型 Gemini 3.1 Pro 成功率達 77.8%，其他前沿模型介於 51% 至 57% 之間，而開源模型僅約 21.5%。研究發現，若僅使用 LLM 作為裁判會遺漏約 26% 的錯誤，常見失敗原因包括遺漏輸入假設或錯誤地接受/拒絕特定輸出。

此研究證明了自動化規格建構（Autoformalization）的潛力，並提供了一套比傳統 LLM 評審更可靠的自動化測試框架。這對於開發具備自我校驗能力、能生成可驗證軟體的強健 AI 代理系統至關重要。