Probabilistic programming languages offer powerful generic inference algorithms to let programmers
write probabilistic models with succinct programming notations. Stochastic variational inference (SVI)
is one of the most popular classes of such inference algorithms. However, many verification challenges
arise to assure that a given probabilistic program runs a valid SVI. Among those, this dissertation aims
at the verification of well-defined variational objectives. We define a Pyro-like probabilistic programming
language and its denotational semantics using a special data structure called random database. Then, we
propose a sufficient set of conditions for the bounded evidence lower bound (ELBO), which is the most
fundamental variational objective. The most remarkable condition is the finite expected execution time
of a program, whose verification is a well-studied research problem. Finally, we generalized our result
to three other variational objectives. The next challenge is to develop an automatic program analyzer
based on our current knowledge.
확률 변분 추론은 확률적 프로그래밍 언어가 제공하는 가장 강력한 추론 알고리즘 가운데 하나이다. 그러나
프로그램이 올바른 확률 변분 추론을 수행하는지 여부를 이론적으로 보장하려면 다양한 검증 문제가 파생
되며, 그중에서도 본 논문이 풀고자 하는 문제는 잘 정의된 목적함수의 검증이다. 본 논문에서는 Pyro와
유사한 확률적 프로그래밍 언어를 정의하고 랜덤 데이터베이스라는 특별한 데이터 구조를 이용하여 표시적
의미론을 기술한다. 이를 바탕으로 유한한 평균 실행 시간을 검증하는 문제로 환원시키는데 성공하였다.
추후 연구과제로는 현재 밝혀낸 사실을 이용하여 자동화된 프로그램 분석기를 개발하는 것이 있다.
