Safe couplings: coupled refinement types

Abstract

We enhance refinement types with mechanisms to reason about relational properties of probabilistic computations. Our mechanisms, which are inspired from probabilistic couplings, are applicable to a rich set of probabilistic properties, including expected sensitivity, which ensures that the distance between outputs of two probabilistic computations can be controlled from the distance between their inputs. We implement our mechanisms in the type system of Liquid Haskell and we use them to formally verify Haskell implementations of two classic machine learning algorithms: Temporal Difference (TD) reinforcement learning and stochastic gradient descent (SGD). We formalize a fragment of our system for discrete distributions and we prove soundness with respect to a set-theoretical semantics.

Document Details

Document Type
Pub Defense Publication
Publication Date
Aug 29, 2022
Source ID
10.1145/3547643

Entities

People

  • Elizaveta Vasilenko
  • Gilles Barthe
  • Juan De La Cierva
  • Niki Vazou

Organizations

  • Instituto Madrileño de Estudios Avanzados
  • Office of Naval Research

Tags

Fields of Study

  • Computer science

Readers

  • Neural Network Machine Learning.
  • Operations Research
  • Theoretical Analysis.

Technology Areas

  • AI & ML
  • AI & ML - Bayesian Inference
  • AI & ML - Machine Learning Algorithms