💻 computer science

Multiobjective Preexpectation Reasoning for Probabilistic Programs

이 논문은 유한 상태 공간을 요구하지 않고도 무한 상태 마르코프 결정 과정(MDP)을 건전하게 처리하기 위해, 사후 기댓값을 볼록 호어 파워도메인(convex Hoare powerdomain) 내의 달성 가능한 가치 집합으로 매핑하는 다목적 사전 기댓값 변환기(multiobjective preexpectation transformer)를 활용하여, 비결정론을 포함하는 확률적 프로그램에서의 다목적 전략 합성을 위한 연역적 프로그램 수준 프레임워크를 소개한다.

원저자: Lena Verscht, Hannah Mertens, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen

게시일 2026-08-14

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Lena Verscht, Hannah Mertens, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

당신이 혼란스러운 성운을 항해하는 우주선의 선장이라고 상상해 보십시오. 당신에게는 두 가지 목표가 있습니다. 목적지에 최대한 빨리 도착하는 것과, 우주 파편으로부터 우주선의 선체를 보호하는 것입니다. 하지만 여기 함정이 있습니다. 더 빨리 이동할수록 충돌할 가능성이 높아지며, 더 안전하게 운전할수록 여정은 길어집니다. 컴퓨터 과학의 세계에서 이것은 전형적인 "계획 문제(planning problem)"입니다. 우리는 의사결정을 내리는 컴퓨터 프로그램을 작성하지만, 때때로 이 프로그램들은 두 가지 유형의 불확실성을 다뤄야 합니다. 바로 무작위성(경로를 결정하기 위해 동전 던지기를 하는 것과 같은)과 비결정론(프로그램이 여러 옵션 중 하나를 선택해야 하지만, 아직 어떤 것을 선택할지 모르는 상태)입니다.

이러한 프로그램들이 올바르게 작동하도록 하기 위해, 과학자들은 "서술자 변환기(predicate transformer)"라는 도구를 사용합니다. 이것은 프로그램이 실행되기 전에 이를 들여다보고 예상되는 결과를 알려주는 마법의 수정구슬이라고 생각하십시오. 만약 당신이 수정구슬에 "안전하게 도착할 확률을 알고 싶다"라고 말한다면, 그것은 안전을 극대화하기 위한 최선의 전략을 계산해 냅니다. 오랫동안 이러한 수정구슬은 한 번에 하나의 목표만을 다룰 수 있었습니다. 하지만 현실 세계에서 우리는 단 하나의 목표만을 원하지 않습니다. 우리는 균형을 원합니다. 즉, "내가 10% 더 빨리 도착하고 싶다면, 안전을 얼마나 포기해야 하는가?"라는 **트레이드오프(trade-off)**를 알고 싶은 것입니다. 이것이 바로 **다목적 최적화(multiobjective optimization)**의 영역이며, 여기서 목표는 단 하나의 완벽한 숫자가 아니라, 가능한 타협점들의 전체 지도인 **파레토 프런트(Pareto front)**를 찾는 것입니다.

이 논문은 이러한 다중 목표 시나리오를 위해 특별히 설계된 업그레이드된 수정구슬을 소개합니다. 저자들인 컴퓨터 과학자 팀은 다목적 사전 기대 변환기(줄여서 "mop")라고 불리는 수학적 프레임워크를 개발했습니다. 이 도구는 단 하나의 숫자 대신 하나의 '형태'를 제공합니다. 즉, 다양한 전략을 혼합함으로써 달성할 수 있는 모든 가능한 결과의 구름을 보여줍니다. 이것은 정교한 레시피 북처럼 작동합니다. 불확실한 선택이 포함된 프로그램을 입력받아, 가능한 결과의 전체 '메뉴'를 계산하여 어떤 속도와 안전의 조합이 달성 가능하고 어떤 것이 불가능한지를 정확히 보여줍니다.

이 논문은 이 새로운 도구가 수학적으로 건전하다는 것을 증명합니다. 즉, 프로그램이 무한히 실행되거나 무한한 상태를 가질 수 있는 경우에도 이 도구가 실제 세계의 동작을 정확하게 반영한다는 것을 의미합니다. 저자들은 이 도구를 예측뿐만 아니라 **전략 합성(synthesize strategies)**에도 사용할 수 있음을 보여줍니다. 다시 말해, 만약 당신이 "결과가 60% 빠르고 40% 안전하기를 원한다"라고 말한다면, 시스템은 그 지점에 도달하기 위한 구체적인 계획("혼합 결정화", mixed determinization)을 수학적으로 구성할 수 있습니다. 이 계획은 목표한 중간 지점을 맞추기 위해 시작 단계에서 두 가지 순수 전략 사이를 결정하는 동전 던지기를 하는 것처럼, 선택을 무작위화하는 방식을 포함할 수 있습니다.

