1. 首頁 > 生活百科 > >

英偉達的AI已經開始接管整個項目了？SATLUTION進化代碼庫登頂SAT

人工智能ai朱嘯虎

英偉達的AI已經開始接管整個項目了？SATLUTION進化代碼庫登頂SAT

文章圖片

英偉達的AI已經開始接管整個項目了？SATLUTION進化代碼庫登頂SAT

文章圖片


【英偉達的AI已經開始接管整個項目了？SATLUTION進化代碼庫登頂SAT】機器之心報道
機器之心編輯部
AI 開發復雜軟件的時代即將到來？
近年來 ， 以 Google 的 AlphaEvolve 為代表的研究已經證明 ， AI 智能體可以通過迭代來優化算法 ， 甚至在某些小型、獨立的編程任務上超越人類 。 然而 ， 這些工作大多局限于幾百行代碼的「算法內核」或單個文件 。

但現實世界的軟件 ， 比如一個頂級的 SAT 求解器 ， 是一個龐大而復雜的系統工程 ， 包含數百個文件、精密的編譯系統和無數相互關聯的模塊 。 手動打造一個冠軍級求解器不僅需要極高的領域知識 ， 而且投入產出比越來越低 。
為此 ， NVIDIA Research 的研究人員提出了 SATLUTION ， 首個將 LLM 代碼進化能力從「算法內核」擴展到「完整代碼庫」規模的框架 。 SATLUTION 能夠處理包含數百個文件、數萬行 C/C++ 代碼的復雜項目 ， 并在被譽為「計算理論基石」的布爾可滿足性（SAT）問題上 ， 取得了超越人類世界冠軍的性能 。

論文標題：Autonomous Code Evolution Meets NP-Completeness 論文地址：https://arxiv.org/pdf/2509.07367SATLUTION 框架通過協調 LLM 智能體 ， 在嚴格的正確性驗證和分布式運行時反饋的指導下 ， 直接對 SAT 求解器的代碼庫進行迭代優化 。 值得一提的是 ， 在這一過程中 ， 它還會同步地「自我進化」其進化策略與規則 。
基于 2024 年 SAT 競賽的代碼庫與基準 ， SATLUTION 進化出的求解器不僅在 2025 年的 SAT 競賽中擊敗了人類設計的冠軍 ， 而且在 2024 年的基準測試集上 ， 其性能也同時超越了 2024 年和 2025 年兩屆的冠軍 。

