OProver：基于多智能体与强化学习的自动化定理证明框架实践

1. 项目概述：当形式化证明遇上“智能体”

最近在AI for Math这个圈子里，OProver这个名字开始频繁出现。简单来说，OProver是一个将“智能体”（Agentic）思想与形式化定理证明（Formal Theorem Proving）深度融合的统一框架。如果你对Lean 4、Coq、Isabelle这些证明助手有所耳闻，或者正在关注如何用强化学习（RL）来攻克数学难题，那OProver绝对值得你花时间研究。

形式化证明，说白了就是用计算机能理解的严格语言来写数学证明，确保逻辑上滴水不漏。但这个过程极其繁琐，就像用最底层的汇编语言去写一个复杂的应用程序，每一步都需要精确无误。传统的自动化定理证明器（ATP）虽然能处理一些逻辑推理，但在面对现代数学庞大的知识体系（比如Mathlib）时，往往力不从心。而OProver的思路很“潮”，它不再把证明过程看作一个单纯的搜索或推理问题，而是构建了一个由多个“智能体”组成的协作系统。这些智能体各有专长，有的负责策略规划，有的负责引理检索（这让人联想到Agentic RAG），有的负责执行具体的证明步骤（Tactic），它们通过一个统一的框架进行交互和学习，共同目标就是完成一个形式化证明。

这个框架的核心价值在于“统一”和“智能体化”。它试图为形式化证明中的各种任务——从高层策略制定到低层规则应用——提供一个可扩展、可学习的架构。对于研究者，它提供了一个探索AI与数学交叉前沿的绝佳平台；对于开发者，它可能意味着未来构建数学证明辅助工具的新范式。接下来，我们就深入拆解一下OProver的设计思路、核心组件以及如何上手实践。

2. 核心架构与设计哲学

OProver的设计并非凭空而来，它深刻回应了当前形式化证明领域面临的几个核心痛点：证明搜索空间巨大、数学知识库（如Mathlib）规模庞大且复杂、人类专家与机器之间的交互效率低下。其架构设计哲学可以概括为“分而治之”与“协同进化”，通过引入多智能体系统，将复杂的证明任务分解并分配给专业化的“子智能体”去处理。

2.1 多智能体协作范式

在OProver的视角下，一个完整的定理证明过程被建模为一个多智能体协作任务。这不同于传统的单一模型端到端预测下一个证明步骤（tactic）的方式。典型的智能体可能包括：

1. 策略规划智能体（Strategic Planner Agent）：这是整个证明任务的“指挥官”。它的输入是整个证明目标和当前的证明状态（Proof State），输出是一个高层的证明策略计划。例如，它可能决定“先尝试使用归纳法”，或者“需要先证明一个关于集合交的引理”。这个智能体通常需要具备对数学证明结构的宏观理解能力。
2. 检索增强生成智能体（Retrieval-Augmented Generation Agent, RAG Agent）：这是“军师”或“图书馆管理员”。当证明陷入僵局，或者策略规划智能体认为需要外部知识时，RAG智能体就开始工作。它从庞大的形式化数学库（如Lean 4的Mathlib）中检索与当前证明状态相关的定理、定义和已证明的引理。这正是“Agentic RAG”研究方向在数学领域的具体应用。它的核心挑战在于如何理解形式化语言表达的数学语义，并进行精准的语义检索，而不是简单的关键词匹配。
3. 战术执行智能体（Tactic Execution Agent）：这是“一线工兵”。它接收具体的子目标（subgoal）和可能的相关引理，负责生成或选择具体的、可被Lean 4内核执行的证明指令（tactic），例如apply,rewrite,simp,ring等。这个智能体需要精通目标语言的语法和语义，并且能够进行可靠的、细粒度的逻辑推理。
4. 状态评估与反思智能体（State Evaluation & Reflection Agent）：这是“质检员”。它监控整个证明过程，评估当前步骤的有效性，判断证明是否在正轨上。当证明失败或陷入循环时，它负责分析原因，并将反馈信息传递给策略规划智能体，以调整后续策略。这个过程模仿了人类证明者“尝试-失败-反思-再尝试”的循环。

