Hacker News Reader

LLMs are fundamentally probabilistic in nature; I think you could prove things about distributions of outputs but nothing like the kind of formal verification you can create with Lean or Rust.

There’s a few papers in this space but it’s still early days, both using Formal Verification to test outputs of LLMs and using LLMs in formal verification itself

Examples of both:

https://sumitkumarjha.com/papers/2023_ICAA_LLM_Dehallucinati...

https://mathai2023.github.io/papers/28.pdf

An LLM is pretty much a black box. You can’t prove anything meaningful about its output.

You are really comparing apples to oranges here, and to say that trying to apply formal verification to a probabilistic lying machine is silly would be a colossal understatement.

Isn't it a fundamental limitation of LLMs that we can't?

Obviously not. It's right in the name, isn't it? LLM = limitless model...