精益软件扩展定律发布

背景

随着大型语言模型（LLM）在代码生成领域的广泛应用，人们发现LLM生成的软件质量参差不齐，安全性隐患突出。现有研究多关注LLM在常见编程语言上的表现，但忽略了代码库规模增长时LLM理解能力的退化问题。与此同时，形式化验证语言（如Lean）因其严格的类型系统和可证明正确性，被视为提升全球软件安全性的潜在路径，但其普及面临“鸡生蛋”困境：缺乏足够多的训练数据，导致LLM难以有效处理Lean代码。

核心内容

本文提出一项研究方案：通过度量LLM在代码库上下文规模增大时的困惑度（perplexity），来估计不同编程语言的“可预测性”扩展定律（scaling laws）。具体方法有两种：一是从零开始训练并微调LLM（成本高），二是在递增的源代码上下文窗口上直接测量困惑度（成本低）。核心假设是：那些在扩展定律中具有更好指数（exponent）的编程语言和代码库，将来会更易于被LLM理解、修复和生成。

特别地，Lean编程语言可能在2026年左右的LLM上，其基线常数和整体损失（total loss）比主流语言更差，但其扩展指数更好。这意味着：随着代码库规模增长，Lean代码的“可预测性”优势会逐渐显现，最终在全局范围内带来程序正确性的巨大收益，从而证明大规模投资重写现有代码库或编写新Lean代码的合理性，最终改善全球网络安全。

当前LLM生成的代码质量普遍平庸甚至不安全（尤其是“vibe coding”方式生成的代码），但未来大部分软件可能仍由LLM产出。如何避免LLM驱动的网络安全危机？一种理想方案是让LLM以可证明安全的方式（如形式化验证系统）编写所有软件，但这一领域进展远远落后。

语言先验（Language Priors）：神经扩展定律方法在深度学习中长期未被充分用于验证现有方法和预测未来应用。例如，在编码智能体（coding agents）领域，人们普遍认为LLM在更常见的语言上表现更好（因数据更多），Luo et al. 2025甚至认为编程尤其“数据饥渴”，因此存在长期锁定效应，升级到Haskell、Rust或Lean等更好技术是不可能的。但本文认为这一结论不成立：流行语言数据多仅意味着LLM初始表现不错；而且语言之间存在知识迁移（如更好的Python技能会部分转移到Haskell，参见Yang et al. 2025）。因此，LLM整体能力的提升可能“水涨船高”，甚至当LLM足够好时，晦涩语言可能迎来复兴，程序员无需花费数年重新学习。

规模失效（Scale Failure）：即便LLM在小规模代码上表现良好，随着代码库扩大，问题会逐渐暴露。例如，Haskell的严格约束在编写一次性小脚本时令人恼火，但在百万行复杂代码中却不可或缺。LLM可以轻松写出短小的Python脚本，因为整个代码可放入上下文窗口；但当代码库变大、变老、超出上下文窗口后，动态类型、异常、猴子补丁（monkey-patching）、依赖升级引发的运行时行为变化等都会导致致命错误，迫使人类程序员花数周调试。

Lean的瓶颈：Lean是目前最极端的编程语言之一（兼顾运行时速度和语言表达能力），其应用已从定理证明扩展到实际程序（如用Lean重写zlib）。理论上，用Lean重写软件可以消除内存安全问题、异常、越界错误，并证明主要属性（如无损压缩）的正确性。但问题在于：现有Lean源代码极少，LLM还不擅长处理Lean代码，更无法自主翻译大型复杂代码库（其I/O或行为比zlib复杂得多）。这就形成了“先有鸡还是先有蛋”的困境：我们想用LLM创建大型Lean代码库，再训练LLM以替换现有代码，但前提是已有大量Lean代码库并已替换了现有代码。此外，Lean是否真的优秀尚不清楚——也许实际的大型Lean代码库最终也会变成一团泥巴，充满临时特殊案例暴力证明（所谓的“mathslop”）。

可预测性代理（Predictability Proxy）：如何测试一个语言设计是否优秀？从LLM视角看，一个好的设计应该让代码库“易读”。充满临时设计决策、暴力破解、bug或重复的代码库，LLM需要阅读更多token才能理解，行为高度不可预测（全局状态、覆盖、陷阱），无法只看一个文件就明白，必须追踪十几个文件。反之，良好架构的代码库（强类型、内存安全）应该是隔离可读的，没有逃生口或后门，一切都是表面所见，通过文档化的接口输入输出——简而言之，“可预测”。

但单纯的可预测性并不充分：大量样板代码、数据或冗余测试用例也可能很“可预测”。此前有人尝试通过单个词的困惑度或gzip压缩后的代码库大小来评估代码质量，结果失败：比如gzip压缩效果最好的是JavaScript，其他语言结果也不令人信服。问题可能不在于“可压缩性”本身，而在于其导数（二阶梯或三阶梯）。良好的大规模设计不一定直观上可预测（“好设计是隐形的”），但随着你看到更多代码，其可预测性应该不断增加。

关键要点

• 提出新颖的实证研究：通过测量LLM在代码库规模增大时的困惑度变化，来量化不同编程语言的“可预测性”扩展定律。
• 扩展定律更好（指数更优）的语言，未来将更易被LLM理解、修复和生成，从而在程序正确性方面获得全局优势。
• Lean语言在初始阶段可能损失更大，但扩展指数更优，有望长期胜出。
• 当前LLM生成的软件质量普遍不高，形式化验证是理想解决方案，但进展滞后。
• 语言先验观点反驳了“流行语言锁定”论，认为LLM能力提升会带动所有语言，并可能复兴晦涩语言。
• 规模失效现象：小规模表现良好的LLM在大规模代码库中可能因上下文窗口限制、动态类型、全局状态等问题产生致命错误。
• Lean面临鸡生蛋困境：缺乏训练数据导致LLM不擅长Lean，而无法用LLM创建Lean代码库又阻碍数据积累。
• 可预测性代理：通过LLM视角下的代码“可预测性”来评估语言设计优劣，但直接使用困惑度或gzip压缩比等指标效果不佳，需考虑高阶导数。

意义与影响

该研究思路为全球软件安全提供了一条可量化的出路。如果验证了Lean（或其他形式化验证语言）在扩展定律上具有优越指数，将有力推动政府和企业大规模投资重写关键基础设施代码，从根本上减少内存安全漏洞、异常崩溃和逻辑错误。同时，该框架也可用于评估新编程语言的设计质量，指导语言和工具链的发展方向。对于LLM开发者而言，理解不同语言的扩展特性有助于优化模型架构和训练策略（例如，针对高扩展指数的语言增加上下文窗口或注意力机制）。长远看，这项研究可能促成一种“预测性安全”范式：在代码库规模增长之前，通过扩展定律预测其安全性退化风险，提前采取形式化验证等措施。当然，该方法仍需实证验证，且需解决高阶可预测性指标的设计问题。