想象你刚接管一家中餐厅的后厨。柜子里堆满了历代大厨留下的菜谱——每一本都写清了食材和步骤，但你面前是六个同时开火的灶台，锅里咕嘟着不同状态的半成品。菜谱会告诉你“这道菜最终怎么做”，却不会告诉你“此刻该先管哪口锅、这一勺盐加在谁身上”。定理证明器 Coq 和 Isabelle 的处境，正像这位翻菜谱的新主厨：引理库、规则库一应俱全，能一丝不苟地验证每个步骤是否合法，却极度缺乏“现在该做什么”的临场判断。证明策略自动生成，就是为了给这台“有菜谱、没判断”的灶台，配上一个看过成千上万次操作记录的“帮厨大脑”。它从历史证明日志里偷师，在关键时刻提醒你“该爆炒这个目标了”“先拆分再归纳”“这条路走不通，换个手法”；还能把几招组合成全新套路。接下来，我们跟着这位帮厨大脑从备菜到出菜，依次看策略推荐、tactic 合成、证明引导、训练数据，以及它在 Coq 和 Isabelle 两套“厨房”里的表现。

岗位关联

掌握证明策略自动生成，能帮你设计更聪明的形式化验证工具——这正是 AI 在数学定理证明与软件验证领域从“演示”走向“交付”的核心技能。

目录
  1. 可视化演示
  2. 背景与动机
  3. 策略推荐
  4. Tactic 合成
  5. 证明引导
  6. 训练数据
  7. 评测对比
  8. 挑战与展望
  9. AI 应用场景
  10. Python 演示
  11. 常见误区
  12. 面试题

可视化演示

可视化定理证明的tactic搜索空间树展开、策略推荐/合成/引导三种方法对比及证明步骤状态转换，滑块调节搜索深度观察成功率变化。

本节配有交互动效（进入视口后自动加载，约 3KB）。

搜索空间：tactic树展开与回溯 根节点：初始证明目标(Goal) tactic分支：Induct/Simpl/Rewrite等策略 成功路径：绿色路径到达Qed闭合 失败分支：红色回溯剪枝 Search = BFS/DFS over Tactic Tree 深度学习引导减少搜索空间

背景与动机

新手主厨最怕的不是没有菜谱，而是“菜谱太多、局面太多”。定理证明器面对复杂定理时也一样：引理库有几万条，每一步可用的规则有几十条，而搜索空间却随证明深度指数膨胀。传统自动化只能靠人工预设的少量启发式规则——好比规定“凡是红烧一律先焯水”，遇到新菜式就失灵。这种“规则写死、无法应变”的困境，就是策略自动化的瓶颈所在。

传统策略的局限性集中在两点。其一，策略由人手工编写，覆盖不了所有目标形态；其二，固定顺序的尝试（先试 A 再试 B）缺少对具体局面的感知，常常在错误分支上耗尽时间。于是研究者把目光转向机器学习：把“选策略”本身当成一个可以学习的决策问题，从大量历史证明中自动总结“什么局面该用什么招”。这也正是“机器学习进场”的含义——不再由人教证明器怎么做，而是让证明器从数据中自己学会怎么做。

用数学语言说，证明策略自动生成就是学习一个“从证明状态到动作”的映射：给定当前目标与历史上下文，模型输出下一步行动的概率。这一视角把策略推荐、tactic 合成、证明引导统一到了同一个决策框架之下。

回头再看那位新主厨：他缺的不是更多菜谱，而是一个能“看锅下菜”的判断力。证明策略的自动生成，正是把这种判断力从历史数据里学出来、装进证明器里。

