LLMs are dead for formal verification. But is treating…
0 reactions
LLMs are dead for formal verification. But is treating software correctness as a thermodynamics problem actually mathematically sound?
We spent the last few years treating code generation like a glorified Markov chain. Now, the pendulum is swinging violently towards formal methods, but with a weird twist: treating program synthesis like protein folding.
Think about AlphaFold. It didn’t "autoregressively" predict the next atom’s position; it used energy minimization to find the most stable 3D structure. The massive $1B seed round for Yann LeCun's new shop, Logical Intelligence https://logicalintelligence.com/ (context from Bloomberg https://www.bloomberg.com/news/articles/2026-03-10/yann-lecun-s-new-ai-startup-raises-1-billion-in-seed-funding ), suggests the industry is about to apply this exact Energy-Based Model (EBM) architecture to formal verification.
Instead of guessing the next token, the premise is to define a system's mathematical constraints and have the model minimize the "energy" until it settles into a state that represents provably secure code.
My take - it’s a theoretically beautiful analogy, but I think it fundamentally misrepresents the nature of computation. Biology has smooth, continuous energy gradients. Software logic does not.
Under the Curry-Howard correspondence, programs map to proofs. But the state space of discrete logic is full of infinite cliffs, not smooth valleys. An off-by-one error doesn't just slightly increase the "energy" of a function - it completely destroys the proof. EBMs require continuous latent spaces, but formal logic is inherently rigid and non-differentiable.
Are we just throwing $1B of compute at the Halting Problem and hoping a smooth gradient magically appears?
#technology
source
We spent the last few years treating code generation like a glorified Markov chain. Now, the pendulum is swinging violently towards formal methods, but with a weird twist: treating program synthesis like protein folding.
Think about AlphaFold. It didn’t "autoregressively" predict the next atom’s position; it used energy minimization to find the most stable 3D structure. The massive $1B seed round for Yann LeCun's new shop, Logical Intelligence https://logicalintelligence.com/ (context from Bloomberg https://www.bloomberg.com/news/articles/2026-03-10/yann-lecun-s-new-ai-startup-raises-1-billion-in-seed-funding ), suggests the industry is about to apply this exact Energy-Based Model (EBM) architecture to formal verification.
Instead of guessing the next token, the premise is to define a system's mathematical constraints and have the model minimize the "energy" until it settles into a state that represents provably secure code.
My take - it’s a theoretically beautiful analogy, but I think it fundamentally misrepresents the nature of computation. Biology has smooth, continuous energy gradients. Software logic does not.
Under the Curry-Howard correspondence, programs map to proofs. But the state space of discrete logic is full of infinite cliffs, not smooth valleys. An off-by-one error doesn't just slightly increase the "energy" of a function - it completely destroys the proof. EBMs require continuous latent spaces, but formal logic is inherently rigid and non-differentiable.
Are we just throwing $1B of compute at the Halting Problem and hoping a smooth gradient magically appears?
#technology
source
| 2,000 mlx | |
| 2 | |
| 0 |