What are the Right Symmetries for Formal Theorem Proving?

先讲一个故事

教学性场景（非论文记载）：设 Lean 证明助手旁有位自动证明系统 Mira。它能证明命题“20! 与 200000 的 gcd 是 40000”，却在只把参数次序交换、数学内容不变后成功率从 98.4% 跌到 68.9%。Mira 的失败并非定理变难：表面形式改变了模型熟悉度。更棘手的是，Lean tactic 有时把条件 x > 1 弱化成 x > 0，信息丢失后无法逆转；只用“可逆群变换”描述证明过程也不够。

论文的转折是把 tactic 诱导的变换看成范畴中的箭头：允许复合，也允许非可逆；再把“证明分布随变换一致”与“等价表述成功概率相同”区分开。实践上，给模型多个已验证等价的说法，让有限推理预算分摊到这些表述上。

故事与技术如何对应

• Mira 的不同说法 → Lean theorem statement 的语义保持 rewrites。
• “把条件变弱” → proof tactic 可诱导非可逆箭头，群作用假设不充分。
• 多说法分配预算 → rewriting ensemble；每个变体的 proof 仍由原 prover 生成并由 Lean 检验。
• 论文事实：miniF2F-rw 用 Lean certificates 约束等价；实验不证明任何现实证明器已获得完整的语义不变性。

先给结论

核心判断：论文将“等价输入导致成功率波动”变成一个有形式定义、可测量的问题，并给出无需重训的补救路径。最有说服力的是跨表述基准与有限预算实验；需要谨慎的是其动态改写、打分和 state-to-statement 仍有工程/模型依赖。

研究动机

形式证明的正确性可由 Lean kernel 检查，但搜索能否找到证明取决于 prover。面向 statement 的 LLM 对 token 表面形态敏感：交换项、改写代数式或采用等价记法都可能改变成功率。传统 ML 对称性常用 group action，要求变换可逆；tactic 从一个 proof state 到另一个 state 却可能丢失信息。作者因此把问题拆成两种不同强度的理想性质。

边界与增量：既有训练时数据增强（EvolProver）尝试学到形式变化；本文不声称替代它，而是提出范畴语言刻画非可逆的 tactic 结构，并测量推理时集成是否可在固定预算下提高鲁棒性。

数学表示及建模

把 theorem statements 作为对象、可执行的语义保持 rewriting/tactic 序列作为态射，构成 rewriting category \(\mathcal R\)。态射可复合，但一般没有逆态射。对 prover \(p_\theta\)，记在命题 \(T\) 上输出可通过 kernel 的 proof 的概率为 \(s_\theta(T)\)。

直觉上，equivariance 讨论整份 proof distribution 怎样随重写迁移；success invariance 只比较“能不能成功”的概率，是更粗的量。作者指出基于 proof-state 的 next-tactic predictor 可自然满足相应的状态变换一致性；端到端 statement LLM 并不自动拥有这些性质。

令从 seed 采样到的等价表述集合为 \(\{T_i\}_{i=1}^K\)，其各自成功率为 \(s_i\)，分配预算 \(n_i\)，总预算 \(N=\sum_i n_i\)。至少一次成功的概率为 \(1-\prod_i(1-s_i)^{n_i}\)。采样极限下对覆盖的等价类聚合可趋向成功率不变；有限预算时，覆盖模型偏好的形式才可能获益，不能解读成任何预算下必然胜过 seed-only。

算法流程 / 方法

1. 离线 benchmark：为 miniF2F 每个题生成 5–15 个形式改写；人工筛查后，构造双向 Lean equivalence certificates，最终 5,726 条（validation 2,922、test 2,804）。
2. 在线采样：从 Mathlib 中无条件等式/等价引理及简化 tactic 采样 rewriting sequences；每步取 top-15，有深度 2 的扩展，限制 AST 复杂度并去重。
3. 组合：对前提与目标表达独立选择 seed 或候选改写，重复生成候选状态；论文用 GPT-5.4 把 Lean internal state 转成更自然的 theorem statement。
4. rerank：用 theorem surprise（输入 token 的平均负对数似然）近似“模型熟悉度”，挑最低 surprise 的 7 个变体，与 seed 一起送入 prover。
5. 验证：证明在变体上生成，使用 Lean tactic-based transfer 还原到原 statement 并由 Lean 检查。

