【斯坦福博士论文】自动推理和大型语言模型的高效算法

这篇论文探讨了自动化推理和大型语言模型（LLMs），通过创新算法研究如何提高这两个领域的效率和有效性。论文由三个主要部分组成，每一部分都关注人工智能的不同但相互关联的方面。 在第一部分，论文深入探讨了自动化推理领域，该领域通过计算方法模仿人类的逻辑推理。研究解决了该领域中的重大挑战，特别是随着问题复杂性的增加，计算需求呈指数级增长的情况。值得注意的是，这一部分强调了可满足性模理论（SMT）方面的进展，重点是提高在复杂性增加时的解决效率。论文通过探索理论组合、代数数据类型和序列，贡献了更高效的推理框架。

转到第二部分，焦点转向LLMs，它们在各种应用中变得至关重要，从内容生成到企业决策支持。尽管LLMs功能强大，但由于巨大的计算资源需求和用户提示的多样性，实现这些模型的高效部署仍是一个挑战。这部分论文提出了新颖的算法和服务基础设施，旨在优化LLMs的性能，特别是在减少延迟和提高实时应用吞吐量方面。创新如FlexGen和S-LoRA被引入，旨在使LLMs在个人计算设备上更加可用，并提供个性化的高吞吐量服务。这一部分还介绍了虚拟令牌计数器（VTC），一种新颖的公平调度算法，确保在高需求的LLM推理环境中公平分配资源，解决服务公平性的问题。

论文的第三部分将前两部分桥接起来，展示了将形式验证和代码生成与LLMs集成的初步结果。该集成旨在利用两个领域的优势，创建更强大和多功能的AI系统。

引言

本论文展示了实现自动推理和大型语言模型（LLM）系统高效算法的几种方法。本章将首先描述这两个领域中的问题及其效率挑战，然后概述论文中提出的研究贡献。

1.1 问题与动机

1.1.1 符号推理与神经网络

人工智能研究传统上遵循两种主要范式：符号推理和神经网络。符号推理，也称为符号AI，利用逻辑和知识表示来解决问题。这种方法在需要显式规则和推理的任务中表现出色，但在处理复杂的非结构化数据时可能会遇到困难。相反，神经网络则松散地受到大脑结构的启发，擅长模式识别和从大量数据中学习。然而，神经网络在推理过程中可能不透明，导致其可解释性较差。随着研究的进展，越来越多的研究集中在结合这两种方法，利用符号推理和神经网络的优势，开发更强大和多功能的AI系统。为了充分利用每种方法的优势，运行它们需要高效的算法和系统。在本论文中，我们首先分别关注加速自动推理的技术（第一部分）和加速大型语言模型推理的技术（第二部分）。然后，在第三部分中，我们展示了利用两者力量的初步结果。 1.1.2 自动化推理与效率挑战

自动化推理通过计算方法模拟人类逻辑推理的挑战。该领域致力于开发能够自动分析和操作逻辑表达式等形式化表示的算法。这种能力远远超出简单计算，允许计算机处理具有复杂逻辑结构的问题。 自动化推理的应用领域与其解决的问题一样多样。在软件和硬件设计中，自动化推理工具用于确保电路的正确性。通过分析组件之间的逻辑关系，这些工具可以识别设计中的潜在错误和逻辑不一致，防止在开发过程中出现昂贵的错误。同样，自动化推理在形式验证中也起着关键作用，这是一种通过数学证明关键系统中不存在错误的技术。在这里，自动化推理工具仔细分析系统的规范和行为，确保其遵循所需属性，消除意外故障的可能性。 自动化推理的关键挑战之一是解决时间问题。随着所处理问题复杂性的增加，找到解决方案所需的计算资源可能呈指数级增长。这在可满足性模理论（SMT）领域尤为突出，在该领域中，任务是确定给定的一阶逻辑公式相对于背景理论（如线性算术或位向量）是否可满足。SMT问题的解决时间可能高度可变，取决于具体理论、公式的复杂性以及底层SMT求解器的性能。自动化推理研究人员在开发更高效的算法和启发式方法以应对这一挑战方面取得了显著进展，但该领域中许多问题的固有复杂性意味着解决时间仍然是一个关键考虑因素。

1.1.3 大型语言模型与服务挑战

基础模型，特别是大型语言模型（LLM），已成为各种应用的核心，彻底改变了各行业中任务的处理和执行方式。除了它们的功能外，LLMs已演变为广泛使用的服务，受到从个人用户到大型企业的多样化客户的采用。这种广泛的应用在多个领域中尤为明显，从个人助手和创意内容生成到高级企业数据分析和决策支持。尽管LLMs具有巨大的力量和能力，但关键在于利用它们的潜力来增强人类生活和生产力。 尽管大型语言模型（LLM）提供了引人注目的能力，但将其有效部署于实际应用中仍存在显著挑战。主要障碍在于硬件资源限制。LLMs由于其复杂的架构和庞大的参数空间，在推理过程中需要大量计算资源。此外，用户提示的不确定性破坏了传统的优化技术。与具有控制格式的训练数据不同，用户提示在长度和复杂性上可能有很大差异。此外，由于LLM生成的迭代性质，实现实时应用的低延迟和高吞吐量变得困难。与单步任务不同，LLM可能需要多次来回交流才能完成一个响应。这些因素需要开发专门的服务基础设施和新颖的调度算法，以优化LLM性能并提供无缝的用户体验。

