夜雨聆风大家好，我是点点，今天是茶谈005期，来聊一聊关于模型参数对模型能力的影响
上周，一篇来自 arXiv 的论文安静上线。没有发布会，没有 CEO 推文，连 Hugging Face 上的讨论区都只有零星几条。
但它的结果让不少人愣住了：一个 4B 参数的模型，在 MiniF2F 定理证明测试中，以 86.1% 的准确率击败了 671B 的 DeepSeek-Prover-V2（82.4%）。
参数量差了 167 倍。如果比作军队，相当于一个连打赢了一个集团军。
这不是微弱优势——3.7 个百分点的差距在 AI benchmark 上意味着一代模型的代差。而这一切发生在一个 4B 模型身上。
4B 怎么赢的？
先说结论：不是 4B 模型变强了，是 671B 模型一直在浪费参数。
Pythagoras-Prover 的核心创新可以拆成三件事：
第一，课程学习（Curriculum SFT）。 不像惯常做法那样把所有难度的证明一股脑丢给模型，他们把训练数据按难度分成 easy / medium / hard 三档，让模型从简单证明开始，逐步往难走。像教小孩做数学——先加减，再乘除，最后才碰竞赛题。听起来很直觉，但在大模型训练中，这种"分龄教学"远没有"暴力灌数据"性感，所以很少人愿意认真做。
第二，动态证明推理过滤。 大模型做定理证明时，中间推理步骤可以拉到几万 token。Pythagoras 的做法是：在训练时硬性裁剪到 8k token，但保留真正有信息量的推理步骤，只丢掉那些重复和冗余。 这不是暴力截断，是做了一轮"去噪"——保留信号，扔掉噪声。8k 的短上下文反而让模型学到更紧凑的推理路径。
第三，也是最关键的——增强 Lean 形式化（Augmented Lean Formalisation，简称 ALF）。 定理证明领域最大的瓶颈不是算法，是数据稀缺。经过 Lean 验证的证明语料极其有限——想象一下，你要训练一个编程模型，但全世界只有几万行经过编译器验证的代码。ALF 的做法是：对已有的形式化命题做变体生成——不是简单的数据增强，而是在保持形式化特征的前提下扰动命题的表面形式，然后通过自蒸馏（self-distillation）填充训练信号。这相当于把一道数学题改写成十种不同表述，让模型学到"本质相同的命题可以有无数种面孔"，而不是死记一种写法。
671B 为什么输？
DeepSeek-Prover-V2-671B 是 DeepSeek-V3 的衍生模型，采用的是 Mixture-of-Experts（MoE）架构。671B 参数听起来骇人，但 MoE 架构的特点是：每个 token 只激活部分专家，实际推理时用到的参数远小于 671B。
问题在于：MoE 的"稀疏激活"在通用任务上是优势，在定理证明这种极度专业化的任务上可能反而成了劣势。 通用大模型需要理解一切——从火锅食谱到量子物理，MoE 的多专家机制正好各管一摊。但定理证明是一个封闭的形式化世界，需要的是深度而非广度。671 个"专家"中，真正理解 Lean 语法的可能只有一小撮，剩下的大量参数要么在睡大觉，要么在做无关的推理，消耗算力但不产出证明。
换句话说，DeepSeek-Prover-V2 就像拿一个大学全科医院去做一台微创手术——设备齐全，但针对性差。
小模型时代真的来了吗？
别急着下结论。先看清几个限定条件：
第一，这是定理证明，不是通用推理。 Lean 定理证明是一个形式化的封闭世界——规则明确、目标清晰、验证自动。这恰好是小模型最容易出成绩的场景。如果换成开放域对话、创意写作或跨模态推理，4B 模型大概率还是被 671B 按着打。
第二，MiniF2F 不是一个特别大的基准。 高中数学竞赛级别的证明题，总共也就几百道。4B 模型在这个数据量上做到高效泛化是合理的，但换成 PutnamBench（大学竞赛，672 道题），32B 模型也只解出了 93 题（13.8%），说明上限还远没到。
第三，ALF 做的 MiniF2F-ALF 基准揭示了一个尴尬的事实：所有模型在上面都掉分。 这说明之前刷高的分数里，有多少是"记住"而非"理解"，值得深思。
但即便有这些限定，Pythagoras-Prover 传递的信号是清晰的：在足够结构化的任务上，精心设计的数据策略和训练流程，可以做到比暴力堆参数更高效。
这不是"小模型替代大模型"的叙事。更准确的说法是：大模型和专用小模型不是竞争关系，而是不同层级的关系。 大模型负责探索问题和定义范式，小模型负责在确认有效的范式内做极致效率优化。就像工业革命不是靠一个超级工厂，而是靠成千上万个专业化车间。
对行业的三个实际影响
1. AI 编程助手的算力成本可以被大幅压缩。 定理证明和代码生成在形式化程度上一脉相承。如果 4B 模型能在证明任务上击败 671B，那在特定代码补全和 bug 修复场景中，专业化小模型也可能做到"足够好"的同时成本降低两个数量级。对于 Cursor、Windsurf 这类产品，这意味着推理成本从"烧钱"变成"可控"。
2. AI 安全验证迎来更现实的路径。 形式化证明是 AI 安全领域最硬核的验证手段之一，但过去受限于计算成本几乎无法大规模部署。4B 模型在消费级 GPU 上就能跑，这让"AI 输出经过形式化验证"这件事从理论可能性变成了工程可行性。
3. "Scaling Law 已死"被再次提及——但这次有数据支撑。 2024 年底开始有人讨论 Scaling Law 的边际收益递减，但缺乏有力实证。Pythagoras-Prover 提供了一个干净的对照实验：在同一个任务、同一个基准上，167 倍的参数差距被更好的数据策略逆转。 这比任何理论推演都有说服力。
我的判断
Pythagoras-Prover 不是"小模型逆袭大模型"的宣言，它更像一个提醒：在 AI 能力的金字塔里，参数规模只是地基，数据策略才是建筑结构。 地基打多宽决定了你能建多高，但建得稳不稳、快不快，取决于结构设计。
671B 模型不会死，甚至不会变弱。但越来越多的 4B 模型会在自己的垂直领域里证明：在正确的问题上用正确的方法，"小"也可以是一种竞争力。
这大概才是 Scaling Law 时代之后，真正值得关注的转向。
消息信源
arXiv 原始论文: https://arxiv.org/abs/2606.12594 (L1，提交日期 2026-06-10) Risewave 论文解读: https://www.risewave.com/pythagoras-prover/ (L2，2026-06-12) EmergentMind 论文分析: https://www.emergentmind.com/papers/2606.12594 (L2，2026-06-12) DeepSeek-Prover-V2 Hugging Face 模型页: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B (L3) DeepSeek-Prover-V2 技术分析: https://deepseeksai.com/prover-v2-671b/ (L2)
