VASO：形式化可驗證的物理AI智慧體自進化技能
VASO是一個框架，透過形式化驗證引導大語言模型生成的機器人技能合約的自我進化。在Clearpath Jackal和PX4四旋翼任務上，VASO在不到100個最佳化樣本下達到了97.2%的規範符合度，優於執行反饋、提示最佳化和微調基線。這是首個將形式化驗證與自進化技能閉環的框架。
隨著基礎模型（如大語言模型）的快速發展，機器人技能的建立成本大幅降低，但信任成本並未隨之下降。傳統的技能進化迴圈依賴執行反饋、單元測試、環境獎勵或LLM自我批判，但這些訊號僅能提供軌跡級別的證據，證明技能在取樣的執行中有效，而無法保證在未測試條件下技能所引發的計劃能夠滿足時序安全合約。為了解決這一問題，來自學界的研究團隊提出了VASO（Verifiably Autonomous Self-Operating）框架，旨在透過形式化驗證引導LLM生成的機器人技能合約實現自我進化。
VASO的核心思想是將每個可重用的機器人技能表示為一個語義合約，該合約包含兩個關鍵的介面：形式化介面和規劃器介面。形式化介面將機器人的狀態、觀測和控制命令與邏輯命題對齊，以便進行模型檢查；規劃器介面則指導可執行行為的生成。在執行過程中，模型檢查器首先過濾掉邏輯不一致的技能合約，然後驗證由該技能引發的計劃是否滿足全域性和區域性的時序規範。如果驗證失敗，VASO將反例軌跡轉換為文本梯度，用於更新可重用的技能合約，同時保持基礎模型的權重不變。
在實驗部分，研究團隊在Clearpath Jackal地面機器人和PX4四旋翼無人機上對VASO進行了測試。結果顯示，VASO在不到100個最佳化樣本的情況下達到了97.2%的形式規範符合度，顯著優於執行反饋、提示最佳化和微調等基線方法。據我們所知，VASO是首個將形式化驗證與LLM生成技能自進化閉環的框架，其中形式反例不僅用於驗證一次性計劃，還成為可重用技能合約的最佳化反饋，從而避免了僅調整規劃器提示或微調模型權重的侷限性。
這項研究為機器人技能的可信進化提供了新的正規化，有望在安全關鍵的物理AI應用中發揮重要作用。透過將形式化驗證融入技能進化迴圈，VASO能夠提供更強的安全保障，確保機器人行為在複雜環境中始終符合預期。