Rust自動形式化證明、LLMs圖模式理解、機械臂動作模仿

（本文閱讀時間：7分鐘）

編者按：歡迎閱讀“科研上新”欄目！“科研上新”匯聚了微軟亞洲研究院最新的創新成果與科研動態。在這裡，你可以快速瀏覽研究院的亮點資訊，保持對前沿領域的敏銳嗅覺，同時也能找到先進實用的開源工具。

「本期內容速覽」

自我進化實現Rust自動形式化證明

基於圖模式的理解基準測試

IGOR: 透過學習統一的動作表示空間讓機械臂模仿人類動作

自我進化實現Rust自動形式化證明

論文連結：

https://arxiv.org/pdf/2410.15756

形式化驗證是透過數學方法來證明軟體正確性的手段，它要求開發者用形式化語言寫出軟體系統需要滿足的屬性，再寫出形式化的證明，用自動定理求解器去證明軟體滿足這些屬性。高昂的人工成本使得開發者對使用這類方法望而卻步，這也導致形式化證明的程式碼很少，即便是大語言模型，也由於缺乏訓練資料難以生成這樣的證明程式碼。

對此，微軟亞洲研究院的研員們透過讓大語言模型自我進化的方式，實現了 Rust 程式碼上的自動形式化證明。自我進化框架能夠迭代式地合成更高質量的資料，並用於訓練更強的能夠生成形式化證明程式碼的模型。

具體來說，研究員們首先收集了大量適合於證明的 Rust 程式碼，將它們翻譯成能夠被證明的形式化語言 Verus，所有被 Verus 編譯器透過的程式碼將被保留作為種子資料進行合成。接下來，用大模型自我進化的方式生成 Verus 規範，即程式碼需要滿足的形式化屬性，在每一輪進化中，前一輪生成的規範將用於訓練一個新的、經過微調的開源模型，從而在下一輪微調中生成更多質量更高的規範。最後，為了獲得能夠透過驗證的程式碼，模型還需要生成證明程式碼以證明上述規範能被滿足。研究員們同樣使用了自我進化的方式微調大模型，在這個過程中，所有合成的能被 Verus 驗證的程式碼將會作為訓練語料，同時，在生成過程中的錯誤程式碼會和它的錯誤資訊一起，作為訓練模型自我 debug 能力的語料。

圖1：自我進化框架示意圖

在由 Verus 專家構建的基準上，經過自我進化的開源模型在自動生成證明程式碼的任務上的 pass@10 透過率達到了70.50%，相較於未經訓練時的17.27%有了巨大的飛躍。這一成果充分驗證了本篇論文中提出的自我進化資料合成與微調框架的有效性。

大語言模型對於圖模式（graph pattern）理解的基準測試

論文連結：

https://arxiv.org/pdf/2410.05298

目前，大量工作已經驗證了大語言模型（LLMs）可以進行最基本的圖推理任務，即 LLMs 可以找到兩個節點之間的連線關係。圖不僅僅可以透過點的連線關係表示特徵，也可以透過帶一定特徵的子圖表示，比如，圖中是否含有三角形連線關係，分子圖中是否含有苯環結構，社交圖中是否含有星狀結構。這些圖模式在圖挖掘以及圖學習中非常重要。

在本篇論文中，研究員們測試了包括 GPT-4、GPT-4o 和 O1 在內的 7 種大語言模型在圖模式識別中的能力，實驗設計中包含了總共4大任務以及11種子任務。具體而言，研究員們考察了這些模型是否能夠在每個圖中使用子圖定義和子圖匹配的方法來識別圖中的子圖特徵。此外，該測試還評估了模型在沒有特定子圖提示的情況下，總結圖資料集的規律並預測其中的特徵，以及這些特徵與資料標籤之間的關係。最後，研究員們在真實資料集上測試了大語言模型的圖模式匹配能力及其圖分類的效果。

表1：對不同型別的圖模式表達方式進行測評

根據不同大語言模型在各類圖模式任務中的表現，研究員們總結出了一些關於大語言模型在圖模式任務上的重要發現。例如：1. 大語言模型具備基礎的圖模式理解能力，隨著模型能力的提升（如 O1 模型），在某些任務中的預測效能會顯著提高；2. 大語言模型可以利用先驗知識增強圖模式理解能力，並將這種能力擴充套件到真實資料集的分析；3. 大語言模型在圖模式認知過程中可能會採用不同的演算法或策略，這將影響模型的預測準確性。

這些發現為未來基於大語言模型的圖模型開發以及提升其對複雜邏輯結構的理解，提供了重要指導。研究員們也將持續對相關問題進行更加深入的探索。

IGOR: 透過學習統一的動作表示空間讓機械臂模仿人類動作

論文連結：

https://arxiv.org/pdf/2411.00785

專案連結：

https://aka.ms/project-igor

在訓練具身智慧領域的基礎模型時，帶有標籤的高質量機器人資料是保證模型質量的關鍵，但直接採集機器人資料成本較高。考慮到網際網路影片資料中展示了豐富的人類活動，包括人類是如何與現實世界中的各種物體進行互動的。那麼，是否可以透過影片資料為人類和機器人學習一個統一的動作表示空間，以實現跨任務和智慧體的知識遷移和下游任務效果的提升呢？基於這一齣發點，研究員們提出了影像目標表示（IGOR，Image-Goal Representation）。

如何學到人類和機器人統一的動作表示？

IGOR 使用了潛在動作模型 LAM（Latent Action Model），將初始狀態和目標狀態之間的視覺變化壓縮為低維向量，並透過最小化初始狀態和動作向量對目標狀態的重建損失進行訓練。這樣，具有相似視覺變化的影像狀態會具有相似的動作向量，代表了它們在語義空間而非畫素空間上的變化。

圖2：IGOR 框架例項，包含了三個基礎模型：Latent Action Model, Policy Model 和 World Model

透過 LAM，研究員們可以將網際網路規模的影片資料轉化為帶有潛在動作標註的資料，大大擴充套件了具身智慧基礎模型能夠使用的資料量。這個統一的潛在動作空間使研究員們能夠在幾乎任意由機器人和人類執行的任務上訓練 Policy Model 和 World Model。透過結合 LAM 和 World Model，IGOR 成功地將一個影片中的物體運動“遷移”到了其他影片中。並且，這些動作實現了跨任務和跨智慧體的遷移。也就是說，用人類的行為給機器人做演示，機器人也能做出正確的動作。如下圖所示，LAM 得到的潛在動作表示可以同時實現跨任務（用手移動不同物體）和跨智慧體（用手的移動指導機械臂的移動）的遷移。