AI推理提效两条路径：测试时扩展与形式化验证

AI推理提效的两条路径：从测试时扩展到验证式推理

在微软研究院印度峰会（MSR India Summit）上，两位研究者分别从系统效率与推理可信两个维度，探讨了当前AI推理面临的核心挑战。帝国理工学院助理教授Hongxiong Fan（同时任职剑桥大学，微软研究院教职学者奖得主）聚焦于「测试时扩展」的效率优化，而微软研究院印度的一位首席研究员则提出了「验证式推理」的全新范式。本文融合两场报告的核心观点，梳理AI推理提效的两条关键路径。

AI推理的成本困境

Hongxiong Fan首先指出了当前AI发展的根本矛盾：算法复杂度的爆炸式增长。在**缩放定律（Scaling Law）**驱动下，模型参数量和计算量自ChatGPT时代以来急剧攀升——最近的开源模型甚至已达到万亿参数规模，给底层计算系统带来了巨大压力。

缩放定律由OpenAI研究人员Kaplan等人于2020年在论文《Scaling Laws for Neural Language Models》中正式提出，揭示了模型性能与参数量、训练数据量、计算量之间的幂律关系。这一发现的深远之处在于它提供了一张「性能路线图」——研究者无需猜测架构改进方向，只需持续扩大规模便能可预测地获得能力提升。然而幂律关系也意味着边际收益递减：性能每提升一个百分点，所需计算量的增幅会越来越大。

2022年DeepMind提出的Chinchilla定律进一步修正了这一认识，指出此前许多大模型实际处于「参数过多、数据不足」的次优状态，最优训练应保持参数量与数据量的特定比例关系——具体而言，参数量与训练token数应大致相等。这一发现深刻影响了业界的训练策略：Llama 2、Mistral等后续开源模型普遍采用了更激进的数据扩充方案，而非单纯追求参数规模。这也解释了为何近年来模型规模的增长开始向数据质量与训练效率方向倾斜。这一发现驱动了GPT-3（1750亿参数）、GPT-4乃至更大规模模型的诞生。然而缩放定律也暗含代价：每次性能翻倍往往需要计算资源增加一个数量级，形成了「能力越强、成本越高」的正反馈困局。

同时，摩尔定律的红利正在消退。摩尔定律由英特尔创始人Gordon Moore于1965年提出，预测集成电路上的晶体管数量每18-24个月翻倍。然而自2010年代中期起，由于量子隧穿效应、散热瓶颈等物理极限，单核性能提升已显著放缓。引用David Patterson（RISC架构之父、图灵奖得主）著作中的数据，自1980年以来CPU性能提升持续放缓，硬件性能的自然红利已近枯竭，未来的效率提升必须更多依赖软件算法与跨层协同设计来实现。能耗问题同样不容忽视：从零训练一个BERT模型的碳排放，相当于五辆汽车整个生命周期的碳排放总和，美国数据中心的能源供应链也已成为瓶颈。

除了环境成本，「可负担性」是近年浮现的关键议题。前沿实验室为保持模型在各类基准测试的领先地位，须投入巨额训练成本，而推理同样不是免费的——有报告显示，AI的使用成本甚至已高于人类劳动力。随着模型持续变大，这一问题只会加剧。核心问题在于：未来即便AI变得极其强大，是否人人都能负担得起？

测试时扩展：小模型的逆袭机会

什么是测试时扩展

面对上述困境，Fan团队选择了「跨栈协同设计」（cross-stack co-design）的研究路径，即在算法、系统、硬件、芯片各层级协同优化，而非孤立地在单一层面发力。其在NeurIPS发表的工作正是算法-系统协同设计的典型案例。

**测试时扩展（Test-Time Scaling）**是OpenAI「草莓项目」提出的概念，核心思想是：既然已在训练上投入大量GPU，不妨在推理阶段也多分配一些算力，通过更多计算来增强模型性能。

这一理念的哲学根源可追溯至两个传统：一是强化学习中的蒙特卡洛树搜索（MCTS），通过在决策树中模拟多条路径寻找最优解，AlphaGo正是凭借这一技术在围棋领域击败人类冠军；二是认知科学中丹尼尔·卡尼曼在《思考，快与慢》中提出的「系统2思维」——测试时扩展本质上是让语言模型从快速直觉的「系统1模式」切换到慢速推理的「系统2模式」，以精确性换取速度的牺牲。OpenAI的o1/o3系列模型通过强化学习训练模型生成长链内部思维，将这一理念推向商业化落地。其哲学与人类解题行为高度类似——难题需要打草稿、反复验算——本质上是用推理阶段的算力换取更高的答题准确率，在输出空间中进行更充分的搜索，以弥补模型参数量不足带来的局限。

