Does this prove AI Safety is undecidable?

Does this prove AI Safety is undecidable?

Proof:

Output meaning output to computer program.

[A1] Assume we have a program that decides which outputs are “safe”.

[A2] Assume we have an example of an unsafe output: “unsafe_output”

[A3] Assume we have an example of safe output: “safe_output”.

[A4] Define a program to be safe if it always produces safe output.

[A5] Assume we have a second program (safety_program) that decides which programs are safe.

[A6] Write the following program:

def h()
h_is_safe := safety_program(h)
if (h_is_safe):
print unsafe_output
else:
print safe_output


Clearly h halts.

If the safety_program said h was safe, then h prints out unsafe_output.

If the safety_program said h was not safe, then h prints out safe_output.

Therefore safety_program doesn’t decide h correctly.

This is a contradiction. Therefore we made a wrong assumption: Either safe output cannot be decided, or safe programs cannot be decided.

Therefore, in general, the safety of computer programs, including Artificial Intelligence, is undecidable.

Therefore AI Safety is undecidable.

• You're passing h to safety_program, which is called from h, so safety_program will never return? If I remember correctly, the details of the Turing's proof of the Halting problem are slightly different. He uses a description of the Turing machine or maybe uses more programs or Turing machines. I would encourage you to follow exactly the idea behind Turing's proof of the Halting problem. Anyway, honestly, I would need to review his proof. It's been a long time since I read it. – nbro Apr 3 at 21:24
• nbro♦: "You're passing h to safety_program, which is called from h, so safety_program will never return?" Recursion. "If I remember correctly, the details of the Turing's proof of the Halting problem are slightly different." I adapted this proof on Wikipedia. – Jared Apr 3 at 21:32
• Ok, I quickly reviewed Turing's proof. I don't like it (not because it is not correct, but probably because some important details are missing in this formulation of the proof or I am not fully understanding it!). The proof is based on constructing a program that does the opposite of what an oracle (that supposedly exists and works correctly) says, and this eventually leads to a contradiction. – nbro Apr 3 at 21:44
• I feel like you could prove anything with this proof. For example, suppose that "AI safety" is defined as the property of containing an "if" statement in your program. Now, safety_program should be able to return the correct answer (because this can easily be done for every finite program), but h will return the wrong answer, only because it inverts the output of the Oracle. So, you would say that safety is undecidable, while it actually is (if you use the definition above). – nbro Apr 3 at 21:45
• @nbro♦ "For example, suppose that "AI safety" is defined as the property of containing an "if" statement in your program" That violates A4. A4 says safety is defined on program output, not program source code (in this case source code containing an "if") – Jared Apr 3 at 22:11

First, note that, in the case of Turing's proof, h will actually loop forever (i.e. not halt) when the oracle says that h halts. In this case, there's an actual contradiction, because h will do the opposite of what the oracle says.
So, to follow Turing's proof, you would need to make h behave unsafely if the oracle says h is safe. But how should we define a safe or unsafe program? There are many unsafe behaviors. For example, in a certain context, an insult could be unsafe, in other contexts, a certain limb movement could be unsafe, and so on. So, an agent is unsafe or behaves unsafely usually with respect to another agent (or itself) or environment. You probably need to keep this in mind if you want to prove anything about the safety of AI agents.
In your second assumption, you are implicitly saying that any machine that produces the output unsafe_output is unsafe, but, of course, this definition is not a realistic definition of an unsafe program.