1. 项目概述：当AI学会“左右互搏”来解数学题

最近在AI圈子里，“Agentic”（智能体化）和“Neurosymbolic”（神经符号）这两个词的热度是越来越高。简单来说，这代表了一种新的AI研究范式：不再是让一个单一的、庞大的模型去“蛮干”，而是让多个具备不同“思维模式”的智能体（Agent）协同工作，把神经网络的直觉感知能力和符号逻辑的严谨推理能力结合起来。这听起来有点像武侠小说里的“左右互搏”，让感性的右脑和理性的左脑一起上阵。而我们这个项目，就是把这个听起来很前沿的理念，实实在在地用到了一个非常经典的数学领域——组合设计（Combinatorial Design）上，并且用Lean 4这个形式化验证工具作为最终的“裁判”和“记录员”。

组合设计是什么？你可以把它想象成一种高级的“编排艺术”。比如，学校要组织一场循环赛，有7支队伍，要求每支队伍每天只打一场比赛，并且任何两支队伍在整个赛程中只相遇一次。怎么排这个赛程表？这就是一个典型的组合设计问题（具体来说是“斯坦纳三元系”问题）。这类问题在实验设计、编码理论、网络调度等领域有着极其重要的应用。传统上，解决这类问题要么靠数学家精巧的构造性证明，要么靠计算机进行穷举搜索，两者都有其局限性。

我们这个项目的核心目标，就是探索如何让大语言模型（LLM）驱动的智能体，模仿数学家“发现”和“验证”组合设计的过程。我们不是简单地让LLM去“猜”一个解，而是设计了一个多智能体协作框架：一个“直觉型”智能体负责提出大胆的猜想和构造思路（发挥神经网络的联想能力），一个“严谨型”智能体负责用逻辑规则去检验和修正这些猜想（发挥符号系统的推理能力），它们相互辩论、相互完善。最后，所有达成一致的、正确的推导步骤，都会被翻译成Lean 4的代码，形成一个可以被机器百分百验证的、无可争议的数学证明。

这不仅仅是解决了一个具体的数学问题，更是一次对AI如何实现真正“推理”和“发现”的方法论探索。它展示了如何将LLM的创造力引导到严谨的数学框架内，为未来AI辅助数学研究、甚至进行自主科学发现，提供了一个可复现的案例。接下来，我就把这个项目的设计思路、实现细节、踩过的坑以及背后的思考，毫无保留地分享给大家。

2. 核心架构设计：构建一个“辩论式”智能体协作系统

整个系统的设计灵感，来源于数学研究中的常见场景：灵感迸发（猜想）与严格验证（证明）的反复循环。我们摒弃了让单个LLM“既当运动员又当裁判”的做法，而是将其拆解为两个角色分明、能力互补的智能体。

2.1 双智能体角色定义与分工

我们设计了两个核心智能体：猜想家（Conjecturer）和检验者（Verifier）。它们的职责和“性格”截然不同。

猜想家智能体由一个大语言模型（例如GPT-4、Claude 3或开源的DeepSeek）驱动。它的核心任务是“发散思维”。

• 输入：当前要解决的组合设计问题的形式化描述（例如：“构造一个阶数为v=7的斯坦纳三元系S(2,3,7)”），以及当前已部分构建的结构或之前失败的尝试历史。
• 处理：它利用LLM在大量数学文本和代码上训练出的模式识别能力，进行类比联想。它可能会说：“这看起来很像一个有限射影平面的结构，也许我们可以从Fano平面（7个点的最小射影平面）入手，尝试将其解释为一个三元系。” 或者它会提出一个具体的构造算法：“尝试用模运算的方法，以模7的剩余类为基础，生成所有形如{i, i+1, i+3}的三元组。”
• 输出：一个具体的、用自然语言或类伪代码描述的构造猜想，以及一段解释其为何可能可行的“直觉性”论证。

检验者智能体则是一个神经符号混合体。它同样有一个LLM作为“解析器”，但背后连接着一个符号推理引擎（我们集成了一个简单的定理证明器，如Z3，或直接调用Lean的API进行小范围检查）。

