在研究 AI Agent 的过程中,我发现了一个有趣的现象:虽然质量至关重要,但成本和执行时间(推理时间)往往成为 Agent 管道中最大的争议点。

像 GPT-5.2 或 Gemini 3 Pro 这样的"推理"大语言模型确实可以提高质量。然而,我注意到它们往往存在生成时间长和 token 使用量增加的问题,从而推高了成本和延迟。当 Agent 需要在每个任务中做出大量决策时,这种权衡就会成为一个重大瓶颈。

在这篇文章中,我将展示如何将 LLM 的角色限制为"翻译器"或"编译器",并将实际的推理工作交给单独开发的逻辑算法。结果如何?我们在超越推理模型准确性的同时,实现了 96.9% 的成本降低和 93.8% 的执行时间缩短。

实现的运营效益

  • 总体准确性提升:89.3% → 90.2%
  • UNSAT 类别准确性提升:65.0% → 86.2%
  • API 成本降低:$29.50 → **$0.91**(降低 96.9%)
  • 执行时间缩短:14.0 小时 → 52 分钟(缩短 93.8%)

在这次开发中,我使用了 gpt-4o-mini。这个模型单独使用时,准确率徘徊在 50% 左右——本质上不比随机猜测好。然而,通过添加后端,我们的准确率超过了 90%,在所有测试模型(包括专用推理模型)中记录了最高的准确率。此外,这种高性能在所有类别和难度级别上都很稳定。

对比目标

  • 纯 LLM(基线):o4-mini(OpenAI)、DeepSeek-R1 等多个模型。
  • 混合方案:gpt-4o-mini + 后端(基于规则的解析 + CNF 形式化 + SAT 求解器)。

本文提供的内容

如果你是一名致力于将 LLM 整合到公司工作流程或开发 Agent AI 的工程师,你可能正在纠结于模型选择以及质量、成本和延迟之间不可避免的权衡。这份工程报告涵盖:

  1. 如何构建 LLM 和求解器的混合结构。
  2. 对成本和延迟影响最大的实施决策。
  3. 如何有效测量 token 使用量和执行时间。
  4. 如何重现"纯 LLM"和"LLM + 后端"之间的比较。

我的目标不是声称后端应该完全取代推理模型。相反,我想展示的是,对于某些类别的决策问题,使用强大的后端可以让明显更小的模型在端到端性能上具有竞争力。

在准确性、成本和时间上实现顶级指标

“基准测试"是验证 LLM 质量最常见的方法。存在数百个基准测试来检查质量的各个方面——有些专门针对数学,有些针对特定的逻辑领域。在大多数讨论中,“准确性"是默认指标。

然而,对于 Agent 系统来说,准确性是必要条件,但不是充分条件。在生产实施中,系统在成本和执行时间方面也必须是可行的。

一个有用的框架:语言问题 vs. 决策问题

我发现许多"LLM 任务"可以分解如下:

  1. 语言处理:从文本中提取结构、实体和关系。
  2. 决策制定:一致性检查、搜索分配和证明不可能性。

LLM 在(1)方面很有效。然而,对于(2),确定性算法(如 SAT 求解器)要可靠和高效得多。

我在本文中采用的方法遵循一个简单的原则:“使用 LLM 进行翻译,使用后端进行决策。”

SATBench 概述(2 分钟解释)

为了测量推理质量、成本和延迟,我使用了斯坦福大学开发的"SATBench"基准测试。这个基准测试于 2025 年发布,专注于经典的布尔可满足性问题(SAT)。任务是确定给定的场景和一组条件是否可以同时满足(SAT),或者这是不可能的(UNSAT)。

我注意到 LLM 通常很难得出"未找到解决方案"的结论。因此,许多模型在这个基准测试的 UNSAT 问题上得分很低。在斯坦福的实验中,gpt-4o-mini 在 UNSAT 问题上只得了 13.2% 的分数,即使是最强大的模型 o4-mini,得分也只有 65.0%——仅略好于 50% 的随机猜测。相比之下,我们的混合模型达到了极高的 86.2%(在所有测试模型中最高)。

