一般性的阅读解析内容

2026-09-06 · 随笔 · 43a908c205b5

以https://spaces.ac.cn/archives/11882 为例子

背景是?

概念(自适应梯度算法的) 什么信息 / 内容 (xx )

1. θt+1=θt−ηtH−1tg(xt,θt)

看到公式

• 这个公式的意义 / 动机 (在这里是学习率更新)
• 来源 (xx论文? 为了解决什么问题?)
• 为什么要设定某些限制? 比如正定?

2. 看作者下一步干了什么 (推导 / 证明 / 加限制? / 提出新内容)

∥θt+1−φ∥2==∥θt−ηtg(xt,θt)−φ∥2∥θt−φ∥2−2ηt(θt−φ)⋅g(xt,θt)+η2t∥g(xt,θt)∥2(2) 这个是新的恒等式出现, 作者写这个的动机是什么? 它说是证明的出发点, 我们不知道它指的是什么证明, 什么出发点, 但是既然是公式, 我们就套用 看到公式xxx那个

这里我们发现它是多个等式, 那就是出现了推导,

使用mathlib进行去歧义, 并且加类型以及明确中间可能的假设, 或者是中间使用的引理

3. 再看下一步

然后我们设法将(θt−φ)⋅g(xt,θt)分离到一边，再通过凸性假设将它跟损失值联系起来： L(xt,θt)−L(xt,φ)≤(θt−φ)⋅g(xt,θt)(3)

下一个公式, 又套用那个模版, 而且这个是使用了假设, 要用lean / torhclean / mathlib写出中间过程, 以及形式化的过程

接下来让ai生成:

从公式精读到 Lean 形式化，再到理解检验

示例：苏剑林《让炼丹更科学一些（九）：经典自适应梯度算法》。

范围与状态：以用户提供的式 (1)—(3) 为正文依据。本次只能取得文章的部分检索信息，未能读取全文；下文的局部证明路线与延伸界是数学重建，不冒充作者后文原句。Lean 部分是尚未编译的证明草稿；已核对若干 mathlib 定义和引理文档，但没有可用的本地 Lean / Lake 编译器。全文不声称完成了机器验证。

1. 可直接交给 AI 的通用指令

请把给定数学文章按论证步骤精读。每次处理一个足够小的片段，使每条结论的来源、类型、假设和用途都能追溯。不要仅按公式编号分段：同一公式内可能有数个论证步骤。

文章入口

说明研究对象、要解决的问题、已有方法及其局限、作者拟获得的结论。结论必须具体，例如累计损失差的上界、期望风险界、最后一次迭代的损失界、参数收敛，不能统一写成“证明收敛”。尚未看到结论时，列出候选目标并标为待确认。

列出必需的先修概念。每个概念说明：是什么；输入和输出是什么类型；在本文承担什么作用；最小例子；常见混淆。只展开理解当前论证必需的内容。

每遇到一个公式或论证动作

依次回答：

1. 说了什么？ 用一句准确的话重述。分类为定义、算法规则、恒等式、假设、定理、近似或经验结论；一行可包含多类动作。
2. 符号是什么？ 给出类型、维度、作用域、量词、依赖关系；区分向量内积、标量乘法、矩阵乘法和标量作用；确认范数种类。
3. 为什么出现？ 说明本步骤想控制的量、承接的结果、后续要用的地方。区分作者明确说明的动机和根据证明结构重建的解释。
4. 来自哪里？ 区分数学依据、算法的历史来源和本文引用来源。恒等式可以来自代数性质，不必给每个公式硬找一篇“首创论文”。文献信息须核实；没查到就标为未核实。
5. 用了哪些条件？ 分别列出定义有意义所需的条件、当前推导所需的条件、后续定理才需要的条件，以及仅为实现方便选择的条件。不要把充分条件自动称为必要条件。
6. 每一步怎样走？ 对等号链和不等号链逐步给出理由，并记录新引入、继承和暂未使用的假设。发现特例化、换范数、换对象或近似，必须明确说出。
7. 怎样形式化？ 先写与原命题一致的 Lean 类型和命题，再补证明。数学条件用假设表达；不得把待证结论作为新增假设。优先使用 mathlib 现有定义；需要自定义时解释与原文概念的对应关系。
8. 怎样检查理解？ 针对这一步生成解释题、推导题、条件删除题、反例题和迁移题。每题必须绑定具体公式、假设或论证连接，附评分要点和错误诊断。

