Here's my vision for verification in AI. Some examples I've been working on :)
* I wrote most of these posts, with some AI assistance in the prose and Lean code.
01 / Inference
The same prompt can get a different answer when the batch changes. I wanted to understand why. We start with three numbers, follow the rounding through the calculation, and prove when a score change preserves the winning token.
Try the two addition orders →02 / Circuit verification
Neel Somani uses circuits and an SMT solver to check a small transformer. I brought its checkpoint into Lean so we could check the exported decisions for all 256 task inputs and recompute them from the weights.
Follow the model, circuits, and checks →03 / Training
Let's train a GPT in Lean :) I trained a 124.4-million-parameter model on one A100, then compared fifty matched updates with PyTorch. The loss improved; turning it into a dependable assistant proved harder.
Alongside the run, we prove results about next-token targets, resuming training, and reusing the attention cache during generation.
Read the experiment →04 / Tensor programming
I'd like to write a tensor calculation in Lean and choose the device when I run
it. We try the custom-function API, build attention with einsum,
and look at the performance measurements. Higher derivatives and binary128
arithmetic let us try other calculations too.
05 / Kimi K3
I wanted to bring the paper-and-proof approach from research mathematics to ML. With K3's report open beside us, we work through its memory, attention, and experts, prove that streaming preserves the logits, and find an endpoint error in the expert-balancing argument.
Open the annotated report →06 / Nemotron
After K3, I wanted to look at NVIDIA's Nemotron and its recurrent memory. Recomputing recent inputs lets it save the state less often. We prove when that replay preserves the state, then check a case where fewer rounded writes leave a larger final error.
Read the state-cache experiment →