技術要約：ニューラル証明埋め込みにおける選択公理の幾何学的測定

問題提起

選択公理（AC）は、歴史的に数学的基礎を古典派と構成派の陣営に二分してきたが、この区別は主に哲学的および方法論的なものに留まっていた。古典的な証明はACによって許容される非構成的なショートカットを利用する一方で、構成的な証明は明示的な証拠（witness）を必要とするが、これら二つのパラダイムが、単なる公理への依存性を超えて検出可能な形で構造的に異なっているかどうかは不明であった。本論文は、選択公理が形式的な証明の空間、具体的にはLean 4のMathlibライブラリ内に、測定可能な「幾何学的シグネチャ」を残しているか、またそのシグネチャがニューラル定理証明器に対して運用上の影響を持つかどうかを調査する。

方法論

データ分割と依存関係の追跡

著者らは、Lean 4のカーネルレベルでの公理依存性追跡を利用して、471,260個の機械証明済み宣言を含むMathlibライブラリを分割している。依存グラフに対する幅優先探索を実行することで、宣言を以下の2つの集合に分類した：

1. 古典的な証明： Classical.choiceに推移的に依存するもの。
2. 構成的な証明： それらに依存しないもの。

古典的な証明の「距離」は、その証明からClassical.choiceまでの最短依存チェーンの長さとして定義される。これにより、証明が公理からどの程度の深さにあるかに基づいてグループ化された層化データセットが作成される。本研究では、ステップ数が2から200の間のタクティクストレースを持つ42,355個の定理（古典的31,144個、構成的11,211個）に焦点を当てる。

ラベルフリー表現学習

バイアスを排除してこれらの証明の幾何学的特性を測定するために、著者らは構成的な証明のみを用いて自己教師ありデノイジング・オートエンコーダを訓練した。

• 入力： 証明は、具体的な引数を破棄し、証明の構成に焦面を置くためにタクティクスのヘッド（例：intro, rw, simp）のシーケンスとして表現される。
• アーキテクチャ： 4層のTransformerエンコーダと2層のデコーダを組み合わせた構成。モデルは、入力シーケンスからマスクされたタクティクトークン（20%の破損）を再構成するように訓練される。
• 埋め込み： 証明の埋め込みは、エンコーダの隠れ状態（パディングを除く）の平均であり、単位球体に正規化される。
• ラベルフリー制約： エンコーダは、訓練中、語彙構築、またはハイパーパラメータ選択において、古典的な証明を一切目にしていない。古典的な証明は、厳密に測定用の保持された集団として機能する。

幾何学的測定

構成的な訓練分布からの古典的な証明の乖離を、依存深度の関数として測定するために、3つの補完的な指標を用いる：

1. 異常スコア (k-NN)： $k$番目に近い構成的な隣接点へのユークリッド距離。
2. 再構成損失： 構成的な証明で訓練されたモデルが、古典的な証明内のマスクされたトークンを予測しようとする際に発生するクロスエントロピー損失。
3. 密度超レベル集合包含率： 構成的な訓練分布によって定義される高密度領域（超レベル集合）の外側に位置する古典的な証明の割合。

運用上の評価

本研究は、2つのシステムを用いて、定理証明の性能に対する幾何学的知見の影響を評価する：

1. aesop： シンボリックな最良優先探索証明器。
2. ハイブリッド (ReProver + aesop)： ニューラル誘導型のアプローチ。タクティクス生成器が最初の動きを提案し、その後にaesopが続く。

主な結果

深度則（The Depth Law）

主要な発見は、「深度則」の存在である。すなわち、古典的な証明と構成的な証明の幾何学的な区別は、Classical.choiceからの距離に応じて予測可能な形で減衰するというものである。