形式化交付标准

• 显示自然语言命题与 Lean 命题的对应关系，包括所有新增假设。
• 保留能解释数学步骤的中间引理；不能只显示一行自动化战术然后宣称读者已理解。
• 如果证明采用更强假设、仅处理一维或特殊函数，必须标明范围变化。
• 编译验证记录应包括实际 Lean 版本、mathlib 提交、命令、退出状态和剩余错误；版本未知时不捏造。
• 含 sorry、admit、新增公理或未完成依赖的结果，不得标为完成证明。必要时检查 #print axioms，区分库的基础公理与人为加入的结论。
• 没有运行编译器就写“未编译草稿”。有编译结果仍须检查形式命题是否忠实于原文。
• 数值实验用于提供直觉或寻找反例；不能替代普遍命题的证明。
• 这些内积和凸性推导先用 Lean + mathlib。涉及具体张量计算或自动微分实现时，再判断是否需要 TorchLean；不虚构其接口或验证能力。

交互与出题

先给一个片段的精读结果，再给少量问题，默认先不展示答案。收集回答后区分概念、类型、假设、代数、证明策略和泛化方面的错误，并只补必要的解释与变式。

不要把“写出了 Lean 代码”“代码通过编译”“形式命题忠实于原文”“人理解了推导”当作同一件事。

2. 本例的背景与类型

研究对象是用损失梯度更新参数的优化算法。普通 SGD 使用一个标量步长；预条件更新进一步允许不同方向采用不同缩放。若预条件子由历史梯度等信息决定，才进一步体现自适应机制。一般矩阵更新框架本身尚未指定具体的自适应算法。

AdaGrad 的经典文献是 Duchi、Hazan、Singer（2011）的 Adaptive Subgradient Methods for Online Learning and Stochastic Optimization。它研究利用历史梯度调整优化几何的方法；这可以作为本例的算法背景，不等于断言一般预条件更新公式首创于该论文。

固定一次迭代，缩写为：

在 mathlib 中可用 EuclideanSpace ℝ (Fin n) 表示欧氏空间。不能仅写 Fin n → ℝ 后就默认其现有范数是欧氏范数。下文证明采用抽象实内积空间，因而也适用于这个欧氏空间。

φ 在局部恒等式和凸性不等式中是任意比较点，不必预先假设它是最优解。若跨迭代求和，则需说明始终使用同一个比较点。

3. 式 (1)：算法规则及正定性的作用

意义：这是参数更新规则。 它描述如何生成下一次参数；没有单凭这一式给出 (\eta_{t+1}) 或 (H_{t+1}) 的更新方法。

当 (H_t=\operatorname{diag}(h_{t,1},\ldots,h_{t,n})) 时，第 (i) 个坐标的有效步长为 (\eta_t/h_{t,i})。取 (H_t=I) 就是普通 SGD。

一个数学动机的重建： 对 (\eta_t>0)，考虑局部模型

第一项希望沿梯度下降；第二项惩罚移动，用 (H_t) 指定各方向移动的代价。对 (\Delta) 求导并令其为零，得到

在有限维实空间中，对称正定让这个二次模型严格凸且具有唯一最小点，同时保证 (H_t) 可逆。这个解释是公式的推导方式，并非关于作者心理动机的断言。

下降方向的检查为

这说明充分小的正步长可以下降，不保证任意有限步长都使损失下降。例：(f(z)=z^2)、(z=1)、(H=1)、(\eta=2)，下一点为 (-3)，损失从 (1) 增至 (9)。

4. 式 (2)：为什么引入距离平方

这里必须明确已经取普通 SGD，即 (H_t=I)。

各等号都须单独标注。最后一个等号使用

这一步需要的条件很少： 实内积空间、向量类型一致、(\eta_t) 为实数。展开不需要凸性，不要求 (g_t) 真的是梯度，也不要求 (\eta_t>0)。