这些智能体在一个统一的框架下运行，通过一个共享的“环境”（通常是Lean 4的交互式证明状态）进行通信和协作。框架负责智能体间的消息路由、状态同步和协同决策。

2.2 统一框架的关键组件

为了实现上述协作，OProver框架通常包含以下几个关键组件：

• 环境封装器（Environment Wrapper）：这是框架与底层证明助手（如Lean 4）交互的桥梁。它将Lean的证明状态、错误信息、目标等封装成智能体可以理解的统一表示（例如，图结构、向量或符号序列）。同时，它也负责执行智能体产生的tactic，并返回执行结果。
• 智能体管理器（Agent Manager）：负责所有智能体的生命周期管理、调度和通信。它定义了智能体之间的交互协议（例如，基于消息队列或黑板模型）。当策略规划智能体发出一个“需要引理”的请求时，管理器会激活RAG智能体；当RAG智能体返回候选引理后，管理器再将它们连同子目标一起传递给战术执行智能体。
• 共享记忆与知识库（Shared Memory & Knowledge Base）：存储证明过程中的中间信息、历史决策、检索到的知识片段等。这为智能体提供了上下文，也便于反思智能体进行分析。知识库则与形式化数学库相连，是RAG智能体的数据源。
• 学习与优化模块（Learning & Optimization Module）：这是框架“智能”的来源。它利用强化学习（RL）来优化智能体的策略。具体来说，将完成一个证明或达到某个中间里程碑视为获得奖励，将证明步骤视为智能体的动作序列。通过RL算法（如PPO、A2C等），框架可以学习如何更好地协调智能体、选择更优的证明策略。这就是“Agentic RL”在其中的作用。

注意：这里的“智能体”不一定都是独立的神经网络模型。有些可能是基于规则的专家系统（如某些简单的战术选择器），有些则是基于Transformer的大语言模型微调而成。框架的统一性体现在对它们一致的接口封装和调度管理上。

3. 环境搭建与核心工具链解析

要深入理解或复现OProver的相关实验，搭建一个稳定、可复现的Lean 4开发环境是第一步。这里不仅涉及Lean 4本身，还包括其包管理器Lake、社区数学库Mathlib，以及相关的工具链。下面我将以Linux/macOS环境为例，详细拆解安装和配置过程中的每一个环节。

3.1 Lean 4、Elan、Lake与Mathlib的安装与关系梳理

很多新手会被Lean 4、Elan、Lake、Mathlib这几个名词搞晕。理清它们的关系至关重要：

1. Lean 4：核心定理证明器/编程语言。它是我们最终要使用的工具。
2. Elan：Lean的工具链管理器。类似于Python的pyenv或Rust的rustup。因为Lean（尤其是配合Mathlib时）对版本要求非常严格，Elan允许你在同一台机器上轻松安装、切换和管理多个不同版本的Lean编译器及工具链。这是安装的第一步，也是保证环境稳定的关键。
3. Lake：Lean的构建系统和包管理器。类似于make+npm/cargo。它用于管理Lean项目的依赖（比如引入Mathlib）、编译项目、运行测试等。当你用leanproject new创建新项目时，Lake的配置文件lakefile.lean会自动生成。
4. Mathlib：Lean社区维护的巨型形式化数学库。它包含了从基础算术到前沿数学的成千上万个定义、定理和证明。绝大多数形式化证明项目都重度依赖Mathlib。

安装实操步骤：

步骤一：安装Elan打开终端，运行官方一键安装脚本。这是目前最推荐的方式，能自动处理路径等问题。

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

安装完成后，重启终端或执行source ~/.bashrc(或~/.zshrc)，然后运行elan --version验证安装。

