华为联合团队夺SAT 2026大赛AI赛道冠军

近期，约束求解与形式化领域国际顶级赛事 SAT Competition 2026 落幕。由华为诺亚方舟实验室、华为云天筹 AI 求解器团队和华中科技大学 John Hopcroft 计算中心组成的联合团队，获得并行 AI 赛道 SAT 组冠军。

SAT 问题被誉为计算复杂性理论中的“珠穆朗玛峰”，从硬件验证、软件测试到密码学分析与 AI 规划，SAT 求解器已成为自动驾驶、EDA 芯片设计等产业研发中不可或缺的核心引擎。SAT Competition 由 SAT Conference 组织，至今已有二十多年历史，以开源、严谨、可复现的评测体系著称，汇聚全球顶尖科研机构与企业团队同台竞技，获奖求解器往往成为学界与工业界标准工具，被国际顶级公司直接采用投入生产环境，冠军含金量远超顶会论文。

2026 年赛事共吸引全球 45 支顶尖队伍参赛，并首次设立 AI 赛道，要求 AI 调优的求解器必须在性能上超越最优非 AI 求解器方可获奖，这意味着 AI 不能仅作为辅助优化，而必须带来真实、可量化、可验证的算法性能提升，标志着 SAT 竞赛从人工算法设计迈入“经典算法 + AI 融合创新”的新阶段。

此次夺冠依托华为云天筹决策智能引擎和 AI 算法自动设计技术，搭建了 SAT 求解器专用的算法自调优流水线，集成了专家知识注入、多智能体协同、经验高效沉淀、多维度多尺度算法评估等核心能力，依托分布式算力集群实现高速算法评测打分，打通全代码仓自动化算法设计链路。这意味着 AI 已不再仅是参数推荐或辅助开发工具，而是深入参与求解器的算法生成、代码演化、性能评测与策略优化全过程，针对各类全新未见数据集，均可实现稳定、可复现的求解性能提升。支撑这次夺冠的算法自动设计能力，使用了华为和城大张青富教授团队联合开发的开源算法设计平台 LLM4AD_Next。该平台融合算法自动设计方向最新成果，覆盖自动算法构建、独立记忆管理、Skill 轻量化部署和自动科研平台等核心能力。

自动算法构建方面，平台依托大模型驱动算法自主探索，通过自然语言输入，可完成算法构思、代码生成、迭代筛选与效果评估，无需依赖人工编写完整算法逻辑。系统结合进化式搜索，不断生成候选方案，自动淘汰无效版本。本次 SAT 竞赛中，这套能力用于 SAT 求解器策略的自动演化，挖掘出超越人工调优的求解方案。

独立记忆管理方面，平台搭载华为诺亚自研的记忆管理平台“MindMemOS”，能够留存任务灵感、项目场景先验以及跨任务通用算法范式，沉淀试错过程中的成功经验与失败教训，避免重复踩坑，让算法设计从“单次搜索”走向“持续积累”。例如在 SAT 求解器迭代过程中，系统记录不同实例集上调优策略的优劣，后续遇到同类问题可直接复用历史经验，减少重复评测开销。

Skill 轻量化部署方面，平台将经过验证的算子、算法模块封装为可复用技能单元，后续任务可直接调用、重组组件，不必每轮从零构建全部代码。随着项目持续迭代，技能库不断沉淀扩充，大模型可基于已有组件做组合创新与二次优化，有效降低算法生成复杂度，缩短开发周期，提升新任务下算法输出的质量与稳定性。目前已支持 10 类自动算法设计方法的 Skill 化部署。

自动科研平台方面，平台打通了从问题定义、算法搜索、基准对比、结果归纳和论文撰写的完整科研链路。该能力基于开源自主科研智能体 AutoResearchClaw 的 23 阶段端到端科研流水线，并针对其在算法设计上的短板做了改进：将 LLM4AD_Next 集成到 AutoResearchClaw，在代码定稿前，先让 LLM4AD_Next 尝试改进核心算法，再用原实验评测方法逐一验证。只有成绩确实更好的版本才会替换原算法，没有变好就保持原样。

该平台面向高校学生、科研人员及广大算法开发者，让更多人能借助这套“让算法自我演化”的工具，更好、更快、更容易地把想法变成可验证的结果。目前该平台已开源开放，可通过链接在线体验和下载尝试。

在线体验: https://llm4ad-next.cn

GitHub 链接: https://github.com/Optima-CityU/LLM4AD_Next

文章来自于微信公众号 “机器之心”，作者 “机器之心”