Lean软件规模定律（阅读时间17分钟）

# 精益软件缩放定律 来源：https://gwern.net/lean-scaling 研究方案，旨在测量编码LLM的困惑度如何随代码库上下文大小缩放，以Lean为例，探讨形式语言是否具有更好的可预测性指数，并可能在全球范围内实现更安全、更可靠的软件。 > 研究思路：通过实验测量编码LLM的困惑度随代码库大小的缩放情况，估算编程语言或其他因素对“可预测性”的缩放定律。这应能转化为整体安全性和可靠性。我们可以用现代LLM进行昂贵测量（从头训练和微调），或通过廉价方式（在越来越大的源代码上下文窗口上测量困惑度）。那些缩放定律指数更优的代码库和编程语言，最终将更易于LLM理解、修复和编写。特别是，Lean编程语言可能（在2026年左右的LLM上）在现有代码库上具有更差的基准常数和总损失，但拥有更好的缩放指数。这意味着用Lean实现的代码最终能胜出，并在全球范围内带来程序正确性的巨大收益——从而有助于证明大规模投资重写现有代码库（或编写新Lean代码）的合理性，进而改善全球网络安全。 编码LLM目前正朝着在近期内编写大部分软件的方向发展，尽管其质量普遍平庸或甚至不安全（“vibecode”软件尤其糟糕）。未来的LLM重写可能有所帮助，但无法保证会实现，也无法弥补我们抵御普遍存在的网络安全LLM攻击所需的漏洞。我们如何避免这种情况？LLM有可能以可证明的安全、可靠的方式编写所有软件，例如形式可验证系统，但这方面的进展滞后。 滞后多少？ ## 语言先验 (https://gwern.net/lean-scaling#language-priors) 神经缩放定律 (https://en.wikipedia.org/wiki/Neural_scaling_law) 方法论在深度学习中的应用仍然不足，用于验证现有方法和预测未来应用。一个例子是编码智能体：人们普遍观察到，LLM (https://en.wikipedia.org/wiki/Large_language_model) 对更常见的语言表现更好，因为可用数据更多。Luo et al 2025 (https://arxiv.org/abs/2510.08702) 认为编程尤其数据饥渴，因此可能存在长期的“锁定”，升级到更好的技术（如 Haskell (https://en.wikipedia.org/wiki/Haskell)、Rust (https://en.wikipedia.org/wiki/Rust_(programming_language)) 或 Lean (https://en.wikipedia.org/wiki/Lean_(proof_assistant))）将不可能。 但这并不成立：作为拥有大量训练数据的流行语言，只意味着LLM*默认起始表现*良好。（由于很难将编程语言与其整体生态系统分离，这里我只提“语言”。） 任何语料库都可以被视为一种“先验”，语言之间存在某种兑换率 (https://gwern.net/doc/ai/scaling/abstract#exchange-rate)，更好的 Python (https://en.wikipedia.org/wiki/Python_(programming_language)) 技能会部分迁移到，例如 Haskell（参见 Yang et al 2025 (https://arxiv.org/abs/2512.13472)）。因此，“水涨船高”是可能的，事实上，更好的编码LLM可能会在LLM变得“足够好”时带来冷门语言的复兴，程序员不再需要花费数年重新学习一切。 ## 规模失效 (https://gwern.net/lean-scaling#scale-failure) 这也不意味着随着代码库扩展它们会一直表现良好。许多事情在小规模下工作良好，但在大规模下却逐渐失效。像 Haskell 这样的语言的“BDSM”纪律，如果你在编写一个快速的临时程序，可能会令人恼火和痛苦，但当你拥有数百万行复杂代码时，它可能变得不可或缺。因此，LLM 编写*少量* Python 可能很容易……但*大量*呢？一个短脚本很容易编写，陷阱很少，尤其是 LLM 可以轻松地在上下文窗口中查看整个脚本。但是，随着代码库变得越来越大、越来越复杂、越来越陈旧，无法再放入上下文窗口，会发生什么？它能保持动态类型 (https://en.wikipedia.org/wiki/Dynamic_types) 和异常 (https://en.wikipedia.org/wiki/Exceptions) 清晰吗？那个黑暗角落里的猴子补丁 (https://en.wikipedia.org/wiki/Monkey-patching) 呢？或者那个在升级过程中改变了运行时行为的依赖项呢？因为如果不能，即使一个错误也可能是致命的，并迫使人类程序员花费数周调试微妙的错误。 在运行时速度和编程语言能力方面，最极端且可能用于实现大型软件程序的编程语言是 Lean，它正经历着突然的流行热潮，因为人们和 LLM 发现它在定理证明之外还有用途，可用于实现真正的程序。甚至像 zlib (https://en.wikipedia.org/wiki/Zlib) 这样的东西也有 Lean 重写版 (https://leodemoura.github.io/blog/2026-2-28-when-ai-writes-the-worlds-software-who-verifies-it/#a-sign-of-things-to-come)！ ## Lean 瓶颈 (https://gwern.net/lean-scaling#lean-bottleneck) 我们现在可以想象用 Lean 重写软件和编写新软件，以消除内存安全问题、异常、越界错误，证明主要属性（如无损压缩）的正确性等。 缺点在于……现存的 Lean 源代码并不多。所以不出所料，LLM 在这方面并不是*那么*好。还不足以自主翻译具有比 zlib 更复杂 I/O 或行为的大型复杂代码库。 因此我们有点“先有鸡还是先有蛋”的问题。我们可以用 LLM 创建大型 Lean 代码库，用于训练，从而用 Lean 替换所有现有代码，但这前提是我们一开始就有大量大型 Lean 代码库，并且大概是通过用 Lean 替换现有代码获得的。 而且，Lean 是否真的那么出色，或者即使存在大量大型 Lean 代码库且 LLM 经过训练，它们是否真的能有效编写大型 Lean 代码库，这并不清楚。也许 Lean 设计得不好——我们怎么知道？也许一个真实的 Lean 代码库最终会变成一团泥浆 (https://gwern.net/doc/www/www.laputan.org/adbd0a074c088fed419b988f18c9a454aab199d4.html)，或者充斥着大量临时特例暴力证明（不免被戏称为“mathslop”）。 ## 可预测性代理 (https://gwern.net/lean-scaling#predictability-proxy) 测试这一点的一种方法是问：从 LLM 的角度来看，一个设计良好的语言应该是什么样的？ 如果它充满了临时设计选择、大量暴力、错误或重复等，从 LLM 的角度看，这应该像一个“难以阅读”的代码库。你需要阅读越来越多的 token 才能理解发生了什么；会有高度不可预测的行为，因为存在全局状态、覆盖和“陷阱”——你不能只看一个文件就理解一切，必须查看十几个其他文件，追踪替换和重写，才能弄清楚它*通常*做*X*，除非这个未文档化的 shell 变量被用户设置了，那样它就会（大概）做*Z*。这意味着你永远无法确定接下来会读到什么；任何时候，都可能有一些随机的东西打断，或者你可能因为原始代码就是有 bug 而预测错一行……即使当前模块写得很好，只使用事实上的“安全子集”，在规模上，代码库也会是好坏参半的鸡蛋——程序员越多，时间越长，复杂度越高，代码就越拼凑。 相反，一个架构良好的代码库，使用强类型内存安全语言，应该是相反的：很容易孤立地阅读代码，因为没有逃生舱口或后门，一切如其所是；事物通过文档化的接口进出，而且，嗯……一句话，*可预测*。 但不仅仅是可预测，因为大量的样板代码或数据或冗余测试用例也可能是可预测的。好的设计，在大规模下，是*越来越*可预测的，因为你看到更多系统并理解其设计。而大规模下的糟糕代码是越来越*不可预测*的，因为看到更多系统并不能帮助你理解其余部分。（糟糕代码越多，语言和系统越宽松，你就越无法确定任何事情，因为即使是最完美的手写代码库中也会有 bug 或意外交互。而“坏”证明（如暴力用例或归约）的特征是你“学不到任何东西”——每个用例都和上一个一样可预测。） 因此，我建议 LLM 预测精度，或困惑度 (https://en.wikipedia.org/wiki/Perplexity) / 每字符比特数 (BPC)，是整个系统可预测性的一个弱代理，而可预测性是一个关键的缩放属性。那些相比竞争对手，在大型系统上越来越可预测的编程语言，将最终与 LLM 配合得更好。 ## 测量设计 (https://gwern.net/lean-scaling#measurement-design) 我们可以用冻结的预训练 LLM（例如 GLM-5.2 (https://z.ai/blog/glm-5.2)）以最廉价的方式经验性地测量这一点： 1. **语料库构建**：按语言获取现有源代码语料库，将其转换为一个大的文本文件（带有适当的元数据头部），可能打乱顺序，或者按依赖排序； 2. **损失测量**：运行 LLM 前向传播，测量完整上下文窗口中每个 token 位置的困惑度（归一化为字节以考虑分词器偏差，并理想情况下按语言归一化以考虑一般行代码长度差异，因为不同语言长度可能相差 10 倍，造成混淆）； - *交叉验证*： - 异常/bug 检测：为了进一步测试，作为一种“逆缩放”，我们可以向上下文窗口中注入噪声，如微妙的 bug；LLM 越惊讶越好。（缺少边界检查、错误的单位转换、符号错误、过于宽泛的异常处理器、静默的类型转换，或看似完美但错误的定理引理，可能在风格上完美，但需要对整个代码库有深入的语义理解才能标记出来。） - 正确性：通过人工上下文限制来隐藏越来越多的代码库，多少采样 rollout 仍然编译并通过所有质量测试？ - **Lean 签名**：特别是，编码 LLM 能否仅凭模块签名头预测出一个可工作的 Lean 模块？类型签名是否将问题空间约束得如此之紧，以至于“只有一种做法”？ - *消融实验*：任何可选组件，如类型签名 (https://en.wikipedia.org/wiki/Type_signatures)，可以被移除/添加，并量化全局收益。（*类型签名*真的有助于编码 LLM……还是只是冗余的混乱？或者它们只在达到一定规模后才有所帮助？） - *语义分析*：在给定语言中，哪些部分特别不可预测？哪些是高度可预测的样板？前者可能反映了 bug 或误导性的源代码，应忽略（也许有些程序员写了非常令人困惑的不一致标识符），后者可能反映了语言设计缺陷，未能提供足够的抽象。 - *核心集 (https://en.wikipedia.org/wiki/Coreset) / 最小上下文*：一个设计良好、模块化程度高的系统，你只需阅读少量关键部分就能理解任何给定部分。LLM 可以尝试生成最小上下文，以实现与完整代码库前缀（oracle）大致相同的损失（参见我的 SAE truesight 提案 (https://gwern.net/sae-truesight)）；越短越好，这应该缩放良好。一个设计良好的 Lean 代码库应该需要更小的上下文窗口（仅类型和定理签名）就能完美预测下一个函数，而 Python 代码库可能需要 LLM 读取 10 个不同的文件来猜测动态运行时行为。 - *改进评分*：重构和清理编辑是否使代码库更可预测？如果是，则提供了有用的训练数据信号，特别是在压力测试编码 LLM 的软件工程“品味”的场景中，比如只通过迭代引入新需求。 3. **位置平均**：按上下文窗口中的 token 位置平均； 4. **曲线拟合**：为每种语言拟合缩放定律； 5. **外推**：最后，外推以寻找交叉点（例如，在多大尺寸下，Lean 代码库会比 Python 代码库在绝对意义上更可预测？编码 LLM 需要多大才能达到足够性能，包括上下文学习或动态评估 (https://gwern.net/doc/www/arxiv.org/d89a27c6115eb714aae5a8393ebba775cff720d2.pdf#deepmind)？）——并将常数/指数作为设计指标。 我认为这足够简单，一个研究生或 MATS (https://www.matsprogram.org/) 项目可以完成。 ## 交叉点预测 (https://gwern.net/lean-scaling#crossover-forecast) 我预测我们会发现，“弱”语言（支持较少不变量、动态类型或可变全局状态等）在小规模（如数千行代码）更容易预测，但缩放指数更差，而最流行的“强”语言（如 Haskell）会在数十万或数百万行代码处“交叉”。我们还会发现，Lean 不一定在任何合理长度下在绝对损失上“交叉”，因为它有一个很高的常数，但它会有最好的缩放指数，因此仍然会在某个点交叉。 这将激励对 Lean 研发和移植进行大规模投资，通过直接购买训练数据来解决先有鸡还是先有蛋的问题。 人们可能还能估计出总训练语料库以及 Lean 与 Python/JS 等的比例，并尝试反推出一个估计：需要*多少*训练数据才能将 Lean 交叉点降低到任何特定仓库规模，方法是在语料库上回归常数。Lean 可能太昂贵，因此还可以尝试估计兑换率，并考虑购买/生成更多其他语言（如 Haskell）的代码是否更具成本效益。（代码可以通过数据标注者在市场上购买，也可以通过使用智能体 LLM 自动转译代码库（可能反复进行）来用算力获取，这大致上应具有尝试次数的对数缩放。） ## 偏差控制 (https://gwern.net/lean-scaling#bias-controls) 初始估计至少会部分受到程序员和领域差异的混淆；Lean 代码强调数学，Lean 程序员非常不寻常（通常是学者或爱好者），而 JavaScript 编程强调由普通程序员编写的 Web 开发和业务代码，因此这些差异本身会驱动不同的指数。目前尚不清楚这些系统性偏差有多严重；如果首次分析发现 JavaScript 缩放优于 Lean，那么朴素方法就必须被抛弃。 这可以通过尝试按“主题”匹配代码库并分析配对差异来部分控制。但随着编码 LLM 越来越好，其评估越来越现实，更大规模的编程语言缩放定律扫描可以通过合成受控比较来消除这些偏差：用两种不同语言编写相同的规范，达到相同的测量质量，*然后*测量困惑度差异。（例如，原始……）