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.
My goal is to produce verified code for a Seldonian algorithm validation test. This involves
(1) proving the underlying mathematics for a desired concentration bound or inequality to be used as the basis for a test,
(2) writing an algorithm for a validation test in HOL4,
(3) verifying that algorithm's correctness and tolerance given possible representation errors (numeric approximation, floating point roundoff),
(4) embodying that algorithm in code in a chosen language (e.g., CakeML's dialect of SML),
(5) and compiling that code with a verified compiler (e.g., CakeML's compiler).
Advisor: Eliot Moss