需分清保证与启发式：证书约束基准变体的语义等价；在线候选的构造/筛选并非对全体等价形式完备。surprise 是 proxy，不等同于实测证明成功概率。

实验设计

• 主模型：DeepSeek-Prover-V2-7B、Goedel-Prover-DPO、Goedel-Prover-SFT；以非 reasoning prover 为主，另有 reasoning 模型附录实验。
• 设置：seed、随机单变体、预验证的 controlled 8 变体、test-time seed+7 在线变体；miniF2F-rw 的 PASS@k，k=8/32/64，各变体 64 次尝试，随机选择统计 20,000 次。
• 外部任务：ProofNet-test、Ineq-Comp seed/trans split；对照训练增强方法 EvolProver。
• 资源/成本：H100 80GB；每次模型生成约 0.5–1.3 秒，完整 5,700×64 生成约 4–5 GPU-days/模型；报告 GPT-5.4 数据构造约 $14.50，在线转换约 $18.19。

实验结果

miniF2F-rw 上随机等价改写通常低于 seed，证实输入形式敏感。DeepSeek-Prover-V2-7B 在 test split PASS@64：seed 66.8%、random 64.8%、controlled 68.8%、test-time 67.6%；集成改善随机改写的脆弱性，controlled 高于 seed，自动 test-time 较 seed 略高。效应并不对每个模型/切分都相同。

Ineq-Comp-trans 是关键外部验证：DeepSeek seed 的 PASS@64 为 37.3%，ensemble 为 45.5%，trans/seed ratio 从 55.9% 上升至 70.3%；Goedel DPO 在 PASS@64 由 15.3% 到 17.0%。ProofNet DeepSeek 23.1%→23.2%，收益很小。故结果支持“某些变换压力下的稳健性改善”，不支持普遍准确率提升。

理论渐近结论与经验结果互补：若预算无限，seed-only 采样成功概率本身趋近 1；集成优势关乎现实的有限预算。Reasoning prover 附录仍有 seed 与随机改写差距，说明显式 CoT 未消除敏感性。

我的评论

强项

把不对称的 tactic 变换从“群作用”扩到范畴是恰当的概念修正；双向 Lean certificate 让 benchmark 不只是未经验证的 paraphrase。结果还把理论概率命题落实到可复现预算与多个数据集。

审稿人会追问

• 覆盖的 rewriting category 由 Mathlib 无条件 lemma、AST 限制和少量 commutativity rule 决定，结论依赖候选生成分布；离完整 \(\mathcal R_T\) 有多远尚未量化。
• 低 theorem surprise 可能选到容易读、却不一定更易证明的表述；更直接的 success predictor 或校准分析值得对照。
• 在线流程用 GPT-5.4 statement conversion，削弱了“纯 prover-side、不依赖额外 LLM”的部署主张；作者说明可由小模型替代，但未在本文全面验证。
• 展示的提升有异质性：ProofNet 很小、一些模型 test-time 不优于 seed。需按预算、成本与任务选择，不能笼统称为 SOTA。

独立结论：贡献主要是定义/评估框架与实用有限预算技巧；它没有证明所有形式化数学任务都应服从单一对称性公理。

One More Thing

“正确性由 kernel 保证”与“搜索过程对等价变换鲁棒”是两个正交指标。以后 theorem prover leaderboard 可同时报告 seed PASS@k 与 verified-equivalent rewrite 的均值、方差、worst-case drop，以及推理成本；否则模型可能靠熟悉的表面模板取得高分，却无法稳健迁移。

完整图谱

下列每个图都按原始 caption 对应页完整覆盖。为保留可核验图像，本页嵌入包含该图的 PDF 页面快照（因此带少量页面上下文）；没有弃用图。

Other Discussion Roles / 其他讨论角色

以下七个角色使用 MIT MAS.S60 课程原始 prompt，从不同责任位置审视同一篇论文。

def ensemble(seed, rewrites, prover, k=8):
    candidates = [seed] + [r for r in rewrites if lean_equiv(seed, r)]
    ranked = sorted(candidates,
                    key=lambda t: theorem_surprise(prover, t))[:k]
    for theorem in ranked:
        proof = prover(theorem)
        if proof and lean_check_transfer(seed, theorem, proof):
            return proof
    return None

Reference / Evidence