基本的なアイデア：数学ロボットのための「翻訳機」

想像してみてください。あなたの手元には、非常に優秀で超高速な数学ロボットがいます。このロボットは、形式論理（Agda、Lean、Rocqなど）と呼ばれる、非常に厳格で精密な言語を話します。ロボットは100%の正確さで定理を証明できますが、その出力はコードの壁のように見えます：forall (a : Int), odd a -> even (a + 1)。

人間にとって、これは解読不能です。まるで、すべての単語が秘密の暗号になっている本を読もうとしているようなものです。

インフォーマライゼーション（非形式化）とは、その厳格なロボットのコードを、人間が実際に読み、理解できる自然言語（英語、フランス語、ドイツ語など）へと翻訳するプロセスです。

この論文は、AIを使って人間の本から数学を「学習」させる方法については習熟してきた一方で、ロボットが自分たちの成果を、人間が書いたかのように自然な形で人間に「説明」する方法を教えることについては、まだ十分な成果が得られていないと主張しています。この論文は、この問題を解決するために、Informathと呼ばれるシステムを紹介しています。

3つの目標：「流暢・生産的・多言語」のトリオ

著者は、優れた翻訳システムには3つの要素が必要であると述べており、これをこのプロジェクトの「聖なる三位一体」と呼んでいます。

1. 流暢であること（自然に聞こえる）：

   • 問題点： 古い翻訳機は、「整数の集合は整数の集合である」と言うような、質の悪いロボットのようでした。硬くて機械的だったのです。
   • 目標： 新しいシステムは、数学の教科書のように聞こえる必要があります。例えば、「$x$ は...であると仮定せよ」と言うべきか、「$x$ を...とする」と言うべきかを知っている必要があります。また、文章をスムーズに結合する方法（例：「$x$ は偶数であり、$y$ も偶数である」ではなく「$x$ と $y$ は共に偶数である」）も知っている必要があります。
   • 比喩： 「左に曲がってください。その後、500メートル直進してください。次に右に曲がってください」と言うGPSと、「左へ行って、ブロックを一つ進み、それから右折してください」と教える人間との違いを考えてみてください。どちらも目的地には着きますが、一方ははるかに分かりやすいものです。

2. 生産的であること（構築が容易）：

   • 問題点： これらの翻訳機を構築することは、かつては辞書の全単語を手作業で彫り刻むようなものでした。膨大な時間がかかり、言語学者とコンピュータ科学者が協力する必要がありました。
   • 目標： 数学者が自分のコードに少しメモを加えるだけで、システムが残りの部分を自動的に判断できるようにすることです。
   • 比喩： 家を一からレンガを積み上げて作るのではなく、「レゴキット」（Resource Grammar Libraryと呼ばれます）を使うようなものです。パーツをパチンとはめるだけで、複雑なエンジニアリング（文法規則など）はシステムが処理してくれます。

3. 多言語であること（多くの言語を話せる）：

   • 問題点： 通常、英語用の翻訳機を作りたい場合は、それ専用のものを構築します。フランス語が必要なら、全く別のものを構築しなければなりません。
   • 目標： どんな言語も話せる一つの「脳」を構築することです。
   • 比喩： ユニバーサルアダプターのプラグを想像してください。真ん中に数学のコードを差し込み、プラグの「ヘッド」を交換するだけで、英語、フランス語、ドイツ語、あるいはスウェーデン語へと出力できます。国ごとに機械を作り直す必要はありません。

仕組み： 「ハブ・アンド・スポーク」システム

論文では、これらの目標を達成するための巧妙なアーキテクチャについて説明しています。忙しい空港のハブ（中心拠点）を想像してください。

1. ハブ（Dedukti）：

   • これが中央の空港です。あらゆる異なる「航空会社」（Agda、Lean、Rocq）が、それぞれの飛行機（数学の証明）をここに飛ばします。
   • Deduktiは、シンプルで普遍的な言語であり、共通の基盤として機能します。各航空会社固有の癖を取り除き、すべてを標準的なフォーマットに変換します。

