# safe-coupling: Relational proof system for probabilistic algorithms

[ bsd3, formal-methods, library ] [ Propose Tags ]

Relational proof system for probabilistic algorithms. Supports two proving methods: upper bound Kantorovich distance between two distributions and establish a boolean relation on samples from two distributions (the latter is stronger).

## Modules

• ApplicativeBins
• ApplicativeBins.Bins
• ApplicativeBins.Theorem
• Bins
• Bins.Bins
• Bins.Theorem
• Data
• Data.Derivative
• Data.Dist
• Data.List
• Examples
• Examples.ExpDist
• Misc
• Misc.ProofCombinators
• Relational
• TCB
• SGD
• SGD.SGD
• SGD.Theorem
• TD
• Lemmata
• Relational
• TD.Lemmata.Relational.Act
• TD.Lemmata.Relational.Iterate
• TD.Lemmata.Relational.Sample
• TD.Lemmata.Relational.Update
• TD.TD0
• TD.Theorem

#### Maintainer's Corner

For package maintainers and hackage trustees

Candidates

• No Candidates
Versions [RSS] 0.1.0.0, 0.1.0.1 ChangeLog.md liquid-base (>=4.14.0 && <4.16), liquid-containers (>=0.6.2 && <0.7), liquid-prelude (>=0.8.10 && <0.9), liquidhaskell (>=0.8.10 && <0.9), probability (>=0.2.7 && <0.3), rest-rewrite (>=0.1.1 && <0.2) [details] BSD-3-Clause 2020-21 Lisa Vasilenko & Niki Vazou, IMDEA Software Institute Lisa Vasilenko, Niki Vazou Lisa Vasilenko Formal Methods https://github.com/nikivazou/safe-coupling https://github.com/nikivazou/safe-coupling/issues head: git clone https://github.com/nikivazou/safe-coupling by oquechy at 2022-06-15T20:05:28Z NixOS:0.1.0.1 38 total (2 in the last 30 days) 2.0 (votes: 1) [estimated by Bayesian average] λ λ λ Docs not available All reported builds failed as of 2022-06-15

[back to package description]

# safe-coupling

Library for relational verification of probabilistic algorithms.

Supports two proving methods:

• Upper bound Kantorovich distance between two distributions
• Establish a boolean relation on samples from two distributions (this is stronger)

Includes two larger examples of verification:

• Stability of stochastic gradient descent (src/SGD) using Kantorovich distance
• Convergence of temporal difference learning (src/TD0) using boolean relations

## A smaller example (src/Bins/Bins.hs)

This function recursively counts how many times the ball hit the bin after n attempted throws:

bins :: Double -> Nat -> PrM Nat
bins _ 0 = ppure 0
bins p n = liftA2 (+) (bernoulli p) (bins p (n - 1))


Throws succeed with probability p which is simulated by bernoulli p. The function returns a distribution over natural numbers. When comparing results of two throwers with respective chances of success p and q > p, we expect the second thrower to score notably better with the increase of n. Formally, we can show that Kantorovich distance between bins p n and bins q n is upper bounded by (q - p)·n.

## Proof (src/Bins/Theorem.hs)

The proof uses four definitions from the library:

• In the first case, no throws were made. Axiom pureDist allows deriving Kantorovich distance between pure expressions. In our case, 0 and 0.
• In the second case, axiom liftA2Dist derives Kantorovich distance between the inductive cases. Numeric arguments specify the expected bound in format a·x + b·y + c where x and y are bounds for the second and third arguments of liftA2 respectively. As the last argument, the axiom requires proof of linearity of plus. It is empty since it can be automatically constructed by an SMT-solver.
• Axiom bernoulliDist upper bounds the distance between calls to bernoulli with q - p — this is our x. The second upper bound y is provided by a recursive call to our theorem.

* A function distInt is used to measure the distance between arguments of liftA2. In this case, all of them provide integer values. A pre-defined distance between n and m is |n - m| but this allows customization.

{-@ binsDist :: p:Prob -> {q:Prob|p <= q} -> n:Nat
-> {dist (kant distInt) (bins p n) (bins q n) <= n * (q - p)} / [n] @-}
binsDist :: Prob -> Prob -> Nat -> ()
binsDist p q 0 = pureDist distInt 0 0
binsDist p q n
= liftA2Dist d d d 1 (q - p) 1 ((n - 1) * (q - p)) 0
(+) (bernoulli p) (bins p (n - 1))
(+) (bernoulli q) (bins q (n - 1))
(bernoulliDist d p q)
(binsDist p q (n - 1))
(\_ _ _ _ -> ())
where
d = distInt


This concludes the mechanized proof of the boundary (q-p)·n.

## Installation

1. Compile the library and case studies

 $cd safe-coupling$ stack install --fast
...
Registering library for safe-coupling-0.1.0.0..

2. Run unit tests on executable case studies

 $stack test ... test/Spec.hs Spec Bins mockbins 1 it: OK mockbins 2 it: OK bins 1 it: OK bins 2 it: OK (0.02s) exp dist mockbins: OK (0.12s) SGD sgd: OK TD0 td0 base: OK td0 simple: OK All 8 tests passed (0.12s) safe-coupling> Test suite safe-coupling-test passed Completed 2 action(s).  In case of errors try $ stack clean