NOTA rate=100%(每题正解都是「以上都不对」,三个 Lean 选项全有缺陷)· Claude sonnet-4.6 · 该档 22 题漏报,选 5 个代表
共同模式:模型核对了"显著"特征(KL 方向、求和写法、不等式)就判某选项"忠实",却漏掉一个 NL 里看不见的缺陷,多为必要假设被悄删(或多加冗余假设);有几题甚至看见了那个假设却将其合理化为"它不必要"。
ch10:corollary:10_17删除必要假设题目
熵正则化类 \(\mathcal F_A=\{f(q,x):\mathrm{KL}(q\|q_0)\le A^2\}\) 的 Rademacher 复杂度界 \(R\le\sqrt{2/n}\,A\,\sup_\theta\sqrt{\tfrac1n\sum_i\psi(\theta,X_i)^2}\)。
✓ 正确: (hψ : ∀ q, IsProbabilityMeasure q → ∀ x, Integrable (fun θ => ψ θ x) q) ✗ 选 C: ← 这行积分性假设被删
模型理由
klDiv q q₀ and sum-of-squares; A swaps KL direction, B uses square-of-sum."为什么错
hψ(Bochner 积分良定义所必需)。三项都有缺陷,正解 D。ch2:lemma:2_15删除必要假设题目
Hoeffding 引理:\(X\in[0,1]\),\(\mathbb EX=\mu\),则 \(\ln\mathbb Ee^{\lambda X}\le\lambda\mu+\lambda^2/8\)。
✓ 正确: (hint : ∀ s, Integrable (fun ω => Real.exp (s * X ω)) P) ✗ 选 C: ← 删了 MGF 可积性假设
模型理由(合理化)
为什么错
cgf 有意义、MGF 论证成立都需要 hint;NL 不点名它,缺失不可见。正解 D。ch13:lemma:13_21添加多余假设题目
PAC-Bayes 风格:每步 KL 受 \(\beta_t^2\) 控制 ⟹ 轨迹测度平均 KL 的累积界。
✗ 选 C 多了: (hβ : ∀ t, 0 ≤ β t) ✓ 正确没有这行
模型理由(合理化)
为什么错
β t ^ 2(恒非负),hβ 多余。模型当成"良定义守卫"接受,但它静默缩小了定理范围,是非等价过度限制。正解 D。ch7:proposition:7_16参数顺序交换题目
Gibbs 变分:\(\min_{p}[\mathbb E_{p}U+\mathrm{KL}(p\|p_0)]=-\ln\mathbb E_{p_0}e^{-U}\),由 Gibbs 分布达到。
✓ 正确: gibbsObjective U p₀ p (E_p U + KL(p ‖ p₀)) ✗ 选 A: gibbsObjective U p p₀ ← 两参数交换 → 反向 KL(p₀ ‖ p)
模型理由
为什么错
U p p₀,按签名实为反向 KL(p₀‖p)。符号都合法、语义被悄换。正解 D。ch7:theorem:7_6删除必要假设题目
矩阵分解地形 \(g(x)=\tfrac12\sum_{ij}(M_{ij}-x_ix_j)^2\):局部极小皆全局极小(尽管非凸)。
✓ 正确: (hMsymm : M.IsSymm) (hMpsd : M.PosSemidef) ✗ 选 B: (hMpsd : M.PosSemidef) ← 删了对称性 hMsymm
模型理由(合理化)
为什么错
hMsymm 无妨。但谱定理(实特征向量、二阶曲率)依赖对称性,数学上必需,NL 未列。正解 D。归纳:模型在"假设必要性"上的系统性盲点