Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery

📄 arXiv: 2604.21187v1 📥 PDF

作者: Benjamin Przybocki, John Mackey, Marijn J. H. Heule, Bernardo Subercaseaux

分类: math.CO, cs.AI

发布日期: 2026-04-23

💡 一句话要点

结合SAT求解器与LLM生成代码，发现双重饱和Ramsey图的无限族

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

关键词: Ramsey图 SAT求解 大型语言模型 形式化验证 自动推理 数学发现 图论

📋 核心要点

  1. Grinstead和Roberts提出的问题：是否存在双重饱和Ramsey-good图的无限族，长期未解决。
  2. 结合SAT求解器和LLM，自动生成代码来搜索和发现满足特定Ramsey性质的图，从而找到无限族。
  3. 利用LLM生成并形式化Lean中的正确性证明，验证了发现的图族的正确性，提升了数学发现的效率。

📝 摘要（中文）

Ramsey-good图是指既不包含大小为$s$的团，也不包含大小为$t$的独立集的图。本文研究了双重饱和Ramsey-good图，定义为这样一种Ramsey-good图：添加或删除任何边必然会产生一个$s$-团或一个$t$-独立集。我们提出了一种结合SAT求解器与定制LLM生成代码的方法来发现这种图的无限族，从而回答了Grinstead和Roberts在1982年提出的问题。此外，我们使用LLM来生成和形式化Lean中的正确性证明。这个案例研究突出了整合自动推理、大型语言模型和形式验证以加速数学发现的潜力。我们认为，这种工具驱动的工作流程将在实验数学中发挥越来越核心的作用。

🔬 方法详解

问题定义：论文旨在解决发现双重饱和Ramsey-good图的无限族的问题。现有的图论研究方法在寻找满足特定复杂约束的图时面临挑战，特别是当图的规模增大时，人工搜索和验证变得非常困难。Grinstead和Roberts提出的问题长期未解决，表明传统方法存在局限性。

核心思路：论文的核心思路是将自动推理（SAT求解）与大型语言模型（LLM）的代码生成能力相结合。SAT求解器用于在给定的约束条件下搜索可能的图结构，而LLM则用于生成定制的代码来验证这些图是否满足双重饱和Ramsey-good图的性质。这种结合利用了SAT求解器的精确性和LLM的灵活性。

技术框架：整体流程包括以下几个主要阶段：1) 使用SAT求解器生成候选图；2) 使用LLM生成代码，该代码能够验证候选图是否满足双重饱和Ramsey-good图的性质；3) 对验证通过的图进行分析，寻找模式，并尝试推广到无限族；4) 使用LLM生成Lean中的形式化证明，以验证图族的正确性。

关键创新：最重要的技术创新点在于将SAT求解器和LLM结合起来，形成一个自动化的数学发现流程。与传统的手工方法相比，该方法能够更高效地搜索和验证复杂的图结构。此外，使用LLM生成形式化证明进一步提高了结果的可靠性。

关键设计：论文中关键的设计包括：1) 定制化的LLM提示工程，以生成能够有效验证图性质的代码；2) 使用Lean进行形式化验证，确保结果的严格性；3) 迭代式的搜索和验证过程，不断优化搜索策略和验证方法。

📊 实验亮点

论文成功地发现了双重饱和Ramsey-good图的无限族，解决了Grinstead和Roberts在1982年提出的问题。通过结合SAT求解器和LLM，实现了高效的图搜索和验证。此外，使用LLM生成Lean中的形式化证明，进一步验证了结果的正确性，展示了自动化数学发现的潜力。

🎯 应用场景

该研究成果可应用于组合数学、图论等领域，为发现新的数学结构和定理提供了一种新的工具和方法。此外，该方法在程序验证、软件测试等领域也具有潜在的应用价值，可以用于自动生成测试用例和验证程序性质。未来，这种结合自动推理、LLM和形式验证的工具驱动工作流程有望在更多科学发现领域发挥重要作用。

📄 摘要（原文）

Ramsey-good graphs are graphs that contain neither a clique of size $s$ nor an independent set of size $t$. We study doubly saturated Ramsey-good graphs, defined as Ramsey-good graphs in which the addition or removal of any edge necessarily creates an $s$-clique or a $t$-independent set. We present a method combining SAT solving with bespoke LLM-generated code to discover infinite families of such graphs, answering a question of Grinstead and Roberts from 1982. In addition, we use LLMs to generate and formalize correctness proofs in Lean. This case study highlights the potential of integrating automated reasoning, large language models, and formal verification to accelerate mathematical discovery. We argue that such tool-driven workflows will play an increasingly central role in experimental mathematics.