• 输入：猜想家提出的构造猜想。
• 处理：
  1. 解析与形式化：其内部的LLM首先将猜想家的自然语言描述，翻译成精确的、无歧义的逻辑断言或数据结构定义。这是关键一步，任何模糊性都必须在这里被消除。
  2. 符号验证：将这些形式化的断言喂给符号推理引擎。引擎会检查该构造是否满足组合设计的所有公理（如：每对元素恰好同时出现在一个三元组中）。对于小型实例，它可能进行穷举检查；对于有参数的猜想，它可能尝试进行符号推导。
• 输出：一个明确的验证结果（“通过”、“失败”或“条件性通过”）。如果失败，必须提供反例或指出违反的公理。例如，检验者可能回复：“你提出的模7构造方案中，元素对(1, 4)同时出现在三元组{1,2,4}和{1,4,5}中，违反了‘每对元素恰好出现一次’的规则。”

这两个智能体被放置在一个迭代辩论循环中。猜想家提出想法，检验者挑刺。如果被驳回，检验者的反馈（反例）会成为猜想家下一轮思考的重要输入，驱动它修正猜想。这个过程循环往复，直到检验者给出“通过”的判决，或者循环次数达到上限。

2.2 Lean 4作为“终审法庭”与知识锚点

为什么选择Lean 4？因为它不是普通的编程语言，而是一个依赖类型的形式化证明语言。在Lean里，写一段代码就是构建一个证明，类型检查器就是最严格的法官。任何逻辑跳跃、未声明的假设都逃不过它的审查。

在我们的系统中，Lean 4扮演两个核心角色：

1. 最终验证器：当双智能体协作产出一个“通过”的构造方案后，我们需要生成一个Lean 4定理（theorem）及其证明（proof）。这个证明会详细描述该组合设计对象的构造过程，并证明它满足所有性质。Lean内核会对整个证明链进行终极验证，确保从基础公理到最终结论，每一步都滴水不漏。这相当于为AI的发现过程提供了一个数学上的“公证”。
2. 交互式反馈源：在智能体协作的中间阶段，我们也可以让Lean提供轻量级反馈。例如，猜想家生成一段Lean代码片段后，可以立即运行Lean检查是否有语法错误或简单的类型错误。这比等待完整的符号验证更快，能快速纠正低级错误，引导LLM写出更正确的形式化表述。

更重要的是，Lean及其庞大的数学库Mathlib，为我们的智能体提供了一个精确的、结构化的知识库。我们可以让智能体在提出猜想时，引用Mathlib中已有的定义和定理（如Finset,Setoid, 组合设计的基本定义design等），这极大地提升了猜想的质量和可验证性。它让AI的“思考”扎根于坚实的数学基础之上，而不是在模糊的自然语言概念中飘荡。

2.3 协作流程与通信协议

整个系统的运行流程是一个标准的多轮对话循环，但带有强烈的目标导向：

1. 初始化：用户输入一个组合设计问题P。系统初始化猜想家和检验者，并将P传递给猜想家。
2. 猜想生成轮：猜想家基于P（和历史对话）生成一个猜想C_i和解释E_i。
3. 检验轮：检验者接收C_i。其LLM解析器先将C_i形式化为F_i，然后符号引擎验证F_i。产生结果R_i（通过/失败+反馈Fb_i）。
4. 判决与迭代：
   • 若R_i为“通过”，流程进入证明生成阶段。
   • 若R_i为“失败”，系统将(C_i, R_i, Fb_i)追加到对话历史中，然后将该历史和原问题P一起，作为新的输入发送给猜想家，启动下一轮（回到步骤2）。提示词会强调：“你之前的猜想C_i因Fb_i被驳回。请分析这个反例，修正你的思路，提出一个新的猜想。”
5. 证明生成阶段：一旦猜想C_k被检验通过，一个专门的证明编写智能体（可由检验者或一个第三方智能体担任）被激活。它利用整个对话历史，特别是被验证通过的构造步骤，编写出完整的Lean 4证明代码。随后调用Lean进行编译验证。
6. 输出：最终输出两份成果：一份是人类可读的、包含迭代历史的发现过程叙述；一份是机器可验证的、纯净的Lean 4证明文件。

