1. 项目缘起：当大语言模型遇上形式化证明

最近在折腾一个挺有意思的玩意儿，我把它叫做 DAP（Deductive Assistant with LLM Proof），一个基于大语言模型（LLM）的自动定理证明辅助系统。这想法不是凭空来的，而是源于我日常工作中一个非常具体的痛点：处理形式化验证和数学证明。

无论是做硬件设计的正确性验证，还是写一些需要严格逻辑保证的软件，形式化证明都是绕不开的一环。但说实话，写证明、找引理、构造中间步骤，这个过程极其繁琐且容易出错。传统的自动定理证明器（ATP），比如 Coq、Isabelle/HOL、Lean，功能强大，但学习曲线陡峭，交互方式也偏向于命令式，你得非常精确地告诉它每一步该做什么。很多时候，我脑子里有个模糊的证明方向，但就是卡在如何把它转化成机器能理解的一系列精确指令上。

与此同时，以 ChatGPT、GPT-4 为代表的大语言模型在代码生成、逻辑推理和自然语言理解上展现出了惊人的能力。它们能理解模糊的意图，生成连贯的文本，甚至能进行一定程度的逻辑推演。一个很自然的想法就冒出来了：能不能让大语言模型来当这个“翻译官”和“灵感助手”，把我用自然语言描述的证明思路，转化成形式化证明器能执行的脚本？或者更进一步，让它直接参与到证明的搜索和构造过程中？

这就是 DAP 框架设计的初衷。它不是要取代 Coq、Lean 这些成熟的证明引擎，而是想作为一层“智能胶水”和“协同推理引擎”，降低形式化验证的门槛，提升证明探索的效率。简单说，就是让机器更懂“人话”，让人能更聚焦于高层的策略和创意，把繁琐的、模式化的步骤交给 AI 去尝试和填充。

2. DAP 系统架构设计：三层协同工作流

DAP 的整体架构设计遵循“协同”与“引导”的原则，核心目标是将 LLM 的创造性、模糊推理能力与 ATP 的精确性、可靠性结合起来。整个系统可以划分为三个核心层次：自然语言交互层、策略规划与代码生成层、以及定理证明执行与验证层。这三层并非严格线性，而是一个存在反馈循环的协同工作流。

2.1 自然语言交互与意图理解层

这是用户与系统交互的入口。用户可以用相对自由的自然语言描述一个待证明的命题、一个证明目标，或者提出一个证明策略（比如“用数学归纳法证明”、“尝试反证法”）。这一层的核心挑战是如何从用户的自然语言输入中，精准提取出形式化系统所需的“结构化意图”。

实现要点：

  1. 提示工程与上下文管理 ：我们设计了一套结构化的系统提示词（System Prompt），明确告诉 LLM（例如调用 OpenAI GPT-4 API 或本地部署的 Llama 3 70B 等模型）它的角色是一个“定理证明助手”，并且熟悉目标后端证明器（如 Lean 4）的语法和常用库。提示词中会包含当前证明环境的上下文，如已定义的变量、引入的假设、当前需要证明的目标等。
  2. 意图分类与参数提取 ：用户的输入可能多种多样：“证明对于所有自然数 n，n*(n+1) 是偶数”、“应用 rewrite 规则简化左边”、“搜索关于‘素数’的引理”。系统需要先对输入意图进行分类。例如：
    • 直接证明请求 ：提取命题的逻辑结构。
    • 策略执行请求 ：识别策略名称（ induction , cases , apply ）及其参数。
    • 信息查询请求 ：识别查询实体（定理名、定义名）。 这可以通过在提示词中明确指令，或训练一个轻量级的意图分类器来实现。
  3. 对话历史维护 ：证明是一个多轮对话过程。系统需要维护一个精简但有效的对话历史，确保 LLM 能理解当前证明进行到了哪一步，避免出现“时空错乱”的回复。我们通常只保留最近几轮的“用户请求-LLM建议-证明器反馈”三元组。

注意 ：这一层完全依赖 LLM，其输出可能存在幻觉或不精确。因此， 绝不能 将 LLM 的输出直接视为可信的证明步骤，它只是一个“建议”，必须交由下一层验证。

2.2 策略规划与形式化代码生成层