P(at∣gt,  ct)P(a_t \mid g_t,\; c_t)
这条式子定义了策略模型的核心命题：在时刻 \(t\)，面对目标 \(g_t\) 和已有上下文 \(c_t\)，模型认为选择动作 \(a_t\) 的把握有多大。
  1. 当前目标 \(g_t\)待证的命题在时刻 \(t\) 所处的状态，相当于锅中菜品的实时火候与形态，包括要证的结论和已有的假设。
    gtg_t
  2. 历史上下文 \(c_t\)从证明开始到目前为止使用过的目标与策略序列，相当于主厨已经完成的备菜和手法记录。
    ct=(g1, a1, …, gt−1, at−1)c_t = (g_1,\, a_1,\, \dots,\, g_{t-1},\, a_{t-1})
  3. 动作 \(a_t\)下一步要执行的具体 tactic，候选集合来自策略库这个“工具墙”。
    at∈Aa_t \in \mathcal{A}
  4. 概率 \(P\)模型对整个“按此动作推进能否成功”给出的置信度，取值在 0 到 1 之间。
    P(at∣gt,  ct)∈[0,1]P(a_t \mid g_t,\; c_t) \in [0,1]

策略推荐

帮厨大脑最基础的功夫是“报菜名”。主厨一犹豫，它就根据锅里状态报出三个选项：“这个目标适合先焯水（intro），那个适合直接收汁（assumption）”。策略推荐做的正是这件事：给每个证明状态推荐最可能奏效的下一步 tactic。

方法上最常用的是监督学习。从证明日志中抽取“目标-实际策略”配对样本，训练一个打分模型；线上推理时，模型对策略库里的每个候选 tactic 打分，取前几名作为建议。目标的结构特征——是全称命题还是等式、有没有嵌套的归纳类型——是模型判断的主要依据，这就是特征设计。进一步地，由于证明是多步决策，实践上会把推荐做成序列模型，让模型记住“这一步之前干过什么”，避免反复犯同样的错。

打分模型通常采用 softmax 形式输出概率分布：

报菜名听起来简单，却决定了整场后厨的走向——推荐准了，后面的合成、引导都轻松；推荐偏了，再好的搜索技巧也难以挽回。

P(a∣g)=exp⁡ ⁣(f(a,g))∑a′∈Aexp⁡ ⁣(f(a′,g))P(a \mid g) = \frac{\exp\!\big(f(a, g)\big)}{\displaystyle \sum_{a' \in \mathcal{A}} \exp\!\big(f(a', g)\big)}
它把“策略 \(a\) 对目标 \(g\) 的适配分数”转成一组概率：分数越高，被推荐的概率越大。所谓策略推荐，就是取其中概率最高的几个候选。
  1. 打分函数 \(f(a,g)\)用参数化模型衡量“策略 \(a\) 适配当前目标 \(g\)”的契合度，分数越高说明越对症。
    f(a,g)=wa⊤ϕ(g)f(a,g) = w_a^{\top}\phi(g)
  2. 指数化 \(\exp\)把任意实数分数变成正数并放大差异，让高分显得更突出，像把几个候选菜品的口碑差距拉开展示。
    exp⁡(f(a,g))\exp(f(a,g))
  3. 归一化分母把当前策略的分数放在“全部策略”的分数总和里一起比较，相当于把所有候选菜名排队后按支持率排名。
    ∑a′∈Aexp⁡(f(a′,g))\sum_{a' \in \mathcal{A}} \exp(f(a',g))
  4. 输出概率得到每个策略被推荐的概率，取最大者就是帮厨大脑给出的最终建议。
    P(a∣g)P(a \mid g)

Tactic 合成

有些菜不是单一手法能完成的：先改刀、再挂糊、最后大火快炒。菜谱上查不到“挂糊后转大火”的现成名词，但大厨可以现场组合出来。Tactic 合成做的正是这种组合创新——它不像推荐那样“从已有的招里选一招”，而是在策略空间之外组合甚至生成新的策略脚本。

技术上有两条路线。一条是组合搜索：把 tactic 视为积木，用束搜索在“长度有限、顺序可变”的组合空间里找一组能走通目标的脚本；另一条是生成式模型：直接学习从目标描述到策略脚本的映射，像让帮厨大脑对着目标状态“口述”一段完整操作。前者可解释、可枚举，后者更灵活、能应对未见过的组合模式。

