技術的概要：組合せ論における機械発見による未踏の対称性のマッピング

問題定式化

本論文は、関数発見として定式化される数学的発見問題の特定のクラスを取り扱っている。すなわち、2 つの集合 $X$ と $Y$ が与えられたとき、厳密かつ剛直な制約を満たしつつ、単純で記号的な記述を許容する関数 $f: X \to Y$ を見出す問題である。著者らはこの設定を**剛直な比例下での単純学習（SLURP）**として形式化した。

SLURP において、定義域 $X$ は「袋（bags）」$B_i$ に分割され、各袋は値域 $Y$ 上の目標分布 $D_i$ と関連付けられる。目的は、以下の条件を満たす関数 $f$ を発見することである：

1. 剛直な比例制約： 各袋 $B_i$ における $f$ の出力は、目標分布 $D_i$ と厳密に一致しなければならない。近似での満足は不十分であり、いかなる逸脱も問題が未解決であることを意味する。
2. 単純性の要件： 関数は、合理的な時間制約内（例えば多項式時間）で評価可能な簡潔な記号的記述（閉形式またはアルゴリズム）として提供されなければならない。この要件は、解が数学的構造を明らかにするものであり、単なる任意の値の割り当てではないことを保証するために本質的である。

著者らはこの枠組みを代数組合せ論、特に $q,t$-ナラヤナ多項式 $N_{n,k}(q,t)$ の研究に応用する。核心的な課題は、組合せ対象（非交差分割）上の単純な統計量（関数）の対を見つけ、これらがこれらの多項式を生成し、その対称性 $N_{n,k}(q,t) = N_{n,k}(t,q)$ を証明する明示的な全単射を構築することである。

手法

本論文は、SLURP インスタンスを解決するための 2 つの異なる機械学習手法を導入する。

1. MapSeek-Functional（自己学習アプローチ）

この手法は、ニューラルネットワーク（具体的にはトランスフォーマーエンコーダー）を用いて目的の関数をモデル化し、以下の 2 つのステップを交互に実行する：

• 制約射影： 現在のモデル $f_\theta$ が与えられたとき、剛直な比例制約を厳密に満たす最も近い関数 $\hat{f}$ を見出す。これには、$f_\theta$ と制約を満たす関数との距離を最小化する最適化問題を解くことが含まれる。
• 教師あり更新： 射影された関数 $\hat{f}$ が擬似ラベルを生成し、これを用いて $f_\theta$ を教師あり学習（SGD）によって更新する。
• 検証： 厳格な停止基準が強制される。モデルが検証セット上で制約を完全に満たす場合のみ、実行は成功とみなされる。検証セットのサイズは、複雑または解釈不可能な解をフィルタリングするためのハイパーパラメータとして機能する。
• 蒸留： 収束後、ニューラルネットワークの振る舞いは、手動または自動的に記号的な数式へと蒸留される。

2. MapSeek-Symbolic（探索アプローチ）

この手法は、定義された形式言語 $\mathcal{L}$ 内で、記号的な数式を直接探索する。

• 探索空間： 数式は、原始記号（変数、算術演算子、論理演算子）のアルファベットから構成される。
• 最適化： 探索は、生成トランスフォーマーデコーダーを用いた**深層クロスエントロピー法（CEM）**を採用する。これは、数式の集団を反復的にサンプリングし、それらの「距離」（制約違反）を評価し、生成モデルを再学習させるためにエリート部分集合を選択する。
• 距離指標： 距離関数 $\delta$ は、候補数式の出力分布と目標分布との間の $L_1$ 差を測定する。著者らは、回帰アプローチ（ソート済み $L_1$ 距離を使用）よりも、分類タスクとして扱うこと（単純な距離指標を使用）の方が効果的であることを発見した。
• 安定性： 著者らは、数式表記における明示的な構造的区切り（空白と括弧）が、構文的には有効だが意味的に冗長な式を生成するのを防ぎ、学習の安定性に不可欠であると指摘した。

主要な貢献と結果

1. SLURP 枠組みとベンチマーク

著者らは SLURP 枠組みを形式化し、skip-pairing ベンチマークを公開する。このベンチマークは、既知の「skip」統計量と対をなす非交差分割上の統計量を見出すことを課題とする。データセットには、非単一ブロックにおける最大要素に基づいた洗練された制約が含まれる。

2. 新しい統計量の発見

両手法を $k=3$ の場合（$n-2$ 個のブロックを持つ分割）に適用した結果、著者らはいくつかの新しい解釈可能な統計量を見出した：

• Mag（マグニチュード）： 暖房開始制約付きの MapSeek-Functional によって発見された。skip 統計量と対をなす。
• Leap： 同質性制約付きの MapSeek-Functional によって発見された。skip 統計量と対をなす。
• Skew： MapSeek-Symbolic によって発見された。skip 統計量と対をなす。
• Mingarc（Min Gap Arc）： ML 発見から導かれた、反転させた「skew」統計量の人間による拡張定義。

3. 組合せ論における未解決問題の解決

最も重要な数学的成果は、$k=3$ の場合における未解決問題 4.1の解決である：

• 対称性の組合せ的証明： 著者らは、分割 $\pi$ を $\psi(\pi)$ に写す明示的な交換全単射を構築した。これにより、統計量の対 $(\text{skip}, \text{leap})$ が交換される：$(\text{skip}(\psi(\pi)), \text{leap}(\psi(\pi))) = (\text{leap}(\pi), \text{skip}(\pi))$。
• これは、明示的な全単射を介した対称性 $N_{n,3}(q,t) = N_{n,3}(t,q)$ の最初の組合せ的証明であり、極めて困難であると広く考えられている問題である。
• 新しい解釈： この研究は、すべての $k$ に対する $N_{n,k}(q,t)$ の、非交差分割（具体的には $(\text{skip}, \text{mingarc})$ 対による）に関する最初の組合せ的解釈を提供する。

4. 形式的検証

再現性と厳密性を確保するため、著者らはすべての数学的発見（新しい統計量、全単射、対称性の証明を含む）をLean 4で形式化した。彼らは自動形式化と証明探索を支援するAristotleシステムを利用し、中核的な結果の完全な機械検証を実現した。

意義と主張

本論文は、機械学習を用いて以前は未知の組合せ統計量を提案し、それらを $q,t$-組合せ論における未解決問題を解決する交換全単射の構築に用いた最初の事例であると主張する。

• 方法的意義： 著者らは SLURP を「証明駆動型の発見枠組み」として位置づける。近似一般化を求める標準的な機械学習とは異なり、SLURP は有限データ上での厳密な制約満足を要求し、最終的には無限領域上で数学的に証明可能な単純な記号的記述を見つけることを目的とする。
• 科学的影響： この研究は、現代の機械学習が、特に剛直な分布制約下での単純な関数発見において、検証可能な数学的発見に有意義に貢献し得ることを示している。
• 限界と今後の課題： 著者らは控えめに、$k=3$ の場合は閉形式解が得られたものの、$k=4$ の実験では現在、失敗モード（例えば、MapSeek-Functional が解釈困難な解に収束する、MapSeek-Symbolic がゼロ距離に到達できないなど）を示していると指摘する。彼らは、解空間の探査の理解と「単純性」の定量化が、依然として未解決の方法的課題であると認めている。

本論文は、これらのツールが熟練した数学者の手中にある場合、人間の直観を活用して数学的発見の範囲を拡大できると結論付けている。特に、明示的な全単射の構築が主要なボトルネックとなっている領域においてである。