Robust Computer Algebra, Theorem Proving, and Oracle AI
Gopal P. Sarma School of Medicine, Emory University, Atlanta, GA USA Nick J. Hay Vicarious FPC, San Francisco, CA USA
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
中文速览
超级人工智能时代即将到来，如何让一个只负责"回答问题"的AI系统（即Oracle AI）既强大又安全，是AI安全领域的核心挑战之一。这篇论文系统梳理了Oracle AI的研究现状，指出当前基于自然语言处理的问答系统因架构过于杂乱、难以形式化验证，并不适合作为严格意义上的安全Oracle来分析。相比之下，计算机代数系统（Computer Algebra Systems, CAS）——比如Mathematica、Maple——可以被视为数学领域的"原始Oracle"，而将CAS与定理证明器（Theorem Provers）整合起来的工作，则为"可证明安全性"这一AI安全核心概念提供了一批具体可操作的研究问题。论文详细梳理了CAS与定理证明器的架构差异、已知缺陷及整合方案，并为有志于AI安全的研究者列出了一系列实际可做的软件项目。这项工作的意义在于，它将超级智能安全这一高度抽象的哲学议题，落地到了数学计算系统这个真实可触的工程领域，为AI安全研究开辟了一条脚踏实地的路径。
原文 arXiv:1708.02553;中英对照 + 大白话阅读 https://aha.fim.ai/paper/1708.02553v2