在这篇文章中，我们介绍了CoreForge项目，探索了如何利用大型语言模型（LLMs）从研究论文中构建一个无权重MaxSAT求解器，而非依赖现有的求解器代码库。该项目专注于基于不可满足性的MaxSAT算法，并采用一种迭代工作流程，结合了与ChatGPT的论文讨论、通过Codex提示的实现，以及反复进行的LLM辅助代码审计和修订。
尽管代码库实现了多个算法和求解器组件，但我们的评估集中在结合核心引导优化、轻量级预处理、核心最小化、与整数线性优化后端的集成以及一种新的核心序列前瞻方法的配置上。我们的经验表明，LLMs可以支持从论文中实施求解器，但仍需外部验证、基准测试和人类指导。在我们的实验中，模糊测试和MaxSAT评估实例未在测试配置中发现错误答案，尽管性能仍低于最佳手工设计的MaxSAT求解器。
我们总结了有效的方法、仍然存在的困难以及对未来LLM辅助求解器开发的经验教训。
博主点评： CoreForge项目展示了LLMs在求解器开发中的潜力，尽管仍需人类的参与和验证，但其在自动化实现中的应用前景令人期待。未来的研究可以进一步提升LLM的性能，缩短与人类工程师之间的差距。