这个协议的关键在于，反馈Fb_i必须是具体、可操作的。模糊的“这不对”毫无帮助。“元素对(x, y)在多个块中出现”这样的反馈，才能引导LLM进行有针对性的修正。

3. 关键技术实现与工具链搭建

理论设计得再漂亮，落地时全是细节。这一部分，我带你看看我们具体是怎么搭起这个系统的，以及其中那些容易踩坑的地方。

3.1 LLM的选型与提示词工程

LLM是整个系统的“大脑”，其选择和质量直接决定了智能体的表现。

选型考量：

• 闭源 vs 开源：像GPT-4、Claude 3这样的闭源模型，在复杂推理和遵循指令方面表现卓越，是快速验证想法原型的利器。但考虑到成本、可控性和数据隐私，长期来看需要探索开源模型。我们试验了DeepSeek-Coder、CodeLlama和MathCoder等专门在代码和数学数据上微调过的模型。发现它们在代码生成上不错，但在深度的、多步的数学类比推理上，与顶级闭源模型仍有差距。
• 关键能力：对于猜想家，我们需要强大的类比推理和创造性思维能力。对于检验者中的解析器，我们需要极致的精确性和指令遵循能力，确保翻译无歧义。我们最终为猜想家选择了创造性更强的Claude 3，为检验者解析器选择了更严谨的GPT-4。

提示词设计是灵魂。绝不能简单地说“你是一个数学助手”。我们的提示词是高度结构化、包含角色、规则和示例的“剧本”。

猜想家提示词核心要素：

你是一位富有创造力的组合数学家。你的目标是为组合设计问题提出新颖的构造猜想。 问题：{problem_statement} 历史对话（最新在最前）： {history} --- 规则： 1. 你的输出必须是纯粹的猜想和解释，不要包含验证步骤。 2. 猜想应尽可能具体，可以是算法描述、数学公式或结构类比。 3. 如果历史中有反馈，你必须直接回应它，解释你如何根据反馈改进了猜想。 4. 优先考虑使用Mathlib中已有的概念（如Finset, Set, design）。 --- 示例（对于另一个问题）： 用户：构造一个4阶完全图K_4的边着色，使得任意两条相邻边颜色不同，且使用颜色最少。 助理（猜想家）：猜想：K_4的边可以用3种颜色着色。构造方法：将四个顶点标号为0,1,2,3。对于边(i,j)，其颜色定义为 (i+j) mod 3。这是一种可能的循环着色方案。 --- 现在，请基于当前问题和历史，提出你的下一个猜想。

这个提示词明确了角色、任务，提供了上下文（历史），规定了输出格式，并给出了一个类似任务的示例（Few-shot Learning），极大地稳定了输出质量。

检验者解析器提示词核心要素：

你是一个严格的数学逻辑翻译器。你的任务是将自然语言描述的数学猜想，转化为精确的、可被符号引擎验证的断言。 猜想：{conjecture} --- 规则： 1. 输出必须是单一的、无嵌套的JSON对象。 2. JSON格式：{"objects": [对象1定义, 对象2定义...], "properties": [需要验证的性质1, 性质2...]} 3. 定义必须使用标准的集合论和逻辑符号（∈, ⊆, ∀, ∃, ∧, ∨, →）。 4. 所有涉及的对象（如集合、函数）必须显式声明其域和陪域。 --- 示例： 输入猜想：“集合{1,2,3}的所有2-子集构成的集合。” 输出：{"objects": ["Let A = {1, 2, 3}", "Let B = { {1,2}, {1,3}, {2,3} }"], "properties": ["B = { S | S ⊆ A ∧ |S| = 2 }"]} --- 现在，请翻译给定的猜想。

通过强制JSON输出和严格的形式化要求，我们最大限度地减少了LLM的“自由发挥”，得到了结构化的、可供下游符号引擎消费的数据。

3.2 符号推理引擎的轻量化集成

