🤖 machine learning

PPDL: LLM-Based Flows as Probabilistic Programs

本文介绍了 PPDL，这是一种概率编程语言，它使开发者能够在基于 LLM 的应用流程中量化并传播不确定性，并在无需修改核心逻辑的情况下实验推理缩放技术，这一点已通过一个针对 Rocq 证明器的定理证明智能体得到了验证。

原作者： Louis Mandel, Guillaume Baudart, Mandana Vaziri, Martin Hirzel

发布于 2026-08-07

📖 1 分钟阅读☕ 轻松阅读

原作者： Louis Mandel, Guillaume Baudart, Mandana Vaziri, Martin Hirzel

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在试图解决一个非常棘手的谜题，但你并不是独自一人，而是有一个聪明又富有创造力的朋友在和你交流。这个朋友是一个被称为“大语言模型”（LLM）的人工智能。他们擅长写故事、解数学题，甚至编写计算机代码。然而，他们并不完美。有时，他们会对错误的答案表现得过于自信，或者可能会编造一些听起来很真实但实际上并不存在的事实。这就是所谓的“不确定性”。

想象一下，你需要解决一个需要很多步骤的极其困难的问题。你先请你的 AI 朋友制定一个计划，然后请他们根据这个计划编写代码，接着请他们检查代码，以此类推。每当你问一个问题时，AI 都会给出一个答案，但这个答案可能是有些摇摆不定的。如果你将十个这样的摇摆不定的答案串联在一起，最终的结果可能会变成一团糟。这就像是在搭建一座由叠叠乐（Jenga）积木组成的塔，每一块积木都略微晃动；随着高度增加，整个塔倒塌的可能性就越大。开发者和用户经常会感到迷茫：“这个答案是对的吗？我们有多确定？我应该信任它吗？”

为了解决这个问题，科学家们尝试了一些技巧。一个流行的想法是“推理缩放”（inference scaling）。这可以理解为让你的 AI 朋友把同一个谜题尝试做十遍，看看哪个答案出现的次数最多。这就像是问一群朋友一个谜语的答案，然后根据多数人的投票来决定。但问题在于，这样做手动操作起来非常麻烦。你必须编写专门的计算机代码来运行那十次尝试，记录哪些看起来不错，并丢弃那些不好的结果。这就像是你每次只想烤一批饼干以确保味道正确时，都必须先建造一座新的工厂。这既复杂又昂贵，而且如果你想尝试不同的烘焙方式，调整起来也非常困难。

论文的核心思想： “神奇记分卡”

这篇论文介绍了一个名为 PPDL（概率提示词声明语言）的新工具。你可以将 PPDL 理解为 AI 工作流中的一个特殊的“神奇记分卡”。通过 PPDL，你不再只是向 AI 提问并得到一个单一答案，而是可以让你的程序天生就能理解 AI 可能存在的不确定性。

它是这样运作的：

流程： 你像平时一样编写给 AI 的指令（例如：“规划代码”，然后“编写代码”，最后“检查代码”）。
神奇因子： 你添加一个特殊的指令，叫做 factor（因子）。这就像是一个记分卡，你告诉 AI：“嘿，如果这个计划听起来逻辑通顺，就给高分；如果代码有错误，就给低分。”
结果： 当你运行程序时，计算机不仅仅给出你一个答案。它会并行地运行整个过程（就像有一百个不同版本的你在同时尝试解开这个谜题）。它会利用你的“记分卡”来权衡结果。如果某条路径看起来非常有希望，计算机就会把更多精力集中在那条路径上。如果某条路径看起来很糟糕，它就会放弃该路径。

最酷的部分在于，你不需要自己编写复杂的“运行十次”的代码。PPDL 会在后台处理所有这些繁重的任务。你只需要编写一次逻辑，系统就会自动找出探索所有可能性的最佳方式。

他们的发现

作者在多个挑战领域测试了这个想法，从解决小学数学题到编写复杂的计算机代码，甚至证明数学定理。

