Bayesian Networks and Proof-Nets: the proof-theory of Bayesian Inference

기술 요약: 베이지안 네트워크와 프루프-넷(Proof-Nets): 베이지안 추론의 증명 이론

문제 정의
베이지안 네트워크(BN)는 결합 확률 분포를 압축적이고 인수분해된 형태로 표현하고 효율적인 추론 알고리즘을 가능하게 하는, 확률적 추론을 위한 표준적인 도구이다. 그러나 기존의 범주론적 확률 추론 접근 방식은 풍부한 구성적 및 그래픽 언어(예: 스트링 다이어그램)를 제공함에도 불구하고, 추론의 계산 비용(시간 및 공간)을 고려하지 못하는 경우가 많다. 반면, 표준적인 BN 알고리즘은 효율적이지만, 그래픽적 추론과 논리의 구조적 특성을 통합하는 깊은 증명 이론적 토대가 부족하다. 저자들은 구성적·그래픽적 추론과 계산 효율성을 동시에 수용할 수 있는 프레임워크, 특히 범주론적 확률론에서 흔히 누락되는 "비용 인식(cost-aware)" 관점을 해결하는 프레임워크를 제공하고자 하는 간극을 식별하였다.

방법론
본 논문은 선형 논리(Linear Logic, LL), 특히 그 그래프 구문인 **프루프-넷(proof-nets)**을 사용하여 베이지안 추론에 대한 증명 이론적 설명을 제안한다. 방법론은 다음과 같다:

1. 형식주의 확장: 저자들은 다중 선형 논리(Multiplicative Linear Logic, MLL)를 **확률 박스(probabilistic boxes)**로 확장한다. 이 박스들은 베이지안 네트워크의 노드와 연관된 조건부 확률 테이블(CPT)을 인코딩한다. 구문은 표준 MLL 노드(tensor, par, cut, axiom)와 구조적 규칙(weakening, contraction), 그리고 이 새로운 확률 박스를 포함한다.
2. 대응 관계: 저자들은 베이지안 네트워크와 베이지안 프루프-넷(bpn) 사이의 건전하고 완전한 대응 관계를 확립한다. bpn은 박스가 CPT를 저장하고, 양의 결론(positive conclusions)이 구별되며, 모든 결론이 양수인 프루프-넷으로 정의된다.
3. 인수를 통한 의미론: 이전 연구([8])의 인수 기반 의미론을 채택하여, bpn의 의미론은 박스와 연관된 인수(factors, CPT)들의 곱을 구한 뒤, 결론에 존재하지 않는 변수들을 주변화(marginalization, 합산)하는 것으로 정의된다. 이는 bpn의 의미론을 BN의 표준 정의와 직접 일치시킨다.
4. 그래프 분해: 유도적 구문에 따라 엄격하게 분해되는 프루프-트리와 달리, 프루프-넷은 유연한 그래프 분해를 허용한다. 저자들은 ax-확장을 통한 **분할(splitting)**을 활용하여, bpn을 cut-노드에 의해 연결된 하위 넷들로 분해하며, 이를 통해 **컷-넷(cut-net)**이라 불리는 구조를 형성한다.
5. 그래프 리라이팅(Graph Rewriting): 본 논문은 컷 제거(cut-elimination)와 그 쌍대인 컷 확장(cut-expansion)을 그래프 리라이팅 과정으로 사용한다. 여기에는 표준적인 축약 규칙과, 그래프를 "가지치기(pruning)"하여 불필ar 변수를 제거함으로써 효과적으로 주변화를 수행하는 특정 box/weakening 축약이 포함된다.

주요 기여

