Lean

进行中

基础类型:

Fin n

基础类型, 小于n的自然数

它的每个元素是一对(值 + 值 < n 的证明)

Fin n 是 Lean 的一个基础类型:“小于 n 的自然数”。它的每个元素是一对(值 + 值 < n 的证明):

lean

– Fin 4 的全部元素:0, 1, 2, 3

– 结构上每个元素是 ⟨val, isLt⟩,比如 ⟨2, (证明 2 < 4)⟩

为什么不直接定义数组类型?

1. 类型不携带长度 vs 携带长度

Array ℝ 的类型里没有长度。你得到处拖着一个旁证 h : a.size = n,每次索引 a[i] 还要再证一次 i < a.size,证明目标里堆满边界义务。Fin n → ℝ 里 n 直接在类型里,索引合法性由 Fin n 自身保证,这些义务整个消失。

2. mathlib 的全部代数结构是往函数类型上装的

这是决定性的一条。mathlib 的 typeclass 实例是给 pi 类型(函数类型)配的:

• Fin n → ℝ 自动是加法群、向量空间、赋范空间——p + q、c • p、‖p‖ 直接能写,相关引理全部现成
• stdSimplex 𝕜 ι 本身就定义在 ι → 𝕜 上(上次 grep 到的 Set (ι → 𝕜))
• 凹性 ConcaveOn、梯度、内积(EuclideanSpace ℝ (Fin n) 字面上就是 Fin n → ℝ 加个内积实例)——后面证 Savage 定理全要用

用 Array ℝ 的话,这些结构一个都没有,你要么自己造实例,要么每步先转换成函数再用引理,两头受罪。mathlib 的矩阵也是同样哲学:Matrix m n α 的定义就是 m → n → α。

3. 相等性干净

两个函数相等 ⟺ 逐点相等(funext),一行搞定。数组相等要穿过内部表示,证明里全是噪音。

4. 证明里不需要“运行”它

数组的卖点是运行时性能:O(1) 随机访问、原地修改。但证明 L(p,p) ≤ L(p,q) 时你从不“执行”这个向量,只对 pᵢ 做符号推理——数组的性能优势为零,表示负担全在。

用的时候当数组用即可是吗

对,读的时候完全当数组用:p i 就是 p[i]。具体对照:

lean

– 字面量:mathlib 有 ![…] 记法

def p : Fin 2 → ℝ := ![0.7, 0.3]

– 索引

#check p 0 – 0.7 (类型 ℝ)

p 1 – 0.3

– 遍历求和

∑ i, p i – 0.7 + 0.3

– 逐元素运算(向量空间实例白送的)

p + q – 逐元素加

(2 : ℝ) • p – 数乘

两个和普通数组不一样的地方,心里有数即可:

1. 没有原地修改。 它是函数,不是可变内存。“改第 i 个元素”写成 Function.update p i x,返回一个新函数,原来的 p 不动。证明里这反而是好事——值从不偷偷变。
2. 下标必须静态合法。 p 1 里的 1 会被自动转成 Fin 2 的元素;写 p 5 直接编译不过。如果下标是个运行期算出来的 k : ℕ,你得给出 k < 2 的证明才能转成 Fin 2——这就是边界检查从运行时挪到了编译期。

在我们的 ProperScoring.lean 里,实际用法基本就这几招:![0.7, 0.3] 造具体分布、p i 取分量、∑ i, p i * S q i 写目标函数,没有更花的了。

如何构造优化器?

奖对罚错

比如 0-1 loss(答对不罚、答错罚 1)或线性评分 −qᵢ,它们都满足“对的分数好、错的分数差”。但它们都不 proper——线性评分那个反例前面算过,它把 (0.7, 0.3) 的诚实报价逼成 (1, 0) 的谎报。关键在于:LM 的场景里没有“对的 q”和“错的 q”,因为下一个 token 本来就不确定,q 是一个关于不确定性的陈述。loss 要罚的不是“答错”(答案 i 是抽签抽出来的,谁也料不到),而是**“报价失真”**。所以合格的标准要升级成:

▎ 不只是奖对罚错,而是罚得恰到好处,使得“如实报出自己的不确定性”成为长期总账下的唯一最优策略。

罚轻了(线性评分):鼓励梭哈。罚的曲线不对:鼓励缩水或夸大。CE 的 −log 曲线恰好是“逼出真话”的一种罚法——这就是 properness 全部内容。类比:好的考试打分制不是“对给分错扣分”就完了,分值曲线设计不好,考生的最优策略就会从“如实作答”变成“策略性押题”。

2. 优化 ≈ 力学——不止像,数学上就是同一套东西

这个类比是严格的,不是修辞:

┌─────────────────────────┬────────────────────────────────────────────────┐

│ 力学 │ 优化 │

├─────────────────────────┼────────────────────────────────────────────────┤

│ 势能面 U(x) │ loss 曲面 L(q) │

├─────────────────────────┼────────────────────────────────────────────────┤

│ 力 F = −∇U │ 负梯度 −∇L │

├─────────────────────────┼────────────────────────────────────────────────┤

│ 小球往低处滚 │ 梯度下降 │

├─────────────────────────┼────────────────────────────────────────────────┤

│ 平衡点(合力为零) │ 驻点(梯度为零),上一轮的“拉力平衡”就是它 │

├─────────────────────────┼────────────────────────────────────────────────┤

│ 单一深谷 │ 凸性:怎么滚都到全 │

├─────────────────────────┼────────────────────────────────────────────────┤ │ 势能墙 │ CE 在单纯形边界的去) │

├─────────────────────────┼────────────────────────────────────────────────┤ │ 摩擦大、局部平地,球卡住 │ Brier 在“自信地错 │

├─────────────────────────┼────────────────────────────────────────────────┤ │ 惯性 │ momentum 优化器字项 │

└─────────────────────────┴────────────────────────────────────────────────┘

连术语都通用:loss landscape(损失地形)、saddle point(鞍点)、energy barrier。数学上梯度流 dq/dt = −∇L(q) 就是过阻尼极限下的质点运动方程。

                                                                                                             把前面所有讨论装进这幅图:properness = "谷底的的要求;文章第 4 节比较 CE 和Brier,比的就是两张地形图——谷底位置相同(都 proper),但坡度分布不同:CE 处处有坡、离谷越远坡越陡(哪儿都滚得动),Brier 在错误顶点附近有一块平地(滚进去就趴窝)。V0 de的就是这两张地形。