英偉達的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.07367

SATLUTION 框架通過協調 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 在數周內便取得了超越頂尖人類水平的成果。

更多細節請參見原論文。