dselsam/certigrad

Leverages formal verification in the Lean theorem prover to prove correctness of stochastic backpropagation and graph transformations (reparameterization, KL-divergence integration) with machine-checkable certificates. Constructs arbitrary stochastic computation graphs with random variable nodes, computing gradients via stochastic backpropagation while maintaining theoretical guarantees that match TensorFlow/Theano-style frameworks. Links with Eigen for matrix operations, achieving competitive performance on standard tasks like MNIST VAE training despite running as a proof-of-concept without ML-specific optimizations.

399 stars. No commits in the last 6 months.