[LG]《Autonomous Code Evolution Meets NP-Completeness》C Yu, R Liang, C Ho, H Ren [NVIDIA Research] (2025)
SATLUTION：首个基于大型语言模型（LLM）的布尔可满足性问题（SAT）求解器仓库级自主进化框架，实现NP完备问题领域的突破。
• 规模空前：可同时演化包含数百个文件、数万行C/C++代码的完整求解器仓库，超越以往仅限单文件百行代码的AlphaEvolve。
• 双阶段智能代理：规划代理负责高层策略思考，编码代理执行具体代码改动，结合静态规则与自我进化规则保障代码正确性与性能提升。
• 严格正确性验证：两阶段验证体系（编译+烟雾测试，SAT/UNSAT结果及DRAT证明校验）确保无误导性优化，避免退化和错误结果。
• 分布式大规模评测：800核CPU集群并行运行400实例测试，实时反馈PAR-2（惩罚平均运行时间）等多维性能指标，指导迭代优化。
• 超越人类专家：仅基于2024年赛题和5个开源求解器为种子，经过70次迭代演化，产出性能超越2025年SAT竞赛冠军的求解器，表现稳定优异。
• 规则与自我进化：结合领域知识与自动规则更新机制，构建可随着迭代持续学习和完善的规则系统，保障演化效率和质量。
• 代码与文档规范化：强制统一仓库结构及文档（CHANGELOG.md、HYPOTHESIS.md、RESULTS.md），实现演化过程全透明、可追溯。
• 资源节约显著：耗费不足2,000美元令牌费用加9,000-13,500美元计算资源，远低于人工开发数月成本。
心得：
1. 从单文件到仓库级的自主演化，是复杂系统自动优化的里程碑，证明LLM结合规则和反馈能驾驭大规模软件工程任务。
2. 严格的验证管控是自动代码演化的根基，防止错误传播、加快迭代速度，是AI自动编程成功的关键。
3. 多维性能反馈（如SAT/UNSAT分解、不同时间阈值分布）促进了更全面且平衡的优化，避免单目标陷阱。
了解详情🔗 arxiv.org/abs/2509.07367
人工智能自动编程算法优化SAT求解器大规模软件演化NP完全