这是 DAP 的“大脑”。它接收来自上一层的结构化意图，并负责生成具体的、可供后端证明器执行的形式化代码（如 Lean 的 tactic 脚本、Isabelle 的 Isar 命令等）。这一层的工作可以进一步细分为全局策略规划和局部代码生成。

全局策略规划 ：对于复杂的定理，LLM 可以扮演“策略师”的角色。例如，当用户提出“证明勾股定理”时，LLM 不会直接生成所有细节代码（那几乎必然出错），而是先输出一个证明大纲：

1.  考虑任意直角三角形ABC，其中角C为直角。
2.  以AB为边向外作正方形ABDE。
3.  通过面积法，证明正方形ABDE的面积等于两个小正方形面积之和。
4.  将面积关系转化为边长关系，即得 a² + b² = c²。

这个大纲本身是自然语言的，但它为后续的逐步形式化提供了清晰的路线图。

局部代码生成 ：这是更常用、也更核心的模式。系统将当前证明状态（一个“目标”，通常包含假设列表和结论）作为输入，结合用户的指令（如“尝试使用反证法”），要求 LLM 生成下一步可能的一个或几个 tactic。

  • 输入 ：格式化的当前目标 (h1 : P) (h2 : Q) ⊢ R ，以及可选的自然语言指令。
  • LLM 任务 ：生成如 apply h1 at h2 或 have h3 : S := by ... 这样的 Lean tactic。
  • 关键设计 ：我们采用 “少量多餐” 的策略。即每次只让 LLM 生成一小步（1-3个tactic），然后立即交给证明器执行。这大大降低了单次生成的复杂度，也便于及时纠错。

代码示例（Lean 4 环境） ： 假设当前证明状态是：

h : n > 0
⊢ n + 1 > 1

用户说：“用 linarith 试试看”。系统会将此指令和状态传给 LLM。LLM 可能生成：

  linarith

执行后，如果目标解决，则进入下一步；如果失败，错误信息会反馈给 LLM 用于调整。

2.3 定理证明执行、验证与反馈层

这是系统的“安全阀”和“裁判”。它由传统的定理证明器（ATP）担任，如 Lean Server、Coq 的 coqtop 。它的职责非常明确：

  1. 执行与验证 ：接收上一层生成的代码片段，在当前的证明上下文中执行。如果代码语法正确且逻辑上推进了证明（或完成了证明），证明器会返回新的证明状态。
  2. 错误反馈 ：如果代码有误（类型错误、找不到定理、逻辑错误），证明器会返回详细的错误信息。 这是黄金般的反馈信号 。
  3. 状态同步 ：将执行后的新证明状态（无论是成功推进还是错误）同步回给系统，作为下一轮交互的上下文。

反馈循环的建立 ：这是 DAP 能否“学习”和“改进”的关键。当 LLM 的建议导致错误时，系统不是简单地抛弃这个建议，而是将 “生成的代码 + 证明器返回的错误信息” 作为一个新的提示，再次发送给 LLM，要求它分析错误并给出修正后的建议。这个过程可以迭代几次。例如：

  • 第一轮 ：LLM 生成 rewrite [add_comm] at h ，但证明器报错“ add_comm 的类型不匹配”。
  • 第二轮 ：系统提示：“你刚才的建议 rewrite [add_comm] at h 出错了，错误是： tactic 'rewrite' failed, lemma is not an equality nor a iff 。当前目标是 ... 。请分析错误并给出新的建议。”
  • 第二轮 LLM ：可能回复“抱歉， add_comm 是 a+b = b+a ，但 h 不是一个等式。或许应该用 have 引入一个新等式，或者尝试别的引理如 add_pos_iff 。”

通过这种“尝试-错误-修正”的循环，LLM 能够更深入地理解特定证明环境的约束和细节，从而生成质量更高的代码。这也模拟了人类在交互式证明中不断试错的过程。

3. 核心实现技术栈与模块拆解

要把上述架构落地，需要精心选型和实现各个模块。下面我以基于 Lean 4 作为后端证明器， Python 作为胶水层， OpenAI API 或 本地 LLM 作为推理引擎的技术栈为例，拆解关键实现。

