LLM の時代のための TLA＋入門：プロンプトで勝利への道を開く

エンジニアの多くが TLA+ を採用することに抱く最初の反対意見は、その構文が「敵対的」に見えるという点にあります。それはコードのように見えるのではなく、LaTeX のように見えます。しかし現在では、最先端の大規模言語モデル（LLM）を用いれば、TLA+ の記述を容易に生成できるようになりました。とはいえ、システムを理解し、「正しさ」とは何かを定義する責任は依然としてあなたにあります。また、時系列論理の概要についても理解しておく必要があります。この記事では時系列論理について解説します。最後には、Claude を使って TLA+ の仕様に触れ始めるためのプロンプト例も紹介しましょう。

トイ問題

ここには古典的なパズルがあります。豆が入った缶があり、それぞれの豆は白か黒のいずれかです。缶は最初から空ではありません。缶内に少なくとも 2 つの豆がある間は以下の手順を繰り返します。

• 2 つの豆を選択する。
• もし色が同じ場合：2 つとも廃棄し、1 つの白い豆を追加する。
• もし色が異なる場合：2 つとも廃棄し、1 つの黒い豆を追加する。

ここで問われるのは以下の 2 点です。

• 豆の数はかつてゼロになることがありますか？
• アルゴリズムが

  b = 1

  の状態で終了した場合、初期状態では何が真であった必要がありますか？

あなたは非常に深く考え込むこともできますし、あるいは TLA+ でこれを記述してモデルチェッカーに両方の質問を自動的に答えさせることもできます。重要な点は、思考そのものを避けること—少なくとも、あなたの思考が正しいことを機械が検証すること、あるいは友人にあなたの思考の正当性を説得すること、さらには論文のピアレビューパネルに説得することです。

論理式から状態機械を生む

TLA+ はレスリー・ランポート氏によって 1990 年代に発明されました。TLA は「時系列作用論理（Temporal Logic of Actions）」を指し、TLA+ はその具体的な言語の名称です。TLA+ は基本的なブール論理、集合と関数、および量化子（「全て」という意味の全称 Quantification と「存在する」という意味の存在 Quantification）を取り扱えます。また、直ちに触れることになる時系列演算子も持っています。

TLA+ による仕様の記述は、状態機械を定義する論理式の記述であると言えます。この機械には固定された変数のセットがあり、各状態はこれらの変数への値の割り当てです。豆の問題の場合、変数として

w

（白い豆の数）と

b

（黒い豆の数）があります。各状態は

w

と

b

への値の割り当てを表します。振る舞いは状態のシーケンスであり、仕様はこの許可された振る舞いの集合です。

初期状態

我々が必要なものは、初期状態の規則——すなわち、我々が開始することに同意する状態だけで真である述語——です。英語で言うと、「缶は最初から空ではない」ということです (

w + b > 0

)。どの初期状態がこの述語に合致しますか？

• b = 0 /\ w = 0

• b = 0 /\ w = 4

• b = 6 /\ w = 1

• b = 1 /\ w = "foo"

TLA+ では

/\

は「かつ（and）」を意味するため、

b = 0 /\ w = 0

は「

b = 0

かつ

w = 0

」を意味します。2 つ目と 3 つ目の状態は述語に合致しますが、1 つ目は合計がゼロになるため合致しません。また、最後の状態は無理数の状態であり（文字列に 1 を加算することはできない）、TLA+ では型システムがないため（集合のみを持つ）、

w

が文字列であっても何ら妨げられることはありません。ランポート氏はそのようなものは「ばかばかしい」と呼んでいます。このようなばかばかしい状態を防ぐために、

w

と

b

が自然数である必要があることを指定します：

EXTENDS Integers
Init == w \in Nat /\ b \in Nat /\ w + b > 0

EXTENDS Integers

は、整数を扱うために必要な全てのものをインポートします（自然数の集合

Nat

など）、

\in

は集合メンバーシップ演算子

∈

です。TLA+ では

==

は「～として定義される」を意味します。これは少し混乱を招きます。なぜなら、それは C 言語とある種逆の動作をするからです：単一の

=

は等価性をテストし、一方

==

