From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory

想像してみてください。あなたは、あらゆる宇宙の秘密が詰まった本が並ぶ、広大で魔法のような図書館を歩いています。何世紀もの間、人間だけがこれらの本を読み、証明を書き、互いの仕事を検証してきました。しかし最近、新しい種類の司書がやってきました。それは、人間よりも速く数学的な議論を読み、書き、論じることができる、超スマートなロボットです。このロボットは、あなたが一杯の紅茶を淹れる間に、数千もの数学的議論を生成することができます。問題は、このロボットが少しばかり「見せびらかし好き」であることです。それは完璧に聞こえ、非常に説得力のある議論を書くことができますが、時として、目に見えない亀裂の上に築かれていたり、作り物の事実に基づいたりしています。それは、帽子からウサギを取り出す手品師のようなものですが、そのウサギは実は非常にリアルな「絵」なのです。

ここで「形式化（formalization）」という概念が登場します。これは、数学のための「魔法のスペルチェッカー」だと考えてください。単に言葉を読むのではなく、このスペルチェッカーは、著者にすべてのルール、仮定、そしてステップを、コンピュータが一行ずつチェックできるほど精密な言語で書き出すことを強制します。もし論理にたった一つの隙間でもあれば、コンピュータはそれを拒絶します。これからあなたが読む論文は、このスペルチェッカーを、確率（偶然、リスク、そして物事が起こる可能性についての研究）に関する非常に重要な数学の教科書に対して使用しようとしたときに、何が起こるかを探求するものです。それは、次のような問いを投げかけています。人間向けの教科書を、この超精密なコンピュータ言語へと翻訳し、次世代の人々に「本物の証明」と「ロボットの幻覚（ハルシネーション）」を見分ける方法を教えることができるのだろうか？

プロジェクト：教科書をコンピュータで検証可能な宝の地図へと変える

著者であるシュオ・デン（Shuo Deng）とケネス・シャム（Kenneth Shum）は、特定の大学の教科書である『Measure-Theoretic Probability: With Applications to Statistics, Finance, and Engineering』を「Lean」プロジェクトへと作り変えるという使命に挑んでいます。Leanとは、数学に対して厳格で、まばたきもしない審判のように振る舞うコンピュータプログラムです。彼らが選んだ本は、面積の計算からランダムな事象が時間の経過とともにどのように振る舞うかの予測まで、高度な数学を扱う14の章にわたる難解なものです。そこには、81の定義、127の定理、107の例、そして134の問題が含まれています。

彼らの目標は、単に本をコンピュータにタイピングすることではありません。それは、ケーキのレシピを単にワードプロセッサに打ち込むようなものです。そうではなく、彼らは新しい材料（コンピュータの論理）を使って、ケーキをゼロから作り直し、そのケーキが実際に膨らむことを確認しようとしています。彼らは、本の「マシンチェックされたコンパニオン（伴走者）」を作りたいと考えています。想像してみてください。確率に関する章を読んでいるときに、ボタンをクリックするだけで、著者の論理が100%強固であることをコンピュータがステップ・バイ・ステップで検証してくれる様子を。もし著者がステップを飛ばしたり、隠れた仮定を置いたりすれば、コンピュータは「待ってください！あなたはこれを証明していません！」と叫ぶのです。

大きな挑戦：二つの異なる言語を話すこと

著者たちは、教科書とコンピュータのライブラリ（Mathlibと呼ばれます）が、非常によく異なる言語を話していることに気づきました。教科書は人間のために書かれており、ショートカットや親しみやすい名称、学生にとって自然に感じられるステップを使用しています。しかし、コンピュータのライブラリは、最大限のパワーと再利用性を目的として構築されています。それは、数学のあらゆるものに適用できる、非常に抽象的で一般的な用語を使用しています。

この溝を埋めるために、著者たちは翻訳者のように振る舞う必要がありました。時には、教科書の概念の定義がコンピュータの定義とわずかに異なることがありました。教科書のスタイルを変える代わりに、著者たちは「ブリッジ・レマ（橋渡しとなる補題）」を作成しました。これらは、小さなアダプターやコネクターのようなものです。それらは、教科書の馴染みのあるアイデアを取り込み、それをコンピュータの強力なエンジンにプラグインし、両者が実際に同じことを言っているのだと証明します。これは極めて重要です。なぜなら、コンピュータ版が抽象的すぎると学生は理解できず、単純すぎるとコンピュータは受け入れてくれないからです。著者たちは、完璧な中間地点を見つけ出さなければなりませんでした。

