SATLUTION：AI自主进化复杂代码库，攻克SAT难题超越人类冠军

人工智能是否正开启复杂软件开发的新纪元？

近年来，以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年基准测试集的性能追踪图表显示，在最初的5-10个迭代周期中，系统取得了快速进展，这主要是因为它整合了多个初始种子求解器的互补优势。

随后，性能提升的速度有所放缓，但仍在持续进行，表明智能体开始处理更细微和复杂的优化问题。

大约在第50次迭代时，SATLUTION进化出的求解器在2024年的基准上已经开始优于2025年的人类设计冠军。

到第70次迭代结束时，其性能已稳定地超越了所有用于比较的基准求解器。整个过程表现出高度的稳定性，由于验证保障措施的存在，没有发生过严重的性能衰退。

SATLUTION自主进化性能曲线，展示其持续优化的过程。

整个SATLUTION自我进化实验过程的总计成本低于20000美元。相比之下，由人类专家开发一个具有竞争力的SAT求解器通常需要数月乃至数年的持续工程投入，而SATLUTION在数周内便取得了超越顶尖人类水平的成果。

更多技术细节和数据分析请参见原论文。