为何这样展开？ 它产生了 (\langle\theta_t-\varphi,g_t\rangle)，而这个量恰好能通过凸性控制损失差。距离平方还会产生相邻迭代的差，方便后续求和。

因此，“证明的出发点”在这个局部结构中的具体意思是：为损失差建立一个可累计的上界。仅凭这两式，不能直接声称参数或最后一次迭代必然收敛。

5. 式 (3)：凸性是在哪一步进入的

假设 (f_t=L(x_t,\cdot)) 在参数空间上凸，并在 (\theta_t) 可微，且 (g_t=\nabla f_t(\theta_t))。那么凸函数的一阶支撑不等式给出

所以式 (3) 不是单凭式 (2) 移项产生的，它另外使用了凸函数的一阶性质。假设是关于固定 (x_t) 后的参数函数，不要求 (L) 对样本 (x) 也凸。

如果继续追问“一阶支撑不等式从哪来”，设 (d=\varphi-\theta_t)。由凸性，对 (0<s\le1)，

减去 (f_t(\theta_t))，再除以正数 (s)：

令 (s\downarrow0)，可微性使左侧收敛到 (\langle g_t,d\rangle)，得到所需不等式。这里每一步的新条件分别是：凸性、(s>0)、方向导数与梯度的关系。

可微性是这条梯度证明路线的条件；不可微凸函数也可改用满足支撑不等式的次梯度。

6. 把两步连接起来：到底在证明什么

现在才使用 (\eta_t>0)，由式 (2) 移项、除以 (2\eta_t)，再结合式 (3)，得到

这就是关键连接：损失差由距离平方的减少量与梯度平方项共同控制。

以下是为解释证明结构补出的固定步长例子，另行假设 (\eta_t=\eta>0)。对 (t=0,\ldots,T-1) 求和：

第二行来自望远镜求和；第三行来自范数平方非负与 (\eta>0)。若再加入 (|\theta_0-\varphi|\le D)、(|g_t|\le G)，就得到 (R_T(\varphi)\le D^2/(2\eta)+\eta TG^2/2)。

若 (D,G>0)、(T\ge1)，取 (\eta=D/(G\sqrt T))，可得 (R_T(\varphi)\le DG\sqrt T)。平均累计差因此有趋于零的上界；若要进一步得到期望风险界，还须交代采样与取期望的条件。

如果 (\eta_t) 随时间变化，带权距离差不能直接按固定步长的方式消掉全部中间项。如果 (H_t\ne I)，每步可考虑 (|v|_{H_t}^2=v^\top H_tv)；若矩阵还随时间变，跨步比较度量也需额外处理。这些都是应由精读流程主动识别的变化。

7. Lean / mathlib 证明草稿

状态：未编译；尚未锁定 Lean 与 mathlib 版本。 以下是拟运行的完整局部证明草稿，不是编译通过记录。它覆盖 SGD 距离恒等式、凸性损失差不等式以及二者的单步组合；不声称完成一般预条件算法的收敛证明。

为显式区分导数与梯度，代码使用 D : E →L[ℝ] ℝ 表示连续线性导数，并用 hgrad 声明 D v = ⟪g, v⟫_ℝ。在欧氏空间中，这正是梯度向量表示导数的关系。也可在适当的空间类型下改用 mathlib 的 HasGradientAt f g θ。

import Mathlib

open scoped InnerProductSpace

namespace FormulaReading

variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]

-- 这里只编码可逆性。正定性是另一个需显式加入的数学条件。
noncomputable def preconditionedStep
    (H : E ≃L[ℝ] E) (η : ℝ) (θ g : E) : E :=
  θ - η • H.symm g

def symmetricPositive (H : E →L[ℝ] E) : Prop :=
  (∀ u v : E, ⟪H u, v⟫_ℝ = ⟪u, H v⟫_ℝ) ∧
  (∀ v : E, v ≠ 0 → 0 < ⟪v, H v⟫_ℝ)