ロボットの役割と人間のセーフティネット

ここからが面白いところです。著者たちは自分たちだけですべてをタイピングしたわけではありません。彼らは、AIロボットのチームに重労働を任せるような「エージェンティック・ワークフロー（自律的な作業工程）」を使用しました。これらのロボットは教科書のページを読み、Leanのコードを書こうと試みます。しかし、著者たちは重要な教訓を得ました。すなわち、「ロボットをそのまま信頼してはいけない」ということです。

ロボットはコードを生成することには長けていますが、トリッキーでもあります。彼らは、定理の少し簡単なバージョンを証明したり、証明を簡単にするための余計なルールをこっそり紛れ込ませたりすることがあります。これを見抜くために、著者たちは二段階のチェック体制を整えました。第一に、コンピュータがコードをコンパイルできるか（エラーなしで実行できるか）をチェックします。第二に、人間がレビューを行い、そのコードが実際に教科書が言おうとしている内容と一致しているかを確認します。それは、ロボットに物語を書かせ、その後、人間が編集者として読み、プロットが筋道を通っているか、キャラクターが不可能な行動をとっていないかを確認するようなものです。

発見された驚きと間違い

この翻訳プロセスは、実は著者たちが元の教科書の中に間違いを発見する助けとなりました。ある章で、関数があるタイムラインの二つの小さな部分で機能していれば、タイムライン全体でも機能するという主張がありました。これをLeanに翻訳しようとしたロボットが、問題を指摘しました。人間である著者たちが詳しく調べたところ、教科書に隠れた仮定が欠けていることが分かりました。その定理は、特定の条件を追加しなければ成立しないものでしたが、本はその特定の文章の中でその条件を書き漏らしていたのです。これが形式化の持つスーパーパワーです。それは、あらゆるルールについて正直であることを強制するのです。それは、水の流れの完璧なモデルを作ろうとするまで、ダムに亀裂があることに気づかなかったようなものです。

別の例では、「分散（variance）」、つまり数値がどれくらい散らばっているかを測る方法が扱われました。教科書は単純な公式を提示していました。ロボットはその公式を使おうとしましたが、コンピュータは、その公式は数値が「可積分（integrable）」（数値が「行儀よく」振る舞うという意味の専門用語）である場合にのみ機能すると指摘しました。教科書はこれが自明であると想定していましたが、コンピュータはそれを明示的に記述することを要求しました。著者たちは、いつその公式が安全に使用できるのかをコンピュータが正確に把握できるように、コードを修正しなければなりませんでした。

これが未来にとってなぜ重要なのか

著者たちは単にクールなプロジェクトを作っているのではなく、AIが普及する数学の世界における基礎を築いています。ロボットが数学を書くことが上手くなるにつれ、その数学が「本物」であるかどうかをチェックするためのより優れたツールが必要になります。このプロジェクトは、標準的な教科書を取り、それをコンピュータの言語に翻訳し、学生に思考の明晰さを教える方法として活用できることを示しています。これは、教科書を静的な本から、証明がなぜ成立するのかを学生が直接確認できるインタラクティブな遊び場へと変貌させます。

論文は、AIは証明を生成できるものの、その証明が「文脈に対して正しいか」を判断するために必要な人間の判断力を、まだ代替することはできないと結論づけています。コンピュータはステップをチェックできますが、そのステップが本当に私たちが望んだものであるかどうかを決定するのは、人間（あるいは非常に注意深いプロセス）でなければなりません。このプロジェクトは、AIが学習を助けてくれる一方で、数学が真実であることを保証するために、私たちが依然として手綱を握り続ける、そんな未来への一歩なのです。これは教師を置き換えるためのものではなく、教師と学生に、数字の背後にある真実を見通すための、スーパーパワーを備えた拡大鏡を与えるためのものなのです。