3.1 后端证明器接口模块

这是与 Lean 4 交互的桥梁。Lean 4 提供了 LSP (Language Server Protocol) 支持，这是我们与之通信的最佳方式。

  1. 启动与管理 ：使用 subprocess 模块启动 lean --server 进程，并建立标准输入/输出的管道通信。
  2. LSP 消息封装 ：实现一个轻量级客户端，能封装和解析 JSON-RPC 格式的 LSP 消息。核心操作包括：
    • textDocument/didOpen ：打开或更新一个临时的 .lean 文件，内容为当前的证明状态和 LLM 生成的代码。
    • textDocument/didChange ：当用户或 LLM 修改内容时通知服务器。
    • textDocument/hover / textDocument/completion ：可用于实现 IDE 类似的提示功能，增强用户体验。
    • 最关键的是监听诊断信息 ：通过 textDocument/publishDiagnostics 事件，实时获取 Lean 服务器返回的错误、警告信息。这些信息是反馈循环的核心输入。
  3. 证明状态提取 ：Lean LSP 的 $/lean/plainGoal 请求可以获取当前焦点的目标（goal）的纯文本表示。我们需要定期或在关键步骤后获取这个状态，并将其格式化成给 LLM 的提示词的一部分。

踩坑记录 ：直接解析 Lean 的完整输出（非 LSP 模式）来获取目标状态非常脆弱，因为输出格式可能随版本变化。LSP 是稳定且结构化的接口，尽管初始设置稍复杂，但长期来看更可靠。另外，要注意处理 Lean 服务器的启动参数，确保它加载了正确的项目依赖（ lakefile.lean ）。

3.2 LLM 集成与提示工程模块

这是系统的智能核心。如何与 LLM 对话，决定了建议的质量。

  1. 模型选择与切换 ：
    • 云端 API（如 GPT-4） ：优点是最强，上下文长（128K），推理能力好。缺点是成本、延迟和网络依赖。适合研究和原型验证。
    • 本地大模型（如 Llama 3 70B, CodeLlama） ：优点是数据隐私性好，无网络延迟，可定制微调。缺点是对硬件要求高（需要大显存），推理速度慢于 API。适合对数据敏感或需要深度集成的生产环境。可以使用 vLLM , llama.cpp 等框架进行高效部署。
    • 小型化专业模型 ：未来方向是针对定理证明数据（如 Lean 的 Mathlib4）微调一个 7B 或 13B 参数的模型，在精度和效率间取得平衡。DAP 框架应设计为可插拔的模型接口。
  2. 提示词模板设计 ：这是艺术也是科学。我们的模板大致如下： 
    你是一个专业的 Lean 4 定理证明助手。你的任务是根据当前的证明目标和用户指令，生成下一步的 Lean tactic 代码。

### 当前证明环境
【这里插入从 Lean LSP 获取的当前目标，格式化为易读的文本】

### 可用定理（上下文相关）
【可选：从当前导入的模块中提取一些相关定理名，帮助 LLM 回忆】

### 用户指令
【用户最新的自然语言指令，例如：“尝试使用归纳法”】

### 历史交互（最近3轮）
【用户: ... 助手: ... (结果：成功/失败：错误信息)...】

### 你的任务
请只生成 **1到3行** 最有可能推进证明的 Lean 4 tactic 代码。不要解释，不要输出 markdown 代码块，直接输出代码。如果认为当前目标无法直接解决，可以输出 `sorry` 或建议一个中间引理（格式：`suggest_lemma: 引理描述`）。
  3. 上下文窗口管理 ：证明过程可能很长，不能把整个对话历史都塞进提示词。我们需要一个摘要或窗口机制。通常保留：初始定理陈述、最近 3-5 轮的交互（包括错误反馈）、以及当前目标。太早的成功步骤可以丢弃。

3.3 状态机与工作流引擎模块

