Robust Computer Algebra, Theorem Proving, and Oracle AI
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingQuestion AnsweringSimilar Papers 제목 키워드 기반
Quantum automated theorem proving
Automated theorem proving, or more broadly automated reasoning, aims at using computer programs to automatically prove or disprove mathematical theorems and logical statements. It takes on an essential role across a vast…
Automated Theorem ProvingAutomated Planning Techniques for Elementary Proofs in Abstract Algebra
This paper explores the application of automated planning to automated theorem proving, which is a branch of automated reasoning concerned with the development of algorithms and computer programs to construct mathematica…
Abstract AlgebraAutomated Theorem ProvingMathematical ProofsComputational Algebra with Attention: Transformer Oracles for Border Basis Algorithms
Solving systems of polynomial equations, particularly those with finitely many solutions, is a crucial challenge across many scientific fields. Traditional methods like Gr\"obner and Border bases are fundamental but suff…
GeoGebra Tools with Proof Capabilities
We report about significant enhancements of the complex algebraic geometry theorem proving subsystem in GeoGebra for automated proofs in Euclidean geometry, concerning the extension of numerous GeoGebra tools with proof …
Automated Theorem ProvingBenchmarkingA state vector algebra for algorithmic implementation of second-order logic
We present a mathematical framework for mapping second-order logic relations onto a simple state vector algebra. Using this algebra, basic theorems of set theory can be proven in an algorithmic way, hence by an expert sy…
Automated Theorem Proving