无论哪条路线，生成出来的脚本都不能直接采信，必须放进证明器真实执行一遍，这就是验证过滤。验证失败的组合被丢弃，验证成功的组合会作为新样本回流到训练数据，形成“生成—验证—再学习”的闭环。

合成相当于给后厨添新菜——它把零散手法组合成可复用的“新招式”，大大扩展了策略库的边界，让证明器不再受限于人工写死的几条套路。

a∗=arg⁡max⁡π  log⁡P(π∣g)s.t.  verify(π, g)=成功a^{*} = \arg\max_{\pi}\; \log P(\pi \mid g) \quad \text{s.t.}\ \ \mathrm{verify}(\pi,\,g)=\text{成功}
合成目标是在“能被证明器验证通过”的约束下，找到概率最高（最像人类写法）的策略脚本。
  1. 候选脚本 \(\pi\)由若干 tactic 按顺序拼成的策略脚本，相当于一套临场设计好的操作流程。
    π=(a1,a2,…,ak)\pi = (a_1, a_2, \dots, a_k)
  2. 生成概率模型逐字展开脚本的概率，反映“这套组合看起来多像大厨的惯用手法”。
    log⁡P(π∣g)=∑i=1klog⁡P(ai∣g,a<i)\log P(\pi\mid g)=\sum_{i=1}^{k}\log P(a_i\mid g, a_{<i})
  3. 验证约束把脚本放进证明器真实执行，只有完整走通才算数，避免“纸上谈兵”。
    verify(π,g)∈{成功,失败}\mathrm{verify}(\pi, g)\in\{\text{成功},\text{失败}\}
  4. 最优选择在满足验证约束的前提下，挑生成概率最高的脚本作为最终合成结果。
    arg⁡max⁡π  log⁡P(π∣g)\arg\max_{\pi}\; \log P(\pi \mid g)

证明引导

真正的后厨调度远不止报菜名：六口锅同时在烧，哪口锅先出锅、哪口锅先灭火、哪口锅糊了要立刻重做。证明引导解决的就是这种“全局调度”问题——它不判断单步用什么招，而是决定整个证明过程的探索节奏。

把证明过程视作一棵搜索树：节点是中间证明状态，边是一次 tactic 应用。每扩展一个节点，策略模型就给它打一个“成功希望”分，搜索器优先扩展高分节点，这就是目标排序与搜索树剪枝。低分分支并不会被永久丢弃，而是保留为备选；当高分分支走到死胡同时，系统回退到次优节点重新尝试，这就是失败回退机制。

单纯追求“希望分”会让搜索在一条深不见底的路上越走越远，所以实践中会在评分中加入深度惩罚——既敢钻牛角尖，又不会真的钻进牛角尖出不来。

引导就像大厅与后厨之间的枢纽——它把推荐的每一招、合成的每一道组合串联成有序的出菜节奏，保证整套后厨不慌不乱地完成整桌宴席。

priority(s)=P(succeed∣s)−λ⋅depth(s)\mathrm{priority}(s) = P(\mathrm{succeed}\mid s) - \lambda\cdot \mathrm{depth}(s)
节点 \(s\) 的扩展优先级 = 模型估计的成功概率 − 深度惩罚。这样既能优先探索有希望的分支，又能及时从无底洞中抽身。
  1. 节点状态 \(s\)搜索树中的一个中间证明状态，包含当前目标和已用假设。
    s∈Ss\in\mathcal{S}
  2. 成功概率模型估计从该状态出发能证完的概率，是“这口锅还值不值得守”的判断。
    P(succeed∣s)P(\mathrm{succeed}\mid s)
  3. 节点深度从根到该状态的步数，越深代表已经投入越多时间，越要警惕空耗。
    depth(s)\mathrm{depth}(s)
  4. 权衡系数 \(\lambda\)控制“敢不敢继续深挖”与“会不会钻牛角尖”的平衡，通常通过实验调参确定。
    λ>0\lambda > 0
  5. 优先级得分最高的节点先被扩展；失败时按照得分顺序回退重试，形成完整的引导循环。
    priority(s)\mathrm{priority}(s)

