Reward hacking will continue to be a problem. For sufficiently astonishing AI-created results, we must remember to ask if AI has not instead found it easier to elaborately fool us.
Postmortem for Kernel Soundness Bug #14576
41–50 of 68 posts
Re: Postmortem for Kernel Soundness Bug #14576
#42[flagged]
Re: Postmortem for Kernel Soundness Bug #14576
#43This thread has some context. A proof-system researcher found some proof-system bugs and presented them a funny way:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean...
A mathematically-inclined reviewer (or an LLM) can quickly identify that it's an exploit. (Two exploits; it's crafted to hit a bug in another proof checker, too.)
The post gestures at this, but a natural follow-up, beyond fixing specific bugs around this exploit, would be to task some security-oriented models with proving False in Lean, or with reviewing the code for potentially unsound steps, missing checks, or even useful 'hardening'. That's happening and bugfixes are landing as a result.
Re: Postmortem for Kernel Soundness Bug #14576
#44Earlier quoted context omitted.
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 de…
Why does the original C verifier have bugs if its supposedly so easy to implement a verifier?
Re: Postmortem for Kernel Soundness Bug #14576
#45Has 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 stateme…
>"what is a true statement" and "what is a derivable statement" should be the same.
you mention completeness in the rest of your comment, so I'm not sure how you aren't aware of this, but the famous incompleteness theorem says that for a consistent set of axioms there will always be true statements you can't prove.[1]
[1] https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...
Re: Postmortem for Kernel Soundness Bug #14576
#46> The practical consequence: checking with an independent kernel still works, since it required two distinct bugs in two implementations, but users who rely on it need current versions of both. Things like this aren't too surprising, given that even much simpler type checkers like Rust's have soundness issues occasionally. I think it's very important to view verified results not as an absolute and unbreakable guarant…
To what degree can you say something like "if the kernel doesn't have metaprogramming [or some other set of features] it's fine". When were the last bugs with a reduced feature set?
Re: Postmortem for Kernel Soundness Bug #14576
#47Has 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 stateme…
Don't Godel's incompleteness theorems mean that completeness is a property you don't want in a prover (as it means the prover must then be inconsistent and this unsuable) and consistency is a property of the prover you cannot prove using the prover itself?
Re: Postmortem for Kernel Soundness Bug #14576
#48Earlier quoted context omitted.
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 de…
Why does the original C verifier have bugs if its supposedly so easy to implement a verifier?
Nothing more complex than Hello world is easy to implement in C without risking mistakes in checking boundary conditions if you are not really careful.
Re: Postmortem for Kernel Soundness Bug #14576
#49Earlier quoted context omitted.
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 de…
As it happens, the Python verifier mmverify.py has an even simpler soundness bug [0], and so far I've reviewed two independent AI-written verifiers that have replicated that bug, since they apparently really like to copy the strategy from mmverify.py. A sound verifier isn't too difficult to write in terms of architecture (I just wrote one myself for differential testing [1]), but it requires some close attention to the details.
That is to say, the Swiss-cheese approach definitely lends authority, but individual implementations are unfortunately not as foolproof as they're made out to be.
[0] https://github.com/david-a-wheeler/mmverify.py/issues/30
[1] https://github.com/LegionMammal978/mm-verifier-tests/blob/ma...
Re: Postmortem for Kernel Soundness Bug #14576
#50Earlier quoted context omitted.
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 stateme…
>"what is a true statement" and "what is a derivable statement" should be the same. you mention completeness in the rest of your comment, so I'm not sure how you aren't aware of this, but the famous incompleteness theorem says that for a consistent set of axioms there will always be true statements you can't prove.[1] [1] https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...
That's not what it says. It says that as long as the logic is rich enough (first-order isn't enough) and consistent there are statements where neither the statement nor its negation is provable. You may choose to create a new logic by adding either the statement or its negation as an additional axiom, and it will (obviously?) remain consistent.
Truth is some sort of value judgment that is outside the scope of formal systems. And looking at how bizarre Gödel statements are, it's unclear if there's any particular justification for declaring them to be true or false.