值得注意的是，测试时扩展并非万能——在事实性问题上，更多推理步骤有时反而会引入更多幻觉，其优势主要体现在具有明确正误标准的逻辑推理、数学和代码任务上。这一局限性揭示了一个深层问题：测试时扩展依赖于模型能够自我验证，但在开放域知识问答中，模型缺乏可靠的自我纠错机制。实验显示，随着分配算力增加，模型准确率持续提升——经过恰当的测试时扩展，开源边缘模型的性能甚至可以匹敌闭源云端模型。

然而这并非免费午餐。基于文本的**长链思维（Long CoT）**推理会引发「输出token激增」。链式思维（CoT）由Google研究人员Wei等人于2022年提出，核心发现是引导模型「一步步思考」能显著提升复杂推理准确率。Long CoT是其延伸，允许模型生成数千乃至数万个中间推理token，包含自我反思与错误修正。然而模型有时会陷入「过度思考」（overthinking），在特定任务中产生超过52倍的额外token，带来更高的能耗和延迟。

验证粒度的最优解

典型的测试时扩展技术包括三类：长链思维（顺序生成）、Best-of-N（并行生成后择优）和束搜索（Beam Search，逐步保留最有希望的推理步骤）。

束搜索是自然语言生成领域的经典解码算法，起源于语音识别和机器翻译，其工作方式是在每一步保留得分最高的K条候选序列（K即束宽），通过有限的并行探索平衡搜索质量与计算成本。与贪心解码（每步仅保留最优选择）相比，束搜索通过维护多条候选路径避免局部最优陷阱；与穷举搜索相比，它又大幅削减了指数级的搜索空间。在推理链的语境下，束搜索的每一「步」可以是一个token、一个句子或一个完整的推理步骤，粒度的选择直接影响验证的频率与成本。Best-of-N代表最粗粒度的验证（生成完整答案后再择优），束搜索代表最细粒度的验证（每一步都做选择），二者之间存在大量中间地带有待探索。

团队围绕三个核心问题展开研究：

• 当前验证粒度是否最优？ 探索性能上界实验发现，现有验证粒度的选择并非最优——理想情况下计算量（FLOPs）可减少75倍，同时准确率提升1.1%。

• 验证的系统成本有多大？ GPU性能剖析显示，当验证粒度极细（每步都验证）且样本数较大（如超过64）时，验证成本会主导整体执行时间，即「粒度越小、样本越多，系统性能越受验证环节制约」。

• 如何确定最优验证粒度？ 团队提出「可变粒度搜索」（Variable Granularity Search），根据任务难度在运行时动态调整验证粒度：困难任务采用细粒度逐步验证，简单任务则用Best-of-N即可。相比束搜索和DVTS等SOTA方案，该方法实现约3%的准确率提升，同时减少52%的计算量。

让小模型跑出云端体验

在后续发表于ASPLOS的工作中，团队进一步验证：本地部署的7B开源模型配合测试时扩展，能在特定任务上匹敌闭源云端模型的准确率。但挑战在于延迟——过多算力分配导致执行时间远超云端响应。

为此团队通过NSight进行GPU剖析，识别出VLM引擎的三大低效点，并提出对应优化：

• 投机式束搜索：短推理路径无需等待长路径完成，可直接投机生成。这一思路借鉴自CPU的分支预测机制——先乐观执行，验证失败时再回滚。2023年兴起的**投机解码（Speculative Decoding）**技术同样遵循此逻辑：用小型草稿模型（通常为主模型参数量的1/10左右）快速生成候选token，由大型主模型并行验证，一次前向传播可接受多个token，突破自回归生成的串行瓶颈。由于大模型的计算瓶颈往往在于内存带宽而非算力，并行验证多个token的成本与验证单个token相近，投机解码因此可在不损失精度的前提下实现2-4倍的吞吐量提升；