我们并不需要实现一个能证明一切的全能定理证明器。对于组合设计验证，很多情况下是检查一个有限结构是否满足若干条公理。这本质上是模型检测问题。

我们的策略是分层验证：

1. 轻量级快速检查（针对小型实例）：如果猜想描述的是一个具体的小型设计（比如v<15），我们直接用Python生成这个结构（如所有三元组的列表），然后编写简单的脚本检查公理。例如，检查“每对点恰好出现一次”，就计算所有点对的出现次数。这速度极快，能立刻给LLM反馈。
2. 中等规模或参数化检查：对于参数化的猜想（如“对所有形如v=6k+1的整数，存在…”），我们集成Z3或SymPy这样的约束求解器/符号计算库。我们将组合设计的公理编码为约束条件，然后让求解器去寻找一个解（验证存在性）或证明无解。虽然不能处理非常复杂的数学归纳，但对于许多组合构造，这已经非常强大。
3. 终极验证接口：对于所有通过前两步检查的猜想，其最终证明都会导向Lean。我们实现了一个简单的Lean服务器客户端。证明编写智能体生成的Lean代码，会通过这个客户端发送到本地运行的Lean服务进行批处理编译。lean --make MyProof.lean如果编译成功（返回0），则证明有效；如果失败，编译器的错误信息会作为反馈返回给智能体进行修正。

注意：直接让LLM生成大段Lean证明成功率很低。我们的策略是“分而治之”：先让智能体用自然语言写出证明大纲，然后将大纲分解成一个个独立的引理（Lemma），再为每个引理分别生成Lean证明。最后用have和calc等策略将它们组合起来。这大大降低了单次生成的难度。

3.3 迭代循环中的状态管理与反思机制

多轮对话中，状态管理至关重要。我们不能让LLM忘记过去。

我们维护的核心状态包括：

1. 完整对话历史：所有轮次的(猜想， 检验结果， 反馈)三元组。
2. 已验证的子目标：在探索过程中，可能先验证了某个构造满足部分性质（例如，所有块的大小正确）。这些已验证的子目标会被缓存，后续猜想可以在此基础上构建，避免重复验证。
3. 失败模式库：记录常见的失败原因（如“某对点出现次数>1”，“某个块大小不对”）。当新的失败出现时，系统可以提示LLM：“注意，这看起来是‘点对重复’类错误，请重点检查你构造的对称性。”

此外，我们引入了反思机制。在连续多次失败（如5次）后，系统不会直接进入下一轮，而是会触发一个“元认知”提示，要求猜想家智能体暂停提出新猜想，而是分析历史失败记录，总结规律，调整自己的问题解决策略。例如：

回顾你最近5次失败的猜想。它们被驳回的主要原因都集中在“点对重复”上。这表明你当前的构造方法可能缺乏某种整体对称性。请暂时停止提出具体猜想，而是思考：在组合设计理论中，有哪些常见的对称构造方法（如循环群作用、有限域上的运算）可以避免这种重复？请列出两到三种高阶策略，然后再应用其中一种策略来生成下一个具体猜想。

这种强制性的“停下来想一想”，能有效打破LLM在低效模式中的循环，引导它进行策略层面的提升，模仿了人类研究者遇到瓶颈时的思考方式。

4. 实战案例：构造S(2,3,7)斯坦纳三元系

光说不练假把式。让我们看一个完整的、简化的运行实例，目标是构造最小的非平凡斯坦纳三元系S(2,3,7)（即7个点，每3个点组成一个块，每对点恰好出现在一个块中，共有7个块）。

初始状态：

• 问题P: “构造一个斯坦纳三元系S(2,3,7)，即一个点集V，|V|=7，和一系列三元组（块）的集合B，满足∀v∈V, 包含v的块数相同，且∀{x,y}⊆V, 存在唯一b∈B使得{x,y}⊆b。”
• 历史: []（空）

第一轮：