更高的准确度： 在测试中，使用带有这些“记分卡”的 PPDL 使 AI 的准确率显著提高。例如，在名为 GSM8k 的数学测试中，标准 AI 的正确率约为 83.8%。但当他们使用 PPDL 结合“重要性采样”（Importance Sampling，这是一种聪明地挑选最佳猜测的方法）时，准确率跃升至 93.7%。
“聪明”的方法胜出： 他们对比了使用记分卡的几种不同方式。有时，仅仅采取“多数票”（最常见的答案）效果很好。但通常情况下，更聪明的方法（如重要性采样和顺序蒙特卡洛法）表现得更好。这些方法就像是一位侦探，他不只是在数票数，而是实际上在调查一个答案为什么好或为什么坏，从而及早丢弃错误的路径，并将精力集中在正确的路径上。
定理证明器案例研究： 为了对系统进行压力测试，他们构建了一个使用 Rocq 工具来证明数学定理的 AI 智能体。这是一个非常困难的任务，AI 必须编写证明，检查是否出错，并反复进行修正。他们发现，“聪明”的方法（顺序蒙特卡洛法）比单纯不断进行随机猜测能更好地找到正确的证明。它能够同时探索许多不同的路径，并迅速放弃那些走投无路的路径。

他们并未声称的内容

作者很谨慎，并没有说这是一个解决所有问题的“万灵药”。他们指出，这些“记分卡”（因子）的质量取决于你输入的信息。如果你的记分卡不好，系统也不会奇迹般地修复它。此外，虽然这种方法让 AI 变得更加可靠，但这并不意味着 AI 突然变得完美了；它只是意味着我们有了一种更好的方法来衡量我们对答案的确定程度。

为什么这很重要

这篇论文表明，通过将 AI 工作流视为“概率程序”（即理解不确定性的程序），我们可以让 AI 应用变得更加可靠，而不会使其构建过程变得异常复杂。这就像是为开发者提供了一套新工具，让他们能够自动处理“一遍又一遍尝试”这类琐碎且混乱的工作，从而让他们能够专注于构建酷炫的事物，而由计算机来计算出获得正确答案的最佳路径。

技术摘要：PPDL：基于 LLM 的概率程序化流

问题陈述

使用大语言模型（LLM）构建可靠的应用面临着巨大挑战，这是由于 LLM 输出中固有的不确定性和缺乏置信度指标所致。在“流”（flows，即多个 LLM 调用和工具交互的序列）中，这一问题会随着执行轨迹（execution trace）的推进而不断累积。虽然推理缩放技术（例如：重复任务、使用验证器）可以提高准确性，但目前的实现往往是临时性的（ad hoc）、与程序逻辑紧密耦合，并且缺乏追踪不确定性或探索替代执行路径的原则性框架。开发者难以评估答案的正确性，也难以在不重写核心流逻辑的情况下实验不同的缩放策略。

方法论

本文介绍了 PPDL（概率提示声明语言），这是首个专门为基于 LLM 的流设计的概率编程语言。PPDL 通过将核心程序逻辑与推理缩放策略解耦，实现了提示编程与概率编程的统一。

核心语言构造

PPDL 构建于 PDL（提示声明语言）之上，后者是一种用于组合 LLM 和工具调用的声明式语言。PPDL 通过引入一个单一的正交原语扩展了 PDL：factor。

sample（隐式）： LLM 调用充当从由模型和当前上下文定义的分布中进行采样的操作。
factor： 该构造根据用户指定的约束（软约束或硬约束）更新当前执行轨迹的概率。约束可以源自 LLM-as-a-judge 评估、基于规则的工具（如 linter、测试套件）或过程奖励模型。
执行模型： PPDL 不仅仅返回单个输出，而是将程序视为执行轨迹上的一个分布。运行时通过概率推理引擎来探索该分布。

语义与推理

