가중 프로그래밍에서의 계수적 비결정성 및 확률적 프로그램 검증을 위한 기계화된 기초에 대한 응용

가중 프로그래밍(Weighted programming)은 Batz 등이 제시한 프레임워크로, 수학적 모델이나 최적화 문제를 반환군(semiring) 위에서 매개변수화된 명령형 프로그램으로 기술하고, 이를 약한 전제 조건 계산법(weakest precondition calculi)과 같은 프로그램 검증 기법으로 분석합니다. 응용 분야로는 확률적 프로그램의 기대 결과에 대한 추론이나 온라인 알고리즘의 경쟁 분석 등이 있습니다. 우리는 가중 프로그래밍을 (1) 계수적 비결정성(countable nondeterminism)과 (2) 사용자 정의 가산 보상(user-defined additive rewards)으로 확장했으며, 이 경우 프로그램은 반환군 대신 모듈(modules) 위에서 매개변수화됩니다. 그 결과로 얻어진 프레임워크는 확률적 프로그램의 기대 자원 소비량과 조합 게임의 최적 점수에 대한 추론을 가능하게 합니다.

기술적인 난제는 임의의 모듈 위에서 (1)과 (2)를 포함하는 가중 프로그래밍에 대한 wp-계산법(wp-calculi)이 건전하지 않을 수 있다는 것입니다. 이는 프로그램 의미론에서 일반적으로 사용되는 연속성 속성이 계수적 비결정성의 존재 하에 깨지는 것으로 잘 알려져 있기 때문입니다. 우리는 가중 결정 과정(Weighted Decision Processes, WDPs)—이는 전이 가중치와 상태 보상을 모듈로부터 가져옴으로써 마르코프 결정 과정(Markov decision processes)을 일반화하는 전이 시스템—의 관점에서 정의된 운영적 진실성(operational ground truth)에 대해 가중 프로그래밍에 대한 wp-스타일 변환기(transformer)가 건전한 조건을 연구합니다. 이러한 조건들을 바탕으로, 우리는 가중 프로그래밍 프레임워크의 다양한 구체적인 사례들이 건전한 약한 전제 조건 추론을 즐긴다는 것을 보여줍니다.

우리는 여러 모듈에 대한 사례 연구를 통해 우리의 wp-의미론(wp-semantics)의 유용성을 입증합니다. 우리는 확장된 가중 프로그래밍 프레임워크와 주요 건전성 결과를 대화형 정리 증명기인 Lean에서 기계화했습니다. 이러한 결과들을 확률적 프로그래밍에 적용함으로써, 우리가 아는 한 마르코프 결정 과정에서 계수적 비결정성을 가진 최소 기대 보상(minimal expected rewards)의 고정점 특성화(fixed point characterization)에 대한 최초의 기계화된 증명을 얻었습니다.