这个模块负责协调所有组件，是 DAP 的“总控台”。它维护一个核心的 证明会话状态 ，并驱动状态迁移。

  1. 会话状态 ：包含以下信息：
    • current_file_content : 内存中虚拟的 .lean 文件内容。
    • proof_goals : 从 Lean LSP 获取的当前目标栈（可能多个目标）。
    • dialogue_history : 结构化的交互历史列表。
    • llm_client : 配置好的 LLM 客户端实例。
    • lean_server : 与 Lean LSP 进程的连接。
  2. 主工作流循环 ： 
    while not proof_finished:
    # 1. 获取用户输入（自然语言或直接tactic）
    user_input = get_user_input()
    
    # 2. 判断输入类型
    if is_natural_language(user_input):
        # 2a. 意图理解（可调用LLM或规则）
        intent = parse_intent(user_input, current_goals)
        # 2b. 构建提示词，调用LLM生成tactic建议
        prompt = build_prompt(current_goals, intent, dialogue_history)
        llm_suggestion = call_llm(prompt)
        # 2c. 清理LLM输出，提取纯tactic代码
        tactic_code = extract_tactic(llm_suggestion)
    else: # 用户直接输入了tactic代码
        tactic_code = user_input
    
    # 3. 执行与验证
    # 3a. 将tactic代码追加到虚拟文件
    append_to_virtual_file(tactic_code)
    # 3b. 通过LSP同步给Lean服务器，并请求诊断
    lean_server.sync()
    diagnostics = lean_server.get_diagnostics()
    new_goals = lean_server.get_goals()
    
    # 4. 处理结果
    if diagnostics.has_errors():
        # 错误处理：将错误信息加入历史，可选择自动重试或通知用户
        dialogue_history.append((tactic_code, "ERROR", diagnostics.error_msg))
        if auto_retry:
            # 进入“错误反馈循环”，用错误信息构建新提示词让LLM修正
            prompt = build_retry_prompt(tactic_code, diagnostics.error_msg, current_goals)
            # ... 回到步骤2b
        else:
            notify_user(f"执行错误: {diagnostics.error_msg}")
    else:
        # 执行成功
        dialogue_history.append((tactic_code, "SUCCESS", None))
        update_current_goals(new_goals)
        if not new_goals: # 目标栈为空，证明完成！
            proof_finished = True
            notify_user("证明完成！")
    
    # 5. 更新UI/显示新的证明状态
    refresh_ui(current_goals, dialogue_history)
  3. 错误恢复与策略 ：这是体验好坏的关键。除了上述的自动重试，还可以实现多种策略：
    • 回溯（Backtracking） ：如果 LLM 连续几次建议都失败，可以自动撤销（ undo ）最后几步，回到一个更早的、稳定的证明状态，然后尝试不同的分支。
    • 多建议投票（Beam Search） ：一次让 LLM 生成 3-5 个不同的 tactic 建议，依次尝试，直到有一个成功。这增加了单步成功的概率，但代价是更多的 API 调用/计算。
    • 人工干预点 ：在关键决策点或多次自动尝试失败后，主动暂停并提示用户做出选择。

3.4 前端用户界面模块

为了提供良好的交互体验，一个图形化或增强的文本界面是必要的。有两种主要方向：

  1. IDE 插件 ：为 VS Code 或 JetBrains IDE 开发插件。这样可以复用 IDE 强大的编辑器和 Lean 官方 LSP 客户端的支持。插件的核心是嵌入我们上述的 Python 服务，并提供一个聊天面板或侧边栏，用于自然语言输入和显示交互历史。优势是集成度高，能与现有 Lean 开发环境无缝融合。
  2. 独立的 Web 应用 ：使用如 Streamlit、Gradio 或自定义 Web 前端。后端运行 Python 的 DAP 核心服务，前端通过 WebSocket 或 HTTP 与后端通信。这样可以提供更定制化的界面，例如并排显示自然语言对话、生成的代码、实时更新的证明状态和可视化证明树。优势是部署灵活，无需依赖特定 IDE。

界面核心元素 ：

  • 目标显示区 ：实时展示从 Lean 获取的当前目标，高亮假设和结论。
  • 交互输入区 ：支持自然语言输入和直接 tactic 代码输入。
  • 对话历史区 ：按时间线展示“用户指令 -> LLM 建议的代码 -> 执行结果（成功/失败+错误）”。
  • 证明脚本区 ：展示累积生成的、已成功的完整 Lean 代码，用户可以随时编辑。
  • 工具箱 ：提供一些快捷按钮，如“常用策略”（induction, rewrite, apply）、“撤销”、“重试”、“格式化目标”等。