-- E 可以取 EuclideanSpace ℝ (Fin n)。
-- 注意：下式不假设 η > 0，也不假设 g 是梯度。
theorem sgd_distance_identity (θ φ g : E) (η : ℝ) :
    ‖θ - η • g - φ‖ ^ 2 =
      ‖θ - φ‖ ^ 2 - 2 * η * ⟪θ - φ, g⟫_ℝ
        + η ^ 2 * ‖g‖ ^ 2 := by
  have hrewrite : θ - η • g - φ = (θ - φ) - η • g := by
    abel
  rw [hrewrite, norm_sub_sq_real]
  simp only [real_inner_smul_right, norm_smul, Real.norm_eq_abs,
    mul_pow, sq_abs]
  ring

-- 凸函数沿任意仿射直线的限制仍然凸。
theorem convex_along_line
    (f : E → ℝ) (θ d : E)
    (hc : ConvexOn ℝ Set.univ f) :
    ConvexOn ℝ Set.univ (fun s : ℝ => f (θ + s • d)) := by
  refine ⟨convex_univ, ?_⟩
  intro a ha b hb u v hu hv huv
  have h := hc.2
    (show θ + a • d ∈ (Set.univ : Set E) from Set.mem_univ _)
    (show θ + b • d ∈ (Set.univ : Set E) from Set.mem_univ _)
    hu hv huv
  have hline :
      u • (θ + a • d) + v • (θ + b • d) =
        θ + (u * a + v * b) • d := by
    calc
      u • (θ + a • d) + v • (θ + b • d) =
          (u • θ + v • θ) +
            ((u * a) • d + (v * b) • d) := by
        simp only [smul_add, smul_smul]
        abel
      _ = (u + v) • θ + (u * a + v * b) • d := by
        rw [← add_smul, ← add_smul]
      _ = θ + (u * a + v * b) • d := by
        rw [huv, one_smul]
  change f (θ + (u * a + v * b) • d) ≤
    u * f (θ + a • d) + v * f (θ + b • d)
  simpa only [hline, smul_eq_mul] using h

-- 不把一阶支撑不等式当作假设：从凸性和导数出发。
theorem convex_loss_gap
    (f : E → ℝ) (θ φ g : E) (D : E →L[ℝ] ℝ)
    (hc : ConvexOn ℝ Set.univ f)
    (hD : HasFDerivAt f D θ)
    (hgrad : ∀ v : E, D v = ⟪g, v⟫_ℝ) :
    f θ - f φ ≤ ⟪θ - φ, g⟫_ℝ := by
  let ψ : ℝ → ℝ := fun s => f (θ + s • (φ - θ))
  have hcψ : ConvexOn ℝ Set.univ ψ :=
    convex_along_line f θ (φ - θ) hc

  -- 链式法则：沿 φ - θ 的方向导数是 D (φ - θ)。
  have hpath :
      HasDerivAt (fun s : ℝ => θ + s • (φ - θ)) (φ - θ) 0 := by
    simpa using
      (((hasDerivAt_id (0 : ℝ)).smul_const (φ - θ)).const_add θ)
  have hD0 : HasFDerivAt f D (θ + (0 : ℝ) • (φ - θ)) := by
    simpa using hD
  have hψD : HasDerivAt ψ (D (φ - θ)) 0 := by
    simpa only [ψ, Function.comp_def] using
      (hD0.comp_hasDerivAt (0 : ℝ) hpath)
  have hψg : HasDerivAt ψ ⟪g, φ - θ⟫_ℝ 0 := by
    simpa only [hgrad] using hψD

  -- mathlib 的凸函数割线斜率引理：ψ'(0) ≤ slope ψ 0 1。
  have hs := hcψ.le_slope_of_hasDerivAt
    (show (0 : ℝ) ∈ Set.univ from Set.mem_univ _)
    (show (1 : ℝ) ∈ Set.univ from Set.mem_univ _)
    (show (0 : ℝ) < 1 by norm_num) hψg
  have hψ0 : ψ 0 = f θ := by
    simp [ψ]
  have hψ1 : ψ 1 = f φ := by
    dsimp [ψ]
    congr 1
    simp only [one_smul]
    abel
  have hsupport : ⟪g, φ - θ⟫_ℝ ≤ f φ - f θ := by
    simpa [slope, hψ0, hψ1] using hs

  have hinner : ⟪g, φ - θ⟫_ℝ = -⟪θ - φ, g⟫_ℝ := by
    rw [inner_sub_right, inner_sub_left,
      real_inner_comm g φ, real_inner_comm g θ]
    ring
  rw [hinner] at hsupport
  linarith

