It is possible of normal code to prove that it is correct using mathematical techniques, and that is often done to ensure that some parts are bug-free. Can we also prove that a piece of code in AI software will cause it to never turn against us, i.e. that the AI is friendly? Has there any research been done towards this?
Can we prove that a piece of code in AI software will cause it to never turn against us?
friendly ai
Unfortunately, this is extremely unlikely.It is nearly impossible to make statements about the behaviour of software in general. This is due to the Halting problem, which shows that it is impossible to prove whether a program will stop for any given input. From this result, many other things have been shown to be unprovable.The question whether a piece of code is friendly, can very likely be reduced to a variant of the halting problem.An AI that operates in the real world, which is a requirement for friendliness to have a meaning, would need to be Turing complete. Input from the real world cannot be reliably interpreted using regular or context-free languages.Proofs of correctness work for small code snippets, with clearly defined inputs and outputs. They show that an algorithm produces the mathematically right output, given the right input.But these are about situations that can be defined with mathematical rigour.Friendliness isn't a rigidly defined concept, which already makes it difficult to prove anything about it. On top of that, friendliness is about how the AI relates to the real world, which is an environment whose input to the AI is highly unpredictable.The best we can hope for, is that an AI can be programmed to have safeguards, and that the code will raise warning flags if unethical behaviour becomes likely - that AI's are programmed defensively.