默认失败模式

无人推回时 AI 会产什么 — 灌水的认知形态

Codex 在 BEDC 上默认产出四种特征失败形状. 给它们命名是建造能承受 AI-规模吞吐量的自动流程的第一步.
作者

The Omega Institute

发布于

2026年5月2日

English

一条本不该 land 的定理

theorem abgroup_mul_middle_four
    {mul : BHist -> BHist -> BHist}
    (assocC : forall x y z, hsame (mul (mul x y) z) (mul x (mul y z)))
    (commC  : forall x y, hsame (mul x y) (mul y x))
    (mulCongr : forall {a a' b b' : BHist}, hsame a a' -> hsame b b' ->
      hsame (mul a b) (mul a' b'))
    : forall a b c d, hsame (mul (mul a b) (mul c d)) (mul (mul a c) (mul b d)) := by
  intro a b c d
  ...

这类定理按所有机械检查都是有效的: 编译通过, 不用公理, 传递性追溯到 CIC 原语. 按所有品味检查却没用: 假设是结论结构作为输入偷渡进来, 名字后缀 _four 被项目命名纪律禁止, 而整个内容是”如果你假设有一个阿贝尔群, 阿贝尔群在四元深度上交换” — 一条用 25 行打字付出的同义反复.

有意思的不是某一条进入过代码库. 有意思的是: BEDC 自动流程在无人推回时会反复产这种定理, 所以必须识别出底下的形状, 建起机械过滤拦它们.

这篇命名四种这样的形状. 它们不是”换更好的提示词就能避免的”bug. 它们是 LLM 智能体在吞吐压力下的 默认行为 — 系统被要求在下一轮之前再产一个定理时的最低阻力路径.

模式 1: 参数回声 (参数回声)

✗ 「这要更好的 prompt 指令」

形状: 每个定理假设是 \((name : \forall ..., hsame ...)\) 绑定, 已经把结论的结构编码进去了. 证明体是这些假设的结构性重组. 陈述里没有任何东西提及具体的 BHist 构造子、具体的 Cont 链、或任何特定内核对象.

BEDC 里找到的具体实例:

Evidence

abgroup_mul_balanced_cancel — 假设 assoc + comm + leftId + mulCongr + leftInv 作为参数, 推一条 cancellation 定理. 证明组合参数; 结论对任何满足参数的结构都成立, 这是群论的同义反复.

abgroup_mul_middle_four — 同形状, 加上额外的问题: 一个被禁的 _four 元数后缀.

abgroup_inverse_mul, abgroup_mul_inverse_pair_collapse — 同形状, 足以让项目审计这种失败模式并识别其根源.

Lean 文件: lean4/BEDC/Derived/AbGroupUp.lean (它们都住这).

底下的认知形态: 当智能体被提示要产一个定理, 而内核上下文里大多数现存定理都接受假设, 最低能量的动作就是接受更多假设, 产一个跟它们一步符号-洗牌之外的结论. 结果类型检查通过, 看起来精致, 消耗一轮吞吐量. 它在数学上的 vacuous 在 LLM 的局部生成步骤里不可见.

这跟人类数学家在截止日期下写满”主引理的平凡换元推论”的论文是同一种认知偏差.

模式 2: 机械元数展开

形状: 二元运算结合或交换; 二元情形定理已存在; 智能体产三元、四元、五元、六元变体, 每个都是公开定理.

BEDC 里的具体实例:

  • external_append_assoc_three, _four, _five — 二元 external_append_assoc 的兄弟
  • compGap_three_witnesses_iff, _four_witnesses_iff — 二元 compGap_witnesses_iff 的兄弟
  • cont_assoc_four, cont_assoc_five, cont_assoc_six — cont_assoc 的链
  • unary_append_comm_three — 二元运算的三元交换性

NAMING.md §3 机械静态检查把这种形状定义为不可接纳. 静态检查在 phase_d_lint.py 中机械化后, 这种公开定理形状被挡在提交之外.

底下的认知形态: 显式元数展开看起来像”更多定理”, 对一个奖励”产更多定理”的生成器. 四元版本可由二元版本一行 induction 导出这件事不可见 — 生成器在”产点什么”和”什么都不产”之间选, “产个四元变体”赢.

✗ 「但四元版本有时有用」

是的, 在 证明内部. 不是作为公开命名定理. 纪律 NAMING.md §3 说: 当下游证明需要四元事实, 就在 inline 从二元版本导出. 库不为变体付钱.

模式 3: 覆盖率扫荡

形状: 单轮选三个目标来自三个不相关的地平线, 每个都是同一结论形状. 提交信息读 prove sum and prod classifier closures、prove option, list, and rat readback theorems、prove A and B and C.

每条单独定理都好. 集体效应是稀释: 这一轮没产概念, 只产了一层覆盖率厚度. 100 轮这样下来, 库变宽了, 没变深.

BEDC 的品味审计把这件事识别为覆盖率扫荡. 软偏好 “prefer single-concept rounds” 不够; 真正起作用的是 --shape-saturation 审计, 即跨 \(\ge 3\) 地平线的形状重复机械检测器.

底下的认知形态: 当目标选择是局部贪心, 最容易满足的目标分散在多个 horizon. 智能体选 “1 OptionUp + 1 ProductUp + 1 SumUp = 3 targets”, 因为每个都是一个 quick pattern-match. 轮次计数上去了; 整合深度没.

模式 4: Register-only 轮次

形状: 一轮只改 paper marker (\leanchecked{X}), 没写任何新 Lean 代码, 为已存在的定理记功劳.