训练数据

帮厨大脑再聪明，也得有老师可偷师。老师们的操作记录——证明日志——就是训练数据。没有这些日志，所谓“从历史证明中学习”就无从谈起，这正是训练数据在整套方法中的奠基地位。

大规模证明库提供了海量可挖掘的证明脚本。把每个证明步骤展开成“执行前的目标状态 + 执行的策略”配对，就得到了监督样本。但日志往往很“脏”：变量命名随意、中间状态重复、大量证明风格不一致，直接灌给模型只会学到噪声。所以第一步是清洗与对齐——统一变量命名、剔除冗余步骤，让样本彼此可比。

样本干净之后，还要通过数据增强提升鲁棒性：变量重命名、目标形态扰动、假设顺序打乱等，都是常见的增广手段。对于只出现几次的长尾稀有技巧，盲目堆数据没有用，借助少样本学习或元学习，让模型从极少例子中抓住要领，反而更有效。

数据像学徒的练手次数——量的积累与质的清洗缺一不可。干净、多样、标注对齐的日志，才能养出一位火候精准的帮厨大脑。

L(θ)=−1N∑i=1Nlog⁡Pθ(ai∣gi)\mathcal{L}(\theta) = -\frac{1}{N}\sum_{i=1}^{N} \log P_{\theta}(a_i \mid g_i)
这是监督学习的交叉熵损失：模型在全部训练样本上“预测得越准，损失越小”。优化器通过最小化它来拟合大厨们的决策模式。
  1. 数据集从证明日志抽取的 \(N\) 个“目标-策略”配对样本，是学徒反复揣摩的练习册。
    D={(g1,a1),…,(gN,aN)}\mathcal{D} = \{(g_1,a_1),\dots,(g_N,a_N)\}
  2. 对数似然模型对“在目标 \(g_i\) 下真实使用了 \(a_i\)”给出的对数概率，越接近真实行为越大。
    log⁡Pθ(ai∣gi)\log P_{\theta}(a_i\mid g_i)
  3. 取平均求负对所有样本求平均并加负号，相当于厨师长统计整批学徒的平均失误率。
    −1N∑i=1Nlog⁡Pθ(ai∣gi)-\frac{1}{N}\sum_{i=1}^{N}\log P_{\theta}(a_i\mid g_i)
  4. 最小化目标优化器调整参数 \(\theta\) 使损失不断下降，模型逐步逼近“大厨的判断力”。
    θ∗=arg⁡min⁡θL(θ)\theta^{*} = \arg\min_{\theta} \mathcal{L}(\theta)

评测对比

Coq 和 Isabelle 是两家灶台完全不同的厨房：一个讲究战术脚本的直火快炒，一个提供“工具皮带”并与外部求解器联动。同一套策略模型搬过去，就像川菜大厨空降西餐后厨，总要花时间重新适应工具和术语。

评测方法上，研究者通常先选定统一基准测试集——比如数学问题基准 miniF2F 这类包含大量标准定理的集合，或者针对证明库迁移设计的任务集——让不同方法在同一批“考题”上比拼。只看成功率还不够，因为暴力搜索也能碰巧做对；所以还要同时报告平均搜索步数、运行时间等开销指标。

实际效果呈现明显差异：在 Coq 上，策略推荐与合成对 induction、lia、auto 这类组合型策略提升显著，因为 Coq 生态本身就高度依赖 tactic 组合；在 Isabelle 上，模型需要与 sledgehammer 等外部自动化工具协作，策略模型更多负责判断“何时调用外部工具、如何利用其结果”——性能取决于协作设计是否巧妙。

两家厨房各有脾气——评测的意义不是争谁强，而是认清“你的模型该为哪套灶台优化”，并据此选择合适的技术路线。

