AI 開發(fā)復(fù)雜軟件的時代即將到來？

近年來，以 Google 的 AlphaEvolve 為代表的研究已經(jīng)證明，AI 智能體可以通過迭代來優(yōu)化算法，甚至在某些小型、獨(dú)立的編程任務(wù)上超越人類。然而，這些工作大多局限于幾百行代碼的「算法內(nèi)核」或單個文件。

但現(xiàn)實(shí)世界的軟件，比如一個頂級的 SAT 求解器，是一個龐大而復(fù)雜的系統(tǒng)工程，包含數(shù)百個文件、精密的編譯系統(tǒng)和無數(shù)相互關(guān)聯(lián)的模塊。手動打造一個冠軍級求解器不僅需要極高的領(lǐng)域知識，而且投入產(chǎn)出比越來越低。

為此，NVIDIA Research 的研究人員提出了 SATLUTION，首個將 LLM 代碼進(jìn)化能力從「算法內(nèi)核」擴(kuò)展到「完整代碼庫」規(guī)模的框架。SATLUTION 能夠處理包含數(shù)百個文件、數(shù)萬行 C/C++ 代碼的復(fù)雜項目，并在被譽(yù)為「計算理論基石」的布爾可滿足性（SAT）問題上，取得了超越人類世界冠軍的性能。

• 論文標(biāo)題：Autonomous Code Evolution Meets NP-Completeness 
• 論文地址：https://arxiv.org/pdf/2509.07367

SATLUTION 框架通過協(xié)調(diào) LLM 智能體，在嚴(yán)格的正確性驗(yàn)證和分布式運(yùn)行時反饋的指導(dǎo)下，直接對 SAT 求解器的代碼庫進(jìn)行迭代優(yōu)化。值得一提的是，在這一過程中，它還會同步地「自我進(jìn)化」其進(jìn)化策略與規(guī)則。

基于 2024 年 SAT 競賽的代碼庫與基準(zhǔn)，SATLUTION 進(jìn)化出的求解器不僅在 2025 年的 SAT 競賽中擊敗了人類設(shè)計的冠軍，而且在 2024 年的基準(zhǔn)測試集上，其性能也同時超越了 2024 年和 2025 年兩屆的冠軍。

SATLUTION 在 2025 年 SAT 競賽基準(zhǔn)測試中的驚人表現(xiàn)。圖中柱狀圖的高度代表 PAR-2 分?jǐn)?shù)（一種衡量求解器性能的指標(biāo)，越低越好）。左側(cè)顏色漸變的柱體是 SATLUTION 進(jìn)化出的求解器家族，它們的分?jǐn)?shù)顯著低于人類設(shè)計的 2025 年競賽冠軍（藍(lán)色）和亞軍（綠色）。

SATLUTION 是如何工作的？

SATLUTION 圍繞 LLM 智能體、一套動態(tài)規(guī)則系統(tǒng)以及一個嚴(yán)格的驗(yàn)證與反饋循環(huán)構(gòu)建。

雙智能體架構(gòu)

該系統(tǒng)由兩個協(xié)同工作的 LLM 智能體驅(qū)動，基于 Cursor 環(huán)境和 Claude 系列模型實(shí)現(xiàn)。

規(guī)劃智能體：負(fù)責(zé)高層次的戰(zhàn)略制定。在進(jìn)化周期的初始階段，它會分析作為起點(diǎn)的求解器代碼庫及其性能，提出有潛力的修改方向。在后續(xù)周期中，它會綜合考量累積的代碼變更、性能指標(biāo)和歷史失敗記錄，為下一次迭代制定新的進(jìn)化計劃。

編碼智能體：負(fù)責(zé)執(zhí)行具體的開發(fā)任務(wù)。它根據(jù)規(guī)劃智能體的藍(lán)圖，直接對 C/C++ 求解器代碼庫進(jìn)行編輯和實(shí)現(xiàn)。其職責(zé)還包括管理輔助任務(wù)，例如更新 Makefile 等構(gòu)建系統(tǒng)配置、修復(fù)編譯錯誤以及調(diào)試功能性或執(zhí)行時錯誤。

規(guī)則系統(tǒng)：引導(dǎo)與約束

規(guī)則系統(tǒng)是確保進(jìn)化過程高效和穩(wěn)定的關(guān)鍵。它為智能體的探索提供了必要的引導(dǎo)，有效減少了在無效或錯誤方向上的嘗試。

在進(jìn)化開始前，研究人員為系統(tǒng)設(shè)定了一套靜態(tài)規(guī)則，編碼了基礎(chǔ)的領(lǐng)域知識和硬性約束。這包括：基本的 SAT 啟發(fā)式算法原則、嚴(yán)格的正確性要求（如必須為無解實(shí)例生成 DRAT 證明）、統(tǒng)一的代碼庫目錄結(jié)構(gòu)規(guī)范以及詳細(xì)的評估協(xié)議。

