A homotopy-type-theoretic generalization of neurosymbolic inference

기술 요약: 호모토피 유형론적 신경-기호 추론의 일반화

문제 정의
현재의 신경-기호(NeSy) 시스템은 대부분 $\sigma$-구조(논리 기호에 대한 값의 할당) 공간 상의 논리적 양량에 대한 믿음 가중 합(belief-weighted sum)으로 정의된 통일된 범함수에 의존한다. 이 범함수는 흔히 가중 모델 카운팅(WMC), 확률 논리, 또는 퍼지 논리로 구체화되는데, 이는 집합(sets) 위에서 작동한다. 저자들은 집합이 구조화된 NeSy에 필수적인 두 가지 핵심 정보를 유실하는 "의도적으로 망각하는(deliberately forgetful)" 객체라고 주장한다.

1. 대칭성(Symmetry): 이론의 대칭성(예: 교환 가능한 개체 간의 스와핑)에 대해 동일한 $\sigma$-구조들을 구분하지 못한다. 결과적으로 표준 범함수는 대칭적인 구조들을 중복 계산(overcount)한다.
2. 증명 다중성(Proof Multiplicity): 쿼리를 입증하는 여러 개의 서로 다른 유도 과정을 하나의 숫자로 붕괴시켜, 사실이 "어떤 방식으로" 증명되었는지에 대한 정보를 무시한다.

이러한 탈범주화(decategorification)는 **추론 지름길(reasoning shortcuts)**이라 불리는 특정 실패 모드로 이어진다. 모델이 논리적 출력에 대해서만 학습될 때, 모델은 출력은 보존하면서도 잠재 개념에 잘못된 의미를 부여하는 인식(지름길)으로 수렴할 수 있다. 표준적인 방법들은 복잡한 앙상블이나 표현력이 높은 밀도 추정에 의존하지 않고는 이러한 "지름길을 인지하는(shortcut-aware)" 사후 분포(동등한 개념들의 혼란 집합에 대한 균등 분포)를 식별하는 데 어려움을 겪는다.

방법론
본 논문은 NeSy 추론의 기초가 되는 집합을 호모토피 유형론(HoTT)의 **유형(types)**으로 대체할 것을 제안한다. 이 프레임워크에서 유형은 단순히 원소를 기억하는 것이 아니라, 원소들이 서로 동일하다고 식별되는 방식(동형 관계)을 기억한다.

저자들은 표준 NeSy 범함수의 네 가지 재료(식 1)를 한 단계 높은 수준으로 "리프트(lift)"한다:

1. 구조 공간 ($\Omega$): 개체의 재명명(renaming)을 기록하는 항등 유형(identity types)을 가진 유형으로 대체된다. 고전적인 구조의 집합은 0-절단(0-truncated) 케이스이다.
2. 논리 함수 ($\ell$): 증명 패밀리 $P: \Omega \to \mathcal{U}$로 대체된다. $P$의 절단 레벨(truncation level)은 설계 파라미터이다: 명제(level -1)는 만족 여부를 확인하고, 집합(level 0)은 유도 횟수를 세며, 그로이드(level 1)는 대칭적인 유도를 식별한다.
3. 추론: **믿음 가중 호모토피 카디널리티(belief-weighted homotopy cardinality)**로 대체된다. 단순한 합 대신, 추론 값은 다음과 같이 계산된다:
   $$N(P, b) = \left\| \sum_{\omega:\Omega} P(\omega) \right\|_{V,b}$$
   이는 각 원소를 그 대칭 군 크기의 역수($1/|Aut(x)|$)로 가중치를 두어 계산함으로써, 대칭적인 구조가 비대칭적인 구조보다 적게 기여하도록 보장한다.
4. 가치 평가(Valuation): 교환 가능한 반군(commutative semiring)의 선택(예: 확률을 위한 $(+, \times)$, 열대(tropical)를 위한 $(\max, +)$)은 호모토피 카디널리티로부터 어떤 수치적 불변량을 읽어낼지를 결정한다.

핵심 기여

1. 이론적 프레임워크: 저자들은 NeSy 추론을 믿음 가중 호모토피 카디널리티로 정식화한다. 이 프레임워크는 고전적 공식에는 없는 두 가지 명시적 파라미터를 도입한다: 대칭 파라미터(허용된 재명명의 군을 정의)와 절단 레벨(증명 추적의 정밀도를 정의).
2. 보존 정리(Conservativity Theorem): Lean 4로 검증된 기계 체크된 정리는 대칭성이 자명하거나(군이 항등원인 경우) 반군이 멱등(idempotent)일 때, 호모토피 카디널리티가 고전적인 집합 기반 범함수로 정확히 붕괴됨을 증명한다. 이는 새로운 프레임워크가 충실한 일반화임을 보장한다.
3. 궤도로서의 추론 지름길: 저자들은 "혼란 집합(confusion set, 동일한 출력을 내는 개념 할당의 집합)"을 이론의 대칭 군에 의한 **궤도(orbit)**로 식별한다.
   • "지름길을 인지하는" 개념 사후 분포는 유일한 대칭 불변 점, 즉 궤도 상의 균등 분포로 식별된다.
   • 이는 **궤도 평균화(Orbit-Averaging)**로 이어진다. 이는 다음과 같이 사후 분포를 계산하는 폐쇄형(closed-form) 방법이다:
     $$\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의 관점에서 읽는 것이 추론 지름길을 일으키는 대칭 구조를 드러냄으로써 "구체적인 이득(concrete payoff)"을 제공한다고 주장한다.

• 이론적 통합: 다양한 NeSy 접근 방식(확률적, 퍼지, 프로비넌스 등)을 더 풍부하고 구조화된 객체의 탈범주화된 관점 아래 통합한다.
• 실용적 효율성: 앙상블을 통해 구현될 수 있다고 생각되었던 "지름길을 인지하는" 사후 분포를 대칭 군에 대해 단일 모델을 평균내는 방식으로 폐쇄형으로 계산할 수 있음을 입증했다.
• 교정(Calibration): 식별 불가능한 개념에 대한 교정 성능을 개선하면서도 식별 가능한 개념에 대한 성능을 저하시키지 않는다. 이는 NeSy 학습의 특정 실패 모드를 해결한다.
• 한계점: 저자들은 현재 프레임워크가 유한 유형($\pi$-finiteness)에 의존한다는 점을 언급한다. "응집(cohesion)"을 통해 호모토피 카디널리티를 연속적인 도메인으로 확장하는 것은 남겨진 과제이다.

이 연구는 집합 기반 추론에서 유형 기반 추론으로의 근본적인 전환을 제시하며, 집합의 "망각"을 유형의 구조적 기억으로 대체하여 추론 지름길의 근본 원인을 직접적으로 해결한다.