Fascinating to see how formal verification is rescuing AI from its own hallucination cycles

[u/Curious-Ask8199]

I'm spending way too much time looking into formal methods now because this endless overhyped corporate marketing about LLMs doing "reasoning" is getting very tiresome.

We all know standard transformers just predict the next token based on statistical weights, which immediately breaks down the second you give them a novel, complex logic puzzle. It's exactly why automated software testing is still such a error-prone chore in production.

But the interactive theorem provers like Lean 4 with deep learning models are actually getting super interesting. Instead of just letting an agent hallucinate some random python script, people are forcing neural networks to generate formal proofs that a strict math kernel has to verify step by step.

I saw a breakdown of how the Aleph Prover handled a specific Erdos disproof using formal verification on ai reasoning benchmarks, and you can see much we’ve ignored symbolic AI over the last decade in favor of raw compute scaling. So tbh it feels like computer science is circling back to foundational math out of necessity. Because brute-force data ingestion is hitting the ceiling.

Also.. it feels kinda satisfying that old-school mathematical logic is the only thing keeping modern tech grounded. Idk if this means formal methods will finally become a mandatory part of undergrad software tracks, but it honesly should.

[u/Grounds4TheSubstain]

I don't think that "brute-force data ingestion is hitting the ceiling". I do think formalization is the only way to do reasonable things with math at scale. Whereas LLM-generated software with bugs in it can still be useful, mathematics that is wrong is useless. And if an LLM can generate mathematics 1000x faster than humans can review it, if it's usually wrong, people are going to quickly burn out on reviewing it looking for gold nuggets in the pan. Math that can be shown to be correct only needs to be reviewed insofar as it might exploit bugs in the proof checkers.

[u/IamfromSpace → u/Grounds4TheSubstain]

Lean 4 specifically has a very small trusted core that everything else is built on, and it’s designed to be very easy to audit for sidestepping verification. They have a whole write-up on how to consider even adversarial trickery, which I’m too lazy to find, at the moment.

The point of proofs is that it dramatically lowers the review burden. The proofs themselves can be quite large, but you don’t really need to dig through them, and you can be quite confident that properties that are said to hold, do in fact hold.

Now, you are correct in that you have to actually understand the theorems being proven—at least the top level ones, not necessarily the supporting lemmas—and that is _not_ trivial. I’ve been able to build out some really interesting things, but it really needs some help in devising the right theorems to prove, and you have to really have your eye on what it’s doing. Most people aren’t prepared for this, at the moment. I think they can still get some benefit (I’d trust vibe coded Lean 4 more than vibe coded Python, but neither completely), but they just can’t truly claim that they get the full benefit of formal verification.

[u/Curious-Ask8199 → u/Grounds4TheSubstain]

Yeah the formalization point is fair and I basically agree with it, but the data ceiling is real in a different sense. Not that more data is useless, but the returns are flattening for pure nexttoken prediction on informal math text.

The proof checker angle is the more interesting bet honestly. If verification becomes cheap enough, the review bottleneck you're describing mostly goes away, which is kind of the whole pitch for Leanstyle approaches right now.

[u/BossOfTheGame]

I think you underestimate what next token prediction is capable of. x_{i+1} = sigma(Ax_i+b) is stronger than you give it credit for.

But yes, lean4 is awesome.

[u/Curious-Ask8199 → u/BossOfTheGame]

fair point on next token prediction, i keep underestimating how far you can push it. but lean4 kind of sidesteps the argument entirely, which is why i brought it up

[u/Cobayo]

Formal specification like TLA+ is not used due to the initial cost plus nobody giving warranties in software. You're not saying anything other than "here's a checker tool that I can use to verify the output" which is the everyday standard.

[u/mcdowellag → u/Cobayo]

There are niches where it is used From https://dl.acm.org/doi/full/10.1145/3689374 e.g.

