이 논문은 nondeterminism (비결정성) 과 conditioning (조건부 추론) 을 모두 지원하는 이산 확률적 프로그램 (Discrete Probabilistic Programs) 을 위한 새로운 추론 엔진인 noDice 를 제안합니다.

다음은 논문의 기술적 요약입니다.

1. 문제 정의 (Problem)

• 확률적 프로그래밍 언어 (PPL) 의 한계: 기존 PPL 들은 복잡한 확률 분포를 직관적으로 모델링할 수 있지만, 대부분의 현대 추론 엔진은 비결정성 (Nondeterminism) 을 지원하지 않습니다. 비결정성은 마르코프 결정 과정 (MDP) 과 강화 학습 등에서 중요한 역할을 하며, 불완전한 정보를 모델링하거나 추상화를 위해 필수적입니다.
• 비결정성과 조건부 추론의 결합 문제: 비결정성과 조건부 추론 (관측 증거에 기반한 베이지안 추론) 을 동시에 다룰 때, 추론이 비분해적 (non-compositional) 이 되는 문제가 발생합니다. 즉, 하위 프로그램의 최대 조건부 확률을 알더라도 전체 프로그램의 최대 확률을 유추할 수 없습니다.
• 기존 접근법의 비효율성: 현재는 프로그램의 운영적 의미 (operational semantics) 를 직접 MDP 로 변환하여 확률적 모델 체커를 사용하는 것이 유일한 대안이지만, 이로 인해 상태 공간이 기하급수적으로 커져 추론이 비실용적이 됩니다.

2. 방법론 (Methodology)

noDice 는 기존 이산 확률적 프로그램 추론 엔진인 Dice 를 확장하여 비결정성을 처리합니다. 핵심 아이디어는 프로그램을 이진 결정 다이어그램 (BDD) 과 대수적 결정 다이어그램 (ADD) 을 통해 컴파일한 후, 이를 마르코프 결정 과정 (MDP) 으로 변환하여 조건부 도달 확률을 계산하는 것입니다.

추론 과정은 다음 3 단계로 이루어집니다:

1. 불리언 컴파일 (Boolean Compilation):

   • noDice 프로그램을 Dice 의 컴파일러를 사용하여 두 개의 불리언 공식 (Boolean formulas) 으로 변환합니다.
   • 하나는 프로그램의 동작을, 다른 하나는 관측 (observations) 을 나타냅니다.
   • 기존 Dice 와 달리, 비결정적 선택 (nflip) 을 추적하기 위해 확률적 플립의 순서와 특성을 기록하는 주석 달린 트레이스 (annotated trace) 를 생성합니다.

2. 결정 다이어그램 구축 (Decision Diagrams):

   • 생성된 불리언 공식을 내부적으로 이진 결정 다이어그램 (BDD) 으로 표현합니다.
   • 이후 두 개의 BDD 를 하나의 대수적 결정 다이어그램 (ADD) 으로 결합합니다. ADD 는 이진 출력뿐만 아니라 다양한 값을 가질 수 있어, 프로그램의 출력과 관측 성공 여부를 하나의 다이어그램으로 통합합니다.
   • 이 단계에서 프로그램의 구조적 중복 (conditional independence 등) 을 제거하여 상태 공간을 압축합니다.

3. MDP 리프팅 및 추론 (Lifting to MDP):

   • ADD 를 기반으로 마르코프 결정 과정 (MDP) 을 구성합니다. ADD 의 노드가 MDP 의 상태가 되며, 확률적 플립은 확률적 전이로, 비결정적 플립 (nflip) 은 비결정적 행동 (scheduler) 으로 매핑됩니다.
   • 조건부 도달 확률 (Conditional Reachability): 프로그램이 특정 값을 반환할 최대 확률은, MDP 에서 '관측이 성공한 상태 (Accepting state)'에 도달하는 조건 하에 '목표 상태'에 도달할 확률로 정의됩니다.
   • Storm 모델 체커: 생성된 MDP 에서 조건부 도달 확률을 계산하기 위해 Storm 모델 체커의 이분법 기반 알고리즘 (bisection-based algorithm) 을 사용합니다. 이는 순환이 없는 MDP 에서 매우 효율적입니다.

