Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

技術要約：書誌学的知識と形式化された数学的知識の間の架け橋となるレイヤーに向けて

問題提起
現代の数学的知識は、現在、構造的に独立した2つのインフラストラクチャに断片化されている。一方には、MathSciNetやzbMATH Openといった書誌データベースがあり、これらは人間が読める研究記録を索引化し、出版メタデータ、引用ネットワーク、および専門家によるレビューを捕捉している。他方には、形式的な証明ライブラリ（例：Leanのmathlib）や対話型定理証明器（ITP）があり、これらは機械的に検証可能な数学を形式的にチェックされたオブジェクトとして符号化している。これらのエコシステムは互いに補完的な関係にあるものの、依然として断絶している。すなわち、書誌システムは結果が形式化されているかどうかを示しておらず、形式ライブラリは出版メタデータではなく内部の依存グラフに基づいて整理されている。古典的な結果を機械化された開発へとマッピングするための「アライメント・アーティファクト」（サーベイ論文やドキュメンテーションなど）は存在するものの、それらのマッピングは断片的で標準化されておらず、検索可能なレイヤーへと体系的に統合されているわけではない。

手法
本論文は、既存のインフラストラクチャを置き換えるのではなく、それらを統合するように設計されたリレーショナル・ブリッジ・データベースを提案している。コアとなる手法は、以下の3つのコンポーネントで構成される。

1. アーキテクチャの統合： 本システムは、書誌レコード（MathSciNetおよびzbMATH Openから）と形式的アーティファクト（Lean、Reservoirなどから）をリンクするアライメント・インフラストラクチャとして機能する。これは新たな査読や形式的検証を行うものではなく、出版物と形式的なコードとの対応関係を記録するアーカイブ・プラットフォームとして機能する。
2. 形式化スコア ($S(P_i)$)： 著者らは、特定の論文 $P_i$ の形式化の程度を測定するための定量的指標を定義する。
   • 論文は数学的命題 $S_i$（定義、補題、定理、予想など）の集合として扱われる。
   • 各命題 $s$ に対して、バイナリ・インジケーター $\phi(s)$ が割り当てられる。これは、命題がLeanにおいて完全に形式化されている場合は1、そうでない場合は0とする。
   • 要件の区別：
     • 純粋な命題（定義、構成、予想）は、形式的オブジェクトの存在のみを必要とする。
     • 証明された命題（定理、補題）は、形式的な命題と完全な形式的証明の両方を必要とする。
   • スコアは次のように計算される：$S(P_i) = 100 \cdot \frac{\sum_{s \in S_i} \phi(s)}{|S_i|}$。
3. クロス・ドキュメント・アライメントによる実現可能性調査： これらのスコアが大規模に推定可能であることを示すために、著者らは大規模言語モデル（LLM）をゼロショット設定で活用した。モデルには、非形式的な数学論文（PDF 1）と、形式化ドキュメントまたはLeanの実装（PDF 2）を比較するタスクが与えられた。モデルには以下の指示が出された：
   • 非形式的なテキストから粒度の細かい数学的命題を抽出する。
   • それらを「純粋（Pure）」または「証明済み（Proved）」に分類する。
   • 形式的なテキストにおける意味的な対応関係を特定する。
   • 一致した命題の比率に基づいて形式化スコアを算出する。

主な貢献

• 相互運用レイヤー： 出版レジストリと形式検証環境を統合し、出版メタデータを形式コードのリポジトリにリンクするデータベースの提案。
• 形式化スコアの定義： 出版物の形式化の範囲を、定義の存在と証明の存在を区別しながら定量化する、厳密な論文レベルの指標（$S(P_i)$）。
• 実現可能性のデモンストレーション： LLMを用いることで、非形式的なテキストを形式的アーティファクトと整合させ、これらのスコアを推定できることを示す概念実証研究。

実験結果
著者らはGoogle Geminiを用い、ファインチューニングなしで6つの数学論文を用いた実験を行った。結果は、異なる程度の形式化を区別するシステムの能力を示した。

• 高いカバレッジ： 次元8における球充填問題は、完全な形式化を示すスコア 100 を受け取った。
• 部分的なカバレッジ： $\zeta(3)$ の無理数性とマルチグレーデッドProjスキームに関する論文は、それぞれ 50 および 67.74（第2の実験では 96.30）のスコアを受け取り、相当程度ではあるが不完全な形式化を反映していた。
• 低い、あるいは無いカバレッジ： 「圏の膨張（Dilatations of categories）」に関する論文は 41.67 を受け、「代数的な磁性（Algebraic magnetism）」に関するサーベイ（Leanによる実装が存在しない）は、無関係なドキュメントと照合した際に 0 を受け取った。
  実験により、モデルは関連する形式化が存在しない場合にそれを正しく識別でき、完全に形式化された著作物と部分的に形式化された著作物を区別できることが確認された。

意義と主張
本論文は、本研究を、書誌学的および形式的な数学のエコシステムを、スケーラブルでマシン・アクション可能な知識グラフへと統合するための第一歩として位置づけている。著者らは、提案するシステムは既存の出版または検証インフラストラクチャの代替ではないことを明言している。むしろ、既存の非公式なアライメント知識を、構造化され、クエリ可能なリソースへと体系化する「接続レイヤー」として機能するものである。

その意義は、以下の点にある：

1. 出版された結果とその形式的な対応物への統一的なアクセスを提供する。
2. 数学文献のどの程度が形式化されているかを大規模に分析することを可能にする。
3. 出版物を形式的な証明オブジェクトへとリンクするための基礎を築き、将来的なAI生成数学や人間とAIのハイブリッド・ワークフローを支援する可能性がある。

著者らは、PDFのパースが曖昧さを導入すること、検索の質がスコアリングの精度に影響を与えること、およびLLMが偽の対応関係を生み出す可能性があることを認め、限界についても言及している。したがって、彼らは本システムを、完全なマッピングを目指すものではなく、関係的アライメントのための「ベストエフォートのフレームワーク」として位置づけており、最終的には現在の書誌学的な慣行と同様に、ハイパーリンクやマッピングが手動でキュレーションされるか、あるいは教師ありプロセスを通じて行われることを想定している。