SATBench 很有用,因为它突出了纯 LLM 推理中的一个常见失败模式:“UNSAT 检测”。仅仅"未找到解决方案"并不能证明 UNSAT。要证明 UNSAT,你需要一个可靠的搜索/证明机制。当推理轨迹不完整时,许多模型倾向于输出 SAT(可满足)答案。

这与现实世界的 Agent 任务密切相关,例如检测约束、策略或需求中的矛盾。

核心思想:将 LLM 视为编译器前端

我将 LLM 视为一个"编译器前端”,它将自然语言转换为正式的中间表示。

LLM 的角色:形式化(翻译)

假设我们有以下条件:

“Blip 显示行为 2,或者 Blip 不显示行为 1。”

LLM 可以可靠地识别:

  • 实体:(“Blip”)
  • 谓词:(“显示行为 2”/“显示行为 1”)
  • 否定:(“不”)
  • 逻辑连接词:(析取/或)

这主要是一项翻译任务。

后端的角色:确定可满足性

一旦翻译成 CNF(合取范式)子句,SAT 求解器就可以确定性地判断 SAT/UNSAT。这避免了纯 LLM 推理在 UNSAT 情况下面临的模糊性。

因此,高成本的"推理搜索"部分从 LLM 调用路径中移除了。

构建一个最小且实用的混合系统

我采用的管道配置如下:

  1. LLM 从用户那里接收自然语言问题。
  2. 问题类型路由器识别问题类型(例如,SMT、COP、PDDL/动作规划、LP)并将其发送到适当的解决管道。
  3. 在 SATBench 的情况下,所有内容都发送到 SAT 管道,在那里选择 SAT 求解器。
  4. 求解器确定问题是 SAT 还是 UNSAT。

在这个管道中,你可以看到虽然 LLM 被用作翻译器/编译器,但它不参与决策。这使我们能够保证准确性,同时显著改善与 LLM 相关的成本和延迟。

既然 SATBench 只是 SAT,为什么还要包括路由?

尽管 SATBench 仅限于 SAT,但我构建路由是为了可扩展性。在真实的 Agent 系统中,任务通常混合多种推理范式(逻辑编程、一阶逻辑推理、CSP、SAT/SMT 风格的一致性检查)。路由提供了一个明确的接口,可以在以后集成其他求解器,而无需更改核心管道。

注意:本文中的所有实证结果都集中在 SAT 路由上。

实施说明和关键工程决策

本节解释对端到端性能产生重大影响的决策。

从 LLM 中消除数字索引生成

在早期迭代中,我发现许多形式化失败不是由于误解句子,而是由于将名称映射到 variable_mapping 中的索引。

例如,如果 variable_mapping 定义为:

“外星生物 2 是 Blip”

如果模型错误地为 Blip 输出像 $x(1, …)$ 这样的文字,数学公式就会变成一个完全不同的问题。

为了解决这个问题,我改变了契约。LLM 不输出数字索引。

相反,LLM 输出命名文字:

1
2
3
4
5

{
  "entity": "Blip",
  "j_label": "behavior 2",
  "neg": false
}

然后,后端使用从 variable_mapping 派生的符号表将名称和标签解析为 $x(i,j,k)$。这将一个脆弱的步骤(索引分配)从概率生成转移到确定性解析。

从 variable_mapping 构建健壮的符号表

在真实数据集中,使用了各种表达式:

  • “0 是 Alice”
  • “0 被指定为 Zorg”
  • “机器 2 指的是打印机”

如果解析器无法提取映射,命名文字就会变成"未知实体”,影响覆盖范围。我通过扩展映射模式、规范化大小写/空格以及添加受控回退路径来解决这个问题。

作为覆盖机制的回退策略

