【ImperialViolet相关文章】长久以来ImperialViolet一直对像Rocq原Coq和Lean这样的依赖类型语言情有独钟。它们提供了一种能编码并强制实施任意微妙不变量的类型系统而在常规语言中这类东西最多只能以注释形式存在且随团队规模扩大易被遗忘进而出现误解和组件契合问题。依赖类型似乎在诱惑着人们正式编写这些不变量让机器来检查。顺便说一句Coq改名了。多年前在普林斯顿的一次Coq会议上ImperialViolet曾建议在英语环境中使用名为Coq的编程语言会是一个障碍当时听众并不认同。ImperialViolet还开玩笑说那里的许多演讲听起来像提利昂·兰尼斯特的演讲可惜没人get到因为那时候该剧最后一季还没播出。【依赖类型语言的证明难题】强大的类型系统往往伴随着巨大的证明工作量。ImperialViolet自己曾花一整天证明简单事情证明过程有趣但耗时还可能出现努力后发现目标错误的情况。seL4项目回顾报告显示工程师花在证明上的时间约是设计和实现时间的10倍证明代码行数是C代码行数的20倍还多。这种开销使使用依赖类型语言编程成为小众行为促使人们尝试将证明过程自动化。ImperialViolet对F*有一定了解在F*中系统试图用SMT求解器自动完成证明义务但容易构造出让求解器陷入困境的情况使用者需培养直觉围绕求解器编写代码这在某种程度上把问题变成了玄学。虽然理论上命题正确时证明内容无关紧要但存在两个复杂因素一是seL4团队所说的“证明工程”需对证明进行结构设计以减少代码更改后重新调整证明的工作量二是过于复杂的证明会导致类型检查器崩溃并消耗大量内存。【大语言模型带来的转机】现在有了大语言模型LLMs结合证明无关性它们有望成为强大的证明自动化形式。有足够自动化后或许不用太担心证明工程且根据ImperialViolet有限的测试LLMs可以避免让类型检查器崩溃潜在地让依赖类型系统变得实用多了。于是ImperialViolet用Lean编写了一个Zstandard解压缩器部分原因是对Zstandard好奇。Zstandard似乎正在赢得取代gzip成为标准压缩工具的竞争它是LZ77风格的压缩器有更好的熵编码和精心设计解压缩速度出色。虽然它不如bzip2优美但实际优势明显。这些测量是在标准参考计算机即作者当时使用的苹果设备上进行的注意y轴是对数刻度gzip和Zstandard在速度方面表现突出不过苹果的gzip经过了特别优化其他设备上的gzip可能会慢一些。Zstandard由Yann Collet开发基于Jarek Duda的开创性ANS工作有一个RFC但内容简洁除非对压缩技术非常熟悉否则可能需反复阅读才能理解。ImperialViolet的同事Nigel Tao写了一篇关于Zstandard的精彩文章如果想了解Zstandard应该去读那篇文章ImperialViolet在这里只解释最有趣的部分——熵编码器并结合一些对Lean的介绍。【熵编码器的工作原理】熵编码器的工作是用最少的比特数对概率不均匀的符号序列进行编码。经典的熵编码器是霍夫曼编码器它构建一棵二叉树符号位于叶子节点通过简单算法生成最优前缀树。霍夫曼树速度快但缺点是每个符号只能使用整数个比特会造成一定的浪费。Zstandard使用霍夫曼树还有一种压缩率更高的熵编码器——有限状态熵编码器FSE。FSE是一种状态机状态数量比符号数量多每个符号分配到的状态比例反映其在数据流中出现的概率。每个状态有三个值对应的符号、从比特流中读取的比特数以及一个基线状态数将其与读取的比特数相加得到下一个状态。通过为更常见的符号分配多个状态编码器不仅选择一个符号还选择该符号要进入的状态这个选择会将信息传递到下一个符号这就是分数比特信息的去向。而且这种熵编码器基于表运行速度非常快。但FSE不能正向工作必须从序列的末尾开始反向工作。此外Zstandard压缩器按反向顺序编码符号但会逐步写入输出所以解压缩器必须定位到块的末尾反向读取比特才能将其还原。基本的熵编码器不考虑符号间的概率关系在Zstandard中是一种传统的Lempel–Ziv结构来利用这些冗余信息FSE主要用于高效编码反向引用的偏移量和长度。【Lean语言的特点与应用】Lean是一种依赖类型语言用例子阐述这个概念更合适。比如一个从流中读取n个字节的函数类型系统知道返回的字节数组长度是n还有一个返回两个数字和一个字节数组的函数对数字和数组长度有特定要求。Lean目前主要作为陈述和证明数学定理的形式语言《代码中的证明》这本书简短而精彩地讲述了Lean的发展历程。Lean和Haskell一样是纯函数式语言但有一些特性使其作为编程语言可能更方便。首先Lean是严格求值的而Haskell是惰性求值的严格求值让程序性能更易预测其次Lean有很棒的“语法糖”单子 do 表示法包含 for 循环、return 语句和 break 语句可进行命令式编程最后Lean有一个优化机制只要对象的引用计数为1就会对其进行可变更新但Lean没有线性类型系统的相关特性可能会影响性能。在ImperialViolet编写的zstd解码器中有一个例子关注数组索引处Lean可以证明数组不为空这是通过相关定理和信息推断出来的。ImperialViolet根据RFC实现了FSE表构造算法在Lean中还可以证明该函数的通用性质现在有几个大语言模型可以在大约20分钟内自动完成这些证明而且只使用每月20美元订阅配额的一小部分明年这可能就会成为标配。不过ImperialViolet在进行证明时需要更改表生成代码Lean团队正在改进这一点。将依赖类型和大语言模型结合并非新想法但在日常软件工程中应用这种结合的工作还不多还需要更多实践经验。非常强的类型可能会放大更改的影响范围Lean是高级语言并不适用于所有场景ImperialViolet编写的简单Zstandard解码器比命令行工具 zstd 慢10倍。尽管如此证明自动化已经到来有了一种新型的编程语言可供使用这很令人兴奋ImperialViolet不会发布代码因为大语言模型可能比他做得更好这一灵感来自于lean - zip。【补充经过验证的汇编代码】AWS开发了LNSym这是一个AArch64的语义和模拟器也许可以用它来证明某些函数的优化汇编实现与其Lean版本的等价性然后在运行时使用汇编代码让大语言模型进行优化而不引入功能错误。经过验证的汇编代码在加密实现中已经很常见但现在也许可以变得“廉价”。ImperialViolet花了一些时间主要借助大语言模型来尝试这个想法仓库中的小popcount示例使用了 bv_decide但这个示例需要的内存超过了系统所能提供的对于非常小的函数是可行的可以为小型Lean函数获得等价性证明然后在运行时调用它们但ImperialViolet和几个大语言模型都无法将其扩展到更大的规模。
