随着开源预训练大型语言模型（Large Language Model, LLM ）变得更加强大和开放，越来越多的开发者将大语言模型纳入到他们的项目中。其中一个关键的适应步骤是将领域特定的文档集成到预训练模型中，这被称为微调。

通常情况下，来自领域特定文档的额外知识与预训练模型已经知道的相比微不足道。在这种情况下，低秩适应（Low-Rank Adaptation，LoRA ）技术证明是有价值的。

通过 LoRA，微调模型仅向预训练模型添加不到0.1%的参数。具体来说，这意味着 LoRA 微调模型仅增加了10~200 MB 的存储，具体取决于配置。从计算角度来看，考虑到与预训练模型相比参数的增加极少，额外的计算负载相对较小。

基于存储和计算的额外开销都很小这一点，我相信构建一个多租户的大语言微调模型的推断服务具有很大潜力。这个服务可以托管成千上万个 LoRA 模型，它们都共享相同的预训练大语言模型。在每个批次的执行中，每个用户请求都会调用一个独立的微调模型，从而分摊存储和计算成本到各种不同的模型中。

在我的上一篇博客文章中，我深入探讨了大语言模型推断中的批处理效应。在这篇文章中，我将详细介绍为什么多租户 LoRA 推断服务具有巨大的潜力。

机器学习模型依赖于批处理(Batching)来提高推断吞吐量，尤其是对于ResNet和DenseNet等较小的计算机视觉模型。GPT以及其他大型语言模型(Large Language Model, LLM)是当今最热门的模型。批处理对于GPT和大语言模型仍然适用吗？让我们一探究竟。

上交了连照片名字都没有的临时工牌，上星期五我为期13周的谷歌实习告一段落。我给谷歌写了7500行C++代码，再加上还没有合并的1000行，我觉得我对自己贡献代码的数量和质量还是比较满意的。这次谷歌实习是我第一次在工业界的经历，感觉收获很多。

每当我的程序崩溃的时候，我都会用核心转储 (core dump) 文件来找出来崩溃发生的具体位置。（关于怎么产生和使用核心转储可以看我之前的文章。）一直以来我调程序的时候都是很开心的……直到我遇到了这个新的 bug。当我把它的核心转储文件载入到 GDB 之后，我很失望地发现所有的堆栈追踪 (stack trace) 都是关于系统库的，没有一行是关于我的代码的。

太长不看：那就看看这个补丁就好了。

让我们踏上探索未知的旅程吧。

我第一次听说 Coq 是在本科的时候。从那以后我就一直很想学 Coq，但是并不知道怎么开始。大部分的 Coq 教程都是在讲逻辑，我觉得并不是很有趣。

上个学期我选了 UW CSE505 这门课。Prof. Zach Tatlock 和 TA Talia Ringer 设计了一系列非常棒的作业来帮我们学习 Coq。在这个课里面，我们证明了一些更加实际的东西，包括一个简单的编程语言的解释器还有一个简单的正则表达式引擎。事实上，我发现我对在 Coq 里面写证明还蛮在行的（但是写规范就完全是另外一回事了），至少在做作业的时候我是这么觉得的。

如果你在自学 Coq，我推荐以下资源：

• UW CSE505 的作业
• Formal Reasoning About Programs 这本书是我们上课的教材。这本书很短，边距很大，空白很多，每一章附带了详细的 Coq 代码。这本书还自带了一个很好用的 Coq 库 frap。
• Software Foundations 如果你真的对形式化验证很感兴趣的话。

我非常高兴我终于能把 Coq 从我的愿望单里面划掉了。不过我并不是形式化验证的狂热粉丝，我觉得我之后也不用用到 Coq。我决定趁我还没完全忘记 Coq，赶紧把我做作业时学会的 Coq 技巧写下来，万一以后哪天我又用到 Coq 了呢，希望也对读者有所帮助。