成功率=1M∑j=1M1 ⁣[证完(gj)]\text{成功率} = \frac{1}{M}\sum_{j=1}^{M} \mathbb{1}\!\big[\text{证完}(g_j)\big]
成功率 = 被策略系统完整证明的目标数 ÷ 测试目标总数。它衡量的是“整道菜能否完整出锅”，而非单步手法是否正确。
  1. 测试目标集基准测试中待证明的 \(M\) 个目标，是统一的“考卷”。
    Gtest={g1,…,gM}\mathcal{G}_{\text{test}}=\{g_1,\dots,g_M\}
  2. 指示函数目标被完整证明记 1，否则记 0，像收菜时“出锅算一盘，糊了不计数”。
    1[证完(gj)]∈{0,1}\mathbb{1}[\text{证完}(g_j)]\in\{0,1\}
  3. 平均求和对所有目标的指示值取平均，即“多少道菜完整端上了桌”。
    1M∑j=1M1[证完(gj)]\frac{1}{M}\sum_{j=1}^{M}\mathbb{1}[\text{证完}(g_j)]
  4. 口径说明成功率只反映“能不能做出来”，还需配合搜索步数与耗时一起看，才能评价帮厨大脑是否真高效。
    成功率∈[0,1]\text{成功率}\in[0,1]

挑战与展望

帮厨大脑最怕的是新菜式：训练时没见过的新结构、新材料，会让经验瞬间失灵。这种“训练分布之外”的泛化难题，是所有策略自动生成方法都必须面对的硬骨头。

当前挑战主要集中在三处。其一是泛化难题：模型在训练时没见过的数学命题上，成功率往往骤降；其二是可解释性：模型推荐“用 induction 而不是 destruct”，却说不清理由，人类难以信任和调试；其三是跨助手迁移：Coq 上练好的模型很难直接用于 Isabelle，需要做领域适配甚至重新设计表示。这三个问题相互牵连，短期内没有银弹。

展望未来，几条路径值得期待。大语言模型可以承担“自然语言描述 → 形式化策略”的翻译，让数学家能够用日常语言指挥证明器；强化学习直接用“证明成功”这一稀疏奖励来优化策略选择，减少对人工标注的依赖；人机协作模式下，模型提供候选、人类做最终裁决——策略自动生成正从“辅助推荐”走向“半自动证明工程师”。

后厨的故事还在继续：帮厨大脑终有一天能独当一面，但真正的好菜，仍然离不开主厨懂得“何时相信机器、何时亲手兜底”。

R新=1∣GNew∣∑g∈GNewPθ(证完∣g)R_{\text{新}} = \frac{1}{|\mathcal{G}_{\text{New}}|}\sum_{g\in\mathcal{G}_{\text{New}}} P_{\theta}(\text{证完}\mid g)
泛化成功率 = 模型在“从未见过的新问题”上的平均证完概率。它衡量的是换一批菜，帮厨大脑还灵不灵。
  1. 新问题集合训练分布之外的全新命题，像后厨突然接到的创新菜订单。
    GNew\mathcal{G}_{\text{New}}
  2. 单题把握模型对单个新目标的完成概率，体现它对“陌生局面”的适应能力。
    Pθ(证完∣g)P_{\theta}(\text{证完}\mid g)
  3. 平均泛化能力对所有新问题求平均，衡量“经验迁移”的整体表现。
    1∣GNew∣∑g∈GNewPθ(证完∣g)\frac{1}{|\mathcal{G}_{\text{New}}|}\sum_{g\in\mathcal{G}_{\text{New}}}P_{\theta}(\text{证完}\mid g)

AI 应用场景

IDE 里的实时策略推荐助手

阶段：策略推荐（监督学习打分模型）

解决的问题：形式化证明新手面对复杂目标常“不知道下一步干什么”，反复查文档、手动试错效率极低。传统 IDE 只能提示语法，无法提示“数学上该往哪走”。策略推荐模型根据当前目标结构与历史上下文，实时推荐 top-3 tactic 并标注置信度，把“翻菜谱”变成“报菜名”，大幅降低入门门槛。