覆盖范围在操作上至关重要。如果系统无法解析命名文字,它不应该崩溃。相反,它应该:

  • 记录失败。
  • 回退到更简单的形式化模式(例如,直接 $x(i,…)$ 输出)。
  • 继续处理数据集。

这种"失败开放"行为通常在具有下游评估或重试策略的 Agent 管道中是首选的。

基于规则的解析作为一等组件

对于匹配常见模板(析取、单元否定、蕴涵形式)的条件,基于规则的解析提供零成本、低延迟和更少的模式失败。事实上,这一层负责显著减少 LLM 调用的总数。

结构化输出、验证和有针对性的修复

结构化输出减少了歧义,但引入了实际的失败模式(小格式错误、杂散否定符号、全角字符、括号不匹配)。

我使用严格的模式验证、规范化和有针对性的修复规则(例如,将 ¬x(…) 转换为 {neg:true, var:“x(…)”})来减少可避免的失败。

求解器后端:确定性可满足性检查

一旦 CNF 可用,可满足性的确定就委托给确定性求解器(DPLL)。这避免了"未找到"和"不存在"之间的混淆——这是纯 LLM 方法在 UNSAT 情况下的主要失败模式。

测量、结果和实际意义

测量的内容

对于纯 LLM 基线和混合系统,我都测量了:

  • 总 Token 数:输入/输出/总计
  • 总运行时间
  • 每个问题的平均时间
  • 准确性:(SAT/UNSAT 的正确性)
  • 覆盖范围:(可以生成最终标签的问题数量)

当目标是优化 Agent 管道而不仅仅是最大化基准准确性时,这种检测是必不可少的。

Token 使用量细分(100 个问题的子集)

为了理解为什么成本下降如此剧烈,我详细分析了 100 个问题的子集。

  • 输入 Token:44,534(纯)vs 53,533(混合)
  • 输出 Token:128,783(纯)vs 17,968(混合)
  • 总 Token:173,317(纯)vs 71,501(混合)
  • LLM 调用次数:100(纯)vs 52(混合)

主要区别在于输出 token 的数量,这主导了成本。

对现实世界 Agent 系统的解释

这些结果表明了实际的工程权衡:

  • 如果 Agent 管道主要由迭代决策等检查主导,用后端替换推理式 LLM 调用可以显著降低成本和延迟。
  • 即使是不执行"推理"的模型,如果它们的角色仅限于形式化,并且由确定性组件处理决策过程,也足够实用。

注意事项和部署考虑

这种方法不是万能的。主要注意事项是:

  • 形式化错误成为主要失败模式:如果自然语言无法可靠地映射到形式表示,求解器是否正确也无关紧要。
  • 领域转移影响基于规则的解析:基于规则的解析适合类模板数据。在非结构化领域,“快速路径"覆盖范围会缩小,需要为更多实例进行 LLM 形式化。
  • 后端选择取决于问题类别:SAT 求解器非常适合布尔代数一致性检查。真实的 Agent 可能需要其他后端,如 CSP、SMT、规划或数据库/查询引擎。

这种模式直接有用的地方

在实际应用中,我预计这种模式最适用于:

  • 配置和兼容性检查。
  • 策略/规则一致性(访问控制、合规约束)。
  • 调度可行性(转换为 CSP/SAT 变体)。
  • 多步骤 Agent 中高度受限工作流的编排。

一般工程原则是:“使用 LLM 将语言转换为结构,使用专门的后端来解决结构化问题。”

总结

到目前为止,基准测试主要用于测量 LLM 的"智能”。展望未来,我预计它们将越来越多地用作测量和保证成本和延迟的工具,同时保持"足够的智能"。

在这次实践中,我展示了使用更旧、更便宜、更快的模型实现更高准确性是可能的。我希望这能为你在内部业务工作流程中开发 AI Agent 或作为 SaaS 提供的 AI Agent 提供有用的参考。

参考资料