超越定理与证明的理论：客座文章

斯科特的前言：我非常感谢我那些才华横溢的同事们，入口厅,拉古·梅卡， 和普拉萨德·拉加文德拉，感谢分享下面关于理论计算机科学（尤其是STOC/FOCS/SODA会议）应如何进化以应对当前正冲击我们领域的人工智能小行星的来访，至少我们人类理论家自其诞生以来一直在实践它。

虽然Pravesh、Raghu和Prasad只代表他们自己，不代表我自己，也不代表整个理论社区，但我发现他们提出的独立“概念轨道”是进一步讨论的绝佳起点。

——SA

考虑到人工智能定理证明器的发展速度，大多数人会承认以下情景在不久的将来至少是合理的：

人工智能定理证明器可以在数小时内证明明确的数学主张，甚至许多已经开放多年的研究充分的论点。此外，这些系统可能以名义上的费用广泛向消费者开放。

作为TCS研究者，让我们假装上述情景已经浮现出来，问自己：我们在这样的世界中扮演什么角色？这是否意味着理论研究的终结？

在思考这个问题时，让我们忽略所有其他混杂因素：

1. 围绕千禧奖问题的最新争议
2. 人工智能公司的动机与行动
3. 在写作、阐述或归因于以往作品方面，现有AI系统存在缺陷。

上述任何一个混杂因素都不会影响我们对“在拥有超人人工智能定理证明者的情况下，理论家应该做什么？”这个问题的答案。

注意我们使用“AI定理证明器”一词，而不仅仅是“AI”。我们认为这一概念区分在考虑这个问题时非常重要。

首先，我们想承认，对于像我们这样的理论家（以及许多更早的一代），研究主要集中在解决问题上。即使我们发展出概念性见解，也大多是为了回答明确的长期问题。我们并不打算让本提案评判某种研究形式优于其他;它只是反映出人工智能定理证明者加速了某种类型的研究活动，并希望充分利用它。这场动荡还带来了巨大的人力代价，这或许是一个更重要的问题，而本提案并未直接解决这个问题（我们没有任何好的观点）。类似观点在各种语境中也被提出过
以前，但现在的时机更为紧迫。

定义、问题与理论：

任何理论科学的目标都是推动人类对观察到现象的理解。除了定理和证明外，理论科学还包含定义、问题和理论。

定义确定了需要观察的对象。好奇心和背景驱动了问题提出。理论解释了观察到的现象。我们相信，即使有超人类AI定理证明器存在，人类仍将继续在定义、问题和理论的生成中发挥核心作用。

定义：人工智能能否定义随机性提取器、流算法或零知识证明？也许可以。但有一些理由相信，人类在制定定义方面仍将扮演重要角色。

例如，提取器的概念源于现实世界中缺乏完美随机源的问题。零知识证明似乎纯粹源于人类的好奇心，受个人味引导。人类的背景和好奇心将继续推动理论研究。

毕竟，我们可以决定观察哪些天体！

理论：请考虑以下思维实验。假设1965年，我们有一台魔法机器，只要按下按钮，给定任何计算问题，就能告诉我们它是否存在多项式时间算法。

这会是计算复杂性理论的终结吗？不会。人类会觉得完全不满意，会问，为什么这些问题没有多项式时间算法？为什么其他问题有？

NP完备性理论识别出一些看似没有高效算法的问题模式。即使在我们拥有一台魔法机器，只需按下按钮就能判断问题是否具有高效算法的世界里，这一理论依然是理论计算机科学的瑰宝。

同样，如果我们有一台机器能预测CSP是否NP完全或属于P，我们就会问：是什么让3-SAT是NP完全的，而2-SAT属于P？这个问题引出了多态性理论，给出了一个令人满意的答案。

理论不仅仅是简洁或高效的回答机制。最好的理论是人类认为“令人满意的解释”——无论那是什么意思。

最后，即使AI定理证明器的能力不断进步，人类的好奇心也会探究更宏大、更深层的问题。以前，即使我们想构建新的模型和理论，证明它们的某些内容是前提，而鉴于长期研究领域中宏大问题已达到极限，我们不得不缩小规模。

如果将AI证明的每个定理视为实验数据点，人类可以提出更宏大的问题，寻找这些定理之间的模式。

一个具体的提案：

我们认为理论家应在研究中采用这些人工智能定理证明器。在某种程度上，这已经在显性或隐性地发生。

作为理论家，我们在引入新模型或提出全新问题时非常节俭，也谨慎避免过快采纳新模型。部分原因是正式证明新定义或模型的性质是一项繁重的任务，可能需要十年和数十篇论文。

人工智能定理证明者可能会彻底改变这种动态。现在正是将工作重新聚焦于定义、问题和理论的时刻。我们需要明确的系统来鼓励和强化这些理论研究部分。

你也可以说下一代人工智能模型可以做到这一点;也许如此，但我们认为必须抓住当前的机会。

为此，我们建议STOC/FOCS/SODA设立一个单独的论文轨道。该轨道专门用于引入新定义、提出新问题或构建解释性理论的论文。该轨道的论文篇幅较短，约少于10页。

论文可以且应当如常包含定理，视情况而定理。最重要的是，这一根本性转变在于论文不必包含定理的证明。相反，作者提供一份精益证书作为论文的补充。

评估在某种意义上也会“正交”这些证明的难度。

本方向的论文应完全根据概念优劣进行评判，完全不依赖证明难度。

审稿必须完全不依赖证明，原因有两个。STOC/FOCS的主课程已经包含前者类别的论文。其次，产出真正新颖的概念论文的一个主要障碍是它们常因证明缺乏技术深度而被评判不佳。

我们认为这两点区别于（ITCS/SOSA），无论如何，这也是我们所有会议，包括STOC/FOCS（“旗舰”会议）都迫切需要的。

明确来说，我们自己也承认需要磨练这些提出新定义、提出深刻有趣问题或构建新理论的能力。独立的概念论文轨道将为初级和资深研究者以及整个领域提供系统化的机制。

我们相信，未来几代研究生将挑战那些我们曾经完全无法触及的研究方向。我们只需要建立一套能够培养理论上新研究方式的体系。

—— 普拉韦什·科塔里，拉古·梅卡，普拉萨德·拉加文德拉。