A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness

기술 요약: 조건부 독립, 베이즈 조건화, 그리고 Pearl의 d-separation 건전성에 대한 큐비컬 정식화

문제 정의
본 논문은 확률적 추론의 형식적 검증에 있어 근본적인 간극을 다룬다. Stone 이후 확률 모나드 정식화에서 흔ไข히 사용되는 표준 볼록 대수 교환 법칙(convex-algebra interchange axiom)은 완전한 베이즈 조건화(Bayesian conditioning)를 지원하기에는 증명 가능한 수준에서 너무 약하다. Coq과 같은 고전적 정식화(classical formalizations)는 조건부 독립(CI)을 실수 값 확률 사이의 명제적 동치로 취급하지만, 이는 고전 논리와 외연성(extensionality)에 의존하며, 구조적 결과인 교차 공리(intersection axiom)를 도출하기 위해 양의 값 가설(positivity hypotheses)과 0이 아닌 확률에 의한 나눗셈을 요구하는 경우가 많다. 또한, 재귀적 베이즈 조건화를 분포의 고차 유도 타입(Higher Inductive Type, HIT) 표현으로 들어 올릴 때 구조적 불일치가 드러난다. 표준 교환 법칙은 재배열된 혼합물(rearranged mixtures)에 대해 단일한 공유 내부 가중치를 가정하는 반면, 베이즈 조건화는 자연스럽게 베이즈 공식에 의해 연결된 서로 다른 내부 가중치를 가진 혼합물을 생성한다.

방법론
저자는 Cubical Agda를 활용하여 큐비컬 타입 이론(Cubical Type Theory) 및 **고차 유도 타입(HIT)**을 이용한 구성적 정식화를 개발한다. 이 방법론은 고전적 접근 방식으로부터 세 가지 구조적 전환에 의존한다:

1. HIT로서의 확률 모나드: 유한 분포(FDist)는 점 질량(point masses)과 이진 가중치 혼합 연산에 의해 생성되는 HIT로 정의된다. 표준 볼록 대수 법칙(멱등성, 반대칭성, 경계 사례, 교환, 반대-결합성)은 경로 생성자(path constructors)로서 부과된다. 이를 통해 분포적 등가성을 단순한 명제적 동치가 아닌 실행 가능한 변환(경로)으로 취급할 수 있다.
2. 구조적 조건부 독립: CI는 실수 값 사이의 점별(pointwise) 동치가 아니라 분포 커널 사이의 경로(kXY z ≡ kX z ⊗D kY z)로 정의된다. 이를 통해 CI 증거(witnesses)가 모나딕 연산을 통해 전달될 수 있는 합성적 추론이 가능해진다.
3. 구성적 가중치 처리: 본 개발은 추상적인 Weight 시그니처(결정 가능한 순서를 가진 순서 체)에 대해 다형적이며, 구체적으로는 유리수($\mathbb{Q}$)에서 인스턴스화된다. 이는 구성적 실수에서의 등가성 결정 불가능성 문제를 피하고, 양의 값과 나눗셈을 명시적으로 처리할 수 있게 한다.

주요 기여 및 결과

• 교환 불일치와 일반화: 핵심적인 기술적 발견은 표준 교환 법칙(medial law)이 완전한 베이즈 조건화를 지원하기에 불충분하다는 것이다. 4-리프(4-leaf) 혼합물을 조건화하면 베이즈 공식에 의해 관계를 맺는 두 개의 서로 다른 내부 절반($q_1$과 $q_2$)이 생성되는데, 표준 법칙은 이들이 동일($q_1 = q_2$)할 것을 요구한다. 저자는 서로 다른 내부 가중치를 허용하는 일반화된 교환 법칙(mix-bayes-interchange)을 도입한다. 이 일반화된 형태가 표준 형태가 두 가중치가 일치하는 특수 사례임을 증명한다.
• 구성적 교차 공리: 본 논문은 교차 공리를 **수축(contraction)**으로 환원함으로써 구성적 교차 공리 증명을 제공한다. 나눗셈을 통한 베이즈 추출 대신, 이 증명은 인수 분해의 구조적 $\Sigma$-타입 증거와 조건부 변수의 존재성 가설을 사용한다. 이를 통해 어떠한 구체적인 양의 분포 모델에 대해서도 공리 없이 교차의 전체 내용을 회복한다.
• Pearl의 do-calculus 검증: Pearl의 do-calculus의 세 가지 규칙 모두가 작은 구조적 인과 모델(SCM) 상의 커널 수준에서 검증되었다:
  • 규칙 1 & 3: 모나드 법칙과 constBind 보조 정리(독립 변수에 대한 개입은 주변 분포를 변화시키지 않음)의 결과로서 검증되었다.
  • 규칙 2: 결합 사전 확률이 인수 분해된다는 구조적 CI 증거를 사용하여 혼돈된(confounded) SCM 상에서 검증되었다. 이는 개입과 조건화 사이의 동등성을 확립한다.
