教導AI推理軟件
AWS團隊通過訓練小型語言模型於Soteria的符號執行軌跡上，使其在C語言錯誤檢測上超過了四倍大的模型。本文探討了這一方法及其對AI輔助軟件工程的影響。
亞馬遜雲服務（AWS）的一個團隊近期發佈了一項研究，利用Soteria的符號執行軌跡來訓練AI模型，使其能夠推理代碼。研究結果引人注目：通過僅用少量Soteria生成的符號執行軌跡對80億參數模型進行持續訓練，該模型在C語言錯誤檢測方面的表現超過了比它大四倍的模型。
現代AI編碼助手正在改變軟件開發的方式，但它們有一個根本侷限性：能夠生成看似正確的代碼，卻難以理解代碼是否真正正確。大型語言模型從海量源代碼中學習，但軟件工程不僅僅是生成語法正確的代碼。人類軟件工程師通過觀察程序運行來理解其行為，而調試、執行軌跡和測試失敗提供了更深的語義理解。
AWS的研究人員直接測量了這一差距。他們構建了包含500個C語言驗證任務的評估集，涵蓋內存安全、溢出、終止、可達性和數據競爭。結果顯示，模型在確認屬性成立方面表現良好（多數超過90%），但在檢測違規時表現不佳。14個模型中有4個捕獲了不到一半的真實錯誤，且隨着程序長度增加，準確率急劇下降。
這正是Soteria發揮作用的地方。Soteria是一款符號執行工具，能夠深入語義層推理軟件行為。它記錄程序狀態、符號值、路徑條件和分支決策，精確捕獲錯誤發生的條件。這些軌跡可以導出為機器可讀的JSON或交互式HTML，從而將符號執行從驗證技術轉變為訓練數據的來源。
研究人員將Soteria在開源C代碼上運行，收集軌跡，然後用這些軌跡對Qwen3-8B模型進行持續預訓練。結果顯示，訓練後模型在軟件驗證任務上表現顯著提升。最佳組合是使用Soteria的錯誤軌跡訓練，並在推理時讓模型逐步推理，這使違規檢測提高了17.9個百分點。訓練後的8B模型檢測違規的可靠性（67%）超過了未訓練的32B模型（57%）。
更重要的是，訓練泛化到了所有五種屬性類型，表明模型學習了通用推理模式，而非記憶特定錯誤形狀。這意味着下一代AI不僅可以從源代碼學習，還可以從程序語義——即代碼實際如何執行——中學習。
Soteria團隊認為，這將在AI和驗證之間創建強大的良性循環：AI生成代碼，Soteria分析代碼生成語義軌跡，軌跡幫助訓練更好的AI模型，再生成更高質量的代碼。長期目標是讓Soteria在crates.io（Rust包註冊表）上運行，生成Rust代碼有史以來最大的語義數據集。
未來的軟件工程將由AI和形式驗證的交互塑造。最強大的系統將結合語言模型的創造力和規模與形式推理的嚴謹性和精確性。Soteria正是為此而建。