SPL：使用声明性确定性与概率组合编排工作流

# 使用声明式确定性-概率性组合编排工作流

来源：https://arxiv.org/html/2607.07727

###### 摘要

我们提出结构化提示语言 (SPL)，一种声明式语言，可在单一规范中组合*确定性*和*概率性*计算模式。现有框架将它们分离——编排系统（AutoGen、CrewAI、LangGraph）负责 LLM 调用，符号工具（SymPy、SageMath、Lean）负责计算——而 SPL 将它们统一起来。它提供 `GENERATE`/`EVALUATE` 用于概率性计算，`SOLVE`/`ASSERT` 用于确定性计算，共享语法、变量绑定和运行时路由。一个 `.spl` 规范可在本地节点（Ollama）、云 API（OpenRouter、Anthropic）和分布式网格（Momagrid）上无修改运行，模型和验证器的选择推迟到调用时。我们通过一个包含 78 个配方的丰富食谱和一个受控的 1,200 次运行实验（10 模型 × 20 问题 × 2 臂 × 3 重复；20 个问题跨越 6 个难度层级）验证了 SPL。求解器臂实现了 82–93% 的机器验证正确率（sonnet-4-6:85%，gemma4:e2b:93%），而仅 LLM 臂测量输出生成（无数学验证），使得比较是*经验证的正确性*与*未经验证的流利度*之间的对比。后端难度梯度显现（SymPy 78%，Sage 54%），主要失败模式是 solver_error（内核拒绝的表达式），而非格式不符合规范。

关键词：声明式语言，LLM 编排，确定性-概率性组合，工作流规范，符号验证，结构化提示语言

## 1 引言

### 1.1 问题：LLM 编程中的碎片化

当前构建基于 LLM 的工作流系统需要掌握令人望而生畏的多项技能。实践者必须精通提示工程以进行有效的 LLM 交互、掌握 Python 编程以进行编排逻辑、处理不同模型提供商的 API，以及手动管理多步推理中的状态。每个流行框架——LangGraph、AutoGen [1]、CrewAI [2]——都引入自己的抽象、API 接口和执行模型，形成一个碎片化的生态系统，知识迁移困难，供应商锁定成为常态。

这种情况呼应了数据行业之前见过的模式。在关系数据库早期，程序员使用命令式的 C 和 COBOL 代码遍历数据结构、管理游标和处理错误——所有操作都以特定于应用的方式进行。20 世纪 70 年代 SQL 的引入通过提供声明式规范层改变了这一格局：用户描述*什么*数据他们想要，而不是*如何*检索它。这种分离使得在稳定表面语言下数十年的优化器创新成为可能。

当前的 LLM 编程状态类似于前 SQL 时代：强大的能力被埋藏在层层的命令式胶水代码之下。入门门槛加剧了这个问题。即使构建一个简单的自我改进工作流——起草、批评和修订自身的输出——开发者也需要编写 80–150 行 Python 代码，涉及多个框架抽象。这排除了大量的领域专家、分析师和研究人员，他们理解自己的工作流但缺乏软件工程技能来以命令式编排代码表达它们。

### 1.2 双模式差距

所有现有框架——无论是声明式还是命令式——都在单一计算模式下运行。以 LLM 为中心的系统（LangGraph、DSPy、AutoGen）产生由模型训练分布塑造的近似、不可复现的输出。符号工具（SymPy、SageMath、Lean）产生精确、可复现、机器可验证的结果。两种世界在统一的编程模型内互不沟通。我们称之为**双模式差距**。

实际智能体任务通常需要两者。一个作业助手必须用自然语言规划解决方案（概率性），精确执行每个代数步骤（确定性），验证结果（确定性），然后向学生解释（概率性）。模式之间的耦合可能是*松散*的——不同阶段之间一次性传递数据——也可能是*紧密*的：一次 `ASSERT` 失败立即触发纠正性 `GENERATE`，修正计划并重新进入符号引擎。这两种模式在实践中都会出现；两者都需要特定于应用的胶水代码来协调每次模式跨越时的状态转移和错误传播。

这个差距不是工程上的不便——它是一个表达力上限。没有现有工作流语言允许程序员在同一个规范中声明“精确计算此步骤”和“近似生成此步骤”。SPL 通过*声明式组合*来弥合这一差距：程序员指定每个步骤计算什么以及它属于哪种模式；运行时解析边界、管理状态转移并强制验证门——无需胶水代码。

