Kolibri 与 MathForm-8B：其中一项准确率声明可由编译器验证

Kolibri与MathForm-8B共享一个许可证，除此之外几乎别无共同之处。两者均采用 Apache 2.0，均为开放权重，且均在近三个月内发布——Aleph Alpha 的 Kolibri 于 2026 年 10 月 3 日发布，OpenBMB 的 MathForm-8B 于 2026 年 8 月 14 日发布——并且两者的模型卡都有很大一部分内容围绕数学展开。相似之处到此为止。Kolibri 是一个拥有 781 亿参数的德语和英语混合专家模型，每个 token 激活 34.6 亿参数，旨在用于受监管的文档工作流。MathForm-8B 是一个 80 亿参数的稠密模型，基于 Qwen3-8B 微调，只承担一项任务：接收用普通英语写成的数学问题，并输出其形式上正确的 Lean 4 陈述。对于任何评估这两者之一的人来说，真正重要的区别并不在于参数规模。而在于 MathForm-8B 的准确性声明是可执行的。你可以用编译器检查它的输出。Kolibri 的则只能通过另一次基准测试运行来检查。

这种不对称就是整篇文章的主旨，而且它的适用范围远远超出这两个模型。厂商的基准测试表是一种宣称；证明助手接受一项形式化则是一个结果。当一个模型的整个输出空间都是机器能够验证的东西时，营销层就消失了——Lean 编译器要么接受该陈述，要么不接受，再多发布帖的叙事包装也改变不了这一点。

MathForm-8B 实际会产生什么

自动形式化是一项范围狭窄、不起眼且真正困难的任务，而模型卡对相关设置的描述具体得令人耳目一新。

• 输入与输出——输入自然语言的数学陈述，输出 Lean 4 形式化结果，并附带定理头。

• 基础模型 — Qwen/Qwen3-8B，经微调；Apache 2.0，与 OpenBMB 发布的其他内容一致。

• 训练——在 FormalVerse 数据集上进行监督微调，随后进行强化学习，由 Lean 编译和语义一致性反馈驱动强化信号。

• 数据流水线——Mathlib 知识检索、编译与语义验证、迭代精炼，然后是轨迹重建。模型卡上的流水线图是本次发布中最具信息量的内容。

• 评估——在语法检查和一致性检查这两项独立检查下的 Pass@8 通过率，覆盖六个基准，以等权宏平均的形式呈现在卡片上的一幅图中，而非以我们能够逐行引用的表格形式呈现。

• 工具链——用于编译检查的运行中的 Kimina Lean Server、用于实验的 Lean 4.21.0，以及一个最大序列长度为 16,384 个 token、温度为 0.6、top-p 为 0.95 的序列。

• 服务 — vLLM 或 SGLang，上下文长度为 16,384 个 token，通过 OpenAI 兼容的聊天接口对外提供。最后这个细节比看起来更重要，因为它意味着模型可以作为一个普通端点接入现有流水线。

注意这两个彼此独立的检查。Syntax Check 关乎 Lean 语句究竟能否解析并通过类型检查。Consistency Check 关乎形式化语句与自然语言问题是否含义相同——这是一项困难得多的性质，因为一条语法上有效却形式化了错误定理的 Lean 语句，比一个编译错误更糟。OpenBMB 把两者都报告出来，这正是正确的做法，也正是这项任务拥有通用推理所不具备的验证闭环的原因。

Kolibri 用数学做什么，以及为什么它是一种与众不同的数字

Kolibri 在基准测试意义上擅长数学。在 Aleph Alpha 自家的后训练评测框架中，当推理强度设为高时，它在 AIME 2025 英语上得分为 96.9，德语为 87.5；在 AIME 2026 上分别为 96.0 和 90.0；在其数学套件上的英语平均分为 96.5，而德语为 88.8。作为同一表格中的背景参考，Kolibri 在 AIME 2025 英语上的 96.9 高于 Nemotron 3 Super 120B-A12B 的 91.7 和 Qwen3.6 35B-A3B 的 84.6，略低于 Qwen3.8 27B 的 97.9。

那些数字中的每一个都是厂商自行报告的，是在厂商自己的评测框架上得出的，没有经过独立复现，而且也没有 Kolibri 的 Artificial Analysis 页面可供交叉核对。这不是在批评这些数字；而是在说明它们属于怎样的一类东西。AIME 分数是选择题考试中最终答案正确的百分比。它能说明的只是，这个模型能得出一个整数。它完全不能说明产生这个答案的推理是否可靠，而且也没有留下任何可供第三方检查的产物。

把MathForm-8B的输出放在旁边，这种差距就一目了然。Kolibri对一道AIME题目的回答是一个数字。MathForm-8B的输出则是一条Lean 4定理陈述，它要么能对Mathlib编译通过，要么不能。如果你正在构建一个系统，其中数学断言必须站得住脚——比如形式化验证流水线、证明助手工作流、审计追踪——那么后一种产物比前一种的价值要高得多，而任何基准测试表格都表达不出这一点。

