Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience

📄 arXiv: 2607.14818v1 📥 PDF

作者: Ruben Martins

分类: cs.LO, cs.AI

发布日期: 2026-07-16

💡 一句话要点

利用LLMs从论文构建MaxSAT求解器的CoreForge经验

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: MaxSAT求解器 大型语言模型 自动化开发 算法优化 代码生成

📋 核心要点

  1. 现有的MaxSAT求解器通常依赖于手工编码，缺乏从研究论文自动生成求解器的有效方法。
  2. 本研究通过结合LLMs与论文讨论、代码实现和审计，提出了一种新的MaxSAT求解器构建流程。
  3. 实验结果显示，尽管性能低于最佳手工求解器，但在测试配置中未发现错误答案，表明LLMs的潜力。

📝 摘要（中文）

我们报告了CoreForge项目，该项目利用大型语言模型（LLMs）从研究论文构建无权MaxSAT求解器，而非从现有求解器代码库出发。该项目专注于基于不可满足性的MaxSAT算法，采用迭代工作流程，结合论文讨论、ChatGPT、通过Codex提示进行实现，以及反复的LLM辅助代码审计和修订。尽管代码库实现了多个算法和求解器组件，但我们的评估主要集中在结合核心引导优化、轻量级预处理、核心最小化、与整数线性优化后端集成以及新型核心序列前瞻方法的配置上。我们的经验表明，LLMs可以支持从论文实现求解器，但仍需外部验证、基准测试和人类指导。在我们的实验中，模糊测试和MaxSAT评估实例未在测试配置中发现错误答案，尽管性能仍低于最佳手工设计的MaxSAT求解器。我们总结了有效的做法、面临的困难以及未来LLM辅助求解器开发的经验教训。

🔬 方法详解

问题定义：本论文旨在解决如何从研究论文中自动构建MaxSAT求解器的问题。现有方法主要依赖手工编码，效率低下且难以快速迭代。

核心思路：论文提出了一种迭代工作流程，结合了LLMs的自然语言处理能力与代码生成能力，通过与研究论文的讨论和反馈，逐步实现求解器的构建。

技术框架：整体架构包括几个主要模块：首先是论文讨论阶段，利用ChatGPT进行理解和分析；其次是通过Codex生成代码；最后是进行代码审计和修订，确保实现的正确性和性能。

关键创新：最重要的技术创新在于将LLMs与传统求解器开发流程相结合，使得求解器的构建可以更快速和灵活，同时引入了新的核心序列前瞻方法。

关键设计：在参数设置上，采用了核心引导优化和轻量级预处理等技术细节，确保求解器在性能和效率上的平衡。

🖼️ 关键图片

fig_0
img_1
img_2

📊 实验亮点

实验结果表明，在模糊测试和MaxSAT评估实例中，未发现错误答案，尽管性能仍低于最佳手工设计的求解器。这表明LLMs在求解器开发中的应用潜力，尤其是在快速迭代和验证方面。

🎯 应用场景

该研究的潜在应用领域包括自动化求解器开发、算法优化和研究论文的快速实现。通过利用LLMs，研究人员可以更高效地将理论转化为实践，推动相关领域的进步。

📄 摘要（原文）

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.