步骤二：通过Elan安装Lean 4Elan安装后，其实已经包含了一个默认的Lean版本。但为了确保使用稳定且与Mathlib兼容的版本，我们通常安装一个特定的工具链。Mathlib社区会推荐一个“稳定”的Lean版本。

# 查看可用的工具链版本 elan toolchain list # 安装Mathlib当前推荐的稳定版本，例如 `stable` 或一个具体版本号如 `leanprover/lean4:v4.10.0` elan toolchain install stable elan default stable # 将其设为默认 # 验证Lean安装 lean --version

此时，lean、lake命令应该都可用了。

步骤三：创建并配置一个使用Mathlib的Lean项目我们不直接“安装”Mathlib，而是在每个Lean项目中声明对Mathlib的依赖。

# 安装 `leanproject` 工具，这是一个管理Mathlib依赖的便捷脚本 pip install mathlibtools # 创建一个新的Lean项目（进入你的工作目录） leanproject new my_oprover_study cd my_oprover_study # 此时，`leanproject` 会自动生成 `lakefile.lean` 并拉取当前兼容的Mathlib版本 # 这个过程会下载大量数据（几个GB），请保持网络通畅。

进入项目后，你会看到lakefile.lean文件，其中已经包含了类似require mathlib from git ...的依赖声明。运行lake build可以编译项目及其所有依赖（包括Mathlib）。

实操心得：网络问题是首次搭建环境的最大障碍。由于Mathlib仓库很大，国内用户可能会遇到Git克隆缓慢或超时。有两个解决方案：一是使用代理（此处不展开，请自行寻找合规的网络加速方案），二是利用Gitee等国内镜像。可以尝试修改lakefile.lean中Mathlib的git地址为镜像地址，但需注意镜像同步可能滞后，可能导致版本不兼容。最稳妥的方法是耐心等待或寻找可靠的网络环境。

3.2 辅助工具与开发环境配置

一个高效的开发环境能极大提升生产力。

1. 编辑器选择与配置：

   • VS Code + Lean 4插件是绝对的主流选择。在VS Code扩展商店搜索“Lean 4”并安装。插件提供了语法高亮、实时错误检查、目标视图（Goal View）、代码补全、定理跳转等强大功能。
   • 打开我们刚才创建的my_oprover_study项目文件夹，VS Code插件会自动识别并加载Lake配置。在底部的状态栏，你应该能看到Lean服务器正在启动并处理文件。打开Main.lean文件，尝试写一个简单的定理，如theorem hello : 1 + 1 = 2 := by rfl，保存后如果没有错误提示，说明环境配置成功。

2. 调试与信息查看：

   • Goal View：在VS Code中，将光标放在by之后的证明体里，编辑器右侧或下方会显示当前的“证明目标”（Goal）。这是交互式证明的核心。
   • Info View：按Ctrl+Shift+Enter(或Cmd) 可以打开信息视图，查看当前光标下术语的类型、文档等。
   • #eval 和 #check：在代码中使用#eval可以求值表达式（对于可计算的类型），#check可以查看任何表达式的类型。这是学习Lean和调试定义的重要工具。

3. 项目结构管理：

   • 一个典型的Lean项目目录包含：
     • lakefile.lean：项目依赖和构建配置。
     • Main.lean：主文件（可改名）。
     • lake-packages/：Lake下载的依赖包，包括Mathlib，不要手动修改。
     • _target/：Lake的构建输出目录。
   • 建议将你自己的定理证明按主题分门别类放在不同的.lean文件中，然后在lakefile.lean中将它们添加到lean_lib的srcDir中，或通过import语句相互引用。

4. OProver核心组件实现深度解析

理解了框架设计并搭建好环境后，我们可以深入OProver各个智能体组件的潜在实现方案。请注意，由于OProver本身可能是一个研究原型或框架概念，以下实现思路是基于公开论文、类似项目（如GPT-f, LeanStep）以及我个人对多智能体系统和形式化证明的理解进行的合理推演和构建。