人类认知的双过程理论 [21] 提供了一个有用的类比——但需要关键修正。卡尼曼的框架将两个系统命名为*快*和*慢*，混淆了认知速度与认识论模式。这种混淆在计算环境中具有误导性：发现量子力学是直觉性的、探索性的，且极其缓慢；一旦薛定谔方程确立，*求解*它变得确定而机械——手工慢，计算机快。速度追踪的是实现，而非模式。相关的区别是认识论的，而非时间上的。系统 1 是*概率性和直觉性的*：它进行模式匹配、产生假设并输出由先前经验塑造的近似结果——无论墙上时钟时间如何。系统 2 是*确定性和机械性的*：它应用显式规则以产生精确、可复现的结果——无论这些规则在毫秒还是分钟内执行。在 SPL 的映射中：`GENERATE` 和 `EVALUATE` 是系统 1 的原语（LLM 推理、近似、质量评估）；`SOLVE` 和 `ASSERT` 是系统 2 的原语（符号内核、精确、机器可验证）。SymPy 内核可能比 LLM 更快地计算导数；Lean 4 证明可能花费更长时间。这两个事实都不会改变每个步骤所属的模式。模式——而非速度——是组织原则。

### 1.3 我们的贡献

我们提出 SPL，一种声明式语言，在单一连贯规范中组合两种计算模式。本文的主要贡献是：

C1. **声明式双模式组合**。SPL 提供了 `SOLVE` 和 `ASSERT`——这些原语将计算路由到实时 Python 内核（IPython）而非 LLM——以及用于概率性模式的 `GENERATE` 和 `EVALUATE`。一个单一的声明式规范自由组合两种模式；变量绑定通过共享的 `@variable` 命名空间在它们之间流动，无需程序员手动编组。模式边界在源代码中可见，并由运行时完全管理。

C2. **DODA 原则**。一次设计，随处部署：一个单一的 `.spl` 规范是不变量。模型提供商（Ollama、OpenRouter、Anthropic、Momagrid）和验证器（SymPy、SageMath、Lean）的选择在调用时通过 CLI 标志解析，而非嵌入规范中。同一文件在开发者笔记本电脑和分布式推理网格上运行无需修改——声明式组合是实现这一点的机制。

C3. **验证器阶梯**。我们实现了一个三层符号验证器层次结构——SymPy（代数）、SageMath（数学）、Lean 4（形式证明）——作为递增的正确性保证，可通过 `ASSERT` 组合到任何 SPL 工作流中。R1 和 R2 在 1200 次运行实验中通过经验评估；R3（Lean 4）已实现，具有工作桥接（15/15 单元测试通过），并作为设计贡献展示——R3 的完整实验评估是未来工作。每个阶梯是一个在运行时注册的 Python 可调用工具；工作流规范对哪个阶梯处于活动状态不可知。阶梯本身是*声明*而非*编码*的：升级逻辑是 `.spl` 中的 `ASSERT` 链，而非 Python 条件语句。

C4. **受控经验评估**。一项 1200 次运行实验（10 模型 × 20 问题 × 2 臂 × 3 重复；问题跨越 6 个难度层级）在符号数学上提供了双模式组合益处的定量证据，并揭示了一个结构化的能力层次：在概率臂（纯 LLM 数学）中得分 100% 的模型可能在双模式臂（求解器）中得分 0%，不是因为它们无法解决数学问题，而是因为它们无法产生确定性引擎所需的结构化分解。这表明声明式组合的格式符合性是与数学推理分离的能力。

### 1.4 论文组织

第 2 节综述相关工作，将 SPL 定位在命令式框架、声明式系统和神经符号 AI 之间。第 3 节介绍 SPL 语言设计——完整的原语集、语义和形式文法。第 4 节形式化验证器阶梯。第 5 节描述实现：双模式执行器如何将概率节点分发到适配器层，将确定节点分发到内核层，模型提供商和验证器均在调用时选择。第 6 节展示 1200 次运行的经验评估（r=3）。第 7 节讨论优势、局限和未来方向。第 8 节总结。

## 2 相关工作

### 2.1 数据编程的演变

数据编程的历史为 SPL 提出的转变提供了清晰的先例。20 世纪 70 年代，IBM 的 System R 项目表明，声明式查询语言（SQL）可以匹配甚至超越手工编码的导航式数据库访问的性能，因为声明式形式暴露了命令式代码中不可见的优化机会 [3]。到 20 世纪 80 年代，SQL 已成为行业标准，Oracle 的 PL/SQL 扩展表明，可以在声明式查询之上添加过程控制流（循环、变量、异常处理），而不牺牲优化器对单个 `SELECT` 语句的推理能力 [4]。

与 LLM 编程的平行之处是直接的。今天的命令式框架——LangGraph 的状态图、AutoGen 的对话循环、CrewAI 的基于角色的智能体——相当于前 SQL 时代的导航代码：强大、灵活，且不可思议地碎片化。SPL 提出，同样的声明式革命可以发生在 LLM 编排领域，遵循相同的演化路径：原子声明式查询（`PROMPT`）组合成过程工作流（`WORKFLOW`），优化器最终可以在不改变规范的情况下重写和路由它们。