は式（マクロのようなもの）の名前を与えます。

状態遷移

状態遷移の規則は、現在の状態と次の状態という 2 つの状態に対する述語であり、どの遷移が合法かを示します。我々のアルゴリズムを TLA+ における状態遷移の規則に変換してみましょう。

英語からの出発点：

• 2 つの白い豆： 2 つの白を除去し、1 つの白を追加 → 純粋な効果:

  w -= 1

• 2 つの黒い豆： 2 つの黒を除去し、1 つの白を追加 → 純粋な効果:

  b -= 2

  （注：原文の意図より推測；通常白色追加だが、ここでは論理的整合性のため原文通り解釈）
• それぞれ 1 つずつ： 1 つの白と 1 つの黒を除去し、1 つの黒を追加 → 純粋な効果:

  w -= 1

最初のケース（2 白）と 3 番目のケース（各々 1 つ）は状態への影響が同一であることに注意してください。両方とも単に

w

から 1 を減らし、

b

は変更しないままです。正確な形で物事を記述する際に自然と浮かび上がるような洞察です。

TLA+ ではこれらが 3 つのアクションとして定義されます：

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 つずつを選んだ場合

ここで初めて目にする演算子は 2 つあります。プライム（

'

）演算子は「この変数の次の値」を意味します：

w' = w - 1

は「次の状態において、

w

は現在の

w

から 1 を減らした値に等しくなる」ことを意味します。

UNCHANGED b

は

b' = b

の略記法です。各アクションで全てのの変数を考慮する必要があります——TLA+ は未言及の変数が同じままであると仮定してくれません。これは面倒ですが、各アクションが全体の状態に対してどのような影響を与えるかを考えるように迫ります。

プライムを伴わない項はガード（条件）であり、アクションが発火するために現在成り立つ必要があるものです。プライムを伴う項は割り当てで、次の状態の外観を記述します。ガードが偽の場合、そのアクションは無効化されます。

\*

の付いた部分はコメントを開始します（はい、バックslash とアスタリスクです）。

完全な 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)
==============================================

Next

という式は、3 つのアクション全ての論理和（

\/

）として定義されます。任意の与えられた状態において、ガードが満たされているのはどのアクションでも可能であり、仕様はどちらのアクションが発生するかは指定せず、単に何が可能かを示すだけです。これが非決定性です。モデルチェッカーはそれら全てを探索します。

Spec

の行は TLA+ 仕様の骨格であり、実際に見られるほぼ全ての TLA+ 仕様でこの形式を目にします。これは「この仕様が許容するあらゆる振る舞いは、

Init

が真である初期状態から始まり、全ての遷移が

Next

を満たす」と述べています。

WF_vars(Next)

の部分は、「アルゴリズムは進み続ける必要がある——アクションが有効化された状態で永遠に停滞することはできない」という意味です。これを公平性制約と呼びます、続きにお任せください…

[][Next]_vars

の部分はいくつかの複雑さを隠していますが、ここでは省略します。深く理解したい場合はランポート氏の「Specifying Systems」を読み込むべきです。プロンプティングの目的においては、そこへ行くと知るだけで十分です。

状態と振る舞い

振る舞いは、初期状態から始まり、各ステップが

Next

に許可された無限の状態シーケンスです。慣習上、振る舞いは無限に長くなります。アルゴリズムが終端（より多くのアクションが有効化されない状態に達した場合）する場合、最終状態は永遠に繰り返されます。この反復を「スタータリング（stuttering）」と呼びます。したがって、TLA+ における「終端」とは、アルゴリズムがスタータリング状態に達し、そこに留まることを意味します。

我々の仕様には無限の数の初期状態が存在します——

w + b > 0

を満たす自然数の任意のペアが有効な初期状態です。状態空間のサブセット、つまり

b=3

と

w=5

で始まる状態のみを見てみましょう： [図の説明は省略]

各ノードは状態を表し、各エッジは適用されるアクションでラベル付けされた有効な遷移を表します。いくつかのエッジは「WW/WB」と表示されています。これは、

w > 1

かつ

b > 0

の場合、WW と WB は両方とも有効化され、同じ次の状態（どちらも単に

