连接表证明器与模仿学习：从专家轨迹学习叶子与连接选择策略

自动定理证明（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 连接表对搜索策略的独特要求

连接条件把每一步的动作空间从“所有可用公式”压缩成“与当前叶子互补的文字所在的公式”，这很好；但动作空间压缩不等于不需要决策。树里可能有多个叶子，每个叶子可能有多个候选互补文字，引擎还得决定搜索顺序。更麻烦的是，连接表搜索经常遇到“局部看似乎正确，但沿某个连接展开若干步后证明失败”的情况，这时必须能高效回溯。所以连接表证明器的性能瓶颈集中在两处：

• 叶子选择顺序。
• 候选连接的优先级。

这两件事用人工启发式来做，总是顾此失彼；用数据驱动的方式直接拟合专家选择，则是模仿学习最擅长的场景。

3. 模仿学习：为什么适合连接表构建

3.1 强化学习在这个场景的天然难点

很多神经证明器把策略网络接在搜索循环上，训练目标想用强化学习，直觉上也很顺：证明成功给正奖励，超时给负奖励，反复试错。但实际落地有几个非常棘手的问题：

• 动作空间是动态的。每一步可选动作取决于当前证明树的形状，不能像围棋那样用固定棋盘动作空间。
• 奖励稀疏。绝大多数搜索路径都以失败或超时告终，探索到正奖励的概率极低。
• 搜索路径很长。一个中等问题的证明可能需要几十到上百步，即使最终成功，哪一步真正起决定性作用也很难定位。

所以纯强化学习训练神经证明器大多需要专家数据做预热，本质上是“先把专家策略学到手，再微调探索”。

3.2 行为克隆与 DAgger

模仿学习解决的是“从专家演示学习策略”的问题。最基础的方法是行为克隆（Behavior Cloning，BC）：把专家轨迹拆成一组组“状态-动作”样本，然后训练一个分类或回归模型，让模型输出的动作分布贴近专家选择。BC 最大的优点是实现简单，数据准备好后就是一个监督学习问题；最大的缺点是分布偏移——训练时模型见到的状态来自专家轨迹，推理时则来自自己的策略，一旦模型的早期动作偏离专家，后面见到的状态就会脱离训练分布。

针对分布偏移，DAgger 的思路是让学习策略在环境中探索，遇到新状态时重新向专家查询标签，把新样本加入训练集迭代优化。在定理证明场景里，专家证明器始终在线可调用，所以 DAgger 的“查询专家”步骤不需要额外人工标注，实现成本比一般机器人场景低很多。

3.3 连接表构建为什么是模仿学习的好目标

有三个原因：

1. 专家数据天然存在。任何能跑通的连接表证明器都留下了完整的搜索日志，包括候选集合和当前步的最终选择。
2. 动作空间可枚举。连接表的候选动作就是“叶子编号 + 连接候选编号”，可以结构化成离散监督信号。
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 python=3.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_factory=list) # 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_size=300, embed_dim=64, num_layers=2, num_heads=4): super().__init__() self.embedding = nn.Embedding(vocab_size, embed_dim) encoder_layer = nn.TransformerEncoderLayer( d_model=embed_dim, nhead=num_heads, batch_first=True ) self.encoder = nn.TransformerEncoder(encoder_layer, num_layers=num_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(dim=1) # [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"], dtype=torch.long), "action_masks": torch.tensor(s["action_masks"], dtype=torch.float), "labels": torch.tensor(s["labels"], dtype=torch.float), } def load_traces(json_path: str): """从专家轨迹 JSON 中加载并转换成向量样本。""" samples = [] with open(json_path, "r", encoding="utf-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_size=32, shuffle=True) model = ActionNet() optimizer = torch.optim.AdamW(model.parameters(), lr=1e-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(f"epoch {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()

几点说明：

1. 上面的ActionNet为了演示做了极大简化。真实场景中，每个动作候选包含叶子索引、连接文字索引，应该把这些信息拼进输入，而不是只用一个全局 state pool 打分。
2. action_masks的作用是屏蔽非法动作。因为动作候选数量在每个状态不同，训练时需要按 batch 内最大动作数补齐。
3. 行为克隆的监督信号是“专家是否选择该动作”，所以用二分类交叉熵。

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_depth=100): """把模型策略接入搜索循环的最小演示。""" 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 10

