Case study: proving sqrt(2) irrational with LPTP and an LLM

あなたは、2000年以上も人間を困惑させてきたミステリーを解決しようとしている探偵だと想像してください。それは、「√2（ルート2）は『有理数』なのか？」という謎です。数学の世界において、有理数とは完璧な分数、つまりパイのきれいな一切れ（3/4や5/2のようなもの）のような存在です。一方、無理数とは、決して単純な分数には書き表すことのできない、終わりのない面倒な小数です。√2は、一辺の長さが1の正方形の対角線の長さであり、古代の数学者たちは、それが分数にはならない「面倒な」数であることを証明しました。

今、あなたの手元には、この問題を解くための全く異なる2つのツールがあります。1つ目は、LPTPと呼ばれる、超厳格でロボットのような審判です。これは非常に精密で論理的な言語（Prologに基づいたもの）を話し、すべてのステップが数学的に完璧である場合にのみ、証明を承認します。もしあなたがわずかでもミスをすれば、審判はガベル（小槌）を叩きつけ、「ダメだ、無効だ」と宣告します。2つ目のツールは、**大規模言語モデル（LLM）**です。これは、あらゆる書物を読み尽くした超スマートでクリエイティブな学生のようなものです。この学生は、物語や数学の問題の「次のステップ」を推測することには長けていますが、時として「ハルシネーション（幻覚）」を起こし、もっともらしく聞こえるものの実際には間違っている事実を作り上げてしまうことがあります。

大きな問いはここにあります。私たちはこれらを連携させることができるのでしょうか？クリエイティブな学生に証明を書くという重労働をさせ、厳格な審判に、その学生が嘘をついていないかを一文ごとにチェックさせることはできるのでしょうか？この論文は、まさにそのパートナーシップについて、この「√2の無理数性」をテストケースとして用いて探求しています。

---

偉大なる証明チェックの連携

この論文において、著者たちは、現代のAI（具体的にはClaudeと呼ばれるモデル）を使用して、√2が無理数であることを証明する手助けができるかどうかを検証しました。ただし、そこにはひねりがありました。証明は、ロボット審判（LPTP）が理解し、検証できる非常に特定の厳格な形式で書かれなければなりませんでした。彼らは単にAIに「それは正しい」と言わせたいのではなく、AIに実際のステップ・バイ・ステップの論理を書かせ、それを審判が採点するという仕組みを目指したのです。

物語はシンプルなアイデアから始まります。√2が無理数であることを証明するには、通常、その逆を仮定します。つまり、それは2つの整数 $p$ と $q$ からなる分数であり、それらの間に共通の因数を持たない（互いに素である）と仮定するのです。計算を進めていくと、最終的に両方の数が偶数でなければならないという矛盾に突き当たります。これは、それらが互いに素であったというルールを破るものであり、元の仮定が間違っていたことを証明します。

著者たちは、AIにこの証明をLPTPの厳格な言語で書かせようと試みました。最初、AIは「ストーリーは知っているが、指定された形式でエッセイを書けない学生」のようでした。AIはステップを飛ばしたり、論理的な飛躍を行ったりしようとし、それが審判によって受け入れられない原因となりました。

ここで、チームワークが発揮されました。著者たちは以下のフィードバック・ループを構築しました：

1. AIが証明のステップを書こうとする。
2. 審判（LPTP）がそれをチェックする。
3. もし審判が間違いを見つけた場合、論理が崩れた「正確な行」を指摘する。
4. 著者たちがそのエラーをAIに見せる。
5. AIがその特定のミスを修正して、再度挑戦する。

このプロセスは、まるで「熱いか冷たいか（ホット・アンド・コールド）」のゲームのようでした。審判は単に「間違いだ」と言うのではなく、「ステップ4でミスをした」と指摘することで、AIが軌道修正できるようにしたのです。

結果：部分的な勝利

実験は成功しましたが、いくつかの注意点もありました。AIは、パズルのより小さく簡単な部分は、自分自身で多く証明することができました。例えば、「もしある数が偶数ならば、その二乗は偶数である」や「2倍の数は偶数である」といったことです。著者たちはこれらを「補題（lemma）」と呼んでいます（小さな補助的な証明）。AIはこれらを正しく、時には人間が考えていなかった新しい補助的なアイデアさえも提示して正解しました。

しかし、証明の中で最もトリッキーな部分、つまり「なぜ√2が分数になり得ないのか」を示す具体的な論理において、AIは行き詰まってしまいました。AIは自力で正しい経路を見つけることができなかったのです。そのため、人間の著者が介入し、AIに「ヒント」を与えたり、あるいはメインの証明構造自体を自ら書き上げ、AIにはその間の小さな隙間を埋めるよう依頼したりする必要がありました。

最終的に、彼らは√2が無理数であるという完全な形式的証明を作り上げました。この証明は部分的にAIによって書かれ、完全にロボット審判によってチェックされました。審判は合格点を出し、その論理が健全であることを確認しました。

これが意味すること

この論文は、AIが今や自力ですべての数学問題を解けるようになったと主張しているわけではありません。実際、著者たちは、人間の指導と厳格なチェックがなければ、AIは単独では成し遂げられないことを明確に示しています。もし人間の導きと厳格な審判がいなければ、AIはおそらく偽物あるいは壊れた証明を生み出していたでしょう。

むしろ、この論文は新しい働き方を提案しています。それは、**「下書きを書くAI、編集者としての人間、そしてファクトチェッカーとしての形式的ツール」**という役割分担です。AIは速くクリエイティブであり、アイデアを生成し詳細を埋めることができ、一方で形式的ツール（LPTP）は、ハルシネーションやエラーを捕まえる「瞬きもしない目」として機能します。

著者たちはまた、他の自動数学ツール（ATPと呼ばれます）を用いて、より速くその任務を遂行できるかをテストしました。これらのツールは高速で無料でしたが、人間にとって読みにくい証明を生成し、検証済みの数学ライブラリに容易に追加することができませんでした。AIのアプローチは、時間はかかり人間による助けを必要とするものの、読みやすく、将来のために安全に保存できる証明を生み出しました。

要約すると、この論文は、人間の直感と機械の精密さのどちらかを選ぶ必要はないということを示しています。AIに重労働（ドラフト作成）をさせ、厳格なツールに採点をさせることで、人間が舵を取り、厳格な審判が地図をチェックするという体制の下で、AIが複雑な数学的真理の証明を支援できるシステムを構築できるのです。√2は依然として無理数ですが、今や私たちはそれを証明するための、新たな協調的な方法を手に入れたのです。