4.1 策略规划智能体的实现：从目标反推策略

策略规划智能体的核心任务是：给定当前证明状态（一堆待证明的子目标），输出一个高层次的证明策略描述。这可以看作一个序列生成问题。

一种可行的技术路径：

1. 状态表示（State Representation）：将Lean的证明状态（一组目标和假设）转化为一个固定维度的向量。这可以通过图神经网络（GNN）来实现，因为证明状态天然是一个图（项是节点，依赖关系是边）。更简单的方法是将目标和假设的文本序列化，通过一个预训练的语言模型（如CodeBERT或专门在Lean代码上微调过的模型）获取其嵌入（embedding）。
2. 动作空间（Action Space）：动作不是具体的tactic，而是高层策略标签，例如：[“induction”, “case_split”, “apply_lemma”, “simplification”, “rewrite”, “use_contradiction”]。这些标签可以预先定义成一个列表。
3. 模型架构：可以采用一个编码器-解码器（Encoder-Decoder）架构，或者直接使用一个序列分类模型（如基于Transformer的分类头）。
   • 编码器：处理证明状态表示。
   • 解码器/分类头：输出一个策略标签的概率分布。
4. 训练数据：可以从Mathlib或其他形式化证明库中提取。每一对数据包括：证明过程中的某个中间状态（作为输入）和接下来人类证明者所采用的高层策略（作为标签）。高层策略需要从具体的tactic序列中抽象出来，这本身就是一个有挑战性的标注或聚类问题。

示例伪代码思路：

# 伪代码，示意流程 class StrategicPlanner: def __init__(self, model_path): self.encoder = load_pretrained_lean_encoder() self.classifier = StrategyClassifierHead() def predict_strategy(self, proof_state: LeanState) -> Strategy: # 1. 将proof_state转换为图或序列表示 state_embedding = self.encoder.encode(proof_state.to_graph()) # 2. 预测策略分布 strategy_logits = self.classifier(state_embedding) # 3. 采样或选择最优策略 strategy_id = torch.argmax(strategy_logits).item() return STRATEGY_LABELS[strategy_id] # 使用 planner = StrategicPlanner("model/planner.pt") current_state = env.get_state() next_strategy = planner.predict_strategy(current_state) # 例如输出 "induction"

这个智能体的输出会传递给其他智能体作为指导方针。例如，如果策略是“apply_lemma”，那么RAG智能体就需要被重点激活。

4.2 检索增强生成（RAG）智能体的实现：在数学知识海洋中精准捕捞

这是OProver中技术挑战最大、也最体现“智能”的部分之一。其目标是根据当前证明状态，从Mathlib中检索出最相关、最有可能用到的定理或定义。

核心挑战：

• 语义匹配，而非字符串匹配：a + b = b + a（加法交换律）和x + y = y + x在数学上等价，但字符串不同。检索系统需要理解数学语义。
• 规模巨大：Mathlib包含数万条定理，直接进行暴力相似度计算不可行。
• 形式化语法：定理是以Lean代码形式存在的，包含复杂的类型信息和语法结构。

实现方案拆解：

1. 知识库预处理（索引构建）：

   • 解析Mathlib：使用Lean的语法分析工具，遍历所有.lean文件，提取出每个定理（theorem）、引理（lemma）、定义（def）的名称、类型（Type）和陈述（Statement）。类型信息至关重要，因为它包含了定理的前提和结论。
   • 生成嵌入：为每个定理的“陈述”生成一个语义向量嵌入。这里不能直接用通用文本模型（如BERT），因为它不理解Lean语法和数学逻辑。需要使用在Lean代码和数学文本上预训练过的专用模型，例如在大量Lean代码和自然语言数学文本混合语料上训练的Transformer模型。将定理陈述输入模型，取[CLS]标记的向量或平均池化后的向量作为该定理的嵌入。
   • 建立向量数据库：将所有定理的嵌入存入向量数据库（如FAISS, Chroma, Weaviate）。同时存储定理的元数据（名称、所在文件、类型等）。