7.2 需要观察哪些指标

最重要的判断不是模型拟合得多好，而是“接入模型后，证明器在同样时间预算下能否证明更多问题”。如果 loss 降得很低但证明率没有提升，问题大概率出在状态编码丢失了信息，或者推理时的动作生成逻辑与训练时不一致。

7.3 失败时的排查起点

如果接入模型后证明率反而下降，第一步不要调模型，先做两件事：确认训练数据的动作候选空间与推理时一致；确认状态序列化在训练和推理时完全一致。我最常遇到的情况就是推理时的候选动作中混入了训练时不会出现的动作类型，导致模型打分失去可比性。第二步是打印一个具体问题的前二十步，人工看每一步的候选集合和模型选择的动作，通常很快能定位到状态表示或动作生成的问题。

8. 常见问题与排查方法

9. 最佳实践与工程建议

第一，专家数据质量优先于数据量。收集轨迹时不要一刀切全收，优先保留那些搜索步数较短、回溯次数较少的问题。你可以在日志里标记每个问题的最终状态，之后用solved=true且回溯次数低于中位数的轨迹作为训练集。好的专家轨迹比大量绕路的轨迹学习效率高得多。

第二，状态编码要区分“已闭合分支”和“待扩展叶子”。我见过不少实现把整棵证明树原样传给网络，导致序列长度快速增加、有效信号被大量闭合分支的噪声淹没。更稳的做法是在序列化时把已闭合子树折叠成单个[CLOSED]token，让模型把注意力集中在还开放的叶子上。如果你的树很大，这几乎是必需的裁剪手段。

第三，动作候选生成必须和训练数据生成使用同一套代码。这个问题最容易踩。训练时你用的是当时证明器给的候选列表，推理时如果换了候选生成逻辑或过滤条件，模型打分的语义就变了。建议把候选生成封装成一个独立模块，在训练脚本和推理脚本中同时引用，不要复制粘贴。

第四，保留符号搜索的回溯能力。模仿学习策略只是帮你把候选动作排序，不需要也不应该替代证明器的回溯机制。哪怕模型概率排第一的动作最终失败，循环仍然可以回到这个决策点尝试第二、第三动作。工程上不要把策略网络做成“唯一决策者”，而是做成“候选动作重排序器”，这样安全得多。

第五，考虑加入 DAgger 迭代。BC 最怕分布偏移，而连接表证明器天然允许在线查询专家。训练一个初版策略后，用它去跑一批新问题，凡是模型搜索超时或失败的问题，切回专家证明器重新跑一遍，把新产生的轨迹加入训练集再训练。这样反复两三轮，策略质量和泛化能力都会明显提升。

第六，记录实验元信息。建议为每次训练记录：专家证明器版本、轨迹过滤规则、状态编码版本、候选生成版本。因为连接表方向迭代特别快，过一个月回看实验结果，经常不知道某个指标对应的是哪版状态表示。一份简单的 YAML 元信息文件，可以帮你省下大量对实验的时间。

10. 总结与后续学习方向

这篇文章主要澄清了一个容易被忽视的事实：连接表的高效性并不来自演算本身，而来自“如何选择叶子与连接”的策略。模仿学习为这个选择问题提供了一条比手工启发式和纯强化学习都更可控的技术路径——你不需要设计奖励，只需要让证明器留下搜索日志，然后用行为克隆把“专家的下一步选择”变成可复用的策略网络。

如果你手头已经有能跑通的证明器，下一步可以这样实践：先花一天时间给它加上轨迹日志；然后选一个小规模问题集，收集几百条优质轨迹，训练一个很小的策略网络；最后把这个网络作为候选动作重排器接回搜索循环，对比接入前后的证明率和平均搜索步数。这个最小闭环能跑通，再考虑做 DAgger 迭代、更换更强的网络编码器、或者引入图神经网络直接编码证明树的结构。

连接表与模仿学习的结合，本质上是符号搜索与数据驱动策略的一次分工：符号引擎负责保证逻辑正确，数据驱动模型负责提供高质量的搜索引导。真正值得深入的方向，不是把证明器整个替换成神经网络，而是研究如何让两者在接口、状态表示、训练反馈三个层面上配合得更紧密。