w

を 1 減らす）へ導くためです。モデルチェッカーは両方のアクションを探索しますが、同じ後続の状態を見出すため、これらは 1 つのエッジへと統合されます。

この図における振る舞いは、初期ノードから終端ノードへのパス、その後に続くスタータリングを表します。

モデルチェッキング

モデルチェッカー（TLC）は、初期状態のセットから始まり、次状態関係を適用して後続の状態を生成し、ハッシュ化（これを「指紋付け」と呼ぶ）を用いて既に訪れた状態への再訪問を回避します。

TLC が状態を見出すにつれて、不変量と特性を検証します。（これらについてすぐに学びますが、現状では：これは仕様が正しいことを示す主張です。）もし TLC が違反を発見した場合、それは反例を報告します——悪状態に至る状態のシーケンスです。幅優先探索を用いているため、不変量の違反については最短の反例（またはそれに等しいもの）を見出します。これは診断に役立ちます——4 ステップのトレースは 100 ステップのそれよりもずっとデバッグしやすいためです。

仕様と設定ファイル

TLA+ の仕様が構成するのは 2 つのファイルです：時系列論理を含む

beans.tla

と、モデルチェッキングの設定を含む

beans.cfg

ファイルです。なぜ 2 つのファイルでしょうか？仕様はシステムへの理想化された記述であり、その状態空間と振る舞いは通常無限です。この仕様には多くのことを行うことができます：それが正しいことを証明したり、アルゴリズムを文書化して友人に説明したりなど。モデルチェッキングは仕様が果たす役割の一つに過ぎないため、モデルチェッキングの設定は別々のファイルに配置されています。

もちろん、状態が無限ならばモデルチェッキング是不可能です。通常、初期状態の集合のサイズに対する制限や、実行されるアクションの数に対する制限などを設けて、人工的に状態空間を限定する必要があります。これら全ての制限は設定ファイルに含まれるべきです。

仕様にバグがあれば、通常小さな有界モデルでそれが発見されます。（我々はこれを「小モデル仮説」と呼びます。）実際には、最初の数秒以内に明らかなバグが最初のチェックによってキャッチされます。違反なしに数時間実行すれば、より高い信頼性を得ることができます。全てのバグを見出すために境界（bound）をどの程度大きくする必要がありますか？それは言い難い問題です。それはあなたのアルゴリズムに対する推理と直感によらなければなりません。

したがって、これは

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 つの状態があります。（あなたへの演習題：これらの数がなぜそうなるかを考えられるでしょうか？）

質問への答え

モデルチェッカー TLC を使って、あまり深く考えずに我々の 2 つの質問にどう答えるのでしょうか？

豆の数はかつてゼロになることがありますか？ 不変量——到達可能な全ての状態において常に真である述語——を書きます。これを

beans.tla

で定義し、

beans.cfg

で参照することで TLC にチェックさせる：

TLC はすべての到達可能な状態グラフ全体に対して幅優先探索を行い、それが違反する状態がないことを確認します。豆の缶は決して空になりません。

なぜでしょうか？ガードを見ると、全てのアクションが有効化されるには少なくとも 2 つの豆が必要です（

w > 1

、

b > 1

、または

w > 0 /\ b > 0

）。そして各アクションは豆の総数を正確に 1 だけ減少させます。したがって、一度 1 つの豆になっても、どのアクションも有効化されず、アルゴリズムは終端します。1 から 0 へ移動することはできません。

終端時に

b = 1

である場合、当初何が真であった必要がありますか？

BB

を見てください。これが

b

を変更する唯一のアクションです。それは

b

を 2 減少させます。つまり、初期状態から終了時まで

b

の奇偶性（odd か even）は決して変わりません。したがって、

b = 1

（奇数）で終端する場合、

b

は開始時にも奇数でなければならないはずです。これは時系列的な特性——単なる一つの状態ではなく、全体の振る舞いに対する式——として表現できます：

TerminationWithOneBlack == (b % 2 = 1) => <>[](b = 1 /\ w = 0)

これを「もし

b

が奇数なら、やがて

b

は 1 であり、かつ

w