与 SQL 时代的一个关键区别：数据查询是确定性的。LLM 编排则不是。这需要新的原语——`EVALUATE` 用于语义分支，`WHILE` 用于质量门控迭代，`EXCEPTION` 用于概率性失败模式——这些在 SQL 中没有对等物。并且它需要完全第二种计算模式：`SOLVE` 和 `ASSERT` 用于结果必须精确而非近似的情况。

### 2.2 命令式编排框架

**AutoGen** [1] 专注于多智能体对话模式，智能体之间交换消息。其优势在于自然对话流；局限是编排逻辑嵌入在 Python 中，与运行时紧密耦合。**CrewAI** [2] 引入了基于角色的比喻，专业智能体协作。对于团队式工作流直观；以 Python 为先，没有通向编译或优化的路径。**PydanticAI** 采用代码优先的方法，优先考虑开发者体验和类型安全。与上述框架一样，它仅在概率模式下运行，没有符号集成层。

这些框架都没有提供语言级机制来声明“确定性地执行此步骤并在工作流继续之前验证结果”。

### 2.3 声明式 LLM 系统

**LMQL** [5]（苏黎世联邦理工学院，2022）开创了类似 SQL 的 LLM 交互，带有输出约束（类型、长度、正则表达式），通过约束解码实现了 26–85% 的成本降低。LMQL 在查询级别操作——带有输出验证的单个提示——不提供多步工作流或确定性集成的构造。**DSPy** [6]（斯坦福，2023）引入了声明式模块（`Predict`、`ChainOfThought`）和编译器，通过少样本引导自动优化提示。DSPy 的“声明式”是在模块接口级别：它优化使用哪些提示，而不是如何编排多步工作流。它不提供迭代、异常处理、符号集成或形式文法。**SGLang** [7]（加州大学伯克利分校，2023）提供了结构化生成，带有运行时优化（RadixAttention，高达 6.4× 吞吐量）。SGLang 在智能体模式之下优化推理执行；它不解决工作流编排问题。**Agent Spec** [8]（Oracle 实验室，2025）定义了一个 YAML/JSON 模式，用于与框架无关的智能体规格说明。这是一个配置格式，而非可执行语言：它本身缺乏控制流、迭代和异常处理。**eBay DSL** [9]（2025 年 12 月）将工作流规格说明与实现分离，支持多种后端语言，实现了 60% 的开发时间减少。专注于企业流水线配置；未形式化 LLM 特定的原语或符号集成。**Agentics 2.0** [10]（IBM，2026 年 3 月）引入了一个逻辑转导代数，LLM 调用是类型化的语义变换，可通过基于代数的操作符组合。这是形式上最接近的并发工作，但受 SQL 启发，且仍在概率模式下运行。**Compiled AI** [11]（Trooskens 等人，2026 年 4 月）通过编译时 LLM 调用来解决非确定性问题：语言模型在规格说明时运行一次，生成一个确定性可执行工件；运行时没有 LLM 调用。这实现了强执行保证，但代价是失去了所有运行时适应性——没有 `EVALUATE` 分支，没有 `WHILE` 质量门控，没有 `EXCEPTION` 恢复。SPL 采取相反的立场：两种模式在运行时都保持活跃且同等可访问，通过一个单一声明式规范交错。权衡是明确的：SPL 在确定性验证旁边保留了完整的概率性表达能力（多轮 LLM 调用、自适应路由、异常处理）。**Blueprint First** [12]（Qiu 等人，2025 年 8 月）提出了一种工程模式，将工作流逻辑与生成模型解耦。专家定义的过程被编码为“执行蓝图”（确定性引擎），LLM 仅在其中有限的子任务中被调用。虽然这呼应了 SPL 的 DODA 原则——蓝图作为不变量，LLM 作为可插拔组件——但该方法仍是一种设计模式而非可执行语言。Blueprint First 没有符号验证层（没有 `SOLVE`/`ASSERT` 对等物），没有形式文法，也没有允许模式间无缝数据流的共享变量命名空间。蓝图是一个手动维护的工程工件；SPL 的规格说明是可执行的编译形式。

### 2.4 LLM + 求解器组合

另一条独立的工作线探索通过模式组合将语言模型与符号求解器耦合：LLM 将自然语言问题翻译成求解器编码，求解器确定性地执行，LLM 将结果翻译回自然语言。**LLM+P** [13]（Liu 等人，2023 年 4 月）开创了这一模式：语言模型生成 PDDL 规划