1.2 我们的方法

1.2.1 走向高效且具表现力的SMT求解

可满足性模理论（SMT）求解在自动化推理中是一种强大的技术，专门解决结合命题逻辑和背景理论的问题。与只处理真假命题的经典命题逻辑不同，SMT结合了可判定的一阶逻辑理论，如算术或等式约束。这允许对涉及整数、实数或特定数据结构的问题进行推理。SMT求解器通过系统地探索搜索空间，在指定的理论下评估公式的真值。由于将逻辑与这些理论相结合的内在复杂性，高效的求解算法和专门的决策过程对于解决现实世界的SMT问题至关重要。可满足性模理论（SMT）求解的最新技术不断发展，重点是提高效率和处理日益复杂的问题。尽管已经取得了令人瞩目的进展，但对于高度复杂的SMT问题实现可处理的解决时间仍然是一个活跃的研究领域。 本论文的第一部分涵盖了这一范围内的三个研究课题，包括更好地理解和提高理论组合的效率以及利用代数数据类型和序列的两种特定理论。在第二章中，我们对SMT中礼貌组合的研究做出了两项贡献。首先是一个困难结果，通过展示一个礼貌理论但不是强礼貌的例子，揭示了礼貌和强礼貌之间的区别。第二项贡献是对礼貌组合方法的优化，借鉴了Nelson-Oppen方法。我们展示了在某些条件下，可以减少礼貌组合所需的枚举安排的复杂性。在第三章中，我们研究了数据类型理论，并证明其是强礼貌的，展示了如何使用礼貌组合将其与其他任意不相交的理论相结合。在第四章中，我们介绍了一种用于推理向量的序列理论。与使用现有的数组理论相比，新的序列理论更具表现力，并且推理速度更快。

1.2.2 走向高效且公平的LLM服务

LLM的一个不可避免的方面是使其能够被各个领域的更多用户访问。扩大访问的目的是赋能各类个人和组织，使他们能够利用这些强大的工具满足其独特的应用和需求。本论文的第二部分探讨了如何提高LLM对所有用户的可访问性。自2022年底LLM在日常生活中被广泛使用以来，对更易于访问的LLM的需求不断增长，这包括：（1）能够在个人计算机上运行LLM，（2）访问个性化服务，以及（3）需要公平的资源分配以防止重度用户的垄断。

第五章（FlexGen）旨在解决第一个需求：在个人计算机上运行LLM。由于高计算和内存需求，传统上只能通过多个高级加速器实现，在内存有限的设备上运行LLM需要卸载，除了传统的模型压缩优化外。尽管激进的卸载会严重影响推理延迟，但FlexGen受到对批处理延迟不敏感任务的需求的驱动。它开始研究在有限资源下的高吞吐量LLM推理。它聚合了GPU、CPU和磁盘的内存和计算资源，并展示了如何在给定设置中获得最佳的卸载策略。我们的方法也是第一个提出使用4位量化KV缓存的，这与卸载策略相结合，使吞吐量比以前的方法高出100倍。

第六章（S-LoRA）旨在解决第二个需求：个性化LLM服务。低秩适应（LoRA）技术可以提供高效的、任务特定的适应，从一个基础模型中创建许多适配器，以实现成本效益高的个性化服务。LoRA适配器通过将适配器与模型参数合并来提供服务，这使得单个适配器的低延迟成为可能，但在同时服务多个适配器时会降低整体吞吐量。S-LoRA探索了LoRA适配器的可扩展服务，通过更好的内存管理、为异构批处理定制的CUDA内核和新颖的张量并行策略，实现了高吞吐量的多适配器服务。与之前的引擎相比，S-LoRA的吞吐量提高了4倍，服务的适配器数量增加了几个数量级。

第七章（VTC）旨在解决第三个需求：公平地为用户服务。LLM推理服务在高需求下处理各种请求。为了保持公平，大多数主要服务实施请求速率限制，防止任何单个客户端垄断队列。然而，这种基本的公平方法在容量可用时可能导致服务未充分利用和客户体验不佳。我们展示了如何将传统网络和操作系统中的公平排队概念应用于LLM服务领域，达到令牌粒度的公平性。我们定义了LLM服务中的公平性问题，并提出了虚拟令牌计数器（VTC）算法，这是一种具有理论保证的新型公平调度算法。广泛的评估展示了VTC在保持公平性方面的有效性，与传统方法相比，为更加公平高效的LLM服务系统铺平了道路。