• 猜想家（基于对有限射影平面的联想）：“猜想：这个三元系同构于Fano平面。构造：令点集V = {0,1,2,3,4,5,6}。块集合B为：{0,1,3}, {1,2,4}, {2,3,5}, {3,4,6}, {4,5,0}, {5,6,1}, {6,0,2}。这是一种模7的循环构造。”
• 检验者：
  • 解析器：将猜想形式化为：V = {0,...,6};B = [列表上述7个集合]; 待验证性质：1. B中每个集合大小为3。2. 任意两个不同点i, j，在B中恰好同时出现一次。
  • 符号引擎（快速Python脚本）：检查性质1通过。检查性质2时发现：点对(0,1)出现在块{0,1,3}中，但点对(0,1)没有出现在其他块？等等，检查发现(0,1)只出现了一次，很好。继续检查所有点对… 发现点对(0,2)出现在块{6,0,2}中，也只出现一次。… 检查所有21个点对，全部恰好出现一次。
  • 结果：通过。
• 系统判决：第一轮就通过了！进入证明生成阶段。

证明生成阶段：

• 证明编写智能体接收通过的构造和完整历史。
• 它生成Lean代码框架：

  import Mathlib.Combinatorics.Design open Finset -- 定义点集和块集 def points : Finset ℕ := {0, 1, 2, 3, 4, 5, 6} def blocks : Finset (Finset ℕ) := {{0,1,3}, {1,2,4}, {2,3,5}, {3,4,6}, {4,5,0}, {5,6,1}, {6,0,2}} -- 证明这是一个设计 theorem fano_is_steiner : Design points blocks 2 3 := by -- 需要证明两点： -- 1. 所有块的大小都是3 (trivial，由blocks定义可知) -- 2. 任意2-子集（点对）恰好被一个块包含 -- 我们可以通过穷举来证明，因为集合很小 apply Design.mk · intro b hb simp [blocks, Finset.mem_filter] at hb -- 这里需要证明b的势为3，实际上blocks中的每个集合显式是3个元素 -- 一种方法是直接decide所有情况 fin_cases hb <;> decide · intro p hp -- p是points的一个2-子集 have : p ⊆ points := hp.1 -- 穷举points的所有2-子集，检查每个是否在恰好一个块中 -- 由于对称性，可以简化证明，但这里为清晰起见，我们使用计算证明 simp [points] at hp -- 将p的具体值枚举出来，然后检查 fin_cases hp <;> -- 这会生成所有21种情况 simp [blocks, Design.incidence_set] -- 每个case后需要证明该点对只出现在一个特定的块中 -- 这里需要具体的证明脚本，略去细节...

• Lean验证：将上述代码（补充完整细节后）提交给Lean。Lean的类型检查器会逐行验证。decide和simp等策略可以自动处理有限的枚举情况。编译成功，定理fano_is_steiner被正式验证。

输出：

1. 发现过程叙述：“系统在第一轮即由猜想家智能体基于Fano平面的类比，成功提出了S(2,3,7)的一个模7循环构造。经检验者验证，该构造满足斯坦纳三元系的所有公理。”
2. 可验证证明：完整的Lean代码文件fano_steiner.lean。

这个案例虽然简单，但完整展示了从问题输入、智能体协作、验证到形式化证明生成的闭环。对于更复杂的设计，迭代轮数会显著增加，但框架是通用的。

5. 遇到的挑战、解决方案与未来展望

在实际构建和测试这个系统的过程中，我们遇到了不少预料之中和预料之外的困难。

5.1 主要挑战与应对策略

1. LLM的“幻觉”与不稳定性：这是最大的挑战。猜想家经常会提出看似合理、但完全错误的数学类比，或者检验者的解析器会错误地形式化一个正确的猜想。

   • 解决方案：
     • 强化提示词约束：如前所述，使用严格的输出格式（JSON）、角色扮演和少样本示例。
     • 验证前置：在猜想家输出后、正式提交检验前，增加一个“合理性自检”步骤。让同一个LLM（或另一个小模型）快速评估猜想是否明显违背已知数学常识（例如，提出一个v=6的S(2,3,6)，而众所周知这是不存在的）。这可以过滤掉一部分低级错误。
     • 多数投票与集成：对于关键步骤（如解析），让多个LLM实例（如GPT-4、Claude 3）同时进行，选择输出最一致或置信度最高的结果。

