Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
8 points by Corbin
8 points by Corbin
Autoformalisation is increasingly used to verify mathematical texts, including those generated by AI, as in OpenAI's announced proof of blow-up of solutions to the Navier-Stokes equations. In this process, an AI system translates the text from a natural language (NL) into a formal language such as Lean. Once this translation is done, the argument expressed in the formal language can easily be mechanically verified. The purpose of this article is to demonstrate why this process may offer no confidence in the original NL argument, owing to the various difficulties in performing the translation semantically faithfully. In particular, we highlight that the problem of resolving ambiguities in mathematical NL text, which is necessary in order to provide semantically faithful translation, is arbitrarily high up in the Solvability Complexity Index (SCI) hierarchy/arithmetical hierarchy (the SCI = ∞). Hence, informally, providing semantically faithful AI autoformalisation is harder than any computational problem including the Halting problem (which has SCI = 1). To demonstrate the effect of this result we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean "verifications". These include OpenAI's announced Navier-Stokes proof. In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.
I think this paper also misses that if an LLM can exploit a bug in Lean, it will.
They're just optimizers that are driving towards maximizing a goal. If they're plugging along and they get incorrect output from Lean, they'll happily use that as a tool to solve the proof.
So if you have a million-line-long Lean proof of something, you're faced with not ever being quite certain that there isn't some "...and then a miracle occurs..." exploit of Lean somewhere in the middle of it.
The one buggy AI Lean proof I’m aware of was a case where someone found a soundness bug in Lean (with or without AI, I’m not sure) then announced the Collatz conjecture to be proved using that bug they found. It was understood to be buggy within a day.
Are there other cases I’m not aware of where an announced proof was found to be based on exploiting a Lean bug?
Obviously unsoundness in the Lean kernel is an issue (which we can't rule out), but I agree with my sibling commenter that this seems quite unlikely to be missed assuming there is a reasonable effort to review the proof. I'm not a Lean expert, but I do formal methods (and know Lean experts myself) and my intuition is that soundness exploits will look something like deriving false. I'm not saying it's trivial to detect something like this (mumble mumble undecidability), but I do think it will smell.
An example of what I mean is if you have a function in Haskell foo :: Enormous -> () whose input is some really complicated type. And you see something like
bar = foo x
-- this is an infinite loop, so it can have any type
where x = let y = y in y
Note also that the paper makes no claims about the invalidity of the Lean proof itself, but only of the mismatch between NL and Lean. Frankly it would be a feat almost as impressive as the N-S proof (which I understand to be enormous) if the Lean translation was 100% faithful to the NL (due to size).
TL;DR: IMO this paper and the possibility of unsoundness should not be taken as evidence that "LLMs can't do proofs." Especially for gargantuan proof artifacts, the only way I would want to interact with a sizable LLM proof is via a theorem prover precisely because NL proofs have no way to rigorously and systematically check them.
Let it be known that I was saying two years ago that LLMs should be amazing at doing proofs precisely because they're machine-checkable (they sucked at proofs during this time). Judging from what the mathematicians are saying I'm not exactly thrilled to be proven right.
I've been wondering if that proof used the Kobayashi Maru method. Glad to see others seriously considering that possibility.