论文将 PPDL 的语义形式化为一个加权采样器（weighted sampler）。

加权采样器： 单个执行轨迹将程序 $p$ 简化为一个值 $v$ ，并带有一个关联的对数得分（由 factor 语句累积而成）。
理想语义： 定义为所有可能轨迹的无限和，并归一化形成输出值的分类分布。
近似推理： 由于理想语义在计算上是不可行的，PPDL 实现了蒙特卡洛近似算法：
- 重要性采样 (IS)： 执行 $N$ 个独立的粒子（traces），并根据它们的最终得分进行重新加权。
- 顺序蒙特卡洛 (SMC)： 在 factor 点引入重采样步骤。得分较低的粒子被丢弃，得分较高的粒子被复制，从而允许系统在流的早期阶段将计算资源集中在有前景的部分轨迹上。
- 多数投票 (Majority Voting)： 一种基准方法，其中所有粒子被赋予相同的权重。

实现

PPDL 是一种通过并行化实现的解释型语言。

并行性： 独立的粒子被并行执行。在单个粒子内部，独立的模型调用通过 future 和延迟数据结构进行并行化，以最大限度地减少阻塞。
正交性： 用户只需编写一次流逻辑。推理算法（IS、SMC 或多数投票）和粒子数量可以在运行时进行配置，无需修改源代码。

主要贡献

PPDL 语言： 首个针对 LLM 与工具调用流的概率提示编程语言，引入了 factor 作为评分和引导执行轨迹的机制。
形式化语义： 对 PPDL 的行为进行了严谨的定义，将基于提示的采样与概率因子之间的相互作用形式化，并定义了由此产生的轨迹分布。
推理缩放框架： 证明了 PPDL 能够支持在不同模型和任务上系统地实验不同的推理缩放算法（IS、SMC、多数投票），而无需重写流逻辑。
案例研究： 实现了一个用于 Rocq 定理证明器的定理证明智能体，展示了概率推理在复杂、迭代的智能体工作流中的效用。

实验结果

作者在多个基准测试（GSM8k, Math500, MBPP, LiveCodeBench, Fever）和多个模型（Granite, Llama, GPT-OSS）上评估了 PPDL。

准确率提升： 推理缩放通常优于基准方案（单次执行，IS@1）。虽然多数投票在某些情况下表现良好，但 重要性采样 (IS) 和 顺序蒙特卡洛 (SMC) 通常能产生更优的结果，特别是当 factor 约束能提供有意义的信息来区分正确与错误的轨迹时。
SMC 的优势： 在复杂的、多步骤的流（如定理证明）中，SMC 显著优于 IS。通过在中间 factor 点进行重采样，SMC 可以更早地将计算重定向到有前景的路径，避免在错误的局部轨迹上浪费 token。
定理证明案例研究： 在 MiniF2F-Rocq 基准测试中，使用 40 个粒子的 SMC 解决了 39% 的问题（95/244），相比之下，基准 IS@1 策略解决了 30%（72.7/244），且两者都在固定的 token 预算内。这表明概率引导可以提高基础模型在挑战性任务上的性能。

重要性与主张

论文声称 PPDL 提供了一种处理 LLM 应用中不确定性的原则性方法。通过将 LLM 流视为概率程序，它允许开发者：

量化不确定性： 用户接收到一个输出分布，从而能够评估置信度，而不是依赖于单个可能错误的答案。
高效实验： 开发者可以通过更改运行时配置（例如，从简单的投票切换到复杂的 SMC）来实验不同的推理缩放策略，而无需重构代码。
解耦逻辑与搜索： 将核心流逻辑与搜索策略（推理引擎）分离，简化了鲁棒智能体工作流的开发。

作者承认，推理缩放并非“万灵药”，其结果质量取决于所提供的约束（factors）的质量，而这些约束可能是不完美的。然而，PPDL 提供了一个灵活的框架，用于集成和测试各种约束来源及推理算法。