2. 翻訳（Grammatical Framework - GF）：

   • 数学がハブに到達したら、それを人間の言葉に変える必要があります。ここでGFが登場します。
   • GFは、熟練したシェフのキッチンのようなものです。数学という材料を、あらゆる言語の美味しい文章へと調理するための「レシピ本」（文法）を持っています。
   • 主語と動詞の一致、複数形による「is」から「are」への変化、フランス語やドイツ語における性別への対応といった、トリッキーな部分を処理します。

3. メニュー（Symbol Tables）：

   • これが秘伝のソースです。数学者はレシピ本全体を書き直す必要はありません。代わりに、「メニューカード」（シンボルテーブル）を埋めるだけで済みます。
     • 「コードの plus を見たら、『和（sum）』と言え」
     • 「odd を見たら、『奇数（odd）』と言え」
   • これにより、複雑な文法の根底部分を壊すことなく、システムを簡単にカスタマイズできるようになります。

「人間らしく聞こえさせる」ための魔法

論文では、数学を自然に聞こえさせることは見た目以上に難しいことが強調されています。Informathが使っているテクニックは以下の通りです。

• 集約（「And」のテクニック）：

  • ロボット： 「$x$ は偶数である。$x$ は3で割り切れる。」
  • 人間： 「$x$ は偶数であり、かつ3で割り切れる。」
  • システムは、より流れが良くなるようにこれらの文章を結合する方法を知っています。

• In Situ Quantification（「隠された」変数）：

  • ロボット： 「すべての数 $n$ について、$n$ は偶数または奇数である。」
  • 人間： 「すべての自然数は、偶数または奇数である。」
  • システムは、変数（この場合は「数」という言葉）を何度も繰り返す必要がないことを理解しています。人間が行うように、変数を適切な場所に隠します。

• 記号的 vs 言語的：

  • 数学においては、記号（$x + y = z$ など）で書くのがベストな場合もあれば、言葉（「$x$ と $y$ の和」など）で書くのがベストな場合もあります。システムは、いつどちらを使用すべきかを判断できます。また、LaTeXコード（数学の組版の標準）を自動生成することも可能です。

この論文が実際に主張していること（および主張していないこと）

主張していること：

• 数学の形式的な証明を取り込み、流暢で自然な響きのテキストに変換できるシステム（Informath）の構築に成功した。
• 事前構築された文法ライブラリとシンプルなシンボルテーブルを使用することで、このシステムを「生産的（使いやすく）」にできることを証明した。
• このシステムが、学部レベルの数学（算術、代数、トポロジー）や、さらには高度なトピック（ホモトピー型論）にも適用可能であることを示した（ただし、高度なトピックはより困難である）。
• このシステムが、AIモデル（LLM）が数学をより上手に行うためのデータを生成するために使用できることを示した。

主張していないこと（本文の記述に基づく）：

• このシステムが、現時点で数学の「すべて」に対して完璧であるとは主張していません。著者は、数学の「通常の言語すべて」をカバーすることは、巨大で継続的な目標であると認めています。
• このシステムが、現在サポートされているもの以外のすべての証明システムを完璧に扱えると主張していません。IsabelleやMizarのようなシステムは、動作原理が異なるため、将来の課題として挙げられています。
• このシステムが人間の数学者を置き換えると主張していません。これは、コンピュータが行ったことを人間が理解するためのツールです。

まとめ

論文は、インフォーマライゼーション（非形式化）は容易ではないという結論で締めくくられています。それは単に形式化（人間からロボットへ）の逆ではありません。形式化（人間からロボットへ）はエラーを自動的にチェックできますが、インフォーマライゼーション（ロボットから人間へ）は、「自然に聞こえること」が主観的で複雑であるため、非常に困難です。

しかし、「ハブ」システム（Dedukti）と「ユニバーサル文法」（GF）を使用することで、著者は、信頼性が高く（事実を捏造しない）、柔軟性があり（多くの言語を話せる）、効率的な（構築に言語学者のチームを必要としない）翻訳機を構築できることを示しています。それは、ロボットの冷たいコードを、温かく読みやすい物語へと変えてくれるのです。