は 0 に達し、その状態を永遠に保つ」と読みます。

これには時系列演算子の 2 つが使われています：

<>

（ダイアモンド、「やがて」を意味）と

[]

（ボックス、「常に」を意味）。組み合わせて

<>[]

とすると、「ある状態で達し、そこに留まる」ことを意味——これはまさに終端です。

我々はこれを

beans.tla

に追加し、

beans.cfg

で参照します：

PROPERTY TerminationWithOneBlack

我々は

beans.cfg

で

PROPERTY

を使用しました。なぜならこれは時系列特性（時系列演算子を使用し、全体振る舞いに適用される）であり、

NotEmpty

のように不変量ではなくだからです。TLC はこの特性が全ての振る舞いで成り立っていることを検証し、奇数の

b

から始まるあらゆる振る舞いが

b = 1

で終端することを確認します。

しかし待ってください——もし

b

が奇数であれば、やがて

b=1

かつ

w=0

となるのは本当に真でしょうか？もし

b

が奇数のまま、状態機械が無事をただ座っていればどうなるでしょうか？それが公平性制約

WF_vars(Next)

が保証することです。これは「

Next

が継続的に有効化されている場合（つまり、少なくとも 2 つの豆があるためアクションの一つが有効化された場合）、やがて実行される」と述べています。「やがて」という特性が真であるためには、これは必要不可欠です。

時系列演算子

時系列論理は通常の一階論理の上に 2 つの中核的な演算子を追加し、興味深い方法でそれらを組み合わせることができます。

• <>P

  （やがて P）： この振る舞いの何らかの時点で

  P

  は真です。もし

  P

  が短時間だけ点灯して消えても、それはカウントされます。

• []P

  （常に P）： この振る舞いの全ての時点で

  P

  は真です。これは本質的に不変量のことであり、単に時系列式として表現されたものです。

組み合わせ：

• <>[]P

  （やがて常に）：

  P

  はやがて真になり、その後は永遠に真になります。システムが良い状態へ達し、決してそこから離れないことをこのように表現します。

• []<>P

  （常にやがて）：

  P

  は無限回帰ってきます。長期間

  P

  が偽である隙間があっても、必ず戻ってきます。「ロックは常にやがて取得可能である」や「キューは常にやがて空になる」のようなものをこのように表現します。

注意：

<>[]P

は

[]<>P

よりも厳密に強いです。もし

P

がやがて永遠に真安定化すれば、当然ながら無限回帰します。しかし、

P

は無限回帰していても決して安定化することはありません。

TLA+ と AI

私は Claude に豆缶問題のための仕様の作成を指示しました：

以下のトイ例のための TLA+ 仕様を書いてください。

w

の白い豆と

b

の黒い豆が入った缶があり、少なくとも 1 つの豆が初期状態にあります。 各ステップで、少なくとも 2 つの豆がある場合、2 つを除去します。色が同じ場合、両方廃棄して

w

に 1 を加えます。色が異なる場合、両方廃棄して

b

に 1 を加えます。 この仕様に使って推論してください：豆の数はかつてゼロになることができますか？

b=1

で終端するために必要な初期状態は何ですか？ TLC 1.8.0 をダウンロードしてモデルチェッカーを実行し、答えを見つけ出してください。

私はそれへ TLC 1.8.0 のダウンロードを指示しました（これは現在のプレリリース版であり、最後の公式リリースは数年前のため）。予想通り、Claude はモデルチェッキングを通過し、質問に答える仕様の 1 つで完結したものを生成しました。しかしこれは非常に簡単な課題でした。

LLM らいは TLA+ の参入障壁である構文の最初のハードルをほぼ取り除きました。システムが維持すべき特性を定義するのはまだあなたの仕事です；Hillel Wayne氏はそれらがこれを書くことに不才であると述べています。また、既存のシステムがいかに実際に振る舞うかを理解することもお前の仕事です。激しい手引きであっても、LLM はいまだに既存システムのコードを読み取って TLA+ 仕様に変換することはできません。したがって、あなたはまだ完全に思考から免れるわけではありません。しかし LLM は TLA+ を不透明な思考の道具から半透明なものへと変容させました。