# Developing Bug-Free Machine Learning Systems With Formal Mathematics

arXiv: https://arxiv.org/abs/1706.08605 · HTML: https://mlsanity.com/paper/1706.08605/

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Jun 2017.

## Built on by (most cited first, 14 of 14)

- [Explanation-Based Human Debugging of NLP Models: A Survey](https://mlsanity.com/paper/2104.15135/) (2021)
- [Outlining Traceability: A Principle for Operationalizing Accountability in Computing Systems](https://mlsanity.com/paper/2101.09385/) (2021)
- [Automatic Fault Detection for Deep Learning Programs Using Graph Transformations](https://mlsanity.com/paper/2105.08095/) (2021)
- [Formalization of a Stochastic Approximation Theorem](https://mlsanity.com/paper/2202.05959/) (2022)
- [Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq](https://mlsanity.com/paper/2301.12893/) (2023)
- [Testing Feedforward Neural Networks Training Programs](https://mlsanity.com/paper/2204.00694/) (2022)
- [Formalized Hopfield Networks and Boltzmann Machines](https://mlsanity.com/paper/2512.07766/) (2025)
- [ExAIS: Executable AI Semantics](https://mlsanity.com/paper/2202.09868/) (2022)
- [Formally Verified Approximate Policy Iteration](https://mlsanity.com/paper/2406.07340/) (2024)
- [Formal Methods for the Informal Engineer: Workshop Recommendations](https://mlsanity.com/paper/2104.00739/) (2021)
- [Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes](https://mlsanity.com/paper/2206.02169/) (2022)
- [Budget-Sensitive Discovery Scoring: A Formally Verified Framework for Evaluating AI-Guided Scientific Selection](https://mlsanity.com/paper/2603.12349/) (2026)
- [Structural Sensitivity in Compressed Transformers: Relative Error Propagation and Layer Removal](https://mlsanity.com/paper/2603.20991/) (2026)
- [Masked Attention Pooling Is Invariant to Padding and Permutation: A Formal Proof in Lean](https://mlsanity.com/paper/2610.17132/) (2026)

## Abstract (arXiv)

Noisy data, non-convex objectives, model misspecification, and numerical instability can all cause undesired behaviors in machine learning systems. As a result, detecting actual implementation errors can be extremely difficult. We demonstrate a methodology in which developers use an interactive proof assistant to both implement their system and to state a formal theorem defining what it means for their system to be correct. The process of proving this theorem interactively in the proof assistant exposes all implementation errors since any error in the program would cause the proof to fail. As a case study, we implement a new system, Certigrad, for optimizing over stochastic computation graphs, and we generate a formal (i.e. machine-checkable) proof that the gradients sampled by the system are unbiased estimates of the true mathematical gradients. We train a variational autoencoder using Certigrad and find the performance comparable to training the same model in TensorFlow.