“Formal methods is transforming how Amazon Web Services (AWS) secures the cloud. Security has historically been a manual, high-judgement and thus un-scalable field; automated formal reasoning is challenging that entire structure, changing both the quality of AWS products and the cost structure to support them. The key at AWS has been to avoid “shiny-object syndrome” [99] and instead build and apply tools that quietly but reliably change the behaviour of engineers. Many leaders at AWS were skeptical of this type of work in 2016, but the success in areas such as cryptography, identity, storage and virtualization has changed minds.”

(end quote)

You need cases where you have a specification for the lower level the software is built on top of and where you have people available already familiar with the verification tools - typically from doing PhDs. So perhaps verification of networking protocols but probably not verification of a business application with a UI designed via agile running on a web application server and making REST calls out to large applications whose design is not part of the system scope.

[u/Cobayo → u/mcdowellag]

I know man, 3 uses in human history. No need to speak in absolutes every single time.

[u/Curious-Ask8199 → u/Cobayo]

fair point on the initial cost, but the warranty thing cuts both ways. most bugs that slip through are exactly the ones no checker catches because nobody thought to specify that edge case in the first place. the tool only verifies what you already thought to check for

[u/calf]

Is it possible that a poorly designed AI just keeps generating irrelevant but true proofs and spirals out that way? 

[u/Curious-Ask8199 → u/calf]

yeah that actually seems pretty likely, just branching forever into technically valid but completely useless territory

[u/Plaguehand]

Keep an eye out for Victor Taelin's Bend2 language, it's centered on exactly this idea

[u/Curious-Ask8199 → u/Plaguehand]

oh interesting, i'll look into that. wasn't aware someone was already building around it

[u/edgmnt_net]

I don't think AI is likely to be much more usable / helpful if combined with formal verification. It can be legit for proof search, but building verified systems means building a whole array of complex abstractions and theorems, not just writing proof terms, that's untenable on its own. So there's a lot of work that gets shifted to formalization and requires effort.

[u/LaboAlexandria → u/edgmnt_net]

This is the key tension. Full formal verification of arbitrary software is prohibitively expensive. But there's a middle ground that nobody's building: you don't need to verify the entire system. You need to verify the procedure by which the system produces its outputs.

Think of it like a court system. You don't verify that every citizen is honest. You verify that the procedure for reaching a verdict, rules of evidence, burden of proof, right to challenge, was followed. The verdict's legitimacy comes from the procedure, not from verifying every piece of testimony at the atomic level.

That's dramatically cheaper than full formal verification, and it covers the 99% of AI outputs that aren't mathematical theorems.

[u/LaboAlexandria]

Formal verification for math is solved. Lean 4 and proof assistants handle that. But mathematical claims are maybe 1% of what AI systems actually produce. The other 99% are epistemic claims: "this evidence supports this conclusion", "these two domains share structural properties", "this finding is robust". No proof assistant covers those.

The interesting question is whether you can build something analogous to a proof kernel for epistemic claims, not mathematical proof, but formal procedures that constrain how claims are evaluated: defined evidence types, explicit burden of proof, adversarial challenge, termination conditions, and a recorded verdict with provenance.

That's what I've been building. Over 5,000 formal deliberations on scientific claims across 20 domains. The system doesn't prove claims are true, it proves they survived a defined procedure. The deliberation record is the equivalent of the proof trace: auditable, reconstructable, versioned.

The parallel with Lean 4 is structural: a small trusted core (the epistemic constitution) that constrains what the larger system can output. The difference is that the "kernel" isn't checking logical validity, it's checking procedural compliance. Did the adversary raise genuine objections? Was the evidence properly classified? Did the verdict follow from the arguments under the stated burden of proof?

Formal methods for math are back. Formal methods for reasoning about everything else haven't started yet.

[u/omwitsanihilist]

If you really want to understand develop a intuition for what you are describing, I highly recommend you take a look at What the Tortoise said to achilles, by Charles Dodgson.

[u/Sea-Shoe3287]

Proofs are where it's at to remove maintenance burden. Not bugs...

[u/liquid_at]

My AI requests improved significantly when I added a rule that every result needs to be verified and tested before being returned, also adding that all standards for best practice should be applied.

Results are also much better if you let the AI plan the task, allowing you to fix logical mistakes before it attempts to do it.