用大模型从论文复现最大可满足性求解器，效果接近手工优化但需人工把关。
Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience
- 通过论文解析+大模型生成代码，迭代实现核心引导优化等算法
- 在模糊测试和评测集上未发现错误结果，但性能仍低于顶尖手写求解器
- 适合想快速原型化求解器或学习算法的开发者，不推荐直接部署
我们报告了CoreForge项目的经验：使用大语言模型（LLMs）从研究论文而非现有代码库构建一个无权重最大可满足性（MaxSAT）求解器。项目聚焦于基于不可满足性的MaxSAT算法，采用结合论文讨论、ChatGPT交互、Codex代码生成及多次大模型辅助代码审查的迭代流程。尽管代码库实现了多个算法与组件，评估重点在于融合核心引导优化、轻量级预处理、核心最小化、与整数线性优化后端集成，以及一种新的核心序列前瞻方法。实验表明，大模型可支持从论文实现求解器，但需外部验证、基准测试与人工指导。在模糊测试和MaxSAT评估实例中，测试配置未出现错误答案，但性能仍低于最优手工设计的MaxSAT求解器。我们总结了可行方案、现存挑战及未来大模型辅助求解器开发的教训。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。