연구진은 로봇이 고장 나지 않고 목표에 도달하려는 사례와 도박사가 모든 것을 잃지 않으면서 수익을 극대화하려는 사례를 포함한 여러 예제로 이들의 방법을 테스트했습니다. 로봇 예시에서 그들은 최선의 전략이 항상 "항상 빠르게 가기" 혹은 "항상 느리게 가기"인 것은 아니라는 점을 보여주었습니다. 때로는 여정의 대부분은 느리게 가다가 마지막에 전력 질주하거나, 이러한 방식들을 혼합하는 것이 최적의 움직임일 수 있습니다. 논문은 이 "mop" 도구가 로봇이 취할 수 있는 모든 경로를 일일이 시뮬레이션하지 않고도 이러한 복잡한 트레이드오프를 기호적으로 계산할 수 있음을 입증합니다.

그러나 저자들은 자신들의 방법이 원하는 지점에 '임의로 가까워질 수 있는' 전략을 찾을 수는 있지만, 특정 지점이 단일 전략으로는 닿을 수 없는 지도의 "날카로운 모서리"인 경우에는 그 지점에 '정확히' 도달하는 전략을 찾는 것이 때때로 불가능하다고 주의를 기울입니다. 그런 경우, 최선은 매우, 매우 가까이 가는 것입니다. 또한 그들은 현재의 방식이 단순한 프로그램에는 가장 잘 작동하며, 재귀 함수나 연속 확률 분포와 같은 복잡한 기능은 아직 다루지 못하고 있으며, 이를 향후 연구 과제로 남겨두고 있다고 지적합니다.

궁극적으로, 이 연구는 고수준의 프로그램 코드와 불확실성 하에서의 의사결정이라는 복잡한 수학 사이의 간극을 메웁니다. 이는 여러 목표를 동시에 추론할 수 있는 방법을 제공하며, "균형을 찾는 것"이라는 막연한 개념을 정밀하고 계산 가능한 과학으로 바꿉니다. 모든 가능한 결과의 집합을 하나의 기하학적 형상으로 다룸으로써, 저자들은 프로그래머가 단순히 안전하거나 빠른 시스템이 아닌, 영리하게 균형 잡힌 시스템을 설계할 수 있도록 강력한 새로운 렌즈를 제공합니다.

기술 요약: 확률적 프로그램에 대한 다목적 사전기대 추론 (Multiobjective Preexpectation Reasoning for Probabilistic Programs)

문제 정의

비결정론(nondeterminism)을 포함하는 확률적 프로그램은 전략(또는 제어기)이 비결정론적 선택을 해결하여 기대 결과(expected outcomes)를 최적화해야 하는 계획 및 제어 문제를 모델링한다. 고전적인 접근 방식은 단일 양(예: 기대 연료 잔량 또는 종료 확률)을 최적화하는 데 집중하지만, 많은 실제 시나리오에서는 여러 개의, 종종 상충하는 목적 함수들을 동시에 최적화해야 한다(예: 성공 확률을 최대화하는 동시에 자원 소비를 최소화함).

다목적 설정에서는 하나의 목적을 개선하면 종종 다른 목적이 저하된다. 최적의 트레이드오프 집합은 **파레토 프런트(Pareto front)**에 의해 포착된다. 마르코프 결정 과정(MDP)에서의 다목적 최적화를 위한 기존 방법들은 주로 유한 상태 모델로 제한되어 있다. 그러나 확률적 프로그램은 종례히 무한 상태 MDP를 유도한다. 또한, 여러 기대를 동시에 추론하고, 전략을 합성하며, 명시적인 상태 열거 없이 무한 상태 공간을 다룰 수 있는 연역적인 프로그램 수준의 계산법(calculus)이 부족한 실정이다.

본 논문은 세 가지 핵심 질문을 다룬다:

Q1: 주어진 프로그램에 대해 동시에 달성 가능한 가치 튜플의 집합(다목적 사전기대)은 무엇이며, 이를 기계화 가능한 프로그램 수준의 계산법을 통해 계산할 수 있는가?
Q2: 주어진 목표 트레이드오프가 주어졌을 때, 이를 실현하는 프로그램 정제(전략)를 어떻게 합성할 수 있는가?
Q3: 이러한 프로그램 수준의 구성 요소들이 (가능한 경우 무한 상태인) 다목적 MDP 이론과 어떻게 연관되며 이를 어떻게 확장하는가?