SATLUTION 在 2025 年 SAT 競賽基準測試中的驚人表現 。 圖中柱狀圖的高度代表 PAR-2 分數（一種衡量求解器性能的指標 ， 越低越好） 。 左側顏色漸變的柱體是 SATLUTION 進化出的求解器家族 ， 它們的分數顯著低于人類設計的 2025 年競賽冠軍（藍色）和亞軍（綠色） 。
SATLUTION 是如何工作的？
SATLUTION 圍繞 LLM 智能體、一套動態規則系統以及一個嚴格的驗證與反饋循環構建 。
雙智能體架構
該系統由兩個協同工作的 LLM 智能體驅動 ， 基于 Cursor 環境和 Claude 系列模型實現 。
規劃智能體：負責高層次的戰略制定 。 在進化周期的初始階段 ， 它會分析作為起點的求解器代碼庫及其性能 ， 提出有潛力的修改方向 。 在后續周期中 ， 它會綜合考量累積的代碼變更、性能指標和歷史失敗記錄 ， 為下一次迭代制定新的進化計劃 。
編碼智能體：負責執行具體的開發任務 。 它根據規劃智能體的藍圖 ， 直接對 C/C++ 求解器代碼庫進行編輯和實現 。 其職責還包括管理輔助任務 ， 例如更新 Makefile 等構建系統配置、修復編譯錯誤以及調試功能性或執行時錯誤 。
規則系統：引導與約束
規則系統是確保進化過程高效和穩定的關鍵 。 它為智能體的探索提供了必要的引導 ， 有效減少了在無效或錯誤方向上的嘗試 。
在進化開始前 ， 研究人員為系統設定了一套靜態規則 ， 編碼了基礎的領域知識和硬性約束 。 這包括：基本的 SAT 啟發式算法原則、嚴格的正確性要求（如必須為無解實例生成 DRAT 證明）、統一的代碼庫目錄結構規范以及詳細的評估協議 。
實驗表明 ， 在缺少這套初始規則的情況下 ， 智能體的表現會顯著下降 ， 容易產生偏離目標的修改 。
該框架的一個核心特點是規則庫本身能夠動態演進 。 在每個進化周期結束后 ， 一個分析器會對過程中的編譯錯誤、驗證失敗和新出現的失效模式進行復盤 ， 并自動提出規則補丁 。
例如 ， 系統可以根據一次失敗的經驗 ， 自動向規則庫中添加一個新的「禁止代碼模式」 ， 從而防止智能體在未來重復同樣的錯誤 。 這使得規則系統與求解器代碼共同進化 ， 不斷提升框架的整體效率和魯棒性 。
驗證與評估流程
為保障代碼質量和求解的正確性 ， 每個新生成的求解器版本都必須通過一個嚴格的流程 。
兩階段驗證第一階段是編譯和基本功能測試 。系統會嘗試編譯新代碼 ， 成功后在一個包含 115 個簡單 CNF 實例的測試集上運行 ， 以捕捉編譯錯誤、段錯誤等基礎問題 。
第二階段是完整的正確性驗證 。通過第一階段的求解器會在一個更大的、結果已知的基準測試集上運行 。 對于其輸出的每一個結果 ， 系統都會進行核查：如果報告「可滿足」（SAT） ， 則驗證所給出的賦值是否正確；如果報告「不可滿足」（UNSAT） ， 則使用外部檢查工具驗證其生成的 DRAT 證明的有效性 。
只有完全通過這兩個階段驗證的求解器 ， 才會被認為是「正確」的 ， 并進入下一步的性能評估 。
分布式評估與反饋通過驗證的求解器會被部署到一個由 800 個 CPU 節點組成的集群上 ， 在完整的 SAT Competition 2024 基準測試集（包含 400 個實例）上進行并行評估 。 這種大規模并行使得整個評估過程可以在大約一小時內完成 ， 從而為智能體提供近乎實時的性能反饋 。
反饋指標非常詳盡 ， 包括已解決的 SAT/UNSAT 實例數量、不同時間段內解決的實例分布、內存使用情況 ， 以及作為核心驅動指標的 PAR-2 分數（一種對未解決實例進行高額時間懲罰的平均運行時指標） 。
實驗結果
SATLUTION 在 70 個進化周期的實驗中 ， 展現了清晰且穩健的性能提升軌跡 。
根據論文中對 2024 年基準測試集的性能追蹤圖表（圖 8）顯示 ， 在最初的 5-10 個迭代周期中 ， 系統取得了快速進展 ， 這主要是因為它整合了多個初始種子求解器的互補優勢 。
隨后 ， 性能提升的速度有所放緩 ， 但仍在持續進行 ， 表明智能體開始處理更細微和復雜的優化問題 。
大約在第 50 次迭代時 ， SATLUTION 進化出的求解器在 2024 年的基準上已經開始優于 2025 年的人類設計冠軍 。
到第 70 次迭代結束時 ， 其性能已穩定地超越了所有用于比較的基準求解器 。 整個過程表現出高度的穩定性 ， 由于驗證保障措施的存在 ， 沒有發生過嚴重的性能衰退 。

SATLUTION 自進化性能曲線 。
整個 SATLUTION 自我進化實驗過程的總計成本低于 20000 美元 。 相比之下 ， 由人類專家開發一個具有競爭力的 SAT 求解器通常需要數月乃至數年的持續工程投入 ， 而 SATLUTION 在數周內便取得了超越頂尖人類水平的成果 。
更多細節請參見原論文 。

    推薦閱讀