• 动态前缀感知调度：在内存受限场景下，优先执行连续生成的推理路径，减少KV缓存驱逐。KV缓存是Transformer推理的核心加速技术——它将已计算的Key-Value矩阵存储在显存中实现O(1)的增量计算，代价是显存占用随序列长度线性增长。在束搜索等多路径推理场景中，多条候选路径共享同一个前缀，理论上可复用同一份前缀KV缓存，这正是前缀感知调度的价值所在。然而当路径数量增多、序列变长时，KV缓存可能占满全部显存，迫使系统将部分缓存驱逐至主内存并在需要时重新加载，造成严重的访存延迟。PagedAttention（vLLM，2023年）等技术借鉴操作系统虚拟内存的分页思想来缓解这一问题——将KV缓存划分为固定大小的「页」，按需动态分配，避免内存碎片化。但在边缘设备上显存容量有限的场景中，缓存管理依然是核心瓶颈；

• 屋顶线模型引导的多模型内存分配：屋顶线模型（Roofline Model）是GPU性能分析的标准工具，将计算任务分为计算瓶颈（compute-bound，受限于FLOPS上限）和内存瓶颈（memory-bound，受限于内存带宽）两类，指导优化方向的选择。通过在以「算术强度」（FLOPs/字节）为横轴、「性能」为纵轴的坐标系中绘制任务工作点与硬件上界，工程师可直观判断当前瓶颈所在并针对性优化。团队基于此合理分配验证器与生成器的GPU内存，确保两个组件都尽量工作在各自的性能上界附近。

综合优化后，本地AI PC上的开源模型可实现与云端闭源模型相近的准确率和响应延迟。

验证式推理：从执行到可信执行

第二场报告转向了另一个维度——可信性。微软研究院印度的研究员指出，当今的AI智能体已能执行复杂的多步骤工作流，涵盖专利律师、零售客服等高价值领域，动辄涉及数十甚至上百个步骤。

合规与正确的双重目标

关键问题是：如何确保智能体「做该做的事，不做不该做的事」？以零售智能体政策为例，一条规则是「退款必须退回原支付方式或礼品卡」，模型的所有工具调用和消息都必须符合此政策。而在专利答复等复杂场景中，政策往往是隐式的——律师们默认遵守的法律准则。

研究框架追求两个目标：合规性（遵循显式或隐式规则）与正确性（最终解决用户问题）。核心平台名为「Interven」，旨在运行时（runtime）对执行中的智能体进行验证与引导（steering）。

形式化验证的引入

当前主流验证方式是「LLM作为裁判」——将数千token的完整轨迹交给一个LLM判断是否合规，但这存在与被测模型相同的不可靠性。研究团队的核心洞见是：将形式化验证的确定性引入真实、混乱的领域。

形式化验证（Formal Verification）是计算机科学中有着数十年历史的严肃领域，其核心工具包括：模型检测（Model Checking，穷举系统所有可能状态，由Clarke、Emerson、Sifakis凭此获2007年图灵奖）、定理证明（如Coq、Lean证明助手，其中Lean近年因被用于自动化数学证明而备受关注）和抽象解释（Abstract Interpretation，Facebook的Infer静态分析工具即基于此原理）。

传统形式化验证的最大障碍是「规范缺口」——工程师难以将模糊的业务需求精确地写成数学规范，这一过程本身往往比编写代码更费时费力。将LLM引入这一流程的核心价值正在于此：LLM擅长理解自然语言的语义并将其转化为结构化表示，而形式化工具擅长在结构化表示上做确定性推理。微软研究院此前的相关工作（如用Copilot辅助生成Dafny验证代码）以及MIT的「按规范合成」研究，都在探索这一人机协作的新范式。真正的挑战在于验证器本身的正确性——生成验证代码的LLM同样可能犯错，形成「谁来验证验证者」的递归困境。研究团队的创新在于构建了「自然语言政策→中间表示→可执行验证代码」的自动转化管道，将形式化验证的确定性带入了本质上模糊的业务规则领域。

其技术路径分为离线和在线两个阶段：

• 离线阶段：将文本政策拆解为规则，再映射到中间表示语言，进而生成对应的验证代码（可理解为检查每条规则的Python代码）。代码中预留「空洞」（holes），待运行时填充上下文相关的具体值（如支付ID）。

• 在线阶段：验证器多为CPU绑定的代码片段。当智能体发起工具调用时，触发对应验证器，仅在提取参数时调用一个小型语言模型（4B模型即可胜任提取任务）。由于大量验证是CPU绑定的，整个过程具有有界延迟。

