PhD Thesis Defense: Jared Yeager, Machine Checked Verification of Validation Tests for Seldonian Algorithms Machine Checked Verification of Validation Tests for Seldonian Algorithms

Content

Abstract

Seldonian algorithms are a class of algorithms that either return a (usually machine learned) model that meets specified safety conditions with specified probability, or return “no solution found”. One fairly natural way to make a Seldonian algorithm is to take an existing algorithm and subject its output models to some safety validation test(s). This validation testing serves as a filter that lets through only models that satisfy the tests, returning “no solution found” otherwise.

In this work we produce verified code for a Seldonian algorithm validation test. This involves (1) proving the underlying mathematics for a Hoeffding’s-inequality-based concentration inequality to be used as the basis for a test, (2) writing an algorithm for the validation test in HOL4, (3) verifying that algorithm’s correctness and tolerance given representation errors of arbitrary precision rationals under operations like square root, (4) embodying that algorithm in code in CakeML’s dialect of SML, (5) and compiling that code with CakeML’s verified compiler.

Advisor

Eliot Moss

Host

Jared Yeager