近期，arXiv上陸續(xù)出現(xiàn)了大模型自動(dòng)優(yōu)化約束求解器的論文，一個(gè)是當(dāng)下熱門的 AI 方向，一個(gè)是比較傳統(tǒng)的算法研究方向，它們的碰撞會(huì)擦出怎樣的火花？

求解器，是工業(yè)軟件的核心計(jì)算引擎，它在芯片設(shè)計(jì)、工業(yè)調(diào)度、智能制造等多個(gè)領(lǐng)域都有重要應(yīng)用。比如，布爾可滿足性問(wèn)題（SAT，Satisfiability Problem）求解器就是電子設(shè)計(jì)自動(dòng)化（EDA，Electronic Design Automation）不可或缺的計(jì)算引擎。而 EDA 軟件則是芯片領(lǐng)域設(shè)計(jì)的至關(guān)重要的工具，也被稱為芯片產(chǎn)業(yè)的“命門”，因此該領(lǐng)域的研究成果與中國(guó)解決芯片“卡脖子”問(wèn)題直接相關(guān)。

圖 | 蔡少偉（來(lái)源：蔡少偉）

中國(guó)科學(xué)院軟件研究所研究員蔡少偉帶領(lǐng)的團(tuán)隊(duì)長(zhǎng)期研究約束求解器，近三年來(lái)該團(tuán)隊(duì)在結(jié)合大模型和約束求解的方向上持續(xù)耕耘，在arXiv上陸續(xù)公開了相關(guān)論文。蔡少偉認(rèn)為，在大模型的加持下，求解器領(lǐng)域即將發(fā)生一次偉大的變革。求解器的研發(fā)周期和門檻將大大降低，算法思路也將由大模型得以擴(kuò)展，這將讓人們能夠更快地研發(fā)更高性能的求解器。

據(jù)了解，該團(tuán)隊(duì)近幾年的一個(gè)重要研究方向是如何利用大模型更快更好地完成求解器研發(fā)工作。在這一方向上，他們已經(jīng)基于大模型研發(fā)了多個(gè)求解器，涵蓋了布爾可滿足性問(wèn)題和偽布爾優(yōu)化（PBO，Pseudo-Boolean Optimization）問(wèn)題的求解器。其中，他們最重要成果便是基于大模型的 SAT 求解器。

該團(tuán)隊(duì)認(rèn)為，基于一個(gè)基礎(chǔ)求解器進(jìn)行優(yōu)化、而非完全從零開始是非常有益的，這樣大模型可以充分利用人類長(zhǎng)期經(jīng)驗(yàn)建立起來(lái)的有效算法框架下進(jìn)行算法設(shè)計(jì)。

近期，對(duì)于布爾可滿足性問(wèn)題，該團(tuán)隊(duì)通過(guò)大模型解決了求解器研發(fā)的三個(gè)關(guān)鍵挑戰(zhàn)：LLM-友好的求解器開發(fā)、自動(dòng)提示優(yōu)化和高效搜索策略。

其中涉及到的關(guān)鍵技術(shù)包括：

第一項(xiàng)關(guān)鍵技術(shù)是模塊化求解器設(shè)計(jì)：該團(tuán)隊(duì)基于以下三個(gè)原則——修改的函數(shù)簡(jiǎn)潔、代碼中類變量共享信息、啟發(fā)式探索中主動(dòng)防錯(cuò)，設(shè)計(jì)了 LLM-友好的求解器，為后續(xù)大模型的自動(dòng)優(yōu)化算法提供了基礎(chǔ)。

第二項(xiàng)關(guān)鍵技術(shù)是自動(dòng)提示優(yōu)化：該團(tuán)隊(duì)通過(guò)采用無(wú)監(jiān)督方法增強(qiáng)了大模型輸出的多樣性，避免了人工設(shè)計(jì)限制。

第三項(xiàng)關(guān)鍵技術(shù)是預(yù)搜索策略：即結(jié)合候選解剪枝和進(jìn)化細(xì)化，引導(dǎo)大模型自動(dòng)地生成高性能求解器。

第四項(xiàng)關(guān)鍵技術(shù)是關(guān)鍵函數(shù)優(yōu)化：通過(guò)大模型修改各個(gè)重要函數(shù)對(duì)代碼，比如一些重要的啟發(fā)式策略，以此不斷地優(yōu)化求解器。

（來(lái)源：https://arXiv.org/abs/2507.22876）

