STRIPS（1971）

符号规划器：谓词写世界，算子搜出计划。它给每个动作附一张效果清单，这层推演正是今日 Agent 所缺。

原文：Fikes & Nilsson, 1971，STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving，Artificial Intelligence 2: 189–208。IJCAI-71 报告，实现用 LISP 运行在 PDP-10 上，服务于 SRI 的机器人研究（Shakey）。

这个概念是什么

STRIPS（Stanford Research Institute Problem Solver）是一个符号规划器。给定当前世界的描述、一组可执行动作和一个目标条件，它要找出一串动作，使执行之后目标成立。

它处理的不是自然语言，也不是从数据里学到的策略。世界写成一阶谓词演算中的合式公式（wff）；每个动作对应一个算子，算子增删公式；计划是算子的有序列表。论文明确区分：对世界模型应用算子发生在规划阶段，执行动作例程才改变物理世界。

经典人工智能称这一支为 planning。1998 年以后的 PDDL 把 STRIPS 风格的领域写成标准输入，仍是同一条技术路线。

关键术语：谓词

谓词是从一组对象到真值的函数。它不返回一个值，而是返回「成立 / 不成立」。

这一节里的三个例子，用的是两种元数：

写法 谓词符号 元数 读法
ATR(a) ATR 1 机器人在位置 a
AT(B, b) AT 2 物体 B 位于位置 b
AT(C, c) AT 2 物体 C 位于位置 c

B、b、a 这些叫常量，换成变量就是 AT(x, y)。谓词符号加实参构成的整体 AT(B, b) 叫原子公式。前面说「世界写成一阶谓词演算中的合式公式」，指的是这些原子公式用逻辑联结词（∧、∨、¬）组合后的式子；目标是 AT(B, a) ∧ AT(C, a)，就是一个合式公式。

所以「世界是谓词集合」的准确含义是：世界模型是一组为真的公式，每条公式说的是某几个对象之间某个关系成立。

谓词对应的英文单词是 predicate。STRIPS 论文里的原话是 first order predicate calculus，对应中文的「一阶谓词演算」，也就是一阶逻辑。读原文时会遇到的相关英文术语如下：

中文 英文 说明
谓词 predicate 从对象元组到真值的函数
谓词符号 predicate symbol AT、ATR 本身，不带实参
命题 proposition 不可再分、没有内部结构
原子公式 atomic formula / atom AT(B, b) 这样的完整式子
合式公式 well-formed formula (wff) 原子公式用联结词组合后的式子
基公式 ground formula / ground atom 不含变量、全部由常量构成
元数 arity 谓词接受几个参数
项 term 常量、变量或函数应用
算子模式 operator schema 带变量的动作模板，如 goto(m, n)
前提 precondition 应用算子前要证明的 wff 模式
增列表 / 删列表 add list / delete list 算子的效果

补充：predicate 在语法学里是「谓语」，与逻辑学里的这个「谓词」是同一个词、不同的领域，读英文材料时靠上下文区分。

关键术语：模型

论文里说的 model（世界模型）指的是「一组为真的公式」，不是机器学习里的那个模型，也不是大语言模型中的模型。

这个词在 1971 年的语境里是逻辑学的用法，与 2023 年说的 model 无关。读原文时，这一处最容易产生错觉。

论文的主要内容

要解决的问题

在「世界模型」的空间里搜索，直到找到一个能满足目标的模型。对任意世界模型，都存在一组可应用的算子；求解器寻找算子的复合，把初始模型变成满足目标的模型。对象是机器人重排物体、在房间之间导航。世界必须容纳大量事实，因此用一阶谓词演算的公式集合，而不是矩阵或表。

直接前驱是 Green 的系统：把「寻找动作序列」完全交给形式定理证明。这条路线受制于框架问题：必须显式说明「这个动作没有改变哪些事实」。STRIPS 把两件事分开：

  • 定理证明只在一个固定的世界模型内部进行，用来回答「某个算子当前是否可用」「目标当前是否成立」。
  • 在世界模型之间搜索用类似 GPS 的手段—目的分析，用来挑选下一个相关算子。

问题空间的三个要素

论文第 2.1 节把问题空间定义为三元组：

  1. 初始世界模型 (M_0)：一组 wff。例如机器人在位置 (a)、箱子 B、C 分别在 (b)、(c)：

    ATR(a)
AT(B, b)
AT(C, c)

    也可以写入一般规则，例如「一个物体不能同时在两个不同位置」。

  2. 算子：按族写成模式（schema）。例如 goto(m, n) 表示从地板上一点 (m) 走到 (n)；代入具体常量后才得到可应用的算子实例。每个算子描述包含：

    • 前提（precondition）：一个 wff 模式。要从当前模型证明它的某个实例，算子才能使用。
    • 效果：必须加入模型的公式列表，以及不再为真、必须删除的公式列表。

  3. 目标 (G_0)：一个 wff。例如「把箱子 B 和 C 都弄到位置 (a)」写成 AT(B, a) ∧ AT(C, a)。

当某个世界模型能够证明目标公式时，问题求解结束。

搜索策略：手段—目的分析

