A homotopy-type-theoretic generalization of neurosymbolic inference

技術要約：ホモトピー型論を用いたニューロシンボリック推論の一般化

問題提起
現在のニューロシンボリック（NeSy）システムは、多くの場合、$\sigma$-構造（論理記号への値の割り当て）の空間上の、信念で重み付けされた論理量の和として定義される統一的な関数に依存している。この関数は、重み付きモデル計数（WMC）、確率論的論理、あるいはファジィ論理として具体化されることが多いが、これらは集合上で動作する。著者らは、集合は「意図的に忘却する」オブジェクトであり、構造化されたNeSyに不可欠な2つの重要な情報を破棄してしまうと主張している。

1. 対称性： 理論の対称性（例：交換可能な個体間の入れ替え）に関して、同一の$\sigma$-構造を区別できない。その結果、標準的な関数は対称的な構造を過剰にカウントしてしまう。
2. 証明の多重性： クエリを証拠立てる複数の異なる導出を単一の数値へと崩壊させてしまい、「どのように多くの方法で」事実が証明されたかという情報を無視してしまう。

この脱圏級化（decategorification）は、「推論のショートカット（reasoning shortcuts）」と呼ばれる特定の失敗モードを引き起こす。モデルが論理出力のみに基づいて学習されると、潜在概念に対して誤った意味を割り当てながらも、出力自体は維持するという「ショートカット」へと収束することがある。標準的な手法では、複雑なアンサンブルや表現力豊かな密度推定に頼ることなく、正しい「ショートカットを考慮した」事後分布（等価な概念の混乱集合上の一様分布）を特定することが困難である。

手法
本論文は、NeSy推論の基礎となる集合を、ホモトピー型論（HoTT）における型へと置き換えることを提案している。このフレームワークにおいて、型は単にその要素を記憶するだけでなく、要素を同一視する方法（同型写像）をも記憶する。

著者らは、標準的なNeSy関数の4つの要素（式1）を一段高いレベルへと「持ち上げ（lift）」ている。

1. 構造空間 ($\Omega$): 個体のリネーミング（名前の付け替え）を記録する恒等型を持つ型へと置き換えられる。古典的な構造の集合は、0-切断（0-truncated）の場合である。
2. 論理関数 ($\ell$): 証明の族 $P: \Omega \to \mathcal{U}$ へと置き換えられる。$P$ の切断レベルは設計パラメータである。命題（レベル -1）は充足性をチェックし、集合（レベル 0）は導出をカウントし、群（レベル 1）は対称的な導出を識別する。
3. 推論: **信念で重み付けされたホモトピー・カルディナリティ（homotopy cardinality）**へと置き換えられる。単純な和の代わりに、推論値は次のように計算される：
   $$N(P, b) = \left\| \sum_{\omega:\Omega} P(\omega) \right\|_{V,b}$$
   これは、各要素をその対称群のサイズの逆数 ($1/|Aut(x)|$) で重み付けしてカウントすることを保証し、対称的な構造が非対称な構造よりも少なく寄与するようにする。
4. 値付け: 選択された可換半環（例：確率のための $(+, \times)$、トロピカル幾何のための $(\max, +)$）は、ホモトピー・カルディナリティからどの数値不変量が読み取られるかを決定する。

主な貢献

1. 理論的枠組み: 著者らは、NeSy推論を「信念で重み付けされたホモトピー・カルディナリティ」として定式化した。このフレームワークは、従来の定式化には存在しなかった2つの明示的なパラメータを導入している：対称性パラメータ（許可されるリネーミングの群を定義する）および切断レベル（証明の追跡の粒度を定義する）。
2. 保存定理: Lean 4で検証された機械チェック済みの定理により、対称性が自明である（群が単位群である）場合、または半環が冪等である場合、ホモトピー・カルディナリティが正確に古典的な集合ベースの関数へと崩壊することが証明されている。これにより、新しいフレームワークが忠実な一般化であることが保証される。
3. 推論のショートカットとしての軌道: 著者らは、「混乱集合（概念の割り当てのうち、同じ出力を与えるものの集合）」を、理論の対称性による**軌道（orbit）**として特定している。
   • 「ショートカットを考慮した」概念事後分布は、唯一の対称不変な点、すなわち軌道上の一様分布として特定される。
   • これにより、**軌道平均化（Orbit-Averaging）**という、この事後分布を計算するための閉形式の手法が得られる：
     $$\bar{p}(c | x) = \frac{1}{|G|} \sum_{g \in G} p_\theta(g^{-1} \cdot c | x)$$
     この手法は、出力保存群 $G$ にわたって単一のベースモデルを対称化する。これはアンサンブルや密度推定を必要としない。
4. 母関数: 交換可能なモデルに対して、このフレーム則は、組み合わせ論的種（combinatorial species）の理論と一致するように、常微分母関数ではなく指数母関数を自然に導き出す。

実験結果
著者らは、MNIST推論ショートカット・ベンチマーク（特定の対称群と、概念の識別可能性に関するグラウンドトゥルースを持つタスク）を用いて、軌道平均化手法の評価を行った。

• 設定: 単一のニューラルネットワークを、マージされたラベルを予測するように訓練した。タスクは、識別可能な数字（軌道のサイズが1）と、混同される数字（軌道のサイズが1より大きい）を区別することである。
• 比較: 単一モデルの軌道平均化ラッパーを、ベースモデルおよび多様性訓練された5モデルのアンサンブル（Bears）と比較した。
• 知見:
  • ベースモデルは、混同される数字に対して過剰に自信を持っていた（高い期待較正誤差、ECE）。
  • 軌道平均化は、ラベル精度を維持しながら、混同される数字に対するECEを0.614から0.010へと減少させ、かつ識別可能な概念の較正も維持した。
  • 多様性訓練されたアンサンブルは、ラベル精度を犠牲にするか、あるいは識別可能な概念を誤較正することによってのみ、同様の較正改善を達成した。これは、単一モデルの軌道平均化が回避できるトレードオフを浮き彫りにしている。

意義と主張
本論文は、NeSy推論をHoTTのレンズを通して読み解くことが、推論のショートカットの原因となる対称構造を露出させるという「具体的な恩恵」をもたらすと主張している。

• 理論的統一: 様々なNeSyのアプローチ（確率論的、ファジィ、プロベナンス）を、より豊かで構造化されたオブジェクトの、脱圏級化された単一の視点の下に統一する。
• 実用的な効率性: アンサンブルが必要であると考えられていた「ショートカットを考慮した」事後分布が、対称群上で単一のモデルを平均化することで閉形式で計算可能であることを示した。
• 較正: 識別可能な概念の性能を低下させることなく、識別不可能な概念に対する較正を改善する。これは、NeSy学習における特定の失敗モードを解決するものである。
• 限界: 著者らは、現在のフレームワークが有限型（$\pi$-finiteness）に依存していることを指摘している。コヒージョン（cohesion）を通じてホモトピー・カルディナリティを連続領域へ拡張することは、未解決の課題である。

本研究は、集合ベースの推論から型ベースの推論への基礎的な転換として提示されており、集合の「忘却」が型の持つ構造的記憶によって置き換えられ、それが推論のショートカットという根本的な原因に直接対処している。