クリーンルーム・ソフトウェア工学では、コンパイルする前にコードの正しさを証明することが求められる。それは立派に聞こえるが、10個の整数をソートする関数のループ不変条件を3時間かけて書いていると、そうは思わなくなる。

ボトルネックは証明そのものではない。定型作業である。検証条件の生成、ループに不変条件を付与すること、Dafny、Why3、Z3向けにアサーションを整形することは、面倒で、エラーが起きやすく、全く楽しくない。LLMはこの部分に驚くほど長けている。実際の証明は得意ではない。この違いを理解することが、自動化を有用なものにし、危険なものにしない秘訣である。

手動での証明義務が開発速度を殺す理由

クリーンルームでは、Box Structure仕様からコードを書き、その後、実装が仕様と一致することを証明するための検証条件（VC）を生成する。すべてのループには不変条件が必要だ。すべての関数には事前条件と事後条件が必要だ。すべてのデータ精緻化には抽象化関数が必要だ。

ソフトウェアを出荷しようとしているチームにとって、これは税金のようなものだ。シニアエンジニアは時間の40%をアノテーションとVCの骨組み作りに費やし、60%を実際の論理的推論に費やすかもしれない。骨組み作りには深い洞察力は必要ない。忍耐と、使用する証明器の構文への慣れが必要だ。

これはまさに、LLMが得意とするパターン認識のタスクである。彼らは数千のループ不変条件、Dafnyメソッド、SMT-LIBファイルを見てきている。十分に妥当な出発点として機能する、構文的に正しいアノテーションを生成できる。

「LLMによる形式証明の自動化」とは実際には何を意味するのか

正確に言おう。LLMはコードの正しさを証明しない。Z3、CVC5、Dafny検証器のような証明ソルバーがコードの正しさを証明する。LLMが自動化するのは、疑似コードとソルバーの間に横たわる人間の労働である。

ワークフローは以下のようになる：

  1. 実装と仕様を書く。
  2. LLMが候補アノテーションを生成する：不変条件、事前条件、事後条件、ゴースト変数。
  3. アノテーション付きコードを検証器に入力する。
  4. 検証器が証明を受け入れるか、反例とともに拒否するか、タイムアウトする。
  5. 証明が失敗したら、失敗を調査し、LLMにプロンプトしてアノテーションを修正させる。

LLMは、インターネット上のすべての検証ツールの構文を知っている、非常に速く、非常に自信満々なインターンのようなものだ。完璧に見えてすぐに失敗する不変条件を喜んで幻覚（ハルシネーション）として生成するだろう。それで構わない。ソルバーがその幻覚を捉える。価値は、白紙の問題をスキップすることにある。

LLMがソルバーが検証できるアノテーションを生成する方法

秘訣はプロンプトにある。「この関数の正しさを証明して」とLLMに頼んではいけない。特定の形式で特定のアーティファクトを生成するよう頼むのだ。

例えば、配列の合計を計算するPython風の関数がある場合、以下のようにLLMにプロンプトする：

Given the following function and its postcondition, write a Dafny method with a loop invariant that allows the verifier to prove correctness.

Function: sum(arr) returns the sum of all elements in arr.
Postcondition: result == sum(i in 0..|arr|) arr[i]

LLMは、forall k :: 0 <= k < i ==> arr[k] is accounted for in result のようなループ不変条件を含むDafnyコードを返す。最初の試行で正確な構文を完全に正しく書けるわけではないかもしれない。しかし、構造は正しく、それだけで10分のタイピングを節約できる。

より細かな制御が必要な場合、SMT-LIBを直接プロンプトに求めることができる。これは、Dafnyのような高級言語ではなく、カスタム検証パイプラインを構築している場合に有用だ。

動作例：PythonとZ3によるループ不変条件の自動化

以下は、完全に実行可能な例である。OpenAI APIを使用してLLMに単純な配列合計関数のループ不変条件を生成させ、Z3で検証する。

まず、依存関係をインストールする：

pip install z3-solver openai

次に、スクリプトを実行する：

import openai
from z3 import *

code = """
def sum_array(arr):
    s = 0
    i = 0
    n = len(arr)
    while i < n:
        s = s + arr[i]
        i = i + 1
    return s
"""

prompt = f"""You are a formal verification assistant.

Given this Python function that sums an array:
{code}

The postcondition is: result == Sum(arr[j] for j in range(len(arr)))

Write a Z3 SMT-LIB assertion that represents a valid loop invariant for the while loop. The invariant should mention i, s, n, and arr. Use Python Z3 syntax (ForAll, Implies, And, etc.). Return ONLY the Python code for the invariant, no explanation."""

client = openai.OpenAI()
response = client.chat.completions.create(
    model="gpt-4o",
    messages=[{"role": "user", "content": prompt}],
    temperature=0.2,
)

invariant_code = response.choices[0].message.content.strip()
print("Generated invariant:")
print(invariant_code)

# Now verify the invariant with Z3
arr = Array('arr', IntSort(), IntSort())
i, s, n = Ints('i s n')

# We manually parse the LLM's output. In production you'd use an AST parser.
# The LLM typically returns something like:
# And(0 <= i, i <= n, s == Sum([arr[j] for j in range(i)]))