2. 在线检索（查询阶段）：

   • 查询构造：当RAG智能体被调用时，输入是当前需要证明的目标（Goal）。同样，使用上述专用模型将目标陈述转换为查询向量。
   • 相似度搜索：在向量数据库中进行近似最近邻（ANN）搜索，找出与查询向量最相似的K个定理嵌入（例如，K=10或20）。
   • 重排序（Re-ranking）：初步检索出的结果可能只考虑了语义相似度，但未考虑类型匹配。一个定理h : A -> B要能应用于目标⊢ B，前提是当前上下文必须有类型为A的假设。因此，需要一个轻量级的重排序模型或规则系统，根据当前证明状态的假设列表，对检索结果进行过滤和重新排序，优先输出那些前提条件可能被满足的定理。

3. 集成到框架：RAG智能体将排序后的定理列表（包含名称和类型）返回给智能体管理器。管理器可能会将这些候选定理作为“上下文”注入到战术执行智能体的提示（Prompt）中，或者由战术执行智能体自行选择使用哪一个。

注意事项：检索质量直接决定了后续证明步骤的成败。常见的坑包括：1) 嵌入模型质量不佳，导致检索不相关；2) 忽略了类型约束，检索出无法直接应用的定理；3) 索引未及时更新，当Mathlib版本升级后，旧的嵌入索引失效。因此，需要建立一套自动化的索引更新流水线。

4.3 战术执行智能体的实现：将策略转化为具体行动

战术执行智能体是最终“动手”的单元。它接收一个具体的子目标（Subgoal）和一组相关的候选引理（来自RAG），然后生成或选择一个能在Lean中成功执行的tactic。

实现方式有多种，目前主流且有效的是基于大语言模型（LLM）微调的方法：

1. 数据准备：收集大量的（证明状态，下一个正确tactic）数据对。这些数据可以从Mathlib的证明历史中提取。每一个步骤，当前的证明状态是输入，人类写出的下一个tactic是输出标签。
2. 模型与输入格式化：
   • 模型：选择一个代码能力强的模型架构，如GPT-NeoX、CodeLlama或DeepSeek-Coder的底座，进行继续预训练或微调。
   • 输入：将证明状态格式化为一个文本字符串。通常包括：
     • 所有当前假设（h1 : P, h2 : Q, ...）
     • 当前要证明的目标（⊢ R）
     • （可选）RAG智能体提供的相关定理列表，作为提示信息。
   • 输出：模型需要生成一个完整的、语法正确的Lean tactic字符串，例如apply h1或refine ⟨?_, ?_⟩。
3. 训练目标：这是一个标准的自回归语言模型训练任务，最大化生成正确tactic序列的概率。
4. 推理与解码：在推理时，给定格式化的证明状态，让模型生成tactic。可以采用束搜索（Beam Search）来获取多个候选，然后尝试执行它们，选择第一个能成功推进证明的（这是一种简单的“执行验证”回馈）。

示例输入格式：

假设: h1: ∀ (x: Nat), x > 0 -> x + 1 > 1 h2: a > 0 目标: ⊢ a + 1 > 1 相关定理: Nat.succ_pos : ∀ (n : ℕ), 0 < n.succ ...

期望模型输出：apply h1 a h2

进阶技巧：单纯的tactic预测可能会生成语法正确但逻辑错误的步骤。因此，OProver框架会通过环境封装器立即执行生成的tactic。如果执行失败（Lean报错），这个失败信号可以作为强化学习的负反馈，或者触发反思智能体进行分析，并让战术执行智能体重新生成。

4.4 基于强化学习的协同优化

单个智能体可以分别训练，但OProver的威力在于智能体间的协同。这就需要引入强化学习（RL）进行全局优化。

将证明过程建模为马尔可夫决策过程（MDP）：

