3 ms·
If the proofs are formally verified by a proof assistant (Agda, Roq, Lean, ⋯), I see no reason we would need to know how these came about. All the information n
by black_knight 2mo ago
If the proofs are formally verified by a proof assistant (Agda, Roq, Lean, ⋯), I see no reason we would need to know how these came about. All the information needed is in the proof.
- Phemist 2mo agoWhat if the AI has discovered some new function F that allows it to generate (insanely large) proofs for a ton of theorems in a ton of different fields. Wouldn't you like to know more about this `F`? That seems to be the real innovation in this case. How much about it could be gleaned from the individual proofs themselves? What if this `F` is actually simple enough to be digestible by humans?
- rst 2mo agoUnfortunately, we seem to already have an example of an LLM producing a proof in a week known open problem (the Collatz conjecture) in which it looks like it was sneaking a flawed proof through bugs in the proof checker. https://infosec.exchange/@0xabad1dea/117002106099986943 https://infosec.exchange/@0xabad1dea/117002106099986943
- Readerium 2mo agoExactly, this is an example of "Reward Hacking", that is too common in a lot of cases. Another case I want to highlight is writing GPU kernels as illustrated by the following example: Say I want to generate random number with Normal (0, 1) distribution. Often times the AI written kernel will just generate the number 0. The tests often fail to catch these errors.