具体案例：一位维护数学形式化库的工程师在 Coq 中证明“自然数乘法分配律”，目标含全称量词与归纳类型。插件识别后推荐 intros; induction n; simpl; auto 的策略片段并给出置信度，工程师一键应用，原先 10 分钟的试错缩短到 10 秒。

大规模证明库的自动补全流水线

阶段：证明引导 + Tactic 合成

解决的问题：把经典教材定理迁移进证明库时，成百上千个“简单但琐碎”的目标需要逐个手动证明，人工成本极高。传统做法是每个目标单独写脚本，而证明引导与合成可以把“验证过滤”作为质检关卡，自动完成大批量目标。

具体案例：某研究组在 Isabelle 中迁移数学分析章节，对剩余 800 个未证明目标批量生成策略脚本，经 sledgehammer 等外部工具协同验证后，约 62% 的目标自动完成，其余交给人类处理，项目整体工期缩短一半。

Python 演示

python57 行
# -*- coding: utf-8 -*-"""策略推荐演示: 从证明脚本日志中学习 tactic 转移规律"""import refrom collections import Counter, defaultdict PROOFS = [    "intros; induction n; simpl; auto",    "intros; destruct H; auto",    "intros; induction n; simpl; lia",    "intros; split; auto",    "intros; induction n; simpl; auto",    "intros; destruct b; auto",    "intros; induction n; simpl; ring",    "intros; split; [auto | omega]",]  def tokenize(script):    """把证明脚本拆成 tactic 列表"""    parts = re.split(r'[;\[\],]|\s+', script.strip())    return [p.strip() for p in parts if p.strip()]  def build_model(logs, n=2):    """n 元语法: 学习 前 n-1 个 tactic -> 下一个 tactic 的计数"""    counts = defaultdict(Counter)    for script in logs:        seq = tokenize(script)        for i in range(len(seq) - n + 1):            cntx = tuple(seq[i:i + n - 1])            nxt = seq[i + n - 1]            counts[cntx][nxt] += 1    return counts  def recommend(model, cntx):    """给定上下文, 推荐下一个 tactic"""    if cntx in model:        return model[cntx].most_common()    if cntx[-1:] in model:        return model[cntx[-1:]].most_common()    return []  def main():    model = build_model(PROOFS, n=2)    print("已从 %d 条证明日志中学习策略转移规律" % len(PROOFS))    test = ["intros", "induction n"]    hits = recommend(model, tuple(test))    print("当前上下文: %s" % " ; ".join(test))    print("推荐下一个 tactic (按次数):")    for tactic, cnt in hits[:3]:        print("  - %s (出现 %d 次)" % (tactic, cnt))  if __name__ == "__main__":    main()
目的：用 n-gram 计数模型从证明脚本日志中学习“上下文 → 下一个 tactic”的转移规律，并针对给定上下文输出策略推荐——这是策略推荐最简单可运行的雏形。
  1. counts = defaultdict(Counter)为每个上下文准备一个计数器，统计其后出现过的 tactic。
  2. for i in range(len(seq) - n + 1):用滑动窗口扫描整条证明脚本，截取连续的“上文-下文”片段。
  3. counts[cntx][nxt] += 1记录“上文 → 下文”的转移计数，这是模型全部知识的来源。
  4. return model[cntx].most_common()按出现次数排序，把最常被“大厨”采用的 tactic 排在最前。
  5. hits = recommend(model, tuple(test))给定当前已用策略 intros; induction n，让模型给出下一步推荐。
  6. if __name__ == "__main__":保证模块既可被导入调用，也能直接运行演示。

常见误区

误区很多人以为用机器学习就能让模型“从零发明”全新的证明策略，像人类数学家那样天马行空地创造前所未见的思路。