研究團(tuán)隊(duì)表示，其基于大模型研發(fā)的 SAT 求解器，在多個(gè)工業(yè)實(shí)例測(cè)試集上領(lǐng)先于人類研發(fā)的求解器。實(shí)驗(yàn)表明，利用大模型針對(duì)現(xiàn)存的工業(yè)級(jí)布爾可滿足性問(wèn)題求解器 MiniSAT 進(jìn)行優(yōu)化，可以使其平均求解速度提速 50%，并在多個(gè)工業(yè)實(shí)例集上超過(guò)目前人類設(shè)計(jì)的最先進(jìn)求解器的性能。

蔡少偉還對(duì) DeepTech 表示，布爾可滿足性問(wèn)題是非確定性多項(xiàng)式時(shí)間（NP，Nondeterministic Polynomial time）完全問(wèn)題的典型代表，而此次成果也意味著諸多的復(fù)雜程序和專業(yè)軟件都會(huì)因?yàn)榇竽Ｐ偷膮⑴c進(jìn)入一個(gè)快速發(fā)展期。其相信，大模型將使得求解器研發(fā)邁上一個(gè)新臺(tái)階，從而能夠更好、更快地服務(wù)各種工業(yè)需求。

據(jù)了解，蔡少偉在 2020 年之前就開始研究求解器的自動(dòng)化設(shè)計(jì)問(wèn)題。2020 年，該團(tuán)隊(duì)曾和自動(dòng)算法設(shè)計(jì)領(lǐng)域?qū)＜?、荷蘭萊頓大學(xué)教授霍爾格·胡斯（Holger Hoos）利用 AI 自動(dòng)配置算法策略來(lái)提升布爾可滿足性問(wèn)題求解器的性能，相關(guān)論文發(fā)表于 2020 年的自然并行問(wèn)題求解國(guó)際會(huì)議（PPSN，Parallel Problem Solving from Nature）上。

在 2022 年 GPT 出現(xiàn)之后，蔡少偉很快想到大模型對(duì)于數(shù)學(xué)建模和數(shù)學(xué)求解器的自動(dòng)化將帶來(lái)重大改革，于是便迅速啟動(dòng)了相關(guān)研究。恰逢復(fù)旦大學(xué)教授魏軻團(tuán)隊(duì)也在進(jìn)行相關(guān)探索，于是雙方一拍即合，立項(xiàng)合作研發(fā)基于大模型的求解器優(yōu)化框架，并邀請(qǐng)了孫一文同學(xué)到中國(guó)科學(xué)院軟件研究所實(shí)習(xí)。

但是，約束求解的工業(yè)實(shí)例較大，大模型無(wú)法直接讀取解析，而求解器的更新迭代又比較慢，數(shù)據(jù)集也很少，所以很難按照傳統(tǒng)思路來(lái)通過(guò)大量數(shù)據(jù)集訓(xùn)練得到合適的求解模型。為此，該團(tuán)隊(duì)轉(zhuǎn)而尋找了一些更加輕量級(jí)的方式，比如多 Agent 框架等。

（來(lái)源：https://arXiv.org/pdf/2509.04007）

接著，該團(tuán)隊(duì)針對(duì)如下兩個(gè)問(wèn)題開展研究：一個(gè)是布爾可滿足性問(wèn)題，另一個(gè)是偽布爾優(yōu)化問(wèn)題。前者是最重要的非確定性多項(xiàng)式時(shí)間問(wèn)題，后者是表達(dá)能力更豐富而形式簡(jiǎn)單的運(yùn)籌優(yōu)化問(wèn)題。定下課題之后，他們?cè)O(shè)計(jì)并實(shí)現(xiàn)了基于大模型的自動(dòng)優(yōu)化框架，但是前期實(shí)驗(yàn)的結(jié)果不盡人意。相比于約束求解專家，大模型更類似于一個(gè)“博學(xué)者”，能力強(qiáng)但是不夠?qū)＞?，因此設(shè)計(jì)出的算法常常毫無(wú)道理、漏洞百出。

為此，他們開始集中于研究“如何讓大模型生成的算法效果更好”這個(gè)問(wèn)題。“這個(gè)階段是最重要的、也是最艱難的，我們保存了大模型所生成的全部代碼，分析了一些錯(cuò)誤和不夠好的結(jié)果，并探究了出現(xiàn)這類情況的原因，進(jìn)而通過(guò)完善框架來(lái)解決這些問(wèn)題?！痹搱F(tuán)隊(duì)表示。

經(jīng)過(guò) 2023 年一整年的奮斗，他們終于在 2024 年初發(fā)布了 AutoSAT，這是首個(gè)基于大模型研發(fā)的布爾可滿足性問(wèn)題求解器。AutoSAT 采用多智能體技術(shù)，以現(xiàn)有求解器作為骨架，該團(tuán)隊(duì)在其中留出了關(guān)鍵位置，以便讓大模型去補(bǔ)上最合適的“拼圖”，從而完成求解器的構(gòu)造。

