TinyTorch, formally verifiable

[sueszli]

Project: https://github.com/sueszli/autograd.lean/

Hi everyone!

After hacking together a C version of TinyTorch¹, I ported my code to Lean, partly to see if I could formally verify the backward kernels, but mostly as an excuse to learn the language.

Along the way I reimplemented microGPT inside it, which helped me understand GPT internals and how to prove properties about gradient computations.

It's not particularly performant, but it has been a very fun exercise in thinking rigorously about autodiff.

I'm very grateful to Prof Reddi and the TinyTorch community for the material and inspiration!

Footnotes

1. https://github.com/harvard-edge/cs249r_book/discussions/1080 ↩

[Shashank-Tripathi-07]

Simply Lovely !!

[sueszli]

Thank you so much! :)

[profvjreddi]

Yea, this is pretty neat. This gave me some new ideas though they haven't settled 🤔 enough to share.

[sueszli]

Very glad it resonated with you!