• 추론에 대한 증명 이론적 설명: 본 논문은 컷 제거와 컷 확장이 베이지안 추론에서 중심적인 역할을 하는 근본적인 이해를 제공한다. 이는 추론을 단순한 계산이 아니라, 증명의 구조적 변환으로 프레임화한다.
• 더 강력한 구성성: 저자들은 그래프에 특화된 "구성 요소(component)"라는 개념을 도입하는데, 이는 기존의 트리 기반 정의보다 강력하다. 저자들은 **정리 5.2 (그래프 구성성)**를 통해, 컷에 의해 연결된 하위 넷들로 그래프가 어떻게 분해되든 상관없이 프루프-넷의 의미론을 구성적으로 계산할 수 있음을 입증한다.
  $$\llbracket Cut(R_1, R_2) \rrbracket = \sum_Z (\llbracket R_1 \rrbracket \odot \llbracket R_2 \rrbracket)$$
  여기서 $Z$는 주변화될 변수들의 이름을 나타낸다.
• d-분리(d-separation)의 그래픽적 증명: 7절에서 저자들은 d-분리(조건부 독립성을 나타내는 기준)의 건전성에 대한 직접적인 다이어그램 증명을 제공한다. 그래프 분해와 의미론의 구성성을 사용하여, 조건부 집합에 의해 레이블된 엣지를 제거한 후 그래프에서 두 변수 집합이 단절되어 있다면, 이들이 조건부 독립임을 보여준다.
• 컷-넷을 통한 효율적 추론: 본 논문은 프루프-넷을 사용하여 효율적인 BN 추론 알고리즘(예: 변수 제거법)을 모사하는 방법을 보여준다. bpn을 루티드 컷-넷(rooted cut-net)(하위 넷들의 트리 형태 구조)으로 변환함으로써, 저자들은 계산 비용이 전체 변수의 수가 아니라 컷-넷의 **너비(width)**에 의해 결정됨을 보여준다.
• 타이핑 및 순차화: 저자들은 그래프 분해(컷-넷)가 항상 시퀀트 계산 증명-트리와 직접적으로 대응하지 않는다는 문제를 다룬다. 저자들은 모든 컷-넷이 $\otimes/\parr$-확장을 통해 하위 넷들이 최대 하나의 컷에 의해 연결되는 동등한 형태로 변환될 수 있음을 입증하여(정리 8.3), 분해 과정을 유효한 시퀀트 계산 증명-트리로 다시 번역할 수 있게 한다.

결과

• 건전성과 완전성: BN과 bpn 사이의 대응 관계가 건전하고 완전함이 증명되었다. 모든 BN은 양의 bpn으로 매핑되며, 양의 bpn의 정규형(normal form)은 다시 BN으로 매핑된다.
• 종료성 및 결합성: 축약 시스템(표준 컷 제거 및 새로운 box/weakening 축약 포함)은 종료성(terminating)과 결합성(confluent)을 갖는다.
• 비용 효율성: 본 논문은 프루프-넷을 컷-넷으로 인수분해함으로써, bpn의 의미론을 계산하는 공간 및 시간 복잡도가 $O(m \cdot 2^n)$ ($n$은 전체 변수의 수)에서 $O(n \cdot 2^w)$ ($w$는 컷-넷의 너비)로 감소함을 보여준다. 이는 BN에서의 변수 제거법이 얻는 효율성 향상과 일치한다.
• 불변성: bpn의 의미론은 축약 및 확장 하에서도 불변하며, 이는 리라이팅 과정 중에 확률적 의미가 보존됨을 보장한다.

의의
본 논문은 "두 접근 방식의 장점을 모두 끌어낸다"고 주장한다: 즉, 베이지안 네트워크에서 발견되는 인수분해된 계산의 효율성과 증명 이론의 그래픽적, 구성적 추론을 결합한 것이다. 베이지안 추론을 선형 논리의 풍부한 도구 상자에 접목함으로써, 저자들은 본질적으로 "자원 인식적(resource-aware)"인 프레임워크를 제공한다. 이를 통해 증명의 구조적 조작(그래프 리라이팅)이 확률적 추론 단계(주변화 및 조건화)와 직접적으로 대응하는 통합된 처리가 가능하다. 이 연구는 추상적이고 구조적인 우아함을 가진 범주론적 확률론과 실용적이고 비용을 고려하는 확률적 추론의 요구 사항 사이의 간극을 메우며, "증명 이론의 초석"(컷 제거)이 효율적인 추론의 메커니즘 역할을 하는 새로운 관점을 제시한다.