有意思的是，这一设计与Fan提出的投机思想异曲同工：验证调用可以异步进行，模型可假设操作正确并继续推进，仅当验证失败时才回滚轨迹。不过对于「写操作」等不可撤销的调用，则需阻塞等待验证结果。这一区分与数据库事务中「乐观锁」与「悲观锁」的哲学如出一辙——读操作并发友好，写操作需要强一致性保障。

引导、反馈与训练

验证只是硬币的一面，真正的价值在于「引导」——在模型出错时即时给予反馈，使其回到合规且正确的轨迹。迷宫数据集实验揭示了一个重要规律：越早给予验证反馈，性能提升越显著；随着轨迹推进，模型置信度增高，反馈的边际收益递减。这一规律与强化学习中「奖励信号的时效性」高度吻合——延迟的奖励信号会因归因困难（credit assignment problem）而大幅削弱学习效率。信用分配问题是强化学习的核心难题之一：当一个决策序列在若干步之后才得到奖励信号时，算法难以判断究竟是哪一步导致了最终结果，进而难以对正确行为进行有效强化。

在Tau-bench基准上，Tau-bench（Tool-Agent-User Benchmark）代表了AI智能体评估从「单步任务」向「多步交互工作流」演进的重要里程碑。与传统NLP基准（如GLUE、SuperGLUE）不同，它同时模拟「用户模拟器」和「工具环境」，使智能体在封闭沙盒中经历近乎真实的交互；它设计了严苛的「通过率」指标，要求智能体在多次独立运行中均能成功完成任务，而非仅凭单次成功；它还显式区分任务完成度和政策合规度两个维度——恰好对应「正确性」与「合规性」两个目标，反映了现实部署中「既要解决用户问题，又要遵守企业规范」的双重约束。配合验证与引导，30B模型可从32%的基线跃升至87分——而GPT-5-mini原版仅47.4分；在更难的模式下，基线24分可提升至55分。所有操作均为黑盒，无需模型内部信息，仅依赖其文本输出。

开放挑战与未来方向

两场报告都指向了共通的开放问题：

• 超越数学与代码的自动形式化：真实政策是「模糊文本的海洋」，如何处理主观条款、非正式表述以及页面间的矛盾条款，是巨大挑战。自然语言处理领域的语义解析（Semantic Parsing）研究已有数十年积累，但将其应用于法律、医疗等高stakes领域的形式化转换，仍面临领域知识稀缺和标注成本高昂的双重困境。

• 验证器的正确性证明：需区分「可靠性」（soundness，绝不误判正确轨迹）与「完备性」（completeness，不漏判错误轨迹）。在形式化验证领域，这两个属性构成了对系统保证强度的完整描述——soundness确保验证器不会错误地「放行」违规行为，completeness确保所有违规都能被检测到。研究团队发现完备性更难保证，这与程序分析领域的经典结论（Rice定理揭示的不可判定性——对于任意非平凡语义属性，不存在能正确判断所有程序是否具备该属性的算法）相呼应。

• 不同参照系的对齐问题：当推理任务基于印度法律、而验证器基于美国法律时，如何确保二者对齐？这在涉及政府、企业、客户三方的合规场景中尤为突出。这一问题本质上是「规范冲突」（specification conflict）在跨文化、跨司法管辖区场景下的具体体现，也是AI全球化部署面临的共性挑战。

• 将验证信号转化为训练信号：中间反馈比单纯的结果反馈更有助于学习，甚至能从失败轨迹中提取价值。这催生了SFT（监督微调）、基于结果的RL（如GRPO）、自蒸馏RL、基于评论者的RL等一系列算法探索。过程奖励模型（Process Reward Model，PRM）与结果奖励模型（Outcome Reward Model，ORM）之争，正是这一议题的学术映射——前者在每个中间步骤给予反馈，后者仅在最终结果处给分，二者的权衡与本节讨论的「验证粒度」问题高度同构。

关于小模型部署的前景，Fan的评估审慎乐观：GPU基础设施已基本就绪，但在算法层面——针对不同任务类型该选择何种验证器、何时触发验证——仍是开放问题，预计需要一到两年才能有清晰答案。在数学等特定领域已展现出令人鼓舞的成果，关键在于如何提升泛化能力。

从测试时扩展的效率优化，到形式化验证的可信保障，两条路径共同勾勒出AI推理走向「普惠且可靠」的技术蓝图。

核心要点