difficultyang retweeted
The big recent progress is the RLibM project, which yes uses exhaustive checking, plus LP to synthesize polynomials. The CORE-MATH project is doing correctly rounded impls for major scalar functions. Softmax is a bit harder because many inputs, so lotta bits
I would really love if there was a consolidated survey on this somewhere! My vibe is "exhaustive checking is not that hard" is the general approach people have gotten to
Low-background YouTube Music is music produced before 2026, the date when AI generated music became good enough to mass proliferate across the catalog.
Anyway. I'm super excited about all of the formal verification projects popping up, at PyTorch HQ we're trying to figure out what exactly we want to do in this space, but I've also been doing a lot of FM educating recently. Hope this helps the discourse!
It is probably possible to prove something along these lines! But what exactly is the theorem you want to prove? If you tried to prove absolute error ≤ 10⁻⁷, well, that will admit the buggy implementation! There's a reason your theorem statements are considered "trusted".
However, AFAICT, there was no FP theorems added, so there's no proof that the new implementation actually fixes the FP precision problem that was claimed to be fixed.
The fix commit switches over to the stable formulas. The (rightly!) requires adjusting the existing real number proofs, since you're now proving things about a different mathematical formula, but not the statements themselves which remain true (good!)
(Aside: There actually is one theorem about tensors containing floating point numbers but it's "did we define CE correctly".)
Real numbers are nice and beautiful and mathematicians love proving theorems with them and it will never tell you anything about the log softmax problem, which is entirely an artifact of floating point representation.
It also proved some theorems about logSoftmax, like that the stated JVP is correct and the conventional numerical stability algebraic rewrite is correct. But importantly, these theorems were all proved on tensors handling REAL numbers.
LeanTorch implemented ops in Lean. Implementing an algorithm in a theorem proving capable language certainly gives you some guarantees, e.g., it is terminating (if you didn't use "partial"), it is well-typed (this can mean a lot with fancy dependent types). Not bug free!
A naive understanding of formal verification might be something like, "Well, if I do it in Lean, then it can't have bugs." WDYM "do it"? WDYM "can't have bugs"? This is entirely the question.
So the log_softmax bug arxiv.org/abs/2610.31642 that's been making the rounds. TorchLean also had the same problem (fixed in github.com/lean-dojo/TorchLe…). How come? This example is pretty illustrative of the proper mindset you need when working on formal verification. 🧵
