Case study: solving P-99 with LPTP and an LLM

コンピュータが単に硬直したロボットのような指示に従うだけでなく、人間が問題を説明する際の、あの曖昧で不完全な方法を実際に理解できる世界を想像してみてください。これは人工知能（AI）、特に**大規模言語モデル（LLM）**と呼ばれる分野の最前線です。LLMを、インターネット上のほぼすべての文章を読み込んだ、非常に賢く博識な学生だと考えてみてください。物語を書くように頼めば書けますし、コードを書くように頼めば書けます。しかし、一つ問題があります。この学生は「ハルシネーション（幻覚）」を起こしやすいということです。つまり、自信満々に事実を捏造したり、一見完璧に見えるコードを書いても、いざ実行しようとすると密かに壊れてしまったりすることがあるのです。

これを解決するために、科学者たちは**形式検証（Formal Verification）を使用します。これは、学生の宿題の全ステップを厳格にチェックし、論理的に間違いが起こり得ないことを保証する、非常に厳しい数学教師のようなものです。コンピュータサイエンスの世界には、「99 Prolog Problems（P-99）」**と呼ばれる有名な課題セットがあります。これらは、論理プログラミングにおける「ジムでの筋力トレーニング」のようなものです。論理プログラミングとは、「どのように（how）」ステップバイステップで行うかではなく、「何を（what）」したいのかを記述するスタイルのコーディングです。研究者たちが投げかけている大きな問いは、「AIという学生に、単純な英語の記述に基づいてコードを書かせ、その直後に数学の教師にそれが本当に正しいかどうかをチェックさせることができるか？」というものです。この論文は、まさにこの実験について探求しています。AIの創造的な自由と、形式論理の鉄壁の安全性とを融合させているのです。

---

実験：厳格な教師とのコーディング・デュオ

この研究において、研究チームは**「バイブ・コーディング（vibe-coding）」と「ヴェリコーディング（vericoding）」**を組み合わせた新しい手法をテストすることに決めました。まず「バイブ・コーディング」を、あなたがナプキンに描いたラフなスケッチをもとに、クリエイティブな友人にツリーハウスを作ってもらう様子だと想像してください。「スライドと秘密のドアがあるツリーハウスが欲しい」と言うだけで、彼らは作り始めます。それは速くて楽しいですが、出来上がったものはグラグラしているかもしれません。一方、「ヴェリコーディング」はその逆です。釘を一本打つ前に、設計図、ストレス・テスト、そして安全検査を要求する建築家を雇うようなものです。

研究者たちは、これら2つのアプローチを組み合わせることができるかどうかを知りたいと考えました。彼らは、クリエイティブなビルダーとして機能させるために、AIモデルであるClaude（具体的にはOpus 4.6バージョン）を使用しました。彼らは、有名なP-99リストの最初の33問を与えました。これらは単純で非公式な英語で書かれています。例えば、一つの問題は単に「リストの最後の要素を見つけよ」と言っています。

AIの役割は以下の通りでした：

1. 問題を解決するためのPrologコードを書くこと。
2. コードが例題に対して正しく動作するかを確認するためのテストファイルを書くこと。
3. コードが安全で、正しく、常に実行が終了することを数学的に保証する形式的証明を書くこと。

証明をチェックするために、彼らはLPTP（Logic Program Theorem Prover）と呼ばれるツールを使用しました。LPTPを、単に「正しそうに見える」という回答を拒絶する、厳格な数学教師だと考えてください。それは、あらゆる主張に対して、ステップ・バイ・ステップの論理的導出を要求します。

結果：魔法と数学の混合

実験は成功しましたが、それは魔法の杖ではありませんでした。チームはこの手法を用いて、**88問中33問（約37.5%）**を解くことに成功しました。舞台裏では以下のようなことが起きていました。

• クリエイティブな部分（バイブ・コーディング）： AIは初期のコーディングにおいて驚くほど優秀でした。AIは、1つの問題につきわずか数分で、58個の論理手続き（実際のコード）と508個のテストケースを作成しました。AIは英語の指示を理解し、正しく動作するコードを生成しました。
• 厳格な部分（ヴェリコーディング）： ここからが本当の仕事の始まりでした。AIは、自分のコードが正しいことを証明しなければなりませんでした。AIは257個の補題（lemma）（小さな数学的事実）を生成し、驚くべきことに11,800行の証明を書き上げました。
• 人間の手による調整： 研究者たちは、ただAIを自由に走らせたわけではありません。彼らはすべてのファイルを手動でチェックしました。テストを実行し、論理的な言明を読み、LPTPで証明を再実行しました。もしAIが行き詰まったり、意味の通じない証明を書いたりした場合、人間が介入してヒントを与えました。例えば、「リストの最後の項目を見つける」という問題について、人間はAIに対し、「ねえ、これは append 関数とどうつながっているの？」と問いかけ、正しい証明を構成できるように手助けをしました。

大きな発見

この論文は、この新しい手法に関するいくつかの重要な事実を明らかにしています。

1. AIは「バイブ・コーディング」が得意になりつつある： AIは、曖昧な英語の記述を非常に素早く、動作するPrologコードへと変換することができました。AIは、現実世界のPrologコードでよく使われる「不純な（impure）」トリックさえも避け、数学の教師（LPTP）が理解できる厳格な論理スタイルを遵守しました。
2. AIには「ヴェリコーディング」のための後押しが必要である： AIはコードを簡単に生成できましたが、それが「なぜ」正しいのかを証明することはより困難でした。複雑な関数的特性（コードが意図した通りに動作することを証明するなど）については、AIは時として、人間がまず論理を平易な英語で説明することを必要としました。一度人間がヒントを与えると、AIはそれを形式化し、証明することができました。
3. まだ「解決済み」の問題ではない： チームは99問すべてを解いたわけではありません。簡単な「最後の要素」問題のように15分で終わるものもあれば、「素因数分解」のように数時間かかるものもありました。研究者たちは、最も難しい問題については、AIが人間の指導なしに自力で正しい証明戦略を編み出すことには依然として苦労していると指摘しています。

未来への展望：「MCP」とのつながり

この論文はまた、彼らが構築しているModel Context Protocol (MCP) という新しいツールについても説明しています。現在、AIと数学の教師（LPTP）は、ファイルやテキストドキュメントを通じてやり取りしており、これは少し手紙をやり取りしているような状態です。新しいMCPツールは、彼らに直通電話を与えるようなものです。これにより、AIはリアルタイムで数学の教師に助けを求め、自分の仕事を即座にチェックし、人間が介入するのを待つことなくエラーを修正できるようになります。彼らはこれを他のAIモデル（Geminiなど）でテストし、一部のモデルは証明の「アイデア」を生成することはできても、厳格なチェックを通過する「有効な」証明を生成できたのはClaudeだけであったことを発見しました。

まとめ

この論文は、私たちが、AIが複雑で論理的なコードを書くためのクリエイティブなパートナーとして機能できる時代に入りつつあることを示しています。しかし、AIは最も困難な部分を乗り切るために、依然として人間の「パイロット」を必要としています。AIはコードを書き、数学的証明のドラフトを作成することもできますが、時として細部の詳細の中で迷ってしまうことがあります。AIのスピードと創造性に、LPTPのような形式的証明チェッカーを組み合わせることで、研究者たちはAIのミスが実際のバグになる前にキャッチするシステムを作り上げました。それはまだ、完全に自動化された「何でも直す」機械ではありませんが、ソフトウェアの信頼性をこれまで以上に速く、より安全に構築するための強力な新しいツールなのです。