Sarma, Gopal P. and Hay, Nick J. (2017) Robust Computer Algebra, Theorem Proving, and Oracle AI. Informatica, 41 (4). pp. 451461.
This is the latest version of this item.

Text
computer_algebra_theorem_proving_AI.pdf Download (436kB)  Preview 
Abstract
In the context of superintelligent AI systems, the term “oracle” has two meanings. One refers to modular systems queried for domainspecific tasks. Another usage, referring to a class of systems which may be useful for addressing the value alignment and AI control problems, is a superintelligent AI system that only answers questions. The aim of this manuscript is to survey contemporary research problems related to oracles which align with longterm research goals of AI safety. We examine existing question answering systems and argue that their high degree of architectural heterogeneity makes them poor candidates for rigorous analysis as oracles. On the other hand, we identify computer algebra systems (CASs) as being primitive examples of domainspecific oracles for mathematics and argue that efforts to integrate computer algebra systems with theorem provers, systems which have largely been developed independent of one another, provide a concrete set of problems related to the notion of provable safety that has emerged in the AI safety community. We review approaches to interfacing CASs with theorem provers, describe welldefined architectural deficiencies that have been identified with CASs, and suggest possible lines of research and practical software projects for scientists interested in AI safety.
Export/Citation:  EndNote  BibTeX  Dublin Core  ASCII/Text Citation (Chicago)  HTML Citation  OpenURL 
Social Networking: 
Item Type:  Published Article or Volume  

Creators: 


Keywords:  superintelligence, Friendly AI, Oracle AI, AI safety, provable safety, computer algebra, theorem proving, value alignment  
Subjects:  Specific Sciences > Mathematics > Logic Specific Sciences > Mathematics > Methodology Specific Sciences > Mathematics > Proof Specific Sciences > Artificial Intelligence 

Depositing User:  Dr. Gopal Sarma  
Date Deposited:  29 Jan 2018 15:28  
Last Modified:  29 Jan 2018 15:28  
Item ID:  14334  
Journal or Publication Title:  Informatica  
Official URL:  http://www.informatica.si/index.php/informatica/ar...  
Subjects:  Specific Sciences > Mathematics > Logic Specific Sciences > Mathematics > Methodology Specific Sciences > Mathematics > Proof Specific Sciences > Artificial Intelligence 

Date:  1 December 2017  
Page Range:  pp. 451461  
Volume:  41  
Number:  4  
URI:  http://philsciarchive.pitt.edu/id/eprint/14334 
Available Versions of this Item

Robust Computer Algebra, Theorem Proving, and Oracle AI. (deposited 09 Aug 2017 12:26)
 Robust Computer Algebra, Theorem Proving, and Oracle AI. (deposited 29 Jan 2018 15:28) [Currently Displayed]
Monthly Views for the past 3 years
Monthly Downloads for the past 3 years
Plum Analytics
Actions (login required)
View Item 