面向LLM时代的TLA+入门：用提示词取胜

# 面向LLM时代的TLA+入门：用提示词走向胜利 来源：https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/ 大多数工程师对使用 TLA+ 的第一反应是语法不友好。它看起来像 LaTeX，不像代码。但现在，前沿的 LLM 可以轻松生成 TLA+。你仍然需要理解自己的系统并定义“正确性”的含义，同时需要对时序逻辑有高层次的理解。我将在本文中解释时序逻辑。在文章末尾，我将展示一个示例提示，用于使用 Claude 开始编写 TLA+ 规范。 ## [一个玩具问题](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#a-toy-problem) ** 这里有一个经典谜题。你有一罐豆子。每颗豆子是白色或黑色。罐子初始非空。只要至少有2颗豆子： - 选择2颗豆子。 - 如果它们颜色相同：丢弃这两颗，添加1颗白色豆子。 - 如果它们颜色不同：丢弃这两颗，添加1颗黑色豆子。 两个问题： 1. 豆子数量能否达到零？ 2. 如果算法终止时 b = 1，那么初始状态必须满足什么条件？ 你可以使劲思考。或者你可以用 TLA+ 写下来，让模型检查器自动回答这两个问题。全部意义在于避免思考——或者至少，让机器验证你的思考是否正确。或者说服你的朋友你的思考是正确的，或者说服你研究论文的同行评审委员会。 ## [逻辑公式如何产生状态机](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#how-logical-formulae-produce-a-state-machine) TLA+ 由 Leslie Lamport 在 1990 年代发明。TLA 代表“动作时序逻辑”，TLA+ 是该特定语言的名称。TLA+ 有基本的布尔逻辑，有集合和函数，以及量词（“forall”和“exists”）。它还有**时序**运算符，我们很快会看到。当你用 TLA+ 编写规范时，你实际上是在编写一个定义状态机的逻辑公式。该机器有一组固定的变量，每个**状态**是变量值的赋值。对于豆子问题，变量有：`w`（白色豆子数量）和 `b`（黑色豆子数量）。每个状态是 `w` 和 `b` 的一组赋值。一个**行为**是一个状态序列，而**规范**是允许的行为集合。 ## [初始状态](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#initial-state) 我们需要一个初始状态规则——一个断言，对于恰好那些我们愿意从之开始的状态为真。用英语说：“罐子初始非空”，即 `w + b > 0`。这些初始状态中哪些匹配该断言？ ``` b = 0 /\ w = 0 b = 0 /\ w = 4 b = 6 /\ w = 1 b = 1 /\ w = "foo" ``` 在 TLA+ 中，“/\\” 表示“与”，所以 `b = 0 /\\ w = 0` 表示“b = 0 且 w = 0”。第二个和第三个状态匹配断言。第一个不匹配，因为 `w` 和 `b` 之和为零；最后一个状态没有意义，因为你不能将 1 和字符串 "foo" 相加。TLA+ 没有类型系统，只有集合，因此没有什么能阻止 `w` 成为字符串。Lamport 称此类事情为“愚蠢的”。我们通过指定 `w` 和 `b` 必须是自然数来防止愚蠢状态： ``` EXTENDS Integers Init == w \in Nat /\ b \in Nat /\ w + b > 0 ``` `EXTENDS Integers` 导入处理整数所需的一切，比如自然数集合 `Nat`，而 `\\in` 是集合隶属运算符 ∈\\in。在 TLA+ 中，`==` 表示“定义为”。这令人困惑，因为它与 C 语言相反：单个 `=` 测试相等性，而 `==` 命名一个公式（类似于宏）。 ## [状态转换](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#state-transitions) 状态转换规则是**两个**状态（当前和下一个）上的一个断言，它说明哪些转换是合法的。让我们将算法转换为 TLA+ 中的状态转换规则。从英语开始： - 2 颗白色豆子：移除 2 个白色，添加 1 个白色 → 净效果：w -= 1 - 2 颗黑色豆子：移除 2 个黑色，添加 1 个白色 → 净效果：b -= 2 - 各 1 颗：移除 1 个白色和 1 个黑色，添加 1 个黑色 → 净效果：w -= 1 注意第一种和第三种情况对状态的影响相同：都是仅从 `w` 中减去 1，`b` 不变。当你精确地写下东西时，这种洞察自然就会浮现。在 TLA+ 中，这些变成三个**动作**： ``` WW == w > 1 /\ w' = w - 1 /\ UNCHANGED b \* 挑选了2个白色 BB == b > 1 /\ b' = b - 2 /\ w' = w + 1 \* 挑选了2个黑色 WB == w > 0 /\ b > 0 /\ w' = w - 1 /\ UNCHANGED b \* 各挑选了1个 ``` 这里我们第一次看到两个运算符。**撇号**（`'`）运算符表示“该变量的下一个值”：`w' = w - 1` 表示“在下一个状态中，w 将等于当前 w 减 1”。`UNCHANGED b` 是 `b' = b` 的简写。你必须在每个动作中说明每个变量——TLA+ 不会假设未提及的变量保持不变。这很烦人，但它迫使你思考每个动作对整个状态的影响。不带撇号的项是**守卫**：动作当前必须满足的条件。带撇号的项是**赋值**：下一个状态的样子。如果守卫为假，则该动作被禁用。`\\*` 开始注释（是的，是一个反斜杠和一个星号）。 ## [完整的 TLA+ 规范](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#a-full-tla-spec) 以下是完整的规范： ``` -------------- MODULE beans ----------------- EXTENDS Integers VARIABLES w, b vars == <<w, b>> \* 所有变量的便捷列表 Init == w \in Nat /\ b \in Nat /\ w + b > 0 WW == w > 1 /\ w' = w - 1 /\ UNCHANGED b \* 挑选了2个白色 BB == b > 1 /\ b' = b - 2 /\ w' = w + 1 \* 挑选了2个黑色 WB == w > 0 /\ b > 0 /\ w' = w - 1 /\ UNCHANGED b \* 各挑选了1个 Next == WW \/ BB \/ WB Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ============================================== ``` 公式 `Next` 定义为所有三个动作的 OR（`\\/`）——在任何给定状态下，满足其守卫的动作都会被启用。这称为**非确定性**：规范没有说明哪个动作会发生，只说明哪些是可能的。模型检查器会探索所有动作。 `Spec` 行是任何 TLA+ 规范的脊梁，你会在读到的几乎所有 TLA+ 规范中看到它。它表示：“该规范允许的每个行为都从 Init 为真的初始状态开始，并且每个转换都满足 Next。”`WF_vars(Next)` 部分表示“算法必须持续取得进展——当某个动作被启用时，它不能永远停顿。”这称为公平性约束（https://www.hillelwayne.com/post/fairness/），稍后详述……`[][Next]_vars` 部分隐藏了一些我准备跳过的复杂性。如果你想深入理解它，请阅读 Lamport 的《Specifying Systems》。对于提示词目的，只需知道它放在那里即可。 ## [状态与行为](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#states-and-behaviors) 一个**行为**是一个无限的状态序列，从一个初始状态开始，其中每一步都被 `Next` 允许。按惯例，行为是无限长的。如果算法终止（达到没有进一步动作被启用的状态），则最终状态无限重复。这种重复称为**停顿**。因此，TLA+ 中的“终止”意味着算法达到一个停顿状态并停留在那里。 我们的规范中有无限多个初始状态——任何满足 `w + b > 0` 的自然数对都是有效的初始状态。让我们查看状态空间的一个子集，即那些从 b=3, w=5 开始的状态： ** 每个节点是一个状态。每条边是一个有效的转换，标有适用的动作。有些边标有“WW/WB”——这是因为当 `w > 1` 且 `b > 0` 时，WW 和 WB 都被启用并导致相同的下一个状态（两者都只是将 `w` 减 1）。模型检查器会探索两个动作，但发现相同的后继状态，因此它们合并为一条边。 一个**行为**在这张图中是从初始节点到终止节点的路径，之后是停顿。例如这样一个行为： ** ## [模型检查](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#model-checking) 模型检查器 TLC 从初始状态集合开始，应用下一状态关系生成后继状态，并使用哈希（它称之为“指纹识别”）来避免重新访问已经见过的状态。当 TLC 发现状态时，它会检查不变量和性质。（我们马上就会了解这些是什么，但暂时知道：这些是证明你的规范正确的断言。）如果 TLC 发现违例，它会报告反例：一个导致坏状态的状态序列。由于它采用广度优先搜索，它会为不变量违例找到**最短**的反例（或其中之一）。这对诊断很有帮助——一个 4 步轨迹比 100 步轨迹容易调试得多。 ## [规范与配置文件](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#the-spec-and-the-config) TLA+ 规范包含两个文件：beans.tla（包含时序逻辑）和 beans.cfg（包含模型检查配置）。为什么是两个文件？一个规范是对系统的理想化描述，其状态空间和行为通常是无限的。你可以用这个规范做很多事情：证明其正确性，或用于记录算法并向朋友解释，等等。模型检查只是规范的几种用途之一，因此模型检查配置放在单独的文件中。当然，如果有无限多个状态，模型检查是不可能的。我们通常必须通过设置初始状态集合的大小限制，或限制执行的动作数量等来人为地约束状态空间。所有这些限制都应放在配置文件中。如果你的规范中有 bug，通常会在一个小规模的有界模型中看到它。（我们称之为“小模型假设”。）在实践中，第一次检查会在第一两秒内捕捉到明显的错误。如果你运行几个小时没有违例，那么你的信心更高。界限需要多大才能发现所有 bug？这很难说。它必须来自你对算法的推理和直觉。 那么，假设这是 beans.tla（和我上面展示的规范相同）： ``` -------------- MODULE beans ----------------- EXTENDS Integers VARIABLES w, b vars == <<w, b>> \* 所有变量的便捷列表 Init == w \in Nat /\ b \in Nat /\ w + b > 0 WW == w > 1 /\ w' = w - 1 /\ UNCHANGED b \* 挑选了2个白色 BB == b > 1 /\ b' = b - 2 /\ w' = w + 1 \* 挑选了2个黑色 WB == w > 0 /\ b > 0 /\ w' = w - 1 /\ UNCHANGED b \* 各挑选了1个 Next == WW \/ BB \/ WB Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ============================================== ``` 这是无界的，无法进行模型检查，因为有无限多个初始状态。为了约束模型，我可以像这样更新 `Init`： ``` CONSTANTS WMAX, BMAX Init == w \in 0..WMAX /\ b \in 0..BMAX /\ w + b > 0 ``` 以下是 beans.cfg： ``` CONSTANTS WMAX = 3 BMAX = 3 SPECIFICATION Spec ``` 现在有 15 个初始状态，总共 17 个状态。（留给你一个练习：你能算出来为什么是这些数字吗？） ## [回答问题](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#answering-the-questions) 我们如何使用模型检查器 TLC 来回答我们的两个问题，而不需要使劲思考？ **豆子数量能否达到零？** 我们写一个**不变量**——一个我们声称在每个可达状态中始终为真的状态断言： ``` NotEmpty == w + b > 0 ``` 我们告诉 TLC 检查这个不变量，方法是在 beans.tla 中定义它，并在 beans.cfg 中引用它： ``` INVARIANT NotEmpty ``` TLC 会在整个可达状态图上进行广度优先搜索，并确认没有状态违反它。豆子罐永远不会空。为什么？看看守卫：每个动作需要至少 2 颗豆子才能被启用（`w > 1`，`b > 1`，或 `w > 0 /\\ b > 0`）。并且每个动作恰好将豆子总数减少 1。因此一旦只剩 1 颗豆子，没有动作被启用，算法终止。你永远无法从 1 到 0。 **如果终止时 b = 1，那么初始状态必须满足什么条件？** 看看 BB，唯一改变 `b` 的动作。它将 `b` 减少 2。这意味着 `b` 的奇偶性（奇数或偶数）从初始状态到结束从未改变。因此如果我们终止时 `b = 1`（奇数），那么 `b` 在初始状态必须是奇数。我们可以将其表达为一个**时序性质**——一个对整个行为（而非单个状态）的公式： ``` TerminationWithOneBlack == (b % 2 = 1) => <>[](b = 1 /\ w = 0) ``` 读作：“如果 `b` 是奇数，那么最终-始终 `b` 将为 1 且 `w` 将为 0。”这使用了两个**时序运算符**：`<>`（菱形，意为“最终”）和 `[]`（方框，意为“始终”）。组合为 `<>[]`，它们意为“最终达到一个状态并停留在那里”——这正是终止。我们将定义添加到 beans.tla 并在 beans.cfg 中引用它： ``` PROPERTY TerminationWithOneBlack ``` 我在 beans.cfg 中使用了 `PROPERTY`，因为这是一个时序性质（它使用时序运算符，适用于整个行为），而不是像我之前对 `NotEmpty` 那样使用 `INVARIANT`。TLC 验证该性质在所有行为上都成立，确认了任何从奇数 `b` 开始的行为都会终止于 `b = 1`。但是等等——如果 b 是奇数，它真的最终会达到 b=1 且 w=0 吗？如果 b 是奇数，然后状态机只是停在那里什么也不做呢？这就是公平性约束 `WF_vars(Next)` 所保证的。它表示如果 `Next` 持续被启用（即，由于至少有两颗豆子，某个动作被启用），那么它最终会执行。这对于任何“最终”性质成立是必需的。 ## [时序运算符](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#the-temporal-operators) 时序逻辑在普通一阶逻辑之上添加了两个核心运算符，你可以以有趣的方式组合它们。 `<>P`（**最终 P**）：在行为的某个时刻，`P` 为真。如果 `P` 短暂闪烁然后停止，那也算。 `[]P`（**始终 P**）：在行为中的每一个时刻，`P` 都为真。这基本上就是不变量所说的，只是用时序公式表达。 组合： `<>[]P`（**最终始终**）：`P` 最终变为真，并且永远保持为真。这就是你表达稳定终止的方式：系统达到一个好状态并且从不离开。 `[]<>P`（**始终最终**）：`P` 无限频繁地返回。可能有很长时间 `P` 为假，但它总会回来。这就是你表达诸如“锁总是最终可获取”或“队列总是最终被排空”的方式。 注意，`<>[]P` 严格强于 `[]<>P`。如果 `P` 最终稳定为永真，那么它当然会不断返回。但 `P` 可以不断返回而从不稳定。 ## [TLA+ 与 AI](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/#tla-and-ai) ** 我提示 Claude 为豆子问题编写一个规范： ``` > 给我写一个 TLA+ 规范，针对以下玩具示例。有一个罐子，里面有 w 颗白豆和 b 颗黑豆，初始至少有一颗豆子。每一步，如果至少有 2 颗豆子，移除 2 颗。如果它们颜色相同，丢弃这两颗并向 w 加 1；如果颜色不同，丢弃这两颗并向 b 加 1。使用该规范进行推理：豆子数量能否达到 0？终止时 b=1 需要什么初始状态？下载 TLC 1.8.0 并运行模型检查器找出答案。 ``` 我告诉它下载 TLC 1.8.0，这是当前的预发布版本，因为上一次官方 TLC 发布是在几年前。如你所料，Claude 一次性生成了一个通过模型检查并回答问题的规范。但这是一个非常简单的任务。LLM 已经移除了使用 TLA+ 的第一个障碍：其语法。你仍然需要定义你的系统必须维护哪些性质；Hillel Wayne 在