Lean Software Scaling Laws
7 days ago
- #LLM Scaling Laws
- #Software Security
- #Formal Verification
- 提议测量编码大型语言模型（LLM）困惑度如何随代码库上下文规模扩展，使用 Lean 作为形式化语言的测试案例。
- 旨在通过编程语言估计“可预测性”的缩放定律，转化为软件安全性和可靠性的改进。
- Lean 可能具有更差的基线性能但更优的缩放指数，表明对程序正确性和网络安全具有长期益处。
- 方法论涉及通过冻结的 LLM 进行实证测量、语料库构建、损失测量和每种语言的缩放定律拟合。
- 预测：像 Python 这样的“弱”语言在小规模下表现出色但缩放指数更差，而像 Lean 这样的“强”语言在大规模下实现反超。
- 需要控制程序员和领域差异的偏差；考虑了上下文学习及失败模式（如生态系统成熟度的影响）。