2. 符号验证的规模限制：穷举验证只适用于小型实例。对于参数化猜想或稍大点的实例，符号引擎（如Z3）可能面临状态爆炸，或者根本无法表达复杂的组合存在性命题。

   • 解决方案：
     • 分层抽象：不要求一次性验证完整构造。先验证构造方法的关键引理（例如，“按此规则生成的集合，其大小是3”）。验证通过后，再在Lean中以此引理为基础进行完整证明。
     • 与Lean深度集成：直接将验证任务转化为在Lean中证明一个更简单的辅助定理（lemma）。让Lean的自动化策略（auto,omega,linarith）或可调用的小型决策过程（decide）来完成验证。这样，验证本身也成了形式化证明的一部分。

3. 证明生成的巨大鸿沟：让LLM直接从自然语言猜想生成完整的、正确的Lean证明，难度极高。

   • 解决方案：采用“人类指导的交互式证明生成”。我们不完全自动化，而是让系统在生成证明大纲和关键步骤后，允许人类专家介入，提供一些高级的证明策略（tactic）提示，或者帮助分解子目标。系统记录这些交互，用于微调LLM或作为后续类似问题的参考。这更像是一个“AI辅助证明编写器”，而非全自动证明生成器。

5.2 性能优化与工程实践

• 缓存：对已验证过的子目标、常见的LLM响应进行缓存，避免重复计算和API调用，显著降低成本和时间。
• 异步与流式处理：将猜想生成、解析、验证等步骤设计为异步流水线。当猜想家在思考下一个猜想时，检验者可以并行验证上一个猜想，提升系统吞吐量。
• 成本控制：使用混合模型策略。轻量级的反思、总结任务使用便宜的小模型（如GPT-3.5）；关键性的猜想生成和解析使用能力强的大模型。精确记录每个任务的Token消耗，设置预算上限。

5.3 未来方向与扩展思考

这个案例只是一个起点。这套“Agentic Neurosymbolic Collaboration”的框架有巨大的扩展潜力：

1. 更复杂的数学领域：从组合设计扩展到图论、数论、多项式代数等领域。关键在于为这些领域构建丰富的、形式化的“背景知识库”（如扩展Mathlib的使用范围），并设计领域特定的提示词模板和验证策略。
2. 更多样化的智能体角色：除了猜想家和检验者，可以引入推广者（尝试将特定构造推广到更一般的情形）、反驳者（专门寻找反例或证明不可能性）、简化者（优化已有的复杂构造）等。形成一个更丰富的“研讨班”式多智能体系统。
3. 从验证到发现：目前系统主要解决“构造验证”问题。下一步是挑战“猜想提出”本身。例如，给定一个组合设计族，让智能体协作去发现其中未知的不变量、对称性，甚至提出新的、有趣的猜想供人类数学家研究。
4. 教育应用：这个系统可以作为一个交互式的“数学研究训练模拟器”。学生可以提出自己的构造思路，由检验者智能体指出逻辑漏洞，由猜想家智能体提供启发性的类比，从而在互动中深入学习数学证明的严谨性和创造性。

回过头看，这个项目的最大价值不在于它解决了某个特定的数学问题（S(2,3,7)的构造早已为人所知），而在于它成功地将前沿的AI智能体技术与严谨的数学形式化验证连接起来，搭建了一条从模糊的直觉灵感，到精确的逻辑验证，再到最终可存档、可复现的形式化证明的可行路径。它证明了，通过精心的架构设计，我们可以让大语言模型这种“统计关联大师”在符号逻辑的框架内有效地工作，发挥其创造力，同时用严格的规则来约束和引导它。

在实际操作中，最深的体会是：提示词工程和系统流程设计，其重要性不亚于模型本身。一个鲁棒的、能处理错误和反馈循环的流程，远比一个强大的但孤立的模型要有用得多。同时，永远不要指望AI一步到位。将大问题分解成小步骤，在每个步骤上设立清晰的、可验证的里程碑，让AI和符号工具各司其职，才是让这类复杂系统跑起来的关键。