自动定理证明ATP在很长一段时间里是符号推理的专属领域归结、Tableau、SMT 抽象方法很多但核心思路都建立在“把逻辑问题变成语法规约下的搜索问题”上。最近几年神经符号结合的方法越来越多可大多数工作都把精力放在“给证明器换一个更好的动作评分函数”上。这篇文章想聊一个更具体、更聚焦的问题当证明演算采用连接表Connection Tableau这种高度依赖目标导向的搜索形式时我们能不能用模仿学习来让模型学会“下一步如何构建证明树”。为什么这个话题值得关注连接表的设计初衷是把证明搜索主动限制在互补连接上每一步只扩展与当前叶子形成互补关系的文字。这个约束带来了很好的剪枝效果但也把核心难点转移到了“选择”上——选哪个叶子、选哪个连接、什么时候回溯全部依赖启发式。传统做法是人工总结规则比如“优先选新叶子”“优先选目标方向的分支”但这些规则往往只在一个领域有效换到另一个问题集就会失效。模仿学习提供了一个不同的思路如果已经有一个能解决问题的证明器哪怕它慢、笨、经常绕路那它留下的搜索轨迹就是专家数据我们完全可以训练一个网络来模仿它的选择逻辑然后把网络作为新的决策头插回搜索循环。本文会按照“概念 → 建模 → 实现 → 验证 → 改进”的顺序展开。实现部分会给出一个最小可运行的模仿学习训练流程包括状态编码、动作定义、专家轨迹收集、行为克隆训练以及推理时如何把模型输出的概率接回证明搜索循环。先声明这是一条实验性技术路径本文不会给出具体基准数据集上的指标——这类指标取决于你的专家证明器、问题分布和状态编码方式。我更想讲清楚方法本身以及真正容易踩到坑的几个环节。1. 这篇文章真正要解决的问题先给一个明确的判断连接表构建过程中的“动作选择策略”是典型的高维组合搜索问题手工启发式效率低、迁移差模仿学习能够在没有奖励工程的前提下从已有证明器的搜索日志中直接学到一个可用的策略从而缩短策略迭代周期并让模型有能力处理更复杂的问题分布。为什么现在聊这个话题因为越来越多的工程场景把自动定理证明当后端服务配置合法性校验、安全策略验证、智能体规划结果检查、程序不变量推断。这类场景的共同点是——同一个推理问题可能来自完全不同的业务领域固定启发式很难覆盖而用户能接受的响应时间又非常有限。连接表类证明器是时间受限场景下的常见选择它的搜索过程每一步都产生大量候选动作策略质量直接决定你能不能在一个合理的深度内闭合所有分支。如果策略只靠人工调节换一个领域就要重新调参很痛苦。模仿学习解决的核心矛盾在这里我们有大量可复现的专家行为却没有一个清晰、可工程化的奖励函数。强化学习在这个场景极其别扭动作空间随证明树变大而爆炸奖励信号极其稀疏随机探索基本无效因此从零训练一个可靠的证明策略成本很高。而模仿学习绕开了奖励设计只要求你有“专家的动作是什么”剩下的就是监督学习问题。把连接树构建过程看成序列决策问题之后模仿学习一下子变得很自然状态就是当前的部分证明树动作就是扩展叶子、选择连接、回溯、判定闭合四种操作专家就是那个已经能跑通的旧证明器。什么样的读者最适合读这篇文章如果你在做神经符号推理、自动定理证明或者正在给自己的可满足性/SMT求解器设计决策模块这篇文章可以作为连接表方向的技术地图。如果你只是对“模仿学习到底怎么落到符号系统里”感兴趣本文的状态编码和搜索接口设计思路也值得一看。读完之后你至少能回答三个问题连接表为什么需要学习型策略模仿学习的数据长什么样怎么把一个行为克隆模型接到递归搜索循环里而不破坏可回溯性。2. 连接表Connection Tableau的核心概念2.1 从普通 Tableau 说起想理解连接表先要理解普通 Tableau。Tableau解析表/语义树的核心思路是反证为了证明 Γ ⊢ φ把 ¬φ 加进前提 Γ然后不断把公式拆分为子公式构建一棵开放证明树。每个分支对应一组“还必须继续处理”的文字集合。如果某个分支同时出现 P 和 ¬P这个分支就闭合了当所有分支都闭合就说明假设 ¬φ 不可满足从而 φ 成立。这个演算的缺点是分支爆炸。只要公式里有几个析取或合取树的分支数量就会急剧增长大量分支其实和要证的结论无关。普通 Tableau 的修剪基本靠“文字出现矛盾就闭合”这种被动剪枝搜索过程中没有主动引导。因此普通 Tableau 很适合教材演示但在中等规模问题上很难直接实用。2.2 连接条件到底约束了什么连接表在普通 Tableau 基础上引入“连接”概念。连接表的扩展不是无脑展开所有子公式而是只允许展开“能与路径上某个已有文字形成互补连接”的叶子。所谓互补连接指两个文字带相反的极性一个是 P一个是 ¬P。形式上连接表要求每个叶子 L 必须与证明树某条路径上的另一个叶子 M 构成连接且 L 是 M 的互补文字。这个“连接条件”避免了大量无关分支的展开既然一个叶子能和路径上某个文字形成矛盾那么沿叶子展开才可能在有限步内促成这个矛盾闭合一个无法和任何路径文字构成互补对的叶子无论怎么展开都不可能直接为闭合该分支做贡献。可以这样通俗理解普通 Tableau 是在一个没有方向感的迷宫里盲目探路每个岔路都要走连接表则在每个路口都问一个问题——“你即将进入的这个通道是否和当前房间里已有的钥匙配对”只有配方成立才允许进入其余通道直接被候选集排除。这个约束把搜索规模从指数爆炸压缩到“沿连接展开”的可见候选集合。2.3 连接表对搜索策略的独特要求连接条件把每一步的动作空间从“所有可用公式”压缩成“与当前叶子互补的文字所在的公式”这很好但动作空间压缩不等于不需要决策。树里可能有多个叶子每个叶子可能有多个候选互补文字引擎还得决定搜索顺序。更麻烦的是连接表搜索经常遇到“局部看似乎正确但沿某个连接展开若干步后证明失败”的情况这时必须能高效回溯。所以连接表证明器的性能瓶颈集中在两处叶子选择顺序。候选连接的优先级。这两件事用人工启发式来做总是顾此失彼用数据驱动的方式直接拟合专家选择则是模仿学习最擅长的场景。对比维度普通 Tableau连接表Connection Tableau扩展条件对子公式无条件展开仅当叶子与路径上文字构成互补连接时展开分支数量容易指数增长通过连接约束大幅缩减候选集搜索引导弱多靠被动闭合剪枝强但依赖动作选择策略主要复杂度分支爆炸叶子与连接的选择决策3. 模仿学习为什么适合连接表构建3.1 强化学习在这个场景的天然难点很多神经证明器把策略网络接在搜索循环上训练目标想用强化学习直觉上也很顺证明成功给正奖励超时给负奖励反复试错。但实际落地有几个非常棘手的问题动作空间是动态的。每一步可选动作取决于当前证明树的形状不能像围棋那样用固定棋盘动作空间。奖励稀疏。绝大多数搜索路径都以失败或超时告终探索到正奖励的概率极低。搜索路径很长。一个中等问题的证明可能需要几十到上百步即使最终成功哪一步真正起决定性作用也很难定位。所以纯强化学习训练神经证明器大多需要专家数据做预热本质上是“先把专家策略学到手再微调探索”。3.2 行为克隆与 DAgger模仿学习解决的是“从专家演示学习策略”的问题。最基础的方法是行为克隆Behavior CloningBC把专家轨迹拆成一组组“状态-动作”样本然后训练一个分类或回归模型让模型输出的动作分布贴近专家选择。BC 最大的优点是实现简单数据准备好后就是一个监督学习问题最大的缺点是分布偏移——训练时模型见到的状态来自专家轨迹推理时则来自自己的策略一旦模型的早期动作偏离专家后面见到的状态就会脱离训练分布。针对分布偏移DAgger 的思路是让学习策略在环境中探索遇到新状态时重新向专家查询标签把新样本加入训练集迭代优化。在定理证明场景里专家证明器始终在线可调用所以 DAgger 的“查询专家”步骤不需要额外人工标注实现成本比一般机器人场景低很多。3.3 连接表构建为什么是模仿学习的好目标有三个原因专家数据天然存在。任何能跑通的连接表证明器都留下了完整的搜索日志包括候选集合和当前步的最终选择。动作空间可枚举。连接表的候选动作就是“叶子编号 连接候选编号”可以结构化成离散监督信号。失败可容忍。即使训练出的策略不如专家搜索循环还有回溯做保底不会因为推理一步走错就全盘崩溃。这些特性让连接表构建场景比一般序列决策问题更适合用法入门——它允许策略不完美因为符号搜索本身具备回退机制。4. 如何把连接表构建建模成序列决策问题4.1 状态表示模仿学习的第一步是定义状态。连接表搜索中状态是“当前部分证明树 已生成文字的连接关系”。常用编码方式是树结构信息每个节点的类型叶子、内部节点、深度、父节点路径。节点文字信息谓词名、正负性、参数数量。连接关系信息当前哪些叶子与哪些路径文字存在互补候选。一个常见做法是把整棵部分证明树序列化成一个 token 序列token 种类包括[LEAF]、[CONN]、[CLOSED]、谓词名、极性标记、树分隔符。序列化之后交给 Transformer 或 BiLSTM 编码。这里需要注意如果 token 序列过长比如超过几百模型能力和训练代价都会上升所以状态编码要尽量压缩把不参与决策的已闭合分支折叠成占位符而不是原样保留全部子节点。4.2 动作空间连接表构建的动作本质上分四类动作类型说明示例选择叶子从当前叶子集合中选一个待扩展目标进入浅层叶子还是深层叶子选择候选连接为选定叶子选一个互补文字作为扩展依据选择目标文字还是前提文字回溯撤销当前分支的最近几步试试其他候选连接当前子分支证明失败判定成功所有叶子都已闭合或不存在待扩展叶子证明完成动作空间是状态相关的动态集合所以网络输出不能是固定类别数而是“对当前候选集中每个候选动作的得分”。这类似阅读理解里的答案候选打分实现上是一个加在编码器输出上的线性层。4.3 专家轨迹收集需要一台已有证明器作为专家。改造它的方式很直接在每个决策点记录三样东西当前状态部分证明树 候选连接集。当前可执行动作列表叶子编号 候选连接编号。专家最终选择的动作。把这些信息按 JSON 或 protobuf 落盘就得到经验池。注意专家不一定是“最优证明器”只要它能解决问题策略迁移就是有效的——我们学的是“如何能完成证明”不是“如何用最短步数证明”。如果你想提高效率后续可以再对策略做 DAgger 迭代但第一版 BC 不需要专家最优。4.4 训练目标与评估口径行为克隆的训练目标通常是多标签交叉熵对每个动作候选网络输出一个二分类概率表示“专家是否会在这一步选择它”。评估时不能只看动作准确率还应该看最终指标证明成功率、平均搜索步数、平均回溯次数。因为最终目标是“让证明器在时间预算内完成更多证明”动作准确率只是中间变量。5. 环境准备与数据组织5.1 运行环境本文示例使用 Python 3.10 和 PyTorch 2.x。这些版本不是硬性要求你可以根据手头环境调整。首次实验不推荐引入过于复杂的分布式训练单机单卡足够跑通小规模原型。# 建议使用 conda 或 venv 创建隔离环境 conda create -n connil python3.10 -y conda activate connil pip install torch pip install wandb # 可选用于实验跟踪5.2 专家轨迹数据格式专家轨迹数据建议用一个 JSON 文件保存一个问题实例的所有搜索步。下面是一个示意结构{ problem: bool_comm_12, steps: [ { state_tokens: [[ROOT], ¬P, P, [OR], [LEAF], Q, [LEAF], ¬Q], actions: [ {action_id: 0, type: select_leaf, target: 3, score: 0.0}, {action_id: 1, type: select_leaf, target: 5, score: 1.0}, {action_id: 2, type: select_conn, target: 4, score: 0.0} ], selected_action_id: 1 } ], solved: true }字段说明state_tokens把部分证明树序列化后的 token 列表。actions当前状态下所有合法动作的候选列表。target是对应叶子或连接在状态序列中的索引。selected_action_id专家在本步实际选择的动作编号。solved该问题是否最终被证明。这个格式是教学示意你可以改成 protobuf、pickle 或任何存储格式但建议保持“一步一记录”的结构因为后续做 DAgger 和过滤样本都要按步骤切片。6. 核心实现最小可运行的模仿学习示例从这里开始进入代码。为了把注意力放在“连接表 模仿学习”的结合上我会简化证明器的内部实现用一个最小示例跑通整个流程。实际工程中网络接口、状态序列化、搜索循环都要根据你的证明器做适配。6.1 定义连接表节点与连接先定义连接表的最小数据结构。这里用 dataclass 表示节点和连接重点展示“互补连接”的判断逻辑。# connection_table.py from dataclasses import dataclass, field from typing import List, Optional dataclass class Literal: name: str # 谓词名如 P negated: bool # 是否带否定 args: List[str] # 参数简单示例直接存字符串 def complement_of(self, other: Literal) - bool: # 两个文字构成互补连接谓词相同、极性相反、参数相同 return ( self.name other.name and self.args other.args and self.negated ! other.negated ) def to_token(self) - str: sign ¬ if self.negated else params ,.join(self.args) return f{sign}{self.name}({params}) dataclass class TableauNode: literal: Literal children: List[TableauNode] field(default_factorylist) # connection_target 记录与该节点叶子形成连接的路径文字索引 connection_target: Optional[int] None is_closed: bool False这段代码里complement_of是最核心的逻辑它判断两个文字是否构成连接表意义上的互补对。在实际证明器中这个判断还会加入变量替换、合一等逻辑这里为了演示直接比较谓词名和参数。6.2 状态序列化与动作候选生成有了节点结构下一步是把证明树序列化为 token 列表同时生成可执行动作候选。这个函数是连接状态与学习模型之间的桥梁。# serialize.py from typing import List, Dict def serialize_tree(root: TableauNode) - List[str]: 把一颗部分证明树序列化为 token 列表。 为了保证顺序稳定采用 BFS 遍历并保留每个节点的索引号。 tokens [] queue [root] while queue: node queue.pop(0) if node.is_closed: tokens.append([CLOSED]) else: tokens.append(node.literal.to_token()) queue.extend(node.children) return tokens def build_action_candidates(root: TableauNode, all_literals: List[Literal]) - List[Dict]: 收集当前状态下所有待扩展叶子以及与它们互补的连接候选。 返回动作候选列表每个动作包含类型、目标节点索引、互补文字索引。 # 先做一次 BFS拿到 nodes 列表和索引映射 nodes [] queue [root] while queue: node queue.pop() nodes.append(node) queue.extend(node.children) actions [] for node_idx, node in enumerate(nodes): if node.is_closed: continue for lit_idx, lit in enumerate(all_literals): if node.literal.complement_of(lit): actions.append({ action_id: len(actions), type: select_conn, node_idx: node_idx, lit_idx: lit_idx, }) # 如果某个叶子没有任何互补候选也要把“回溯”作为备选动作 if not actions: actions.append({action_id: 0, type: backtrack, node_idx: -1, lit_idx: -1}) return actions这里的关键思路是动作不是固定类别而是从当前证明树实时生成。模型的输入是serialize_tree得到的 token 序列输出是对每个build_action_candidates动作的打分。注意build_action_candidates只是演示逻辑真正证明器里还要考虑已使用连接不能重复、深度限制、变量合一等约束。6.3 行为克隆训练脚本接下来是训练部分。我用一个简单 Transformer Encoder 做编码器输出每个动作的得分。为了控制篇幅这里把网络结构精简到一个可复制的版本。# train_bc.py import json import torch import torch.nn as nn from torch.utils.data import Dataset, DataLoader class ActionNet(nn.Module): 轻量级动作打分网络token 嵌入 - TransformerEncoder - 分类头。 def __init__(self, vocab_size300, embed_dim64, num_layers2, num_heads4): super().__init__() self.embedding nn.Embedding(vocab_size, embed_dim) encoder_layer nn.TransformerEncoderLayer( d_modelembed_dim, nheadnum_heads, batch_firstTrue ) self.encoder nn.TransformerEncoder(encoder_layer, num_layersnum_layers) self.score_head nn.Linear(embed_dim, 1) def forward(self, state_ids, action_masks): # state_ids: [B, T], action_masks: [B, A] emb self.embedding(state_ids) # [B, T, D] encoded self.encoder(emb) # [B, T, D] state_pool encoded.mean(dim1) # [B, D] # 对每个动作候选打分这里用同一个 state_pool 重复 A 次 # 实际中可以再把动作内容拼进去本文从简 scores self.score_head(state_pool) # [B, 1] scores scores.expand(-1, action_masks.size(1)) # [B, A] scores scores.masked_fill(action_masks 0, -1e9) return scores class TraceDataset(Dataset): def __init__(self, samples): self.samples samples def __len__(self): return len(self.samples) def __getitem__(self, idx): s self.samples[idx] return { state_ids: torch.tensor(s[state_ids], dtypetorch.long), action_masks: torch.tensor(s[action_masks], dtypetorch.float), labels: torch.tensor(s[labels], dtypetorch.float), } def load_traces(json_path: str): 从专家轨迹 JSON 中加载并转换成向量样本。 samples [] with open(json_path, r, encodingutf-8) as f: traces json.load(f) # 这里简化处理假设 traces 是一个列表每个元素已经包含 # state_ids, action_masks, labels 字段。 # 正式实现时需要先从 state_tokens 建立词表再做 token-id 映射。 for t in traces: samples.append(t) return samples def train(): samples load_traces(data/traces.json) dataset TraceDataset(samples) loader DataLoader(dataset, batch_size32, shuffleTrue) model ActionNet() optimizer torch.optim.AdamW(model.parameters(), lr1e-3) loss_fn nn.BCEWithLogitsLoss() model.train() for epoch in range(30): total_loss 0.0 for batch in loader: state_ids batch[state_ids] action_masks batch[action_masks] labels batch[labels] scores model(state_ids, action_masks) loss loss_fn(scores, labels) optimizer.zero_grad() loss.backward() optimizer.step() total_loss loss.item() print(fepoch {epoch}: loss{total_loss / len(loader):.4f}) torch.save(model.state_dict(), action_net.pt) print(saved model to action_net.pt) if __name__ __main__: train()几点说明上面的ActionNet为了演示做了极大简化。真实场景中每个动作候选包含叶子索引、连接文字索引应该把这些信息拼进输入而不是只用一个全局 state pool 打分。action_masks的作用是屏蔽非法动作。因为动作候选数量在每个状态不同训练时需要按 batch 内最大动作数补齐。行为克隆的监督信号是“专家是否选择该动作”所以用二分类交叉熵。6.4 推理时的搜索循环训练结束后模型需要作为策略头接回证明器的搜索循环。下面演示一个通用搜索骨架重点是展示如何用模型输出分值来选择动作并保留回溯能力。# search_loop.py import torch def choose_action_with_policy(model, state_ids, action_masks): model.eval() with torch.no_grad(): scores model(state_ids.unsqueeze(0), action_masks.unsqueeze(0)) probs torch.softmax(scores, dim-1).squeeze(0) # 简单策略取最大概率的合法动作也可以按概率采样增加探索 return int(torch.argmax(probs).item()) def run_search(problem, model, max_depth100): 把模型策略接入搜索循环的最小演示。 root init_tableau_from_problem(problem) # 需要由你的证明器实现 stack [(expand, root, 0)] for _ in range(max_depth): action_type, node, depth stack.pop() if action_type expand: state_tokens serialize_tree_to_ids(root) # token - id candidates build_action_candidates(root, problem.literals) action_masks build_mask(candidates) action_idx choose_action_with_policy(model, state_tokens, action_masks) # 执行动作修改证明树 apply_action(root, candidates[action_idx]) if is_proof_complete(root): return proved elif action_type backtrack: rollback(root) if depth max_depth: return timeout return timeout这个循环的核心要点是模型只负责输出动作候选的优先级证明器仍然负责符号约束的正确性。如果某条路走不通搜索循环可以回溯到上一个决策点换一个概率次优的动作继续尝试。因此即便模型不是完美专家整体证明能力也不会被单步错误一票否决。7. 运行效果与验证方法7.1 训练与推理命令假设你按上面的脚本结构保存了文件并且已经准备了data/traces.json运行流程是python train_bc.py python run_experiment.py --model action_net.pt --data data/problems/run_experiment.py需要你自己补齐测试集加载和指标统计逻辑。下面是一个最小评估脚本示例python eval_bc.py \ --model action_net.pt \ --expert_prover ./baseline_prover \ --test_problems data/test_problems \ --timeout 107.2 需要观察哪些指标指标含义建议训练 loss行为克隆损失是否持续下降正常应降到 0.1 以下动作预测准确率模型预测与专家选择是否一致不能只看这个它不代表证明能力证明成功率测试问题中能证明的比例核心指标与基线证明器对比平均搜索步数单问题平均展开次数策略有效时通常比专家更短平均回溯次数单问题平均回退次数策略差时回溯次数会大幅上升最重要的判断不是模型拟合得多好而是“接入模型后证明器在同样时间预算下能否证明更多问题”。如果 loss 降得很低但证明率没有提升问题大概率出在状态编码丢失了信息或者推理时的动作生成逻辑与训练时不一致。7.3 失败时的排查起点如果接入模型后证明率反而下降第一步不要调模型先做两件事确认训练数据的动作候选空间与推理时一致确认状态序列化在训练和推理时完全一致。我最常遇到的情况就是推理时的候选动作中混入了训练时不会出现的动作类型导致模型打分失去可比性。第二步是打印一个具体问题的前二十步人工看每一步的候选集合和模型选择的动作通常很快能定位到状态表示或动作生成的问题。8. 常见问题与排查方法问题现象可能原因排查方式解决方案训练 loss 下降但证明率不高状态编码丢失关键结构信息打印序列化后的 token 与专家状态对比增加树深度、叶子位置、已闭合状态等 token动作候选数量波动太大batch 补零严重候选生成未合理约束统计候选数分布为动作筛选增加合法性约束或按树深度分桶训练同样的状态在训练和推理时 token 不一致序列化遍历顺序不稳定对同一问题复现多次比较 token 序列固定 BFS/DFS 顺序禁止依赖字典序做遍历模型对某些动作类别不敏感动作样本不均衡查看每个动作类型的出现频率对少数类做重采样或调整损失函数权重搜索频繁回溯但结果很差模型输出概率没有区分度查看 softmax 后概率分布是否均匀减少动作候选数量让候选间差异变大专家轨迹中有冲突动作不同证明器轨迹混合检查专家来源和记录时间一个策略只对应一个专家源或按规则统一9. 最佳实践与工程建议第一专家数据质量优先于数据量。收集轨迹时不要一刀切全收优先保留那些搜索步数较短、回溯次数较少的问题。你可以在日志里标记每个问题的最终状态之后用solvedtrue且回溯次数低于中位数的轨迹作为训练集。好的专家轨迹比大量绕路的轨迹学习效率高得多。第二状态编码要区分“已闭合分支”和“待扩展叶子”。我见过不少实现把整棵证明树原样传给网络导致序列长度快速增加、有效信号被大量闭合分支的噪声淹没。更稳的做法是在序列化时把已闭合子树折叠成单个[CLOSED]token让模型把注意力集中在还开放的叶子上。如果你的树很大这几乎是必需的裁剪手段。第三动作候选生成必须和训练数据生成使用同一套代码。这个问题最容易踩。训练时你用的是当时证明器给的候选列表推理时如果换了候选生成逻辑或过滤条件模型打分的语义就变了。建议把候选生成封装成一个独立模块在训练脚本和推理脚本中同时引用不要复制粘贴。第四保留符号搜索的回溯能力。模仿学习策略只是帮你把候选动作排序不需要也不应该替代证明器的回溯机制。哪怕模型概率排第一的动作最终失败循环仍然可以回到这个决策点尝试第二、第三动作。工程上不要把策略网络做成“唯一决策者”而是做成“候选动作重排序器”这样安全得多。第五考虑加入 DAgger 迭代。BC 最怕分布偏移而连接表证明器天然允许在线查询专家。训练一个初版策略后用它去跑一批新问题凡是模型搜索超时或失败的问题切回专家证明器重新跑一遍把新产生的轨迹加入训练集再训练。这样反复两三轮策略质量和泛化能力都会明显提升。第六记录实验元信息。建议为每次训练记录专家证明器版本、轨迹过滤规则、状态编码版本、候选生成版本。因为连接表方向迭代特别快过一个月回看实验结果经常不知道某个指标对应的是哪版状态表示。一份简单的 YAML 元信息文件可以帮你省下大量对实验的时间。10. 总结与后续学习方向这篇文章主要澄清了一个容易被忽视的事实连接表的高效性并不来自演算本身而来自“如何选择叶子与连接”的策略。模仿学习为这个选择问题提供了一条比手工启发式和纯强化学习都更可控的技术路径——你不需要设计奖励只需要让证明器留下搜索日志然后用行为克隆把“专家的下一步选择”变成可复用的策略网络。如果你手头已经有能跑通的证明器下一步可以这样实践先花一天时间给它加上轨迹日志然后选一个小规模问题集收集几百条优质轨迹训练一个很小的策略网络最后把这个网络作为候选动作重排器接回搜索循环对比接入前后的证明率和平均搜索步数。这个最小闭环能跑通再考虑做 DAgger 迭代、更换更强的网络编码器、或者引入图神经网络直接编码证明树的结构。连接表与模仿学习的结合本质上是符号搜索与数据驱动策略的一次分工符号引擎负责保证逻辑正确数据驱动模型负责提供高质量的搜索引导。真正值得深入的方向不是把证明器整个替换成神经网络而是研究如何让两者在接口、状态表示、训练反馈三个层面上配合得更紧密。