Safe Couplings: Coupled Refinement Types

Vasilenko, Vazou, Barthe, [2022] “Safe Couplings: Coupled Refinement Types”

https://nikivazou.github.io/static/drafts/safe-couplings.pdf

presenter: Lisa

1. Introduction

refinement types + relational logic

relational refinement types offer limited support to reason about programs with diverging control-flow (non-syntax-directed)

2. Overview

2.1 The Probability Distribution

PrM probabilistic monad (wrapper)

bins running example

2.2 Relational Specifications & Lifting

stochastic dominance

reuses probabilistic couplings (probabilistic equivalent of cartesian products) in the form of “diamond”

2.3 Relational Proofs

2.4 Quantitative Specifications and Kantorovich lifting

Kantorovich metric - distance on distributions

2.5 Distance Proofs

uses “ghost” functions to split out one step

3. Implementation of safe-coupling

3.1 Liquid Haskell Preliminaries

3.2 Data.Dist: Definition of Distance

3.3 Monad.PrM: Definition of the Probabilistic Monad

3.4 TCB.Axioms: Assumption of Relational Axioms

3.5 TCB.Dist: Assumption of Distance Specifications

3.6 Theorems: Proof of Relational Properties

4. Case studies

4.1 Case Study I: Convergence of TD(0)

Temporal Difference, classical algorithm for Reinforcement Learning

4.2 Case Study II: Stability of SGD

convergence + sensitivity

4.3 Quantitative Summary

5. Proof system

5.1 Syntax

5.2 Type system

5.3 Axioms

5.4 Proof System

5.5 Denotational Semantics

5.6 Soundness

5.7 Continuous distributions

works only for discrete distributions, QBS?

7. Conclusion & future work

verify implementation, more automation