4. 实战演练：用 DAP 证明一个简单命题

让我们通过一个具体的例子，看看 DAP 如何辅助完成一个证明。我们要在 Lean 4 中证明： ∀ (n : ℕ), 0 ≤ n 。这是一个非常简单的命题，但足以演示完整流程。

初始状态 ： 用户打开 DAP，创建一个新项目。系统后台启动 Lean LSP 服务。用户在界面中输入定理陈述：

example (n : ℕ) : 0 ≤ n := by
  -- 光标停在这里，目标状态为 `n : ℕ ⊢ 0 ≤ n`

第一轮交互 ：

  • 用户输入（自然语言） ：“这个怎么证？感觉很明显但不知道用哪个引理。”
  • DAP 内部流程 ：
    1. 状态机获取当前目标： n : ℕ ⊢ 0 ≤ n 。
    2. 构建提示词（包含目标、用户问题、空历史）。
    3. 调用 LLM（例如 GPT-4）。
    4. LLM 可能生成： exact Nat.zero_le n 。
  • 执行与验证 ：
    1. 系统将 exact Nat.zero_le n 插入到证明脚本中。
    2. 通过 LSP 同步给 Lean。
    3. Lean 检查通过，目标解决，返回空目标栈。
  • 界面反馈 ：对话历史显示“用户：这个怎么证？ -> 助手建议： exact Nat.zero_le n -> 结果：成功”。证明脚本区更新为完整代码。界面显示“证明完成！”。

一个更复杂的、需要多轮交互的例子 ：证明 ∀ (a b : ℕ), a + b = b + a （加法交换律）。虽然 Mathlib4 中已有 add_comm ，但我们假装不知道，让 DAP 引导我们。

  1. 用户输入 ：“证明加法交换律，用归纳法。”
  2. DAP/LLM 建议 ： induction a with | zero => ... | succ a ih => ... （它生成了一个归纳法的骨架）。
  3. 执行 ：Lean 接受 induction a ，目标分解为两个子目标： case zero 和 case succ 。
  4. 当前目标（ case zero ） ： b : ℕ ⊢ 0 + b = b + 0
  5. 用户输入 ：“处理第一个情况，0+b=b+0。”
  6. DAP/LLM 建议 ： simp （因为 0+b 和 b+0 都有简化规则）。
  7. 执行 ： simp 成功，解决第一个子目标。自动进入第二个子目标 case succ 。
  8. 当前目标 ： a b : ℕ, ih : a + b = b + a ⊢ succ a + b = b + succ a
  9. 用户输入 ：“现在这个 ih 是归纳假设，怎么用？”
  10. DAP/LLM 建议 ： rw [Nat.succ_add, Nat.add_succ, ih] （它尝试用关于 succ 的引理和归纳假设进行改写）。
  11. 执行 ：Lean 可能成功，也可能因为引理顺序问题失败。如果失败，错误信息（如“rewrite did not change”）会反馈。
  12. DAP 自动重试 ：系统将错误信息和当前目标再次发给 LLM。
  13. LLM 修正建议 ： rw [Nat.add_succ, Nat.succ_add, ih] （调整了顺序）。
  14. 执行 ：成功。所有子目标解决，证明完成。

在整个过程中，用户不需要记住 Nat.zero_le 或 Nat.succ_add 这些具体的引理名，只需要用自然语言描述意图和策略，DAP 负责找到并拼装正确的“乐高积木”。即使 LLM 拼错了，证明器的即时反馈也能帮助它（或用户）快速纠正。

5. 挑战、局限与未来展望

尽管 DAP 这样的框架前景诱人，但在实际开发和测试中，我遇到了不少挑战，这也是当前阶段的局限所在。

1. LLM 的可靠性与“幻觉” ：这是最大的问题。LLM 可能会生成语法正确但逻辑错误的 tactic，或者推荐一个不存在的定理名（如 Nat.zero_lt 拼成 Nat.zero_lt ）。虽然证明器能捕获最终的逻辑错误，但一些微妙的语义错误可能在早期逃过检查，直到很久以后才暴露。 解决方案 ：严格依赖证明器作为最终仲裁者；对 LLM 生成的定理名，在调用前可以通过 LSP 的 workspace/symbol 查询进行验证；建立定理和引理的“可信库”白名单。

