certigrad

Tech stack & purpose

Certigrad is a proof-of-concept system for developing machine learning software with formal correctness guarantees, specifically for optimizing stochastic computation graphs through verified implementation. The project uses the Lean theorem prover to construct formal specifications and machine-checkable proofs that the implementation satisfies its mathematical specification, including certified proofs of correctness for stochastic backpropagation and graph transformations. Built in Lean and interfacing with the Eigen library for tensor operations, Certigrad was developed by Daniel Selsam, Percy Liang, and David L. Dill at Stanford University, with support from the Future of Life Institute.

Community & reference links

• arxiv.org/abs/1706.08605
• github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/grads_correct.lean#L20-L27
• github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/mnist.lean#L44-L66
• github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/prog.lean#L16-L38
• github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/transformations.lean#L52-L57
• github.com/dselsam/certigrad/blob/master/src/certigrad/backprop_correct.lean#L13-L25
• github.com/dselsam/certigrad/blob/master/src/certigrad/kl.lean#L79-L90
• github.com/dselsam/certigrad/blob/master/src/certigrad/reparam.lean#L70-L79
• github.com/dselsam/lean/tree/certigrad
• github.com/leanprover/lean
• Lean Theorem Prover

Languages

Contributors

• 
  Daniel Selsam199 commits · 324 followers
• 
  amanvell1 commits · 3 followers