-- η > 0 在除以 2η 并保持不等号方向时进入。
theorem one_step_loss_bound
    (f : E → ℝ) (θ φ g : E) (D : E →L[ℝ] ℝ) (η : ℝ)
    (hc : ConvexOn ℝ Set.univ f)
    (hD : HasFDerivAt f D θ)
    (hgrad : ∀ v : E, D v = ⟪g, v⟫_ℝ)
    (hη : 0 < η) :
    f θ - f φ ≤
      (‖θ - φ‖ ^ 2 - ‖θ - η • g - φ‖ ^ 2
        + η ^ 2 * ‖g‖ ^ 2) / (2 * η) := by
  have hgap := convex_loss_gap f θ φ g D hc hD hgrad
  have hdist := sgd_distance_identity θ φ g η
  have hpos : 0 < 2 * η := by positivity
  have hscaled := mul_le_mul_of_nonneg_left hgap (le_of_lt hpos)
  apply (le_div_iff₀ hpos).2
  nlinarith [hscaled, hdist]

end FormulaReading

未来实际验收：把上方代码保存为 FormulaReading.lean，在已配置并锁定 mathlib 的项目内执行 lake env lean FormulaReading.lean，修复全部编译错误，记录真实版本与输出，并检查最终定理的假设。这里没有执行该命令，也没有声称已完成这一验收。

本例实际核对的库入口包括 内积与范数恒等式、凸性定义、凸函数的割线斜率引理、梯度的形式定义和链式法则。

8. 从本例生成的开放式习题

这里采用解释题和推导题；正式交互时先只展示题目，答案与评分标准在用户作答后展开。

答案与评分要点

每题按 0—2 分判断：0 分为结论错误或无有效依据；1 分为结论基本正确但关键条件或理由缺失；2 分为结论正确且准确说明关键连接。分数用于定位薄弱点，不当作完整理解的认证。

1. 更新 (\theta)；没有给出下一步标量步长或矩阵的生成机制。
2. 取 (H_t=I)，转为 SGD。
3. 代入更新、重排向量、范数平方改写为自身内积、双线性展开、内积对称、标量提出。
4. 恒等式仍成立。除以 (2\eta) 时若 (\eta<0) 不等号须反向；优化方向也改变。
5. 式 (2) 不使用凸性；式 (3) 的一阶支撑性质使用凸性与梯度关系。
6. 使用 (f((1-s)\theta+s\varphi)\le(1-s)f(\theta)+sf(\varphi))，对 (s>0) 移项除法，再令 (s\downarrow0)。
7. 例 (f(z)=-z^2)、(\theta=0)、(\varphi=1)，梯度 (g=0)，式 (3) 会要求 (1\le0)。
8. 局部恒等式对任意比较点成立。比较点变化时不能沿用固定比较点的望远镜求和；需计入变化。
9. 不能。例 (f(z)=z^2)、(\theta=1)、(H=1)、(\eta=2) 得到 (\theta_+=-3)，损失 (9>1)。
10. 距离平方展开产生梯度内积；凸性将损失差界于该内积；移项求和时相邻距离差抵消。
11. 对 (t=0,\ldots,T-1)，中间项为 (\sum_{t=1}^{T-1}A_t(1/(2\eta_t)-1/(2\eta_{t-1})))，另有首项 (A_0/(2\eta_0)) 与末项 (-A_T/(2\eta_{T-1}))。
12. 欧氏展开含 (-2\eta\langle\theta-\varphi,H^{-1}g\rangle+\eta^2|H^{-1}g|^2)。用同一步的对称正定 (H) 加权后，可得交叉项 (-2\eta\langle\theta-\varphi,g\rangle) 与末项 (\eta^2g^\top H^{-1}g)，便于接上凸性不等式。

错误如何反馈到下一轮