2. 提示词工程的脆弱性 ：系统的表现极度依赖提示词的设计。不同的模型、不同的定理领域可能需要微调提示词。一个在代数上工作良好的提示词，在拓扑学证明中可能效果很差。 解决方案 ：开发可配置、可切换的提示词模板库；探索使用少量示例的“少样本学习”（Few-shot Learning）嵌入到提示词中。

3. 性能与成本 ：频繁调用大型 LLM（尤其是 GPT-4）成本高昂，且延迟显著。对于长证明，交互体验会受影响。本地模型虽然隐私好，但推理速度（尤其是 70B 模型）依然是个问题。 解决方案 ：对常见的、模式化的证明步骤（如简单的 simp , rw , apply ），可以构建一个本地的、基于规则的或小模型驱动的快速决策器，只有遇到复杂情况时才求助大模型。缓存成功的“问题-解决方案”对，供后续复用。

4. 与大型数学库的集成 ：Mathlib4 这样的库庞大而复杂，包含成千上万的定理。让 LLM 在如此巨大的搜索空间中精准定位所需引理，非常困难。 解决方案 ：结合检索增强生成（RAG）。当用户提出一个目标时，系统可以先从 Mathlib4 的索引中检索出一组语义相关的定理和定义，然后将这些候选条目作为上下文提供给 LLM，极大地缩小搜索范围，提高建议的准确性。

5. 用户控制与可解释性 ：用户不能完全做“甩手掌柜”。系统需要让用户清楚每一步在做什么，为什么这个建议可能有效。当自动证明陷入死胡同时，用户需要能方便地介入、手动调整或回溯。 解决方案 ：提供清晰的证明状态可视化（如目标树）；为 LLM 的每个建议提供一个简短的自然语言理由（“我建议使用 induction ，因为命题是关于自然数 n 的”）；设计直观的撤销、分支管理功能。

未来展望 ：

  • 专业化微调模型 ：收集 Lean/Mathlib4 上的人类证明数据，微调一个专精于定理证明的“代码模型”，这有望在较小参数量下获得比通用 LLM 更好的性能。
  • 证明规划与符号推理结合 ：让 LLM 负责高层的策略规划和自然语言交互，而将一些低级的、符号化的等式推导、不等式求解交给专门的、可验证的符号计算引擎（如 linarith , omega , ring ），形成混合推理系统。
  • 教育应用 ：DAP 可以成为学习交互式定理证明的绝佳工具，像一位随时在线的助教，帮助学生理解证明策略，探索不同的证明路径。

构建 DAP 的过程，是一个不断在“AI 的创造性”和“逻辑的严谨性”之间寻找平衡点的过程。它不是一个能完全自动证明一切的黑箱，而是一个强大的协同工具，将人类的方向性指导和直觉，与机器的计算力和不知疲倦的搜索能力结合起来。对于需要高可靠性的软硬件验证、数学形式化项目来说，这样的工具或许能成为突破生产力瓶颈的关键。至少，它让我在写证明的时候，感觉不再是独自面对一堵冰冷的代码墙，而是有了一个可以随时讨论、尝试的伙伴。

Logo
AI Agent技术社区

Agent 垂直技术社区，欢迎活跃、内容共建。

更多推荐

cover

HarmonyOS 6（API 23）实战：基于HMAF的「具身智脑」——PC端具身智能体仿真与机器人任务规划平台

avatar AI Agent技术社区

Agent 越聊越笨？我把上下文修剪了一下，token 砍了 50%，质量反而涨了

这篇文章总结了AI Agent在对话过程中上下文管理的关键优化策略——修剪（Pruning）。通过分析47个Agent项目，作者发现平均58%的上下文内容是冗余信息（过时对话、未使用工具定义、重复约束等），这些无效token不仅增加API成本，还会降低模型表现。

avatar AI Agent技术社区
cover

Agent 工具越用越乱？5.1k Star Omnigent，直接给 Claude Code/Codex/Cursor 加一座调度塔

avatar AI Agent技术社区