• 浅い深度における鋭い分離： 深度2（古典的な補題を直接呼び出す証明）において、分離は顕著である。k-NN異常スコアは0.847のAUCを達成し、再構成損失は構成的なベースラインより**34.5%高く、古典的な証明の43%**が構成的な90%密度領域の外側に位置する。
• 判別不能性への減衰： 深度が増すにつれ、各指標は構成的なベースラインへと収束する。深度9以上では、3つの指標すべてがチャンスレベル（AUC $\approx$ 0.5、損失 $\approx$ ベースライン、包含率 $\approx$ 90%）に近づき、深い古典的な証明は構成的なものと幾何学的に区別できなくなる。
• 単一パラメータ混合則： 著者らは、この勾配を、構成的な分布 $P$ と直接的な古典的分布 $R$ の混合としてモデル化している。深度 $d$ の分布 $Q_d$ は、$Q_d = (1 - \lambda_d)P + \lambda_d R$ とモデル化され、ここで $\lambda_d$ は減少する混合重みである。正規化すると、これら3つの異なる測定値は単一の曲線に収束し、単一パラメータ則を支持している。

ロバスト性コントロール

このシグネチャは、以下の潜在的な混乱因子に対して頑健である：

• キーワード： 明示的な古典的タクティクスマーカー（例：classical, by contra）を削除しても、深度2のAUCはわずかに低下するのみ（0.847から0.754へ）であり、シグナルが語彙的ではなく構造的であることを示している。
• 長さ： 埋め込みを証明の長さに応じて残差化しても、勾配は消失しない。
• 著者/ファイル/トピック： 著者、ファイル、および数学的サブドメインを制御する混合効果モデルを用いても、シグナルは特定の文脈内で持続することが確認された。
• 命題 vs 証明： 定理の**命題（statement）**は、証明と比較してはるかに弱い深度勾配を示しており（集計AUC 0.604）、証明（集計AUC 0.675）よりも弱い。これは、シグナルがトピック（定理の内容）よりも構成的（証明の構造）な性質であることを裏付けている。
• 公理の特異性： propextやQuot.soundも深度勾配を示すが、Classical.choiceが最も急峻な勾配を生じさせており、独自の運用上の結合を示唆している。

運用上の帰結

幾何学的シグネチャは、証明器の性能と相関している：

• aesopの失敗： aesopは構成的な定理の**20.0%を解決するが、古典的な定理はわずか1.5%**しか解決できない（13倍の差）。幾何学的シグナルとは異なり、この運用上のギャップは深度とともに平滑化することはない。古典的な証明は、公理からの距離に関わらず、aesopにとって困難なままである。
• ニューラル誘導： ニューラル・タクティクス生成器（ReProver）を追加すると、このギャップは約5倍（22.0%対4.5%）に圧縮されるが、解消はされない。
• 予測能力： 異常スコアを加えることで、異常スコアは証明の長さのみを用いる場合よりもaesopの失敗を有意に良く予測する（AUCは0.766から0.841へ上昇）。

意義と主張

本論文は、選択公理が証明空間において測定可能な幾何学的相関を持つという、初の経験的証拠を提供することを主張している。著者らは以下のように述べている：

1. 構造的区別： 古典的／構成的な境界は単なる哲学的な立場ではなく、ニューラル埋め込みによって可視化される証明構成の構造的特性である。
2. 運用の関連性： この幾何学的シグネチャは単なる抽象的な好奇心ではない。それは自動定理証明器の性能を予測する。 「深度則」は、証明が公理から遠ざかるにつれて構造的に構成的な証明に似てくることを示唆しているが、aesopのようなシンボリックな証明器にとっての運用上の障壁は、Classical.choiceの存在に特有なままである。
3. 方法論的貢献： 本研究は、単一のクラス（構成的な証明）に対するラベルフリーの自己教師あり学習が、論理的依存性によって定義される保持されたクラス（古典的な証明）の構造的境界を明らかにできることを示しており、メタ数学的分析のための新しいツールを提供している。

著者らは因果メカニズムについては慎重な姿勢を保っており、幾何学的シグネチャと運用上のギャップが強く関連しているものの、特定の原因（構造的障壁か、あるいはルールセットの設定か）についてはさらなる調査が必要であると述べている。本研究は、コミュニティに対し、形式ライブラリにおける同様の構造的軸を特定するための招待状として位置づけられている。