Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Postmortem for Kernel Soundness Bug #14576

leodemoura.github.io

Post reply on HN
Print view View original

31–40 of 68 posts

Re: Postmortem for Kernel Soundness Bug #14576

#31

Post by daishi55 »

Zsfe510asG wrote: post #15
adw wrote: post #11

Earlier quoted context omitted.

What is the error rate of human programmers? Anyone who tells you that either human or A.I. code is magically exempt from issues is selling you something.

There are humans who make very few mistakes. The presence of Claude in a project however tells you something about the attitude of the project: - Probably too close to corporations. - Does not care about slop. We have seen many projects that adopted AI under corporate pressure circle the drain. Often the corporations themselves backpedaled after some months.

> There are humans who make very few mistakes

Mmm there are humans who think they make very few mistakes. Ones who actually make few mistakes, not sure about that one. Could be a mistake that they catch themselves very quickly, but I just don’t think humans are very good at generating 100% reliable output on the first try anywhere close to most of the time.

Re: Postmortem for Kernel Soundness Bug #14576

#33

Post by jonathrg »

IsTom wrote: post #13
cperciva wrote: post #9

Earlier quoted context omitted.

A counterexample of the form "X cycles to X after N steps" is easy to check. A counterexample of the form "starting with X we keep going up forever" is hard to check in finite time.

And still that requires X to not be particularly large. It could conceivably be in ballpark of BB(40).

This feels like saying there are probably hundreds of stars in the universe

Re: Postmortem for Kernel Soundness Bug #14576

#34

Post by xelxebar »

derdi wrote: post #20
michaelfm1211 wrote: post #18

Reminds me of this: https://mathoverflow.net/questions/513742/are-we-stuck-with-... I know this is an implementation bug not a meta-theory bug, but I'd almost consider the fact soundness bugs are possible as a bug in the ideology, or at least a severe drawback. Stuff like this just wouldn't happen in Metamath. In a future where AI is autogenerating formalizations, why not have the AI use a harder but airtight system…

Took me about 90 seconds to find a Metamath implementation bug that apparently allowed proving something that shouldn't be provable: https://github.com/metamath/metamath-exe/issues/184

That's with the original C verifier only. The actual database is cross-checked by 6 independent implementations. This is the whole point of Metamath: its kernel is so tiny that you can implement a verifier in a weekend.

Metamath isn't a silver bullet in the design space of formal proof tools, but I personally think it just about nails the metatheory we want. Maybe some explicit facility around definitions would be desireable.

Re: Postmortem for Kernel Soundness Bug #14576

#35

Post by xelxebar »

de_aztec wrote: post #4

So essentially: One cannot trust the code produced by an LLM, even if the code is a formal proof passing the verifier.

I would expect proofs that exploit kernel bugs to look fishy, so someone reading the proof could catch the smell.

That said, I'm sure there's also room for underhanded Lean programming as well, which would be even more interesting.

Re: Postmortem for Kernel Soundness Bug #14576

#36

Post by Gehinnn »

Has there ever been a bug that allowed to prove a previously unproven statement, without allowing the user to prove "false" by exploiting the bug directly?

If every bug-exploiting proof would make it easy to prove false, putting a bounty on proving false could increase trust in the validity of verified but obscure Lean proofs.

Re: Postmortem for Kernel Soundness Bug #14576

#37

Post by jojomodding »

remywang wrote: post #6

Isn’t a disproof of the Collatz conjecture easy to check as it should just be a counterexample? Or is the proof not constructive?

No, Lean allows non-constructive proofs so a proof could be like "if the Riemann hypothesis is true the counterexample is 42 otherwise it is the first nontrivial zero" or something like this, and then you don't get a fully closed counterexample.

Re: Postmortem for Kernel Soundness Bug #14576

#38

Post by estherney »

Gehinnn wrote: post #36

Has there ever been a bug that allowed to prove a previously unproven statement, without allowing the user to prove "false" by exploiting the bug directly? If every bug-exploiting proof would make it easy to prove false, putting a bounty on proving false could increase trust in the validity of verified but obscure Lean proofs.

We want Lean4 (or any other deduction system that we use, for that matter) to be correct, i.e. "what is a true statement" and "what is a derivable statement" should be the same.

"every statement that can be derived also holds" is the difficult part to show, and something we refer to as soundness. For some fancy logics, it's not even possible to show, hence the discovered Kernel Soundness Bug in Lean!

"every statement that holds can also be derived", a notion known as completeness, is often a trivial property; in practice, we use refutation completeness instead, i.e. "every statement that doesn't hold can derive false". A bug that would allow a user to prove/derive a previously unproven statement would fall under this category of "completeness bug".

However, such completeness bugs immediately show up in testing. Generally, deduction systems have two kinds of rules: a handful of rules that are enough to establish (refutation) completeness, and then a few extra rules to optimize inference. Because so few rules are needed for completeness, lots of test cases will break if one of the rules break.

--

I'm not actually sure how the completeness situation looks like for proper provers like Lean. It's my graduate student's hubris to assume completeness remains easy to show for more advanced systems than the Superposition calculus ;)

Re: Postmortem for Kernel Soundness Bug #14576

#39

Post by markasoftware »

Gehinnn wrote: post #36

Has there ever been a bug that allowed to prove a previously unproven statement, without allowing the user to prove "false" by exploiting the bug directly? If every bug-exploiting proof would make it easy to prove false, putting a bounty on proving false could increase trust in the validity of verified but obscure Lean proofs.

A correctness bug in a proof checker by definition means that you can prove false.

Re: Postmortem for Kernel Soundness Bug #14576

#40

Post by UqWBcuFx6NV4r »

Cantinflas wrote: post #29
rzmmm wrote: post #12

Earlier quoted context omitted.

The implementation of the kernel is relatively trivial, it's an intentional design choice.

As claude would say, "relatively" is carrying a lot of weight in that frase. Definitely load-bearing — would not pass a quick smoke test.

but where’s the seam!?
Post reply on HN