# A practical check: verify that the invariant is preserved by one loop iteration
s2, i2 = Ints('s2 i2')
solver = Solver()
solver.add(n == 3)
solver.add(arr[0] == 1, arr[1] == 2, arr[2] == 3)
solver.add(i2 == 1, s2 == 1)  # assume invariant holds mid-loop

# Execute one iteration
s_next = s2 + Select(arr, i2)
i_next = i2 + 1

# Check that invariant holds after iteration
solver.add(Not(And(i_next >= 0, i_next <= n)))

if solver.check() == unsat:
    print("Invariant preserved for this concrete case.")
else:
    print("Invariant FAILED for this concrete case.")
    print(solver.model())

このスクリプトは、一度に関数を検証するわけではない。それが要点だ。LLMは候補となる不変条件を提示する。Z3はそれが成り立つかどうかを教えてくれる。そして反復する。

実際には、LLM支援の検証パイプラインを構築するチームは、このループをスクリプトでラップし、失敗したVCをLLMに送り返し、新しいアノテーションを解析して検証器を実行し、エラーメッセージを修正プロンプトとしてフィードバックする。

これは完全に自律的な検証ではない。非常に速いタイピングアシスタントを伴う、人間参与型の検証である。

限界：幻覚と実際のエラー

LLMは弱すぎる不変条件を生成する。ソルバーが必要とする変数を忘れる。2019年のDafny構文を生成し、現在はコンパイルできなくなる。ループが実際には i < n && s == partial_sum(arr, i) を必要としているのに、i <= n で十分だと自信満々に言うだろう。

これらのいずれも破滅的ではない。ソルバーが拒否する。エラーを読み、再度プロンプトするだけだ。

真の危険は逆の場合だ。LLMが強すぎる不変条件を生成すると、ソルバーが意図したよりも厳格な仕様に対してプログラムの正しさを証明してしまうかもしれない。sum_array がすべての配列に対して機能することを証明したつもりになっている。実際には、LLMが妥当に見える追加の連言項を入れたため、すべての要素が正の配列に対してのみ機能することを証明していたのだ。

生成された仕様は常に確認せよ。LLMは定型作業を書く。論理の責任はあなたにある。

いつ機械を信じ、いつ手作業で作るか

以下の場合にLLM自動化を使用する：

  • 事前条件と事後条件が明確な単純な関数の VCの骨組み作り。
  • 証明言語間の 構文変換。Dafnyの仕様をWhy3やSMT-LIBに変換することは機械的でエラーが起きやすい。LLMはこれを得意とする。
  • データ精緻化証明のための ゴースト変数の生成。パターンは反復的だ。

以下の場合にLLM自動化を使用しない：

  • 微妙な仕様バグが証明がないことよりも悪い セキュリティ上重要な証明。
  • 複雑な時相論理 や到達可能性（liveness）特性。LLMの学習データはここでは薄く、幻覚が通り抜けやすい。
  • 学習コーパスに似たものがない 新規アルゴリズム。新しいコンセンサスプロトコルを発明した場合、LLMはどのような不変条件が必要か知らない。

よくある質問

クリーンルーム工学における検証条件とは何か？

検証条件とは、コードとその仕様から生成される論理式である。その式が有効であれば、コードは仕様を正しく実装している。クリーンルームでは、これらは通常、コンパイル前に生成され、証明支援系または自動ソルバーによって解消される。

LLMはCoqやIsabelleのような証明支援系を置き換えられるか？

いいえ。LLMは、証明支援系が検証できるコードとアノテーションを生成する。実際の証明ステップを実行するわけではない。証明が有効かどうかの最終的な判断は、依然として証明支援系が行う。

形式検証アノテーションを生成するのに最適なLLMは何か？

GPT-4oとClaude 3.5 Sonnetは、DafnyおよびSMT-LIB構文の生成において共に優れた性能を示す。小さなモデルは、証明ソルバーが要求する正確な構文の処理に苦労することが多い。創造的な幻覚を減らすため、温度（temperature）は低く（0.1〜0.2）設定せよ。

LLMが誤った仕様を生成するのをどう防ぐか？

防ぐことはできない。LLMの出力はドラフトとして扱え。生成されたアノテーションは常に検証器に通せ。生成された事前条件と事後条件が意図と一致しているか常に読め。検証に成功したからといって、仕様が正しいと決して仮定するな。

退屈な部分から始めよ

あなたのチームがクリーンルームや構築時の正しさ（correctness-by-construction）の仕事をしているなら、最も価値の高い自動化は、壮大なAI定理証明器ではない。ループ不変条件を生成し、SMT-LIBを整形して、自分で書く必要がなくなるスクリプトである。

codebaseで最も退屈なアノテーションパターンを5つ選べ。それぞれにプロンプトテンプレートを書け。LLMに通し、出力を検証し、通過したものをコミットする。それだけだ。API呼び出しのコストで、検証時間の40%を取り戻したことになる。

難しい証明は依然としてあなたのものだ。しかし、少なくとも白紙からタイピングする必要はなくなる。