Another variant for checkable and profitable Orcale: use the AI to solve math problems, publish the solutions and earn money on it. In that case the input may be very short, like “prove Goldbach conjecture”, but output could be arbitrary long and may be dangerous, if there are some encoded messages. To escape it, we need another Oracle, which only checks proofs on some formal language.
Here is assumed that if the proof is true and is in a formal language, there is no hidden messages in the text.
Another way to check proofs is to run two slightly different non-communicating Oracles and compare outputs.
Here is assumed that if the proof is true and is in a formal language, there is no hidden messages in the text.
That is never something safe to assume. I can write formally correct proofs that contain hidden messages quite easily—add extra lemmas and extra steps. Unless we’re very smart, it would be hard for us to detect which steps are unnecessary and which are needed, especially if it rewrites the main proof thread somewhat.
Another way to check proofs is to run two slightly different non-communicating Oracles and compare outputs.
I’ll accept that as a part of a submission if a) you develop it more, in a formal way, and b) you repost it as a top level comment.
Another variant for checkable and profitable Orcale: use the AI to solve math problems, publish the solutions and earn money on it. In that case the input may be very short, like “prove Goldbach conjecture”, but output could be arbitrary long and may be dangerous, if there are some encoded messages. To escape it, we need another Oracle, which only checks proofs on some formal language.
Here is assumed that if the proof is true and is in a formal language, there is no hidden messages in the text.
Another way to check proofs is to run two slightly different non-communicating Oracles and compare outputs.
That is never something safe to assume. I can write formally correct proofs that contain hidden messages quite easily—add extra lemmas and extra steps. Unless we’re very smart, it would be hard for us to detect which steps are unnecessary and which are needed, especially if it rewrites the main proof thread somewhat.
I’ll accept that as a part of a submission if a) you develop it more, in a formal way, and b) you repost it as a top level comment.