Answers.Body: <ol>
  <li><p>Every program halts, or continues</p>
  </li>
  <li><p>Given N steps, enough time and space (*), halting within N steps is provable</p>
  </li>
  </ol>
  <p>3 (from 2). Halting always has proof: run program until halt; count number of steps; verify claim of halting (within number of steps)</p>
  <ol start="6">
  <li><p>(Program is safe) implies (program is proved safe)</p>
  </li>
  <li><p>(Safety proved) implies (public understands the proof)</p>
  </li>
  <li><p>(Program is safe) implies (program always halts (safely) or continues (safely)) [from 1, 6] and ((public) understands (safety proof)) [from 7]</p>
  </li>
  <li><p>(Public not understand claimed safety proof this moment) implies (don't run program this moment) [common sense]</p>
  </li>
  </ol>
  <p>(*) This universe is finite. Some numbers too big to be computed in this universe</p>
  <p>Have you seen perfect software?</p>
  <p>Have you seen software make mistakes?</p>
  <p>Why trust life-death decisions to software?</p>
  <p>Why trust government decisions to software?</p>
  <p>Why trust business decisions to software?</p>
  <p>If scientists may not recognize AI is intelligent, what if you don't recognize something beyond AI in front of you?</p>
  <p>(After enough doubt, all you can do is TRUST)</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-02-25T04:10:46.137Z
Answers.LastActivityDate: 2021-02-25T04:10:46.137Z
Answers.UserDisplayName: Jesus is Lord
Body: <p>According to <a href="https://en.wikipedia.org/wiki/Rice%27s_theorem" rel="nofollow noreferrer">Wikipedia</a></p>
  
  <blockquote>
    <p>In computability theory, <strong>Rice's theorem</strong> states that all non-trivial,
    semantic properties of programs are undecidable. A semantic property
    is one about the program's behavior (for instance, does the program
    terminate for all inputs), unlike a syntactic property (for instance,
    does the program contain an if-then-else statement). A property is
    non-trivial if it is neither true for every computable function, nor
    false for every computable function.</p>
  </blockquote>
  
  <p>A <strong>syntactic property</strong> asks a question about a computer program like "is there is a while loop?"</p>
  
  <p>A <strong>semantic properties</strong> asks a question about the behavior of the computer program. For example, does the program loop forever (which is the Halting problem, which is undecidable, i.e., in general, there's no algorithm that can tell you if an arbitrarily given program halts or terminates for a given input)? </p>
  
  <p>So, Rice's theorem proves all non-trivial semantic properties are undecidable (including whether or not the program loops forever).</p>
  
  <p>AI is a computer program (or computer programs). These program(s), like all computer programs, can be modeled by a Turing machine (Church-Turing thesis).</p>
  
  <p>Is safety (for Turing machines, including AI) a non-trivial semantic question? If so, is AI safety undecidable? In other words, can we determine whether an AI program (or agent) is safe or not?</p>
  
  <p>I believe that this doesn't require formally defining safety.</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-04-03T18:39:55.210Z
Comments.Text: I think an answer to your question may actually depend on the definition of "safe AI". For example, if you define a safe AI as any program that can run on a TM that does not contain a while loop (of course, this is a stupid example), then "AI safety" is a syntactic property.
Comments.UserDisplayName: nbro
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-04-04T00:48:29.313Z
Comments.Text: nbro♦: Is there any way to prove AI safety if "safe" is not a syntactical definition?
Comments.UserDisplayName: Jesus is Lord
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-04-04T01:28:52.737Z
Comments.Text: I would need to think about it. I had never thought about it.
Comments.UserDisplayName: nbro
Tags: <agi><proofs><ai-safety><theory-of-computation>
Title: Does Rice's theorem prove safe AI is undecidable?
UserDisplayName: Jesus is Lord
ThreadText: # Does Rice's theorem prove safe AI is undecidable?
  
  (Asked by: username_0 on 2020-04-02)
  
  According to [Wikipedia](https://en.wikipedia.org/wiki/Rice%27s_theorem)
  
  > In computability theory, **Rice's theorem** states that all non-trivial,
  > semantic properties of programs are undecidable. A semantic property
  > is one about the program's behavior (for instance, does the program
  > terminate for all inputs), unlike a syntactic property (for instance,
  > does the program contain an if-then-else statement). A property is
  > non-trivial if it is neither true for every computable function, nor
  > false for every computable function.
  
  A **syntactic property** asks a question about a computer program like "is there is a while loop?"
  
  A **semantic properties** asks a question about the behavior of the computer program. For example, does the program loop forever (which is the Halting problem, which is undecidable, i.e., in general, there's no algorithm that can tell you if an arbitrarily given program halts or terminates for a given input)?
  
  So, Rice's theorem proves all non-trivial semantic properties are undecidable (including whether or not the program loops forever).
  
  AI is a computer program (or computer programs). These program(s), like all computer programs, can be modeled by a Turing machine (Church-Turing thesis).
  
  Is safety (for Turing machines, including AI) a non-trivial semantic question? If so, is AI safety undecidable? In other words, can we determine whether an AI program (or agent) is safe or not?
  
  I believe that this doesn't require formally defining safety.
  
  **Tags:** agi, proofs, ai-safety, theory-of-computation
  
  > **Comments:**
  > **username_1**: I think an answer to your question may actually depend on the definition of "safe AI". For example, if you define a safe AI as any program that can run on a TM that does not contain a while loop (of course, this is a stupid example), then "AI safety" is a syntactic property.  
  > **username_0**: username_1♦: Is there any way to prove AI safety if "safe" is not a syntactical definition?  
  > **username_1**: I would need to think about it. I had never thought about it.  
  
  ---
  
  ## 1 answers
  
  ### Answer by username_0 on 2021-02-25. Score: -2
  
  1. Every program halts, or continues
  2. Given N steps, enough time and space (\*), halting within N steps is provable
  
  3 (from 2). Halting always has proof: run program until halt; count number of steps; verify claim of halting (within number of steps)
  
  6. (Program is safe) implies (program is proved safe)
  7. (Safety proved) implies (public understands the proof)
  8. (Program is safe) implies (program always halts (safely) or continues (safely)) [from 1, 6] and ((public) understands (safety proof)) [from 7]
  9. (Public not understand claimed safety proof this moment) implies (don't run program this moment) [common sense]
  
  (\*) This universe is finite. Some numbers too big to be computed in this universe
  
  Have you seen perfect software?
  
  Have you seen software make mistakes?
  
  Why trust life-death decisions to software?
  
  Why trust government decisions to software?
  
  Why trust business decisions to software?
  
  If scientists may not recognize AI is intelligent, what if you don't recognize something beyond AI in front of you?
  
  (After enough doubt, all you can do is TRUST)
  
  
  ---
  
  