방법론

저자들은 프로그램 수준에서 작동하는 다목적 사전기대 변환기(denote mop)를 개발한다. 이 접근 방식은 벡터 형태의 기대치를 처리하기 위해 고전적인 약한 사전기대(wp) 계산법을 확장한다.

1. 다목적 사전기대 변환기 (`mop`)

핵심 혁신은 사후기대(postexpectations) 튜플 $(f_1, \dots, f_n)$ 을 동시에 달성 가능한 값들의 집합으로 매핑하는 것이다.

도메인: 이 변환기는 $\mathbb{R}_{\ge 0}^n$ $R_{\geq 0}^{n}$ 의 볼록 호어 파워도메인(convex Hoare powerdomain) 위에서 작동한다. 이 도메인의 원소들은 다음과 같은 성질을 갖는 $\mathbb{R}_{\ge 0}^n$ $R_{\geq 0}^{n}$ 의 부분집합들이다:
- 비공집합(Non-empty): 항상 영 벡터(zero vector)를 포함한다.
- 하향 폐쇄(Downward closed): 만약 어떤 값 벡터가 달성 가능하다면, 그보다 지배(dominated)되는 임의의 벡터도 달성 가능하다.
- 볼록 폐쇄(Convex closed): 혼합 전략(결정론적 선택들을 무작위화함)을 통해 그 결과들의 임의의 볼록 결합을 달성할 수 있다.
- 스콧 폐쇄(Scott closed): "거의 달성 가능한" 점들(달성 가능한 점들의 수열의 극한)을 포착하여, 단일 전략에 의해 상한(suprema)이 도달되지 않을 수 있는 무한 상태 시스템에서의 완전성을 보장한다.
의미론(Semantics): 변환기는 프로그램 구조(skip, 할당, 순차 구성, 확률적 선택, 가드된 비결정론적 선택, 루프)에 대해 귀납적으로 정의된다.
- 가드된 비결정론적 선택의 경우, mop은 파워도메인에서의 점별 상한(pointwise supremum)을 취하며, 이는 각 분기(branch)들의 스코트 폐쇄적이고 볼록 폐쇄적인 합집합에 해당한다.
- 루프의 경우, mop은 특성 함수의 최소 고정점(lfp)으로 정의되며, 변환기의 $\omega$ -연속성 덕분에 존재가 보장된다.

2. 스칼라화를 통한 전략 합성

특정 트레이드오프를 달성하는 전략(결정론화)을 합성하기 위해, 저자들은 **스칼라화(scalarization)**를 사용한다.

가중 합(Weighted Sums): 가중치 벡터 $w$ 는 여러 목적을 하나의 스칼라 기대치 $w \cdot f$ 로 결합한다.
축소(Reduction): 특정 트레이드오프에 대한 전략을 찾는 문제는 가중 합 목적 함수를 최대화하는 단일 목적 전략을 찾는 문제로 축소된다. 기존의 단일 목적 프로그램적 전략 합성 기술(예: [Batz et al. 2024a])을 사용하여 $w \cdot f$ 를 최대화하는 순수 결정론 $C_w$ 를 찾을 수 있다.
혼합 결정론(Mixed Determinizations): 단일 결정론적 전략이 (특히 노출되지 않은 점(non-exposed points)의 경우) 모든 파레토 최적점을 달성하지 못할 수 있으므로, 저자들은 혼합 결정론을 도입한다. 이는 서로 다른 순수 결정론들 사이를 선택하기 위해 초기 동전 던지기를 수행하는 프로그램들이다. 달성 가능한 점들의 집합은 이러한 순수 결정론들의 결과들의 볼록 껍질(convex hull)의 폐쇄(closure)와 같음이 입증되었다.

3. 루프 추론 및 종료

본 논문은 불변량(invariant)을 사용하여 루프를 추론하기 위한 규칙을 제공한다:

상한(Upper Bounds): 슈퍼인베리언트(superinvariants)를 이용한 파크 유도(Park induction)를 통해 도출된다.
하한(Lower Bounds): 특정 종료 조건 하에서 서브인베리언트(subinvariants)를 사용하여 도출된다:
- 악마적 거의 확실 종료(Demonic Almost-Sure Termination, dAST): 모든 비결정론적 해소가 확률 1로 종료된다.
- 악마적 확실 종료(Demonic Certain Termination, dCT): 모든 실행이 유한한 단계 내에 종료된다.
- $\omega$ -불변량( $\omega$ -invariants): 언롤링 깊이(unrolling depth)를 추적하는 일련의 불변량으로, 종료 가설 없이 적용 가능하지만 무수히 많은 증명 의무(proof obligations)를 요구한다.

