2
$\begingroup$

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?

Improve this question
$\endgroup$
5
$\begingroup$

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.

Improve this answer
$\endgroup$
  • $\begingroup$ Just because it's impossible to make general statements doesn't mean that verification of properties isn't possible for many types of system. $\endgroup$ – NietzscheanAI Aug 6 '16 at 7:40
  • $\begingroup$ In practice, the problem arises not because of we don't know how to verify complex systems (which can, at least in principle, be addressed methodologically) but because of the difficulty in formalizing 'friendly'. $\endgroup$ – NietzscheanAI Aug 6 '16 at 7:49
  • 1
    $\begingroup$ @user217281728 I've updated the answer in the light of your first comment. Indeed there are many subclasses that we can make statements about, like the context-free languages. But these are too limited to form an AI that operates in the real world. $\endgroup$ – S.L. Barth - Reinstate Monica Aug 6 '16 at 7:56
  • 1
    $\begingroup$ I'm not sure that there's any language (provably halting other otherwise) that can readily formalize a concept as ill-defined as 'friendly', so in practice, we agree. As per my answer, my hope is that it might be able to make defensive inroads into the formalization problem via obligation calculii... $\endgroup$ – NietzscheanAI Aug 6 '16 at 8:18
3
$\begingroup$

Here are some examples of recent work on verifying certain properties of autonomous systems [RoboCheck].

However, to achieve the same kind of thing for the notion of 'friendly' using formal verification (i.e. 'proving correctness using mathematical techniques'), it would (at the least) seem necessary to be able to express 'friendly' within a logical formalism, (i.e. as a predicate testable within a model-checker, so that we can be sure a system never enters an undesirable state).

However, it's not immediately clear that 'friendly' has a more specific definition than 'a desire not to harm humans', so much more low-level detail is needed.

Some previous work in this general area that might be useful in this respect include:

  • Deontic Logic - a logical calculus of obligations.
  • Elephant 2000 - John McCarthy's description of a promise-based programming language.
Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.