类型与神经网络

# 类型与神经网络 来源：https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html 发布于 2026年4月20日 本文亦转载至 [GLAIVE 博客](https://glaive-research.org/2026/04/20/types-and-neural-networks.html) 神经网络正被用于生成越来越多的高级编程语言代码，例如 Idris、Lean 和 Agda，这些语言支持高度泛型且可证明正确的编程。 然而，大多数生成代码的前沿模型——大语言模型（LLMs）——将训练过程与类型检查过程分离开来。它们被训练为输出固定类型的结果：`List Token`。为了获得有效的代码，该输出随后在*后训练阶段*通过多种临时的方式解析为目标语言的特定类型。 这些临时手段是什么？它们有效吗？我们是否应期望它们有效？更重要的是，我们能否从头重建 LLM，使其能够*训练*出带类型的输出？ ## 训练后强制执行类型 如今，LLM 的训练目标是预测给定语料库中的下一个词元，从而得到如下类型的函数： ``` LLM : List Token -> D (List Token) ``` 其中 `D (List Token)` 表示一个词元列表上的分布。LLM 接收输入提示词，一次生成一个词元的分布——从下一个词元分布中采样并将结果反馈回去。出于本文目的，我们将 `Token` 简化为 `Maybe Char`，即模型能生成的字符或信号生成终止的 `STOP` 词元。[1](https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html#fn1) 本节所述方法均将该训练好的网络视为固定的。它们仅修改推理过程，并沿两个维度展开： 1. 粒度（Granularity）：类型检查器被调用的频率？是在发出 `STOP` 词元时调用，还是每个词元都调用？ 2. 带宽（Bandwidth）：类型检查器反向传递什么信息？是结构化的错误消息，还是仅仅是二元的接受/拒绝信号？ 这些方法在这两个维度上处于两极，且都未能从根本上解决类型化生成问题，但在此描述它们有助于我们理解问题的症结所在。 #### 1. 尝试；编译；报错则重试 这是大多数程序员的做法。他们将原始文本键入编辑器；编译器要么将其处理成结构化数据(https://andrevidela.com/blog/2025/program-pipelines.idr/)，要么返回错误供程序员消化后再重新提交。 同样的循环也可以应用于 LLM。[2](https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html#fn2) 假设任务是生成类型为 `List Int` 的值，模型会生成一个候选项——比如，“`\[``1``,``2``,``3``\]``STOP`”——然后由控制器将其交给类型检查器。如果通过，任务完成；如果不通过，将错误反馈给模型要求重试。沿着我们的两个维度，这种方法具有低粒度（仅在生成 `STOP` 词元后调用类型检查器）和高带宽（错误是结构化消息，模型可进行推理）。 但存在一个问题。假设任务改为生成 `Either Char Double` 类型的值，而模型以“`\``1``,``2`”开头——这已经无法挽回，因为该类型的任何值都不会以`\[`开头。直到完整生成结束前，没有任何机制能察觉！此时整个序列被拒绝，模型重新开始。这极其浪费资源。 可通过缩短循环来补救——每次检查前生成的词元更少——在极限情况下，这正是经验丰富的依赖类型程序员所做的：走一小步，看编译器反馈，再走下一步。但这仅解决了粒度问题。与程序员不同，LLM 不会跨会话保留所学内容：此方法未更新权重，意味着下次运行时模型仍从相同状态开始。 #### 2. 约束解码 另一种方法是在采样每个词元*之前*咨询类型检查器，并屏蔽会导致非法类型结果的词元概率。 例如，若模型正在生成 `List Int` 类型的值，且已产生词元“`\[``1``,``2``,``3`”，则将字母的词元概率设为零，并在剩余词元中进行采样。[3](https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html#fn3) 尽管类型推断通常不可判定，但该方法已有广泛研究，并已应用于 JSON Schema 和各种类型系统的受限片段。[4](https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html#fn4) 沿我们的维度，它位于对角线另一端：最大粒度（每个词元）、最小带宽（每词元仅一比特）。此处输出保证通过类型检查！但存在一个大问题：**这仅防止模型说出某些内容，并未改变模型*想要*说出的内容**。 举例说明：若模型在示例中习惯为字母分配高概率，屏蔽它们会迫使其采样模型认为低概率的词元。每一步，掩码仅检查词元*是否可能*导向合法输出，而未考虑模型在各分支上保留的概率质量。这可能导致生成过程被困在仅存低概率补全的分支中，产生通过类型检查但越来越荒谬的输出。[5](https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html#fn5) 与前一种方法一样，梯度无法流过掩码，因此模型无法学会适应并为密集分支分配更高概率，因为权重从未更新。 ## 训练期间学习时间 上述方法虽然看似奇怪，但确实有效。采用重试循环的前沿模型取得了实质性进展：FrontierMath 得分从发布时的不足 2%(https://arxiv.org/abs/2411.04872) 到不到两年内接近 50%(https://epoch.ai/benchmarks/frontiermath-tier-4/)，ARC-AGI-2(https://arcprize.org/leaderboard) 和 SWE-bench(https://www.swebench.com/) 的得分也是如此。在国际象棋方面，GPT-4 作为通用训练的副产品，ELO 等级达到约 1371(https://blog.mathieuacher.com/GPTsChessEloRatingLegalMoves/)（中级玩家水平）。 这些都是显著的成就。但在那些我们知道如何训练*在训练过程中利用结构*的模型的领域，性能提升更为惊人。国际象棋就是其中之一。AlphaZero 系统在训练期间利用游戏规则结构，参数规模仅为 GPT-4 的约 30 分之一（<6000 万 vs 1.8 万亿），却达到了超人类 ELO (>3400)(https://arxiv.org/abs/1712.01815)。并且 AlphaZero 从未走出非法步法，而 GPT-4 在 30% 的对局中会出现非法步法。 那么依赖类型编程语言呢？这是一个极其丰富的领域，人们不禁想问，如果我们将其编译器紧密集成到神经网络训练中会发生什么？遗憾的是，这尚未发生：**我们实际上还不知道如何实现这一点**。目前大多数生成类型化代码的模型就像不知道规则就上场打球的人一样令人惊讶的是它们的表现有多好。 如果国际象棋的经验可以类推，那么编码语言规则显然是值得探索的。唯一的问题是：你如何对类型系统求导？既然类型是离散的、不可微的对象，你如何学会产出带类型的输出？ #### 对结构求导 为了理解求导，让我们从一个更简单的问题开始。如何在 Haskell 中编写以下类型的函数，模拟简单的输出结构选择：余积（coproduct）？ ``` f :: (x, p) -> Either a b f = ? ``` 如果你尝试写出它，无论多想创意，最终形状都是： ``` f (x, p) = if c (x, p) then Left (f_l (x, p)) else Right (f_r (x, p)) ``` 对于某个谓词 `c : \(x, p\) -> Bool` 和两个映射 `f_l :: \(x, p\) -> a`, `f_r :: \(x, p\) -> b`。别无其他选择。[6](https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html#fn6) 要生成 `Left` 或 `Right`，你必须通过 `c` 划分输入空间来承诺其中一个。当返回 `True` 时走左边，否则走右边。 这种分解并非 Haskell 的特性——它是范畴 \( \mathbf{Set} \)（集合范畴）的一个属性，该范畴是一种*广延（extensive）*范畴。[7](https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html#fn7) 这一属性正是对向余积映射求导研究的核心，最著名的有 CHAD (https://arxiv.org/abs/2103.15776) 和 高阶函数的高阶自动微分 (https://arxiv.org/abs/2101.06757?)。它们利用这一定理，并且似乎无需重试或约束解码——向我们展示了如何在*训练阶段*构建输出为结构化类型的网络。 但我们上面看到——这些方法要求我们程序员手动划分输入空间，而不是让神经网络自动学习。这意味着，给定一个网络 \(f : X \times P \to A + B\)，如果你的模型一开始猜错了分支 \(A\)，它永远无法通过梯度更新来修正，因为它从一开始就没能学会划分。[8](https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html#fn8) 同样的故事适用于通过其他结构（如对、归纳类型、函数对象(https://julesh.com/posts/2026-02-20-categorical-semantics-ultimate-backpropagator.html)）进行的自动微分。所有这些方法都*剥夺了模型学习结构的能力*。这是一个重要的视角，但在前述文献中被忽视了。当然，这是合理的，因为它们的重点是自动微分而非学习。但我从未见过明确承认这种区别，理应明确指出。 通常，我们不仅想要一种在一个*已知*程序中传播梯度的方法，而是希望具备学习程序本身的能力。 #### *针对*结构求导 我们还有另一种学习程序 \(f : X \times P \to A + B\) 的方式。与其固定划分，不如学习它？这巧合地解答了我们在做出离散选择时如何反向传播梯度这一问题：我们*根本不需要对离散选择求导*。相反，我们为每个离散选择*收集证据*，对其进行归一化，然后采样以决定下一步。 也就是说，我们使用三个映射： 1. 可微映射 \(f_c : X \times P \to D(\text{Bool})\) 2. 可微映射 \(f_A : X \times P \to A\) 3. 可微映射 \(f_B : X \times P \to B\) 然后，为了在给定 \((x, p) : X \times P\) 的情况下生成类型 \(A + B\) 的输出，我们对 \((x, p)\) 应用 \(f_c\)，然后从所得分布中*采样*。得到的布尔值指示是使用 \(f_A\) 还是 \(f_B\)。换句话说，\(f\) 现在是一个类型为 \(X \to D(A + B)\) 的映射，同时生成输出类型选择及其值的分布。 问题来了：我们如何对此求导并使用监督学习进行训练？也许出乎意料的是，这很简单。我们仅对被选中的分支求导，并使用交叉熵损失将生成的分布与真实分布进行比较。这意味着，只要我们能提供这三个神经网络，就能得到一个效果（effectful）神经网络，类型为 \(f : X \times P \to A + B\)。 该方法从构造上即可产出类型正确的输出。与前一种方法不同，它允许网络*学习*正确的输出类型。它还直接涵盖前一种方法：将采样温度设置为 `t=0` 即可恢复 `argmax`，即*对结构求导*。 更进一步，这个余积可以看作是由有限集索引的依赖对的一个实例。它可以以多种方式推广，并可迭代生成一组类型化结构数组，全部以完全严谨的方式进行！正如我们将在（后续帖子中）看到的——实现这一点的核心是*容器*理论，而推进此事的唯一途径就是*构建所需的类型化基础设施*！ 这令人无比兴奋。 当然，这一想法在文献中已有一定程度的研究。最粗略地说，教师强制法（teacher forcing）是其无类型变体。2017 年出现的抽象语法网络 (Abstract Syntax Networks, ASNs) (https://arxiv.org/abs/1704.07535) 也描述了这一点，但没有（依赖）类型。与 AlphaZero 一样，ASN 早于 LLM 时代，但并未进一步扩展规模。也许这是因为在这种方法能大放异彩的依赖类型语言缺乏知名度？谁知道呢？ 当然，还值得一提的是 AlphaZero 和 AlphaProof。它们使用约束解码，但*在训练阶段*，仅通过强化学习更新所选分支。在 AlphaZero 中，这在国际象棋、围棋和将棋上达到了超人类表现。但到了 AlphaProof，情况则不同。尽管强化学习方法类似，所有模型的输出空间仍然只是 `List Token`。这意味着类型决定了哪些策略获得强化，但梯度仍流经粗粒度的词元类型，与底层编程语言的类型完全解耦。 ## 结语 LLM 基于扁平的词元词汇表运行。我们在其外围应用的每种结构技术——如重试或约束解码——都是试图在没有意义概念的输出上强加意义。“针对结构求导”所提出的是：输出空间本身即可携带意义。词元不再是不透明的字符或子词；它与生成输出所在的领域意义紧密相连。这意味着，我们的编程语言结构越丰富，收益就越大。 这看起来像是在反对规模扩展和“痛苦的教训”（Bitter Lesson）。事实并非如此。我认为这是一种让规模在正确对象上发挥作用的举措。正如在国际象棋中，将游戏规则编码进训练所产生的飞跃，是今天任何数量的推理时搜索都无法企及的；这里的举措是将编程语言本身编码进训练，并在真正反映我们要产出内容的结构上应用规模。 最后，“对结构求导”与“针对结构求导”的区别，本质上是将类型级选择视为固定脚手架与将其视为网络可学习内容的区别。两者都能产出类型正确的输出，但只有后者能使输出的具体细节得以学习。用于统一描述这些类型化动作空间的数学语言——涵盖求和、乘积、归纳类型以及依赖类型——最终便是容器（containers）与依赖透镜（dependent lenses）的语言。 这才是这条研究路线真正有趣的地方。 感谢 Jules Hedges (https://julesh.com/) 和 Andre Videla (https://andrevidela.com/) 对本文章草稿提供的反馈意见。 --- 1. 实际上，一个词元由以下两者之一组成：1) 2-4 个字符的组合，旨在近似熵最优编码（高频字符组合获得较短编码）；或 2) 不透明*元词元*之一，不携带字符内容，而是用于向运行 LLM 的*控制器*发送控制流信号。这方面的一个基本例子是 `STOP` tok