實(shí)驗(yàn)表明，在缺少這套初始規(guī)則的情況下，智能體的表現(xiàn)會顯著下降，容易產(chǎn)生偏離目標(biāo)的修改。

該框架的一個核心特點(diǎn)是規(guī)則庫本身能夠動態(tài)演進(jìn)。在每個進(jìn)化周期結(jié)束后，一個分析器會對過程中的編譯錯誤、驗(yàn)證失敗和新出現(xiàn)的失效模式進(jìn)行復(fù)盤，并自動提出規(guī)則補(bǔ)丁。

例如，系統(tǒng)可以根據(jù)一次失敗的經(jīng)驗(yàn)，自動向規(guī)則庫中添加一個新的「禁止代碼模式」，從而防止智能體在未來重復(fù)同樣的錯誤。這使得規(guī)則系統(tǒng)與求解器代碼共同進(jìn)化，不斷提升框架的整體效率和魯棒性。

驗(yàn)證與評估流程

為保障代碼質(zhì)量和求解的正確性，每個新生成的求解器版本都必須通過一個嚴(yán)格的流程。

• 兩階段驗(yàn)證
  

第一階段是編譯和基本功能測試。 系統(tǒng)會嘗試編譯新代碼，成功后在一個包含 115 個簡單 CNF 實(shí)例的測試集上運(yùn)行，以捕捉編譯錯誤、段錯誤等基礎(chǔ)問題。

第二階段是完整的正確性驗(yàn)證。 通過第一階段的求解器會在一個更大的、結(jié)果已知的基準(zhǔn)測試集上運(yùn)行。對于其輸出的每一個結(jié)果，系統(tǒng)都會進(jìn)行核查：如果報告「可滿足」（SAT），則驗(yàn)證所給出的賦值是否正確；如果報告「不可滿足」（UNSAT），則使用外部檢查工具驗(yàn)證其生成的 DRAT 證明的有效性。

只有完全通過這兩個階段驗(yàn)證的求解器，才會被認(rèn)為是「正確」的，并進(jìn)入下一步的性能評估。

• 分布式評估與反饋
  

通過驗(yàn)證的求解器會被部署到一個由 800 個 CPU 節(jié)點(diǎn)組成的集群上，在完整的 SAT Competition 2024 基準(zhǔn)測試集（包含 400 個實(shí)例）上進(jìn)行并行評估。這種大規(guī)模并行使得整個評估過程可以在大約一小時內(nèi)完成，從而為智能體提供近乎實(shí)時的性能反饋。

反饋指標(biāo)非常詳盡，包括已解決的 SAT/UNSAT 實(shí)例數(shù)量、不同時間段內(nèi)解決的實(shí)例分布、內(nèi)存使用情況，以及作為核心驅(qū)動指標(biāo)的 PAR-2 分?jǐn)?shù)（一種對未解決實(shí)例進(jìn)行高額時間懲罰的平均運(yùn)行時指標(biāo)）。

實(shí)驗(yàn)結(jié)果

SATLUTION 在 70 個進(jìn)化周期的實(shí)驗(yàn)中，展現(xiàn)了清晰且穩(wěn)健的性能提升軌跡。

根據(jù)論文中對 2024 年基準(zhǔn)測試集的性能追蹤圖表（圖 8）顯示，在最初的 5-10 個迭代周期中，系統(tǒng)取得了快速進(jìn)展，這主要是因?yàn)樗狭硕鄠€初始種子求解器的互補(bǔ)優(yōu)勢。

隨后，性能提升的速度有所放緩，但仍在持續(xù)進(jìn)行，表明智能體開始處理更細(xì)微和復(fù)雜的優(yōu)化問題。

大約在第 50 次迭代時，SATLUTION 進(jìn)化出的求解器在 2024 年的基準(zhǔn)上已經(jīng)開始優(yōu)于 2025 年的人類設(shè)計冠軍。

到第 70 次迭代結(jié)束時，其性能已穩(wěn)定地超越了所有用于比較的基準(zhǔn)求解器。整個過程表現(xiàn)出高度的穩(wěn)定性，由于驗(yàn)證保障措施的存在，沒有發(fā)生過嚴(yán)重的性能衰退。

SATLUTION 自進(jìn)化性能曲線。

整個 SATLUTION 自我進(jìn)化實(shí)驗(yàn)過程的總計成本低于 20000 美元。相比之下，由人類專家開發(fā)一個具有競爭力的 SAT 求解器通常需要數(shù)月乃至數(shù)年的持續(xù)工程投入，而 SATLUTION 在數(shù)周內(nèi)便取得了超越頂尖人類水平的成果。

更多細(xì)節(jié)請參見原論文。