两者实际会相遇的地方

如果把它看作一场对决，这种配对没什么意思：一个 8B 专家模型在数学形式化上胜过 78B 通用模型，却在其他所有方面落败，包括德语行政公文、长上下文文档推理，以及跨一百步智能体轨迹的工具调用。但二者并非替代关系，真正有用的问题是：由两者共同构建的流水线会是什么样。

自然的组合方式是路由式的组合。一个具备强大推理能力和工具调用能力的通用模型负责接入、消歧与检索；而那百分之二需要形式化产物的情形，则调用专家模型。手工来做，意味着两家供应商、两份合同、两套 SDK、两组凭据，以及一个需要有人维护的调度层。这正是单一端点能体现其价值的场景：一个兼容 OpenAI 的密钥，一条路由规则把数学形态的请求送往形式化器端点、其余一切送往通用模型，并在其中之一变慢时进行故障转移。这正是路由 DSL 的职责——把若干模型组合成一次调用，而不是在开发阶段就硬编码一个选择——而在让一组模型共同作答有用的地方，则由模型融合来覆盖。Kolibri 和 MathForm-8B 都不在目前的 OrcaRouter上；我们按各种供应商与模型拼写方式在目录中检索了这两者，都没有找到。这个组合论证关乎问题的形态，而不是这两个具体的端点。

目录上展示的，正是该模式中通用型的那一半，而且价格可以量化衡量。Qwen3.8-27B 标价为每百万输入 token 0.33 美元、输出 2.40 美元，上下文窗口为 262,144 个 token；Qwen3.8-Max 则为 2.00 美元和 6.00 美元，窗口为 100 万 token。对于一支正在探索是否值得在文档流水线中加入形式化步骤的团队来说，成本最低的实验就是把通用型工作路由到那里，测量真正需要 Lean 产物的请求量，然后才决定是否值得配置一个 16,384 token 的专家端点。供应商的标价是原样透传的，每个 token 都不加价，所以一旦供应商调价，这些数字当天就会变化。

许可证是它们唯一完全相同的那一行

两者均采用 Apache 2.0 许可，而在定制研究许可证和可接受使用附加条款十分常见的这一类中，这是一个真正值得指出的对等点——这意味着两个模型在被商业使用、修改或再分发之前，都不需要经过法律审查。

在其他方面，这些要求有所不同。Kolibri 带来约 78 GB 的权重占用，以及硬件下限：两张 A100 80 GB 卡、两张 H100 SXM5、一张 H200、一张 B200 或一张 B300，外加厂商的 aleph-alpha-inference 包和 vLLM 插件。MathForm-8B 以 bfloat16 精度约为 16 GB 权重，可在单块现代加速器上以 16,384 token 的上下文提供服务；其依赖项是 Lean 工具链，以及用于评估管线的运行中的 Kimina Lean Server。其中一种部署适合放在工作站里。另一种则不行。

这些上下文数字恰恰说明了相反的情况，而且差距悬殊。Kolibri 的原生窗口为 262,144 个 token，经验证可达 1,048,576 个 token，这正是它成为文档模型的原因：一份完整的德国监管申报文件或航空航天维护手册都能在一次调用中容纳。MathForm-8B 按设计上限为 16,384 个 token，因为形式化请求就是单个问题陈述，没有理由更长。这两个数字都不是缺陷。它们只是描述了不同的任务。

选择，以及下面的验证问题

• 如果你的输出必须可校验，就选 MathForm-8B。如果下游系统使用 Lean 4，或者关键在于让证明助手对结果签字确认，那么没有通用模型能替代它，而需要审视的是 Syntax Check 和 Consistency Check 下的 Pass@8 数字，而不是任何 AIME 行。

• 如果你需要这样一个模型——它能在长上下文中读取德语和英语文档、跨文档进行推理、调用工具、在上下文不足以支撑答案时拒绝作答，并且能够在自己的边界内、以一句话就能说明白的许可证来部署——那就选 Kolibri。数学是它具备的一项能力，而不是它所代表的产品。

• 如果你正在构建形式化流水线，就要同时考虑两者。不是把它们当作替代方案，而是当作同一条路由规则背后的两个端点，只在需要它的那一小部分请求中调用专家。

而且，如果你要凭一个基准分数来评估两者中的任何一个，先做个测试：问问这个数字留下了什么产物。对于 MathForm-8B，有一个 Lean 文件和一个编译器，编译器要么接受它，要么不接受，而你今天下午就能亲自运行这两者。对于 Kolibri，只有一个发布表格里的百分比，由厂商报告，未经复现，也没有独立的索引页面可供核对——而证伪它的唯一方法，是下载 78 GB 的权重，租用硬件，再重新运行测试框架。当你决定要把什么投入生产时，这种不对称性比分数本身更有价值。