확률적 프로그램의 효율적인 프로그래밍 가능 추론을 위한 증분 계산 (Incremental Computation)

확률적 프로그램 (Probabilistic programs)에서의 추론 (Inference)은 일반적으로 높은 사후 밀도 (posterior density)를 가진 실행 사례를 찾기 위해 가능한 많은 프로그램 실행을 평가해야 합니다. 추론을 대규모 데이터셋으로 확장하기 위해서는, 값비싼 중간 결과들을 처음부터 다시 계산하는 대신 이러한 수많은 평가 과정 전반에 걸쳐 공유하는 것이 매우 중요합니다. 본 논문은 프로그램 입력이 변경될 때 (결정론적) 프로그램 출력을 효율적으로 재계산하는 기술인 증분 계산 (incremental computation)에 기반하여, 이러한 공유를 실현하는 새로운 접근 방식을 제시합니다. 먼저, 우리는 표현력이 풍부한 확률적 프로그램이 자신의 밀도 함수 (density functions)를 계산하는 결정론적 프로그램으로 어떻게 컴파일될 수 있는지를 보여줍니다. 그다음, 증분 $\lambda$-calculus ($\lambda$-calculus)를 기반으로, 표현력이 풍부한 함수형 프로그램 (functional programs)을 구성적으로 증분화 (compositionally incrementalizing)하는 일반적인 기술을 개발하고 이를 이러한 밀도 계산에 적용합니다. 결과적으로 생성된 증분 밀도 (incremental densities)는 기존 시스템에서 잘 지원되지 않는 비모수 모델 (nonparametric models)을 포함하여 광범위한 몬테카를로 추론 (Monte Carlo inference) 알고리즘을 가속화하는 데 사용될 수 있습니다. 나아가, 증분 밀도 계산을 별도의 밀도 계산 단계와 증분화 단계로 분해함으로써 정확성 (correctness)에 대한 모듈식 추론 (modular reasoning)이 가능해집니다. 이는 임시방편적인 (ad-hoc) 증분화 기능이 건전성 버그 (soundness bugs)의 알려진 원인이 되는 기존 시스템의 주요 문제점(pain point)을 해결합니다. 우리는 각 단계를 독립적으로 검증하기 위해 의미론적 논리 관계 (denotational logical relations) 논증을 개발하였으며, 이를 Julia 프로토타입으로 구현하였습니다. 그 결과, 다양한 모델과 추론 알고리즘에서 데이터셋 크기에 따른 점근적 실행 시간 (asymptotic runtime) 개선을 확인하였습니다.