作為領(lǐng)域內(nèi)的首次嘗試，他們?cè)谝粋€(gè)包含幾百行 C++ 代碼的現(xiàn)存入門級(jí)布爾可滿足性問(wèn)題求解器 EasySAT 上進(jìn)行了實(shí)驗(yàn)，結(jié)果發(fā)現(xiàn) EasySAT 的性能得到了顯著改善。在 1 個(gè) AMD EPYC 7763 節(jié)點(diǎn)上進(jìn)行算法演化，以及經(jīng)過(guò) 60 輪的迭代演化之后，EasySAT 完全求解不了任何一個(gè)實(shí)例的問(wèn)題類型上，而該團(tuán)隊(duì)研發(fā)的 AutoSAT 不僅比 EasySAT 更佳，甚至可以超過(guò)當(dāng)時(shí)的全球前沿求解器 Kissat 的性能。

該團(tuán)隊(duì)回憶稱：“2023 年，大模型的能力還沒(méi)有現(xiàn)在這么強(qiáng)大，一個(gè)重要的局限就是處理長(zhǎng)代碼的能力不足。但是到了 2024 年，大模型能力有了一定提升，于是我們開始使用大模型修改更加復(fù)雜的布爾可滿足性問(wèn)題求解器。”

2025 年 7 月 30 日，對(duì)于他們來(lái)說(shuō)是一個(gè)難忘的日子。這一天，他們成功研發(fā)了第二個(gè)基于大模型技術(shù)改進(jìn)的布爾可滿足性問(wèn)題求解器——AutoModSAT，其核心思想是將復(fù)雜求解器改造得具備 LLM-友好的特征，并利用 prompt 自動(dòng)優(yōu)化方法來(lái)提升編寫算法的多樣性，以及通過(guò)預(yù)搜索策略來(lái)減少搜索空間。

他們還使用這一方法改進(jìn)了工業(yè)界常用的一個(gè)著名的開源 SAT 求解器 MiniSAT，期間依舊是在 1 個(gè) AMD EPYC 7763 節(jié)點(diǎn)上進(jìn)行算法演化，經(jīng)過(guò) 60 輪迭代演化之后，他們針對(duì)來(lái)自布爾可滿足性問(wèn)題比賽實(shí)例、電子設(shè)計(jì)自動(dòng)化場(chǎng)景以及不同約束優(yōu)化問(wèn)題的數(shù)據(jù)集篩選了不同難度的數(shù)據(jù)，結(jié)果發(fā)現(xiàn)其所研發(fā)的 AutoModSAT 均能超過(guò) Kissat 3.1.1 和 Cadical 2.0 等現(xiàn)存求解器，也能超過(guò)包含各種調(diào)參版本在內(nèi)的多個(gè) SOTA 求解器的表現(xiàn)。這表明大模型已經(jīng)可以優(yōu)化工業(yè)級(jí)別的求解器。

（來(lái)源：https://arXiv.org/pdf/2507.22876）

在本次研究伊始，他們能夠確定的是：大模型一定能用在求解器研發(fā)上。但是，具體用在哪里？怎么應(yīng)用？成本是否合理？這些問(wèn)題都是未知的。于是，他們齊心協(xié)力進(jìn)行探索，每周都開會(huì)分享自己通過(guò)調(diào)研學(xué)習(xí)到的新知識(shí)，最終才確定了合理的技術(shù)路線?！鞍ê竺骈_發(fā)框架實(shí)驗(yàn)也是這樣，大家總是一起想辦法，一起驗(yàn)證 idea 是否有效，一起分析現(xiàn)有實(shí)驗(yàn)結(jié)果。”研究團(tuán)隊(duì)表示。其繼續(xù)說(shuō)道：“當(dāng)時(shí)看起來(lái)很痛苦，畢竟這是世界上的新技術(shù)、新方法，就好像在黑暗里走迷宮，只能大家互相鼓勵(lì)，一起摸索。”

最終，團(tuán)隊(duì)產(chǎn)出了大模型優(yōu)化 PBO 求解器論文《AutoPBO: 基于大模型的局部搜索偽布爾優(yōu)化求解器優(yōu)化》（AutoPBO: LLM-powered Optimization for Local Search PBO Solvers）[1] 以及大模型優(yōu)化 SAT 求解器論文《AutoSAT：基于大模型的 SAT 求解器優(yōu)化》（AutoSAT: Automatically Optimize SAT Solvers via Large Language Models）[2] 和《復(fù)雜 SAT 求解器中基于大模型的啟發(fā)式自動(dòng)探索》（Automatically discovering heuristics in a complex SAT solver with large language models）[3]。團(tuán)隊(duì)成員李瑾媛、孫一文分別是第一作者，蔡少偉擔(dān)任通訊作者，復(fù)旦大學(xué)魏軻老師為后兩篇論文的共同通訊作者。

