Robust Computer Algebra, Theorem Proving, and Oracle AI

ResearchSpace/Manakin Repository

Show simple item record

dc.contributor.author Sarma, GP en
dc.contributor.author Hay, NJ en
dc.date.accessioned 2018-07-18T04:42:52Z en
dc.date.available 2018-07-18T04:42:52Z en
dc.date.issued 2017 en
dc.identifier.citation CDMTCS Research Reports CDMTCS-512 (2017) en
dc.identifier.issn 1178-3540 en
dc.identifier.uri http://hdl.handle.net/2292/37499 en
dc.description.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. en
dc.publisher Department of Computer Science, The University of Auckland, New Zealand en
dc.relation.ispartofseries CDMTCS Research Report Series en
dc.rights Items in ResearchSpace are protected by copyright, with all rights reserved, unless otherwise indicated. Previously published items are made available in accordance with the copyright policy of the publisher. en
dc.rights.uri https://researchspace.auckland.ac.nz/docs/uoa-docs/rights.htm en
dc.source.uri https://www.cs.auckland.ac.nz/research/groups/CDMTCS/researchreports/index.php en
dc.title Robust Computer Algebra, Theorem Proving, and Oracle AI en
dc.type Technical Report en
dc.subject.marsden Fields of Research en
dc.rights.holder The author(s) en
dc.rights.accessrights http://purl.org/eprint/accessRights/OpenAccess en


Full text options

This item appears in the following Collection(s)

Show simple item record

Share

Search ResearchSpace


Advanced Search

Browse