正解绝大多数系统是在既有 tactic 的组合空间里做推荐与合成，学的是“何时用哪一招、怎么把招组合起来”，而不是无中生有。这就像帮厨大脑学会把焯水、改刀、爆炒组合成新菜，但每招每式都来自既有后厨传统。所谓“生成”，本质是“决策自动做对”，而非“手艺凭空创造”。

为何常见：“生成”一词天然暗示创造力，加上媒体常用“AI 证明定理”渲染全能感，容易让人脑补出一位机器数学家。

误区觉得只要把几十万条证明日志直接灌进模型，模型自然会变强，堆数据就能解决一切。

正解证明日志高度冗余，大量重复套路加上少数长尾技巧；若不先清洗、对齐、去重，模型只会背下常见模式，对稀有目标形态依旧无感。去掉重复样本、扰动目标形态、补足少样本技巧，往往比单纯加数据更有效。数据不是越多越好，而是越“干净多样”越好。

为何常见：CV/NLP 领域“数据量即正义”的直觉深入人心，被直接套用到定理证明上，忽略了证明数据的结构化与长尾特性。

误区策略推荐模型 top-1 准确率达到 80%，就认为它能证明 80% 的定理。

正解推荐准“下一步”只解决单步问题；证明是一条多步链路，一步偏了需要回退、换招、重搜。评估系统必须看“完整证明成功率”以及搜索步数和耗时，而不能只看单步推荐准确率。单步准确率高，可能只是因为它擅长猜中常见的开头几步。

为何常见：学术界常用 accuracy 这类简单指标，让人误把单步正确率当成整局胜率，就像只看刀工就判断整桌菜好吃。

误区既然都是定理证明器，在 Coq 上练好的策略模型换个接口就能在 Isabelle 上跑。

正解两个证明助手的 tactic 语言、逻辑内核、标准库与目标表示差异巨大，学到的特征很难直接复用。直接迁移效果通常很差，需要做领域适配、跨语言建模，甚至把外部求解器纳入协作设计。这就像川菜大厨空降西餐后厨，刀具、灶台、术语全得重新适应。

为何常见：深度学习“预训练+微调”的通用性口碑被过度外推，忽视了形式化工具链之间深刻的异构性。

面试题

Q1. 证明策略自动生成的核心目标是什么？

单选题 · easy

  • A.取代人类数学家独立提出新公理
  • B.从历史证明中学习并自动选择策略组合← 正确答案
  • C.让编译器自动修复所有代码语法错误
  • D.把自然语言论文自动翻译成形式化证明

答案：B。核心目标是让证明器学会“何时用哪一招”，即从历史证明中学到策略选择的临场判断。A 是“发明新数学”的夸大说法；C、D 分别是编译器和翻译任务，与策略选择无关。好比帮厨大脑的本分是报菜名，而不是改写菜谱。

Q2. 策略推荐最常用的建模方式是？

单选题 · mid

  • A.把证明过程视为序列决策，预测下一步策略← 正确答案
  • B.用随机搜索穷举所有可能的证明策略
  • C.用正则表达式直接匹配代码仓库中的模式
  • D.用 SQL 查询证明状态数据库得到结果

答案：A。策略推荐把“当前目标+历史上下文”映射到“下一个 tactic”，本质上是序列决策下的监督学习。随机搜索只是暴力备选手段，不是建模方式；正则与 SQL 都无法理解目标结构的语义，自然无法给出有泛化能力的推荐。

Q3. 策略推荐与 tactic 合成最关键的区别是？

单选题 · mid

  • A.合成是在既有策略空间外组合生成新策略← 正确答案
  • B.合成负责解释推荐负责执行证明过程
  • C.合成只适用于 Isabelle 推荐只用于 Coq
  • D.两者本质相同只是不同论文里的叫法

答案：A。推荐是从策略库里选已有招式；合成是把招式组合或直接生成新脚本，并且要经过验证器过滤。B、C、D 都把两者混为一谈，实际上它们解决的问题不同、技术路线也不同。

Q4. 证明引导阶段通常会做哪些操作？