• 状态（State）：整个多智能体系统的状态，包括Lean的证明状态、各个智能体的内部状态（如历史记录）等。
• 动作（Action）：由智能体管理器协调产生的一系列动作。这可能是一个复合动作，例如：（策略规划智能体选择“induction”）-> （RAG智能体检索与归纳假设相关的引理）-> （战术执行智能体生成induction n with ...）。
• 奖励（Reward）：
  • 稀疏奖励：最终成功证明整个定理时，给予一个大的正奖励（+1）。证明超时或彻底失败时，给予负奖励（-1）。
  • 中间奖励：为了缓解稀疏奖励问题，可以设计中间奖励信号。例如：每成功关闭一个子目标（subgoal）给予一个小奖励；使用到的引理与当前目标的相关度（由RAG系统评分）可以作为奖励的一部分；证明步骤的简洁性也可以作为奖励因子。
• 策略（Policy）：策略函数决定了在给定状态下，智能体管理器应如何协调各个智能体采取动作。这个策略函数本身可以是一个神经网络，它观察全局状态，输出对各个智能体的调度权重或动作建议。

训练流程：

1. 让当前的智能体系统（策略）在大量定理上尝试进行证明。
2. 收集轨迹（状态、动作、奖励序列）。
3. 使用RL算法（如PPO）更新策略网络的参数，目标是最大化累积奖励。
4. 策略网络的更新会间接影响各个智能体的行为。例如，它可能学会在证明初期更多调用策略规划智能体进行宏观布局，在证明细节处更多依赖战术执行智能体，并在遇到瓶颈时精准激活RAG智能体。

这个过程计算成本极高，但它是实现智能体间“默契配合”的关键。通过RL，系统可以学习到何时该检索、检索什么、何时该尝试哪种基础战术等高阶启发式规则。

5. 实践挑战、常见问题与调试技巧

即使理解了所有原理，在真正尝试构建或使用类似OProver的系统时，你一定会遇到无数挑战。下面分享一些从实验和社区经验中总结的常见问题与应对策略。

5.1 环境与依赖管理中的“坑”

1. Lake构建失败，提示“unknown package”或版本冲突。

   • 原因：Lake的依赖解析出现问题，可能是网络超时导致包未完整下载，或者是lakefile.lean中声明的版本与本地已缓存版本不兼容。
   • 解决：
     • 删除lake-packages目录和lakefile.lock文件，然后重新运行lake build。这会强制重新解析和下载所有依赖。
     • 检查lakefile.lean中的git引用是否指向正确的提交哈希或标签。对于Mathlib，通常使用require mathlib from git “https://github.com/leanprover-community/mathlib4” @ “v4.10.0”这样的格式来锁定版本。
     • 确保Elan的Lean工具链版本与Mathlib的要求匹配。Mathlib仓库的lean-toolchain文件指明了要求的Lean版本。

2. VS Code Lean插件报错“无法启动Lean server”或“找不到lake”。

   • 原因：环境变量PATH未正确设置，或者VS Code未在正确的项目根目录下运行。
   • 解决：
     • 确保终端中可以正常执行lean --version和lake --version。
     • 在VS Code中，使用“文件”->“打开文件夹”的方式打开整个项目目录（包含lakefile.lean的目录），而不是直接打开单个.lean文件。
     • 查看VS Code的输出面板（Output），选择“Lean 4”通道，查看具体的错误日志。

3. 导入（import）语句报红，找不到模块。

   • 原因：.lean文件未被Lake识别为项目的一部分，或者导入路径错误。
   • 解决：
     • 确保文件位于项目src/目录下（或lakefile.lean中lean_lib指定的目录下）。
     • 导入项目内的其他文件，使用相对于src/的路径，例如import MyProject.Subdir.MyFile。
     • 导入Mathlib中的模块，直接使用其标准命名空间，如import Mathlib.Algebra.Group.Basic。VS Code插件通常提供自动补全。

5.2 智能体训练与推理中的典型问题