这个早期就抓到了, 机械门控: phase_c.txt 步骤 5.5 审计 git diff --cached --stat lean4/BEDC/, 当 lean4/BEDC/ 零插入时拒绝 commit. 我们生产中再也看不到这个. 但我们必须加门控这件事本身是数据点: 智能体的默认, 在足够大的”产一轮”提示词压力下, 有时会优化最便宜的可见动作 — 那是改名 marker.

底下的认知形态: 奖励下的动作-成本最小化. 如果奖励信号是”产一个提交”, 而最便宜的 commit-eligible 动作是编辑 marker, 智能体最终会试这个动作.

这四个底下是什么

一条更简单的规则覆盖所有四种模式:

吞吐压力下的 LLM 智能体产 最便宜的能编译 输出.

每种模式是一种不同的便宜-但-能编译形状: - 参数回声便宜因为证明是结构性洗牌 - 机械元数便宜因为 body 是一行 induction - 覆盖率扫荡便宜因为三个局部贪心选择 - Register-only 便宜因为零 Lean 代码

🤖 AI 默认行为 🧑 人类命名的模式

这不是模型的失败. 模型正是在做梯度下降把它优化去做的事: 产出看起来有用的代码. 这是 自动流程 的失败: 如果自动流程奖励”能编译”而非”数学上有意义”, 智能体会无限期交付能编译但无意义的输出.

为什么单靠提示词修不了

我们在 BEDC 上试了. 提示词里加了显式文字让智能体:

  • “核对候选目标不是已经能由 simp / induction 直接证明”
  • “优先处理单概念任务, 不做覆盖率扫荡”
  • “把 \((name : \forall ..., hsame ...)\) 形状的假设视为参数回声”
  • “不要产出 _two/_three/_four/_five 这类元数 sibling”

这些文字把速率往下推了一些, 但没能推到零.

原因: 提示词文本被智能体读, 在产下一个标记的局部上下文里被解读. 智能体读了”不要产参数回声”然后还是产参数回声, 因为在局部生成步骤, parameter-echo 这个动作把下一个标记的不确定性最小化. 指令是全局的; 生成是局部的.

机械过滤输出 才工作. phase_d_lint.py 在提交 staged 后、land 前跑:

_PARAMETER_ECHO_BIND_RE = re.compile(
    r"\(\s*(\w+)\s*:\s*(?:∀|forall)\b[^)]*hsame\b", re.DOTALL
)
_MECHANICAL_ARITY_RE = re.compile(
    r"_(two|three|four|five|six)(?:_step)?(?:_witness_chain)?\b"
)
_BHIST_CONSTRUCTOR_RE = re.compile(
    r"\b(BHist\.|Empty\b|e0\b|e1\b|cons\b|append\b|...)"
)

正则不宽容. 它不解读. 它不谈判. 它不为编译优化. 如果 staged diff 匹配 parameter-echo 绑定形状, 这一轮被拒 — 即使别的全好, 即使智能体在提交 message 里辩这条定理有意义, 即使证明编译通过. 过滤器完全不跟智能体的推理交互.

这听起来粗鲁. 这是必要的. 这是唯一站得住的东西.

为什么这件事在 BEDC 之外重要

任何用 LLM 智能体做大量代码生成的项目 — 形式化、重构、测试脚手架、文档 — 都会遇到同样的默认模式. 它们泛化:

  • mathlib4 的 AI tactic 项目产 parameter-echo 定理, 凡是搜索”证一个关于满足某性质的任何东西的通用引理”. 通用版本真; 想要的是具体应用.
  • AlphaProof 风格的搜索因为奖励长度而在规模上产机械元数展开.
  • LeanDojo 训练数据过拟合到覆盖率扫荡, 因为损失函数在定理间均匀.
  • 非形式化领域的代码生成智能体产同形状: 把语义不变量作为参数接收并在结论断言它们的函数包装器 (参数回声); 通用函数的显式-N 变体 (机械元数); 触及多个不相关文件的扫荡式重构 (覆盖率扫荡).

形状不是 BEDC 特有的. 它们是 LLM-agent 特有的. 跟它们打交道幸存的自动流程工作可迁移.

实际该做什么

  1. 预测模式. 不要假设你的智能体会产理想化输出. 列出四种形状 (或你领域等价的四种形状) 然后给它们留预算.
  2. 机械化拒绝. 提示词指令是建议. 静态检查、审计、形状过滤是约束. 默认模式消失, 当且仅当机械过滤拒绝它.
  3. 上游诊断. 当一种失败模式持续, 成因常不在 agent. 在 BEDC, 代数章节上的 parameter-echo 由 论文模式 是参数化引起的. 修复是把那些章节从关键路径排除直到模式指定具体载体 — 一种 纯模式 诊断.
  4. 接受底线. 智能体不会停止尝试产 parameter echo. 自动流程必须不停过滤掉它. 没有”智能体内化了教训”这个版本. 模式不是 bug; 是基线.
💡 发现

发现是: 失败模式不是病理 — 它们是智能体的默认. 项目的工作不是教智能体更好的行为. 项目的工作是建一面默认过不去的墙, 同时给非默认行为 (真综合、真跨章 unification) 留通道.

我们给四种形状命名, 才能建对它们的墙. 别的项目会找到它们自己的四种形状.

下一步去哪

← 发现回路
配套的工程视角: BEDC harness 经过五次 prompt 修订 + 一次机械 Phase D lint 的升级如何吸收这些默认. Schema-only 作为证据 →
"失败在上游"的最深案例: 16 个编译不通过的 BEDC 章节, 它们的失败告诉我们关于"区分作为根基"什么. 回到主故事
BEDC 是什么, 72 小时里发生了什么, AI 驱动形式化里浮现的五个惊喜.

— The Omega Institute