Answers.Body: <p>Here are some examples of recent work on verifying certain properties of autonomous systems <a href="https://www.cs.york.ac.uk/circus/RoboCalc-event/courses/" rel="nofollow">[RoboCheck]</a>.</p>
  
  <p>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).</p>
  
  <p>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.</p>
  
  <p>Some previous work in this general area that might be useful in this respect include:</p>
  
  <ul>
  <li><a href="https://en.wikipedia.org/wiki/Deontic_logic" rel="nofollow">Deontic Logic</a> - a logical calculus of obligations.</li>
  <li><a href="http://www.jfsowa.com/ikl/McCarthy89" rel="nofollow">Elephant 2000</a> - John McCarthy's description of a promise-based programming language.</li>
  </ul>
  
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2016-08-06T07:40:02.787Z
Answers.LastActivityDate: 2016-08-06T07:40:02.787Z
Answers.UserDisplayName: NietzscheanAI
Answers.Body: <p>Unfortunately, this is extremely unlikely.</p>
  
  <p>It is nearly impossible to make statements about the behaviour of software in general. This is due to the <a href="https://en.wikipedia.org/wiki/Halting_problem">Halting problem</a>, 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.</p>
  
  <p>The question whether a piece of code is friendly, can very likely be reduced to a variant of the halting problem.<br>
  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.</p>
  
  <p>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.<br>
  But these are about situations that can be defined with mathematical rigour.</p>
  
  <p>"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.</p>
  
  <p>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.</p>
  
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2016-08-06T07:40:56.257Z
Answers.Text: Just because it's impossible to make general statements doesn't mean that verification of properties isn't possible for many types of system.
Answers.UserDisplayName: NietzscheanAI
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2016-08-06T07:49:11.020Z
Answers.Text: 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'.
Answers.UserDisplayName: NietzscheanAI
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2016-08-06T07:56:27.493Z
Answers.Text: @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.
Answers.UserDisplayName: S.L. Barth is on codidact.com
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2016-08-06T08:18:04.227Z
Answers.Text: 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...
Answers.UserDisplayName: NietzscheanAI
Answers.ContentLicense: CC BY-SA 3.0
Answers.CreationDate: 2016-08-06T07:24:41.043Z
Answers.LastActivityDate: 2016-08-06T07:51:00.567Z
Answers.LastEditDate: 2016-08-06T07:51:00.567Z
Answers.UserDisplayName: S.L. Barth is on codidact.com
Body: <p>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. </p>
  
  <p>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 <a href="https://en.wikipedia.org/wiki/Friendly_artificial_intelligence" rel="nofollow">friendly</a>? Has there any research been done towards this?</p>
  
Tags: <friendly-ai>
Title: Can we prove that a piece of code in AI software will cause it to never turn against us?
UserDisplayName: wythagoras
ThreadText: # Can we prove that a piece of code in AI software will cause it to never turn against us?
  
  (Asked by: username_0 on 2016-08-06)
  
  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](https://en.wikipedia.org/wiki/Friendly_artificial_intelligence)? Has there any research been done towards this?
  
  **Tags:** friendly-ai
  
  
  ---
  
  ## 2 answers
  
  ### Answer by username_2 on 2016-08-06. Score: 5 | Accepted answer
  
  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](https://en.wikipedia.org/wiki/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.
  
  > **Comments:**
  > **username_1**: Just because it's impossible to make general statements doesn't mean that verification of properties isn't possible for many types of system.  
  > **username_1**: 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'.  
  > **username_2**: @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.  
  > **username_1**: 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...  
  
  ---
  
  ### Answer by username_1 on 2016-08-06. Score: 3
  
  Here are some examples of recent work on verifying certain properties of autonomous systems [[RoboCheck]](https://www.cs.york.ac.uk/circus/RoboCalc-event/courses/).
  
  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](https://en.wikipedia.org/wiki/Deontic_logic) - a logical calculus of obligations.
  * [Elephant 2000](http://www.jfsowa.com/ikl/McCarthy89) - John McCarthy's description of a promise-based programming language.
  
  
  ---
  
  