4. 연산적 대응성(Operational Correspondence)

저자들은 프로그램 수준의 mop 변환기와 확률적 프로그램의 연산 의미론으로서의 가산 상태, 유한 행동 MDP 사이의 엄격한 연결을 확립한다.

이들은 MDP를 위한 볼록 호어 파워도메인 상의 일반화된 **벨만 연산자(Bellman operator)**를 정의한다.
mop 변환기가 이 벨만 연산자의 최소 고정점과 정확히 일치함을 증명하며, 이는 거의 달성 가능한(almost achievable) 기대 보상 벡터의 집합을 특징짓는다. 이 대응 관계는 유한 상태를 가정하지 않고도 성립한다.

주요 기여

다목적 사전기대 변환기: 약한 사전기대를 다목적 설정으로 보수적으로 확장하는, 볼록 호어 파워도메인 상의 잘 정의되고 단조적이며 $\omega$ -연속적인 변환기인 mop을 도입하였다.
불변량 기반 추론: 불변량 기반 루프 추론을 다목적 설정으로 격상시켜, 상한 및 하한(dAST/dCT 조건 포함)에 대한 규칙을 제공하였다.
전략 합성: 증거가 되는 전략을 합성하는 규칙을 개발하였다. 본 논문은 순수 결정론만으로는 모든 파레토 최적점을 달성하기에 부족할 수 있지만, 혼합 결정론(순수 결정론들을 무작위화함)이 달성 가능한 집합의 스코트 폐쇄(Scott-closed) 볼록 껍질 내의 모든 점을 달성할 수 있음을 보여준다.
연산적 건전성: mop 변환기와 연산적 MDP 의미론 상의 일반화된 벨만 연산자 사이의 정확한 대응 관계를 증명하였다. 이는 기존의 유한 상태로 제한되었던 다목적 MDP 검증 결과들을 일반화한다.
사례 연구: 다음 세 가지 사례 연구에 기계론을 적용하였다:
- 로봇(Robot): 위험 대 속도의 트레이드오프를 다루며, 파레토 프런트 계산과 혼합 전략 합성을 보여준다.
- 카지노(Casino): 무한한 보상을 가진 도박 시나리오로, $\omega$ -불변량과 dAST를 이용한 추론을 보여준다.
- 큐(Queue): 적응형 서버 시스템으로, 변화하는 환경 파라미터 하에서 트레이드오프를 기호적으로 특징짓는 프레임워크를 보여준다.

결과 및 의의

본 논문은 mop이 무한 MDP에 대한 기호적, 프로그램 수준의 접근 방식을 제공한다고 주장한다.

완전성: 변환기는 거의 달성 가능한 점들의 집합을 정확하게 포착한다. 파레토 프런트는 이 집합의 경계로 식별된다.
합성 능력: 프레임워크는 특정 트레이드오프를 달성하는 전략(결정론)을 기계적으로 구성할 수 있게 하며, 이는 대상 점이 "노출(exposed)"되어 있거나(가중 합에 의해 최적화 가능) 그러한 점들에 의해 근사될 수 있는 경우에 해당한다. 노출되지 않은 점의 경우, 단일 가중 합을 통한 정확한 합성이 실패할 수 있지만, 해당 점은 노출된 점들에 의해 임의로 가깝게 근사될 수 있다(Straszewicz의 정리).
한계: 저자들은 정확한 최적 결정론의 존재를 위한 충분 조건(달성 가능한 집합의 스코트 폐쇄성)을 검증하는 것이 항상 쉽지는 않다는 점을 솔직하게 언급한다. 또한, 현재 프레임워크는 단순한 명령형 언어(pGCL)로 제한되어 있으며, 아직 프로시저, 재귀, 힙 조작 또는 연속 분포를 지원하지 않는다. 할인된 보상(discounted rewards)이나 장기 평균(long-run averages)과 같은 목적 함수도 현재 범위 밖이다.

요약하자면, 본 연구는 미분 가능한 프로그램 검증과 다목적 MDP 이론 사이의 간극을 메우며, 비결정론을 포함하는 확률적 프로그램에 대한 트레이드오프를 추론하기 위한 통합된 계산법을 제공한다.