확률적 프로그램의 조건부 확률을 위한 베이즈 규칙

확률적 프로그램은 풍부한 확률 모델을 표현하기 위한 엄격한 프로그래밍 언어 기반을 제공하며, 어려운 통계 추론 문제를 해결하기 위한 언어 수준의 지원을 제공합니다. 확률적 프로그램이 확률 이론으로부터 물려받는 핵심적인 이론적 과제 중 하나는 확률이 0인 관측값에 대한 확률 분포를 조건화하는 것입니다. 많은 언어들이 이러한 과제를 처리하기 위해 계산 규칙(computational rules)을 사용하는데, 이는 일부 문제에는 잘 작동할 수 있지만 다른 문제에서는 통계적으로 건전하지 않을 수 있습니다. 본 논문은 확률적 프로그램을 조건화하기 위한 원칙적인 수학적 접근 방식을 소개합니다. 우리는 먼저 '소프트 조건화(soft conditioning)'와 '이웃 극한(neighborhood limits)'에 기반한 기존 기술들이 측도 이론(measure theory) 관점에서 의미론적 문제(semantic issues)를 보이며, 건전한 통계적 추론과 불일치하는 추론 결과를 산출함을 보여줍니다. 기하 측도 이론(geometric measure theory)의 도구들을 활용하여, 우리는 확률적 프로그램 트레이스에 대한 새로운 분해 기반 의미론(disintegration-based semantics)을 구성함으로써 건전한 조건화를 가능하게 합니다. 이 이론은 조건부 분포의 명시적인 베이즈 규칙 표현을 제공하며, 이는 정규화되지 않은 사후 밀도(unnormalized posterior densities)에 접근할 필요가 있는 널리 사용되는 확률적 추론 알고리즘과 직접적으로 호환됩니다. 우리의 베이즈 규칙은 루프(loops), 분기(branches), 이산형(discrete), 연속형(continuous), 혼합형 분포를 가진 확률 모델, 다양체(manifolds)에서의 관측값, 미분 가능 구조(differentiable structure), 그리고 실제에서 발생하는 추가적인 모델링 모티프까지 처리합니다.