发表机构
Carnegie Mellon University（卡内基梅隆大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究利用大语言模型从论文构建无权重 MaxSAT 求解器，采用结合论文讨论、代码实现及审核修订的迭代流程，评估特定配置，发现虽未现错误答案，但性能低于手工设计求解器，总结了相关经验教训。
AI 中文摘要
我们报告了 CoreForge，这是一项利用大语言模型（LLMs）从研究论文而非现有求解器代码库构建无权重最大可满足性（MaxSAT）求解器的经验。该项目聚焦于基于不可满足性的 MaxSAT 算法，遵循迭代工作流程，将与 ChatGPT 的论文讨论、通过 Codex 提示进行实现以及重复的大语言模型辅助代码审核和修订相结合。虽然代码库实现了多种算法和求解器组件，但我们的评估集中在结合核心引导优化、轻量级预处理、核心最小化、与整数线性优化后端集成以及新的核心序列前瞻方法的配置上。我们的经验表明，大语言模型可支持从论文实现求解器，但需要外部验证、基准测试和人工指导。在我们的实验中，模糊测试和 MaxSAT 评估实例在测试配置中未发现错误答案，不过性能仍低于最佳手工设计的 MaxSAT 求解器。我们总结了哪些可行、哪些仍有困难以及对未来大语言模型辅助求解器开发的经验教训。
英文摘要
We report on CoreForge, an experience in using large language models (LLMs) to build an unweighted MaxSAT solver from research papers rather than from an existing solver codebase. The project focuses on unsatisfiability-based MaxSAT algorithms and follows an iterative workflow that combines paper discussions with ChatGPT, implementation through Codex prompts, and repeated LLM-assisted code audits and revisions. Although the codebase implements several algorithms and solver components, our evaluation focuses on configurations that combine core-guided optimization, lightweight preprocessing, core minimization, integration with integer linear optimization backends, and a new core-sequence lookahead approach. Our experience suggests that LLMs can support solver implementation from papers, while requiring external validation, benchmarking, and human guidance. In our experiments, fuzzing and MaxSAT Evaluation instances did not reveal wrong answers in the tested configurations, although performance remains below the best hand-engineered MaxSAT solvers. We summarize what worked, what remained difficult, and the lessons for future LLM-assisted solver development.
