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).


[Skip to Readme]

Modules

  • ApplicativeBins
    • ApplicativeBins.Bins
    • ApplicativeBins.Theorem
  • Bins
    • Bins.Bins
    • Bins.Theorem
  • Data
    • Data.Derivative
    • Data.Dist
    • Data.List
  • Examples
    • Examples.ExpDist
  • Misc
    • Misc.ProofCombinators
  • Monad
    • Monad.PrM
      • Monad.PrM.Laws
      • Monad.PrM.Predicates
      • Relational
        • TCB
          • Monad.PrM.Relational.TCB.EDist
          • Monad.PrM.Relational.TCB.Spec
        • Monad.PrM.Relational.Theorems
  • 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

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1.0.0, 0.1.0.1
Change log ChangeLog.md
Dependencies 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]
License BSD-3-Clause
Copyright 2020-21 Lisa Vasilenko & Niki Vazou, IMDEA Software Institute
Author Lisa Vasilenko, Niki Vazou
Maintainer Lisa Vasilenko <vasilliza@gmail.com>
Category Formal Methods
Home page https://github.com/nikivazou/safe-coupling
Bug tracker https://github.com/nikivazou/safe-coupling/issues
Source repo head: git clone https://github.com/nikivazou/safe-coupling
Uploaded by oquechy at 2022-06-15T20:05:28Z
Distributions
Downloads 152 total (2 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2022-06-15 [all 2 reports]

Readme for safe-coupling-0.1.0.1

[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. Install stack https://docs.haskellstack.org/en/stable/install_and_upgrade/

  2. Compile the library and case studies

     $ cd safe-coupling
     $ stack install --fast
     ...
     Registering library for safe-coupling-0.1.0.0..
    
  3. 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