圖 | 相關(guān)論文（來(lái)源：arXiv）

值得一提的是，基于大模型的 SAT 求解器逐漸引起了更多關(guān)注。2025 年國(guó)際 SAT 比賽的主賽道冠軍由湖北工業(yè)大學(xué)羅茂教授等人和法國(guó)皮卡爾第大學(xué)李初民教授的合作團(tuán)隊(duì)聯(lián)合獲得。根據(jù)他們的介紹文檔來(lái)看，其主要技術(shù)采用了蔡少偉團(tuán)隊(duì)在此方向的 AutoSAT 系列技術(shù)改進(jìn)了前沿求解器 Kissat。2025 年 9 月，英偉達(dá)結(jié)合 AlphaEvolve 和蔡少偉團(tuán)隊(duì) AutoModSAT 技術(shù)的優(yōu)點(diǎn)（這也是該論文介紹的唯二兩個(gè)相關(guān)工作），使用 Cursor 和 Claude 構(gòu)建了大規(guī)模多智能體系統(tǒng)，利用了 800 個(gè) AMD EPYC 7F72 計(jì)算節(jié)點(diǎn)批量快速測(cè)試了大模型生成的求解器代碼，每輪迭代可以評(píng)估更多求解器版本，從而研發(fā)了求解器 SATLUTION，最終在 SAT Competition 2025 數(shù)據(jù)集上超過(guò)了 2025 年 SAT 冠軍求解器?！斑@些都表明大模型在修改求解器方面已經(jīng)建立起了可行的技術(shù)路徑?！痹搱F(tuán)隊(duì)表示。

據(jù)了解，該團(tuán)隊(duì)已有成員全職創(chuàng)辦了一家名為晞德求索的公司，公司業(yè)務(wù)聚焦于求解器研發(fā)和數(shù)學(xué)技術(shù)服務(wù)，致力于更好地服務(wù)工業(yè)軟件公司。目前，該公司正在不斷完善求解器矩陣，并且研發(fā)的基于大模型的自動(dòng)數(shù)學(xué)建模工具 SeedModeler 也在國(guó)際比賽獲得佳績(jī)，在 SAT 求解器和運(yùn)籌優(yōu)化求解器方面也已打造出商業(yè)化產(chǎn)品，并正在服務(wù)一些著名企業(yè)。

而在后續(xù)，蔡少偉團(tuán)隊(duì)會(huì)繼續(xù)深化該研究，在更復(fù)雜的求解器上進(jìn)行研究，并將提升資源的投入，通過(guò)使用更多的資源來(lái)在更復(fù)雜的智能體系統(tǒng)開展研究。另外，該團(tuán)隊(duì)也計(jì)劃在更多約束求解問(wèn)題上嘗試這種基于大模型的自動(dòng)化框架?！皬哪壳敖?jīng)驗(yàn)來(lái)看，大模型應(yīng)用在其它約束求解問(wèn)題上也有較大的潛力?！痹搱F(tuán)隊(duì)表示。

參考資料：

1.Jinyuan Li, Yi Chu, Yiwen Sun, Mengchuan Zou, Shaowei Cai."AutoPBO: LLM-powered Optimization for Local Search PBO Solvers."arXivpreprintarXiv:2509.04007 (2025).

2.Yiwen Sun, Furong Ye, Xianyin Zhang, Shiyu Huang, Bingzhen Zhang, Ke Wei, Shaowei Cai."Autosat: Automatically optimize sat solvers via large language models."arXivpreprintarXiv:2402.10705 (2024).

3.Yiwen Sun, Furong Ye, Zhihan Chen, Ke Wei, Shaowei Cai."Automatically discovering heuristics in a complex SAT solver with large language models."arXivpreprintarXiv:2507.22876 (2025).

4.Cunxi Yu, Rongjian Liang, Chia-Tung Ho, Haoxing Ren."Autonomous Code Evolution Meets NP-Completeness."arXivpreprintarXiv:2509.07367 (2025).

5.Hang Ding, Mao Luo, Chu-Min Li, Shunwei Li, Runyao Chen, Caiquan Xiong, & Xinyun Wu (2025). A Self-Optimizing Framework for SAT Solvers via Population Evolution and Large Language Model Collaboration. In Proceedings of SAT Competition 2025: Solver and Benchmark Descriptions (pp. 15–17).

6.Chuan Luo, Holger H. Hoos, Shaowei Cai: PbO-CCSAT: Boosting Local Search for Satisfiability Using Programming by Optimisation. PPSN (1) 2020: 373-389

運(yùn)營(yíng)/排版：何晨龍