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
Low-background YouTube Music is music produced before 2026, the date when AI generated music became good enough to mass proliferate across the catalog.
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.
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".
(Aside: There actually is one theorem about tensors containing floating point numbers but it's "did we define CE correctly".)
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.
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. 🧵
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.
arxiv.org/pdf/2609.34272v1 I am annoyed that I have to read this but the abstract (at least) is LLM slop text