多选题 · mid

  • A.对搜索树剪枝，跳过注定失败的分支← 正确答案
  • B.对子目标排序，优先攻克简单的目标← 正确答案
  • C.利用失败试错信号动态调整搜索策略← 正确答案
  • D.直接修改数学公理以保证命题可证

答案：ABC。剪枝、目标排序、失败回退是证明引导的三个核心动作，像主厨安排出菜顺序并准备补救预案。D 修改公理相当于“改题”，是作弊行为，不属于证明引导的范畴。

Q5. 策略模型的训练数据主要来自哪里？

单选题 · mid

  • A.由人工为每个目标手写下一步建议标注
  • B.从已有证明脚本中抽取目标与策略的配对← 正确答案
  • C.随机生成大量不可证明的命题作为样本
  • D.从百科词条爬取数学知识作为训练语料

答案：B。证明日志天然包含“目标状态 → tactic”的配对，几乎零成本获得海量监督信号。人工标注成本过高且难规模化；随机命题大多不可证明，无法作为有效正样本；百科词条与证明器内部状态格式完全不兼容。

Q6. 跨证明助手迁移策略模型时，最根本的障碍是？

单选题 · hard

  • A.两者的策略语言逻辑内核与标准库差异大← 正确答案
  • B.因为 Isabelle 没有提供机器学习接口
  • C.因为 Coq 的证明速度比 Isabelle 快得多
  • D.Isabelle 不支持形式化数学定理证明

答案：A。Coq 与 Isabelle 的 tactic 语言、逻辑内核、标准库差异巨大，“目标表示”无法直接对齐，模型学到的特征难以复用。B、C、D 都是事实错误——Isabelle 不仅支持形式化证明，还拥有丰富的自动化工具链。

Q7. 强化学习在证明策略生成中的作用是？

单选题 · hard

  • A.用成功的稀疏奖励反向优化证明策略选择← 正确答案
  • B.用强化学习替代所有底层证明搜索算法
  • C.强化学习只用于压缩证明日志存储空间
  • D.强化学习负责把证明翻译成自然语言解释

答案：A。证明成功与否是稀疏但明确的奖励信号，强化学习可以据此优化“先探索哪个节点、用哪个策略”的决策。它是对搜索的引导而非替代；压缩日志、翻译解释都不是强化学习在该领域的主要职责。

Q8. 评估策略自动生成系统时，合理的做法包括？

多选题 · hard

  • A.在统一基准测试集上对比证明成功率指标← 正确答案
  • B.同时报告平均搜索步数与计算资源开销← 正确答案
  • C.分别在 Coq 与 Isabelle 上考察迁移效果← 正确答案
  • D.只看推荐准确率因为这是唯一重要指标

答案：ABC。成功率、资源开销、跨平台表现构成完整评估体系；只看 top-1 准确率会高估单步能力而忽视整局成败。好比一道菜好不好吃要看最终成菜，而不是只看刀工是否标准。

Q9. 证明搜索树中“死胡同分支”指的是？

单选题 · easy

  • A.应该继续深入探索的最大希望最优分支
  • B.已尝试但无法再向前推进的证明分支← 正确答案
  • C.必须被保留用于回溯的根状态节点
  • D.只能交给人类数学家手工证明的分支

答案：B。死胡同分支是尝试展开后发现所有子目标都无法继续（如归纳假设用不上、规则不匹配）并被标记失败的分支。根节点是起点而非死胡同；没有证据表明只有人类能处理那些分支，策略模型也能学会绕开。

Q10. 以下哪些属于证明策略自动生成的技术路线？

多选题 · easy

  • A.监督学习方式训练策略推荐分类模型← 正确答案
  • B.组合搜索与生成式模型实现策略合成← 正确答案
  • C.用搜索引导与失败回退优化证明过程← 正确答案
  • D.用数据库索引加速查询引理库的代码

答案：ABC。推荐、合成、引导三大技术路线正好对应“报菜名—组合新招—全局调度”。数据库索引属于工程优化手段，不属于策略生成的研究路线，因此 D 不选。