教導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正是為此而建。