若对每个模型盲目应用全部可用算子，后继树会大到无法处理。STRIPS 采用 GPS 策略：

  1. 用定理证明器尝试从当前模型 (M) 证明当前目标 (G)。
  2. 若证明成功，这一层目标完成。若失败，把未完成的证明当作 (M) 与 (G) 之间的差（difference）。
  3. 寻找效果能够推进该证明的相关算子；其前提成为子目标。
  4. 对子目标重复同一过程。子目标在当前模型中可证时，应用对应算子，得到新模型，再回头考虑原来的目标。

一个最小例子：目标 ATR(b)。若机器人不在 (b)，证明失败。算子实例 goto(m, b) 相关；子目标是前提 ATR(m)。若初始模型含 ATR(a)，则 ATR(a) 可证，应用 goto(a, b) 得到新模型，其中 ATR(b) 成立。

搜索树的每个节点是 (\langle)世界模型, 目标表(\rangle)。相关算子被选出时，并不预先知道它会排在最终计划的第几步。实现上，STRIPS 在一个模型内部调用基于归结的定理证明器处理带参数的 wff 模式，在模型之间维护上述搜索树。论文后半给出在房间中行走、推箱子等实例。

作者标明的限度

  • 规划与执行分离：算子应用改变的是模型；物理动作由独立的执行与监控模块负责。
  • 框架问题并未从哲学上消失，而是用增删列表把「未列出的公式保持不变」写成操作约定。后来文献称此为 STRIPS 假设。
  • 世界必须能被写成谓词；开放文本、传感器噪声、未建模的副作用不在该问题空间内。

关键术语

术语 在这篇论文里的含义
世界模型 一阶谓词演算公式的集合，描述某一时刻的世界
算子 / 算子模式 动作在模型上的对应物；模式含参数，实例化后才能应用
前提 应用算子前必须从当前模型证明的条件
增列表 / 删列表 应用算子后加入、删除的公式；未列出的公式默认不变
计划 从初始模型走到目标可证模型的算子序列
差 当前模型无法完成目标证明时，未完成证明所代表的缺口
框架问题 如何简洁地表示「动作不改变哪些事实」

和 AI Agent 的关系

STRIPS 是符号规划器：谓词写世界，算子搜出计划。它给每个动作附一张效果清单，这层推演正是今日 Agent 所缺。

它的循环在世界模型空间里反复搜索，直到目标可证；动作由执行程序在计划算出之后完成。观察是定理证明器对当前模型的询问，不是开放文本回执。决策核心是定理证明加搜索，世界是谓词集合，而非工具 JSON 或屏幕。后来 LLM Agent 中的 Planning，古典形态就是这一支，控制流在规划器，不在解码过程中。它也不是 ReAct、不是 Function Calling，不是编码运行时的祖先产品。

两者都在做同一件事：让机器自己决定下一步做什么；区别在于如何处理「一个动作会改变什么」，而这个区别决定了各自的能力边界。

STRIPS 的做法，是给每个动作附两张清单。第一张写做这件事需要什么，即前提；第二张写做完之后世界加上什么、去掉什么，即增列表与删列表，合起来就是效果。页面里那个 goto(m, n) 动作，两张清单是：前提「在 m」，效果「去掉『在 m』，加上『在 n』」。

有了这两张清单，规划器就能在动手之前推演。目标是「在 b」，当前是「在 a」，对不上；哪个动作能产生「在 b」？goto(m, b)，代入 n=b。它的前提是「在 m」，而当前「在 a」成立，于是 m=a，得到 goto(a, b)。整条链条算完，机器人还没有移动一步。这就是它能搜索、能给出计划的全部依据。

今天的工具不是这样。给模型一份工具说明，上面通常只有参数：「查天气」要城市名，「跑测试」要命令，「发邮件」要收件人和正文。没有哪一份说明会写调用之后世界变成什么样。 模型因此只能反过来做：先把工具调出去，看返回了什么，才知道刚才发生了什么。

这个差别在短任务上看不出来，任务一长就显出来。STRIPS 可以在一棵搜索树里比较不同动作的后果，挑一条走；LLM Agent 没有这棵树，它只有当前上下文里已经发生的事。事先推演退化成事后试错，而试错有两个代价：每一步都真的作用在环境上，每一步都要占用上下文。规划能力弱、失败之后不会修改计划、副作用不可预期，都可以追溯到这里。

那为什么不给今天的工具也补上这两张清单？因为写清单要求环境能够被形式化。goto(m, n) 之所以写得清楚，是因为「位置」可以被写成谓词；而「把这个仓库的测试修绿」没有形式化的状态可写，「订一张去上海的票」牵涉几十个外部系统，都无法事先说清一个动作会改变什么。STRIPS 只能处理能被写成谓词的环境，这就是它的边界。

所以这一页记的不是「Agent 的祖先」，而是一次取舍。古典 Agent 用形式化的世界与效果模型换来可证明的计划，代价是只能处理能被写成谓词的环境；LLM Agent 放弃了这些保证，换来在开放语言空间里的通用性。丢掉的那部分形式化，正好落在今天最不可靠的地方。