1. 战术执行智能体生成的tactic语法正确但逻辑错误，导致证明卡住。

   • 现象：模型输出了apply h，但当前上下文中并没有名为h的假设，或者类型不匹配。
   • 排查：
     • 强化执行验证：不要只相信模型输出。每一个生成的tactic都必须立即发送到Lean内核执行。如果执行失败（返回错误信息），这个tactic就应该被丢弃。可以将错误信息作为反馈，让模型进行重试（类似“批评-修正”循环）。
     • 丰富输入上下文：确保输入给模型的证明状态信息是完整和准确的，包括所有局部假设的精确名称和类型。
     • 数据质量检查：检查训练数据中是否存在“脏数据”，比如包含了未导入的定理或错误的tactic。

2. RAG智能体检索的定理不相关，浪费计算资源。

   • 现象：检索返回的定理在数学语义上可能有点关联，但完全无法应用到当前目标上。
   • 排查与优化：
     • 嵌入模型评估：在独立的测试集上评估嵌入模型的质量。构建一个测试集，包含（目标，相关定理列表）对，计算检索的命中率（Recall@K）。
     • 引入类型过滤：在重排序阶段，加入严格的类型一致性检查。例如，使用Lean的元编程（Meta Programming）能力，在后台尝试将检索到的定理“统一”（unify）到当前目标上，如果立即失败（如类型不匹配），则大幅降低其排名。
     • 混合检索：结合语义检索（向量搜索）和符号检索（基于定理名称、关键字或类型结构的匹配），提高召回率。

3. 强化学习训练不稳定，奖励不收敛。

   • 现象：证明成功率在训练过程中波动很大，没有持续上升的趋势。
   • 解决思路：
     • 奖励塑形（Reward Shaping）：设计更密集、更平滑的中间奖励。例如，给予“子目标数量减少”以奖励，而不仅仅是最终成功。
     • 课程学习（Curriculum Learning）：不要一开始就在最难的定理上训练。从Mathlib中筛选出简单到复杂的定理，让智能体系统先学习证明简单的，再逐步增加难度。
     • 专家示范（Expert Demonstration）：单纯使用RL探索效率太低。可以结合模仿学习（Imitation Learning），先用监督学习的方式在人类证明数据上预训练各个智能体，让它们具备基础能力，然后再用RL进行微调和优化协同策略。这被称为“预训练+RL微调”范式。

5.3 性能与效率优化

1. 推理速度慢：调用LLM生成tactic、进行向量检索都是耗时操作。

   • 优化：
     • 缓存：对常见的证明状态和查询进行缓存。如果相同的子目标再次出现，直接使用之前成功的tactic。
     • 模型轻量化：对战术执行模型进行知识蒸馏，得到更小、更快的模型用于部署。
     • 并行尝试：对于战术执行，可以让模型一次性生成多个候选tactic（如通过束搜索），然后并行地尝试执行它们，选择第一个成功的。这虽然增加了单步计算量，但可能减少总步数。

2. 与Lean交互的开销：每次执行tactic都要启动Lean进程或进行IPC通信，开销巨大。

   • 优化：使用Lean的服务器模式或内存中的交互式会话，避免频繁的进程启动。一些研究框架（如lean-gym）提供了高效的Python与Lean交互接口。

构建OProver这样的系统是一个系统工程，涉及机器学习、形式化方法、软件工程等多个领域。最大的体会是，没有一劳永逸的“银弹”。成功往往来自于对每个组件细节的精心打磨，以及对整个系统工作流程的深刻理解。从搭建一个能跑通的最小原型开始，用简单的定理进行测试，然后逐步增加复杂度，迭代优化每个模块，是唯一可行的路径。在这个过程中，深入阅读Mathlib中的经典证明，理解人类证明者的思维过程，对于设计更合理的智能体行为至关重要。这个领域正在快速发展，每一天都可能出现新的思路和工具，保持学习的心态是应对挑战的最好方式。