3. 주요 기여 (Key Contributions)

1. noDice 언어 및 의미론 개발: 비결정적 선택 (nflip), 확률적 선택 (flip), 그리고 1 등 관측 (observe) 을 지원하는 비재귀적 함수형 언어 noDice 와 그 형식적 의미론을 정의했습니다.
2. 새로운 추론 알고리즘: 결정 다이어그램 (ADD) 을 사용하여 컴팩트한 MDP 를 생성하고, 이를 통해 비결정적 프로그램의 최대 출력 확률을 조건부 도달 확률로 추론하는 알고리즘을 제시했습니다.
3. 효율성 검증: 다양한 벤치마크 (Runway, Coupon Collector, Bayesian Networks, 3SAT 등) 에 대해 noDice 를 구현하고 평가했습니다.
   • 상태 공간 축소: noDice 는 직접적인 MDP 인코딩이나 기존 모델 체커 (Storm) 에 비해 훨씬 작은 MDP 를 생성했습니다.
   • 성능 우위: 특히 변수가 많고 상태 공간의 차원이 높은 문제 (예: 쿠폰 수집 문제, 베이지안 네트워크) 에서 Storm 보다 훨씬 빠른 성능을 보였습니다. 반면, 상태 공간이 작고 단순한 문제에서는 오버헤드 때문에 Storm 이 더 빠를 수 있음을 확인했습니다.

4. 실험 결과 (Results)

• 상태 공간 축소: noDice 는 ADD 를 활용하여 프로그램의 구조적 중복을 제거함으로써 MDP 의 상태 수를 크게 줄였습니다. 예를 들어, 'Runway' 및 'Coupon' 벤치마크에서 noDice 가 생성한 MDP 크기는 Storm 이 생성한 것보다 수백 배에서 수천 배 작았습니다.
• 추론 시간: 대부분의 벤치마크에서 noDice 는 Storm 보다 빠른 추론 시간을 기록했습니다. 특히 'Alarm'과 같은 복잡한 베이지안 네트워크나 '3SAT' 문제에서 Storm 은 시간 초과 (TO) 를 겪은 반면, noDice 는 성공적으로 추론을 완료했습니다.
• 비결정성의 영향: 비결정적 연산의 비율이 증가해도 noDice 의 컴파일 시간은 크게 변하지 않았으며, 모델 체킹 시간만 약간 증가했습니다. 이는 ADD 구축이 비결정성의 본질에 무관하게 작동함을 의미합니다.

5. 의의 및 결론 (Significance)

• 비결정성과 조건부 추론의 통합: 기존에는 불가능하거나 비효율적이었던 비결정성과 조건부 추론의 결합을 효율적으로 해결하는 첫 번째 체계적인 접근법 중 하나입니다.
• 확장성: 무한 루프나 연속 분포는 지원하지 않지만, 이산적이고 루프가 없는 프로그램에 대해 매우 확장 가능한 추론을 제공합니다.
• 실용성: noDice 는 복잡한 시스템 (예: 자율 주행 차량의 센서 추적, 네트워크 보안, 강화 학습 전략) 에서 최악의 경우 (worst-case) 시나리오를 분석하는 데 필수적인 도구가 될 수 있습니다.
• 향후 작업: 무한 루프 처리, 최적 프로그램 생성 (Synthesis), 그리고 더 큰 규모의 프로그램으로의 확장 등이 향후 연구 과제로 제시되었습니다.

요약하자면, noDice는 결정 다이어그램을 중간 표현으로 활용하여 비결정적 확률적 프로그램의 추론 문제를 효율적인 MDP 조건부 도달 문제로 변환함으로써, 기존 모델 체커의 한계를 극복하고 대규모 문제에서도 실용적인 추론을 가능하게 합니다.