PhilSci Archive

Robust Computer Algebra, Theorem Proving, and Oracle AI

Sarma, Gopal P. and Hay, Nick J. (2017) Robust Computer Algebra, Theorem Proving, and Oracle AI. [Preprint]

[img]
Preview
Text
computer_algebra_theorem_proving_AI.pdf

Download (504kB) | Preview

Abstract

In the context of superintelligent AI systems, the term “oracle” has two meanings. One refers to modular systems queried for domain-specific 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 long-term 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 domain-specific 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 well-defined 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:
Share |

Item Type: Preprint
Creators:
CreatorsEmailORCID
Sarma, Gopal P.gopal.sarma@emory.edu0000-0002-9413-6202
Hay, Nick J.nnickhay@gmail.com
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 > Computer Science > Artificial Intelligence
Depositing User: Dr. Gopal Sarma
Date Deposited: 09 Aug 2017 12:26
Last Modified: 09 Aug 2017 12:26
Item ID: 13309
Subjects: Specific Sciences > Mathematics > Logic
Specific Sciences > Mathematics > Methodology
Specific Sciences > Mathematics > Proof
Specific Sciences > Computer Science > Artificial Intelligence
Date: 8 August 2017
URI: http://philsci-archive.pitt.edu/id/eprint/13309

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Actions (login required)

View Item View Item