Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience
该论文报告了 CoreForge，这是一项旨在证明大型语言模型能够通过迭代工作流，直接根据研究论文成功协助构建功能性无权值 MaxSAT 求解器的实验，尽管所生成的系统仍需要人类的指导与验证，且在性能上落后于手工设计的求解器。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下你是一名正在试图解开一个巨大的、纠缠不清的线索结的侦探。在计算机科学的世界里，这个结被称为“约束问题”（constraint problem）。你有一份规则清单（比如“红球必须在左边”或者“蓝球不能紧挨着绿球”），而你的任务是找到一种排列方式，让每一条规则都感到满意。有时，要让所有人同时满意是不可能的，因此目标转变为寻找一个能让“最多人”满意的排列方案。这就是“MaxSAT 求解器”（MaxSAT solver）的工作——它是一个超级聪明的计算机程序，充当着顶级解谜大师的角色，在无法找到完美解时，寻找出最优的解。
几十年来，构建这些解谜工具一直是人类专家的工作。他们必须阅读复杂的科研论文，理解深奥的数学理论，并花费数年时间编写数百万行代码，不断微调那些极其细微的细节，以使求解器足够快，从而具备实用价值。但最近，一种新型的数字助手来到了：大语言模型（LLMs）。这些是像 ChatGPT 这样能够写故事、写诗甚至编写计算机代码的 AI 大脑。一个关键的问题是：AI 能否读懂一篇研究论文，并从零开始构建一个可以运行的解谜求解器，而无需人类编写哪怕一行代码？这正是“CoreForge”项目旨在解决的谜团。
CoreForge 实验：教 AI 构建解谜求解器
在一个名为 CoreForge 的项目中，来自卡内基梅隆大学的研究员 Ruben Martins 决定测试 AI 的极限。他并没有要求 AI 去修复一个已经存在的、有缺陷的解谜求解器，而是挑战它利用研究论文作为其唯一的说明手册，从零开始构建一个求解器。这就像是递给机器人一叠由名厨编写的食谱，并要求它在从未见过炉灶的情况下，建造一个餐厅厨房并烹饪出一顿五星级大餐。
这个过程并非 AI 直接吐出完美程序的“一蹴而成”的魔术。相反，它是人类与机器之间一场漫长的、迭代式的舞蹈。人类研究员会挑选一篇研究论文，与 AI 讨论核心思想，然后要求 AI（具体使用的是一种名为 Codex 的编程工具）编写代码。但 AI 并未获得免责权。人类随后会进行测试、检查漏洞，并要求 AI 修复其错误。他们不断重复这个循环，就像学生和导师一起攻克一道难题一样，直到拥有一个可以工作的求解器。
他们构建了什么？
结果是一个包含超过 25,000 行 C++ 代码的庞大代码库。AI 成功地将论文中复杂的数学思想转化为了可运行的软件。它实现了几种先进的策略，包括：
- 核心引导优化（Core-guided optimization）： 一种求解器通过从错误（称为“核心/cores”）中学习，以避免重复犯错的方法。
- 预处理（Preprocessing）： 在尝试解决谜题之前先对其进行清理，使其变得更容易解决。
- 前瞻（Lookahead）： 一个由 AI 协助发明的全新功能，求解器可以通过进行几次快速的“模拟演练”来预测最佳策略，然后再投入到真正的解决方案中。
成功了吗？
故事中最令人惊讶的部分是，AI 并没有作弊。研究人员进行了数千次测试，包括“模糊测试”（fuzzing，即向求解器投喂随机、混乱的数据以观察其是否崩溃）以及与官方竞赛基准进行对比。他们发现，在测试的配置中，错误答案的数量为零。该求解器在数学上是正确的。它不仅仅是在猜测，而是真正正确地解决了谜题。
但它够快吗？
这里有一个陷阱。虽然 AI 构建了一个正确的求解器，但它并不是最快的一个。与经过多年精雕细琢的人类工程求解器相比，CoreForge 速度较慢，且能解决的谜题较少。这就像 AI 造出了一辆行驶完美且绝不会出车祸的车，但它的时速只有 40 英里，而最好的真人制造的赛车时速可以达到 120 英里。
研究人员发现，AI 非常擅长理解高层级的思想并将其转化为代码。然而，它在“微调”细节方面表现挣扎——即那些让求解器变得极速的、细微且激进的优化。AI 有时还会增加一些多余的步骤，导致速度变慢，就像是在本该走直线的时候绕了远路。
结论
CoreForge 的经验表明，AI 确实可以帮助根据研究论文构建复杂的软件，但它还没有准备好取代人类工程师。AI 需要人类的引导来检查其工作、决定保留哪些想法，并帮助它避免陷入缓慢的循环。
该论文总结道，虽然我们尚未达到能够自主构建世界级求解器的程度，但我们正在接近。AI 证明了它能够读懂“食谱”并搭建起“厨房”。下一步是教会它如何成为一名名厨，知道如何精准地调节火力与时机，从而赢得比赛。目前，最好的结果来自于团队协作：由人类提供策略，而 AI 负责完成编写代码的繁重工作。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。