• 재귀적 베이즈 조건화: 전체 지지 파편(full-support fragment)에 대한 재귀적 베이즈 조건화를 위한 전사 함수(total function)가 정의된다. 저자는 이 함수를 전체 HIT로 들어 올리는 데 필요한 6가지 코히어런스(coherence) 의무를 모두 해결한다. 다섯 번째 코히어런스(교환)는 앞서 언급한 일반화된 법칙을 필요로 한다.
• 마르코프 범주 정렬: FDist 모나드가 마르코프 범주(Fritz 및 Cho–Jacobs의 의미)의 구체적인 인스턴스임을 검증한다. 비자명한 delete-naturality 공리(전체 질량 보존)는 HIT 귀납법을 통해 증명되며, 이는 경로 생성자가 확률적 정규화를 올바르게 포착함을 확인한다.
• D-Separation 건전성: 임의의 유한 방향 비순환 그래프(DAG)에 대해 Pearl의 d-separation 정리의 건전성을 구성적으로 검증한다. 이는 경로별 축소 없이 조상 인수 분해(ancestral factorization)를 통해 유도되는 다중 요소 집합($X, Y, Z$)에 대한 개입 형태와 기본 패턴에 대한 베이즈 형태를 모두 포함한다.

의의 및 주장
본 논문은 이 정도의 일반성을 가진 체계 내에서, 유형론적 프레임워크 전체를 사용하여 Pearl의 d-separation 정리의 건전성 방향을 구성적으로 기계 검증한 첫 번째 사례라고 주장한다.

• 계산적 내용: CI가 하나의 단언(assertion)인 고전적 정식화와 달리, 큐비컬 접근 방식은 계산적 내용을 제공한다. CI 증거는 실행 가능한 변환이며, 사후 분포는 Agda의 정규화기(normalizer)에 의해 계산되는 실행 가능한 항(term)이다.
• 기초적 교정: 본 연구는 확률 모나드의 표준 대수적 기초가 베이즈 조건화를 지원하기에 "너무 약다"는 점을 식별한다. 제안된 교환 법칙의 일반화는 모나딕 설정 내에서 완전한 베이즈 추론을 목표로 하는 모든 프레임워크를 위한 필수적인 구조적 개선으로 제시된다.
• Mahadevan의 스택 검증: 본 논문은 Mahadevan의 토포스 인과 모델(TCM) 프레임워크의 "최하단 레이어"를 검증한다. 이는 do-calculus의 커널 형태 항등식과 가환 분포 모나드가 구성적으로 성립함을 확인하며, 이는 층(sheaves)과 강제 의미론(forcing semantics)과 같은 토포스 이론적 기계론 위에 구축될 수 있는 검증된 기질 역할을 한다.
• 제로 공리(Zero Postulates): d-separation 건전성과 베이즈 조건화를 포함한 전체 개발 과정은 추상적 순서 체(ordered-field interface, $\mathbb{Q}$에서 인스턴스화됨) 이상의 제로 공리로 검증되었다. 여기에는 이전에 사용되었던 부정확한 경계값의 제거와 고전적 나눗셈을 구성적이고 양의 값 보호가 적용된 연산으로 대체하는 과정이 포함된다.

결론적으로, 조건부 독립과 조건화의 구성적 내용은 고전 논리와 외연성을 결합하는 것이 아니라, 확률의 대수적 법칙이 타입의 정의 자체에 내재되어 있는 큐비컬 타입 이론의 구조적, 경로 기반 추론에 의해 가장 잘 포착된다.