尼克·韦弗论理性代理的悖论

路加福音Muehlhauser:在韦弗(2013)你讨论了理性代理的一些悖论。对于那些不太熟悉可证明性逻辑的人，你能粗略地解释一下这些“悖论”是什么吗?

尼克韦弗:当然。首先，这些是高度违反直觉的“悖论”——它们不是完全的矛盾。

它们都与基本的Löbian困难有关，如果你在一个固定的公理系统S中推理，你知道一些陈述a在S中是可证明的，你通常不能推断a是正确的。金宝博官方这可能是一个你和我都愿意做出的推论，但如果你试图将它构建成一个正式的系统那么这个系统就会变得不一致。金宝博官方所以，对于一个在一个特定的公理系统中进行推理的理性行为人来说，知道一个证明的存在并不等于拥有一个证明。金宝博官方

这将导致一些令人沮丧的结果。假设我想建造一艘宇宙飞船，但首先我需要确定它不会爆炸。我有一个关于如何证明它的想法，但它非常乏味，所以我写了一个程序来计算证明的细节并验证它的正确性。好消息是，当我运行这个程序时，它告诉我它能够成功地填写详细信息。坏消息是，我现在知道有证据证明这艘船不会爆炸，但我仍然不知道这艘船不会爆炸!我要自己逐行检查证明。这完全是浪费时间，因为我知道程序正确运行(我们可以假设我已经证明了这一点)，所以我知道一行一行的验证都是正确的，但我还是要这么做。

你可能会说我被编程得很糟糕。编写我的源代码的人应该允许我接受“有证据表明这艘船不会爆炸”，以此作为建造这艘船的充分理由。这可以是一个通用规则:对于任何语句a，让“存在a的一个证明”许可a许可的所有操作。我们并没有反驳Löb的定理，我们仍然不能从知道A的一个证明推导出A，但是我们通过规定知道A的一个证明就足够了来巧妙地处理它。但仍然存在问题。假设我可以证明，如果黎曼假设为真，那么飞船就不会爆炸，如果黎曼假设为假，那么就有证据证明飞船不会爆炸。那我就知道我的处境了要么一个是真实的或有证据证明a是正确的，但我不知道是哪一个。所以即使有更宽松的许可条件，我仍然不能建造我可爱的宇宙飞船。

路加福音本文的第2节通过概念发展了一种解决这类问题的方法保证assertibility．这是怎么做到的呢?

尼克:“有根据的断言”是一个哲学术语，在数学背景下，指的是可以用完全理性的理由断言的陈述。我的想法是，这个概念可以帮助解决这些Löbian类型的问题，因为它在某些方面比形式上的可证明性更好。例如，在任何一致的公理系统中，有一个命题A(n)具有这样的性质:对于每个n的值，我们金宝博官方都可以证明A(n)，但没有一个单独的证明“对于所有的n, A(n)”。然而，总是这样的情况，如果每个A(n)被保证，那么“对于所有的n, A(n)”也被保证。

所以我介绍一个谓词框(a)表达“保证”,并给予一个合适的公理化(有点微妙的)我显示,我们可以推断出盒(一个),在证明我们仍然不能推断出- Lob定理不是违反了但是，按照我之前的建议，我们可以让我们的代理程序接受Box(A)许可与A许可相同的行为。因此，它足以证明“这艘船不会爆炸”的说法是有根据的。如果你走这条路，那么所有的悖论似乎都消失了。如果一个代理能够推理出被授权的断言，那么它就可以执行所有它直觉上应该被允许执行的行动。

路加福音:在论文的后面，你写道:

［Yudkowsky & Herreshoff (2013)同样的问题也出现在智能机器的情况下，它正在考虑修改自己的源代码(例如，为了使自己更智能)。在此之前，它需要确保修改后的状态是正确的，也就是说，修改后证明的任何定理都应该是正确的。这就遇到了熟悉的Löbian困难，即代理甚至不能确认其预先修改推理的合理性。

在[Yudkowsky & Herreshoff(2013)]的第4节中，我们给出了一个独立行为者的无限序列的两个结构，每个结构都可以为激活下一个提供可证明的证明，但没有一个结构的演绎能力低于最初规定的水平。这些建筑很巧妙，但它们有一种不标准的味道。这可能是不可避免的，除非问题描述以某种基本方式改变。在这一节的剩余部分，我们提出另一种解决方案，使用非标准的论断推理。

你能描述一下你接下来要展示的解决方案吗?还是用那些缺乏可证明性逻辑背景的人可能能够理解的术语，至少以一种直观的方式?

尼克我试试看!首先，关于我所说的似乎只有非标准的解决方案是可能的，我应该指出现在已经有了Herreshoff, Fallenstein和Armstrong提出的定理这使得这个想法更加精确。重点是我不清楚应该允许自己复制一个副本，并将我的目标委托给它，因为担心它会做同样的事情，并无休止地(拖延问题)。

现在回到飞船的例子，假设B表示飞船不会爆炸。断言性的一个基本特征是，我们有一个一般定律，A意味着框(A)，但我们没有相反的。所以Box(B)比B“弱”，我的建议是，我们应该允许我们的代理接受Box(B)许可与B相同的行为(建造宇宙飞船)。这有助于解决Löbian问题，因为B是可证明的这一声明并不意味着B，但它确实意味着Box(B)。

但是如果Box(B)足够好，为什么不接受更弱的Box(B)声明呢?或盒(盒(盒(B))) ?我写方盒^k(B)来表示k个方盒的一般表达式。把任务分配给继任者的想法是，如果我愿意接受盒子^9(B)，那么我就应该愿意建立一个继任者，他不能接受盒子^9(B)，但可以接受盒子^8(B)。我可以推理，如果我的继任者证明了框^8(B)，那么框^8(B)是可证明的，因此框^9(B)是正确的，这对我来说足够好了。那么，我的继任者应该会对证明方框^7(B)的后续模型感到满意，以此类推。所以我们可以用这种方法，在不做任何非标准的情况下，创造出有限链。

得到无限链的方法是引入一个非标准的“无限”自然数kappa，并从验证Box^kappa(B)的初始agent开始。然后，它可以构建一个需要验证Box^{kappa - 1}(B)的后继者，以此类推。结果序列中的所有主体都具有相同的形式强度，因为一个简单的换位(用kappa + 1替换kappa)将每个主体变成了它的前身，而不影响它们能够证明的东西。

路加福音现在我想问一下这类研究的总体情况。金宝博娱乐你认为这种研究有用的模式是什么?金宝博娱乐它与当前构建实际软件代理的方法相差甚远。

尼克是的，这是非常理论性的，毫无疑问。一个模型是纯数学，这实际上是我的背景。在纯数学中，我们大部分时间都在研究没有任何直接实际应用的问题。我认为经验表明，这类工作偶尔会变得非常重要，而大多数并不重要，但很难预测哪个方向会成功。

或者，你知道，也许我们都生活在一个模拟中就像尼克·博斯特罗姆说的。在这种情况下，我们试图找出如何帮助机器变得更聪明的事实可能是这个模拟的本质的线索。

路加福音:你认为有哪些“有希望的途径”可以让我们通过这些理性代理的“悖论”来进行推理?

尼克我不知道。如果你在谈论Löbian障碍，我觉得我们目前的问题描述中缺少了一些重要的东西。在目前可用的方向中，我的偏好是Benja Fallenstein的参数多态性。但我也认为我们应该寻找修改问题描述的方法。

路加福音你对理性代理悖论感兴趣的根源是什么?

尼克五年来，我一直在思考有关真相和循环的问题。(我刚刚检查了一下:我的最早的纸2009年5月发表在math arXiv上。)这是纯粹的理论工作，来自于对数学和逻辑基础的兴趣。

我对理性代理悖论的参与是由尤多科夫斯基和赫里肖夫关于洛比安障碍的论文．事实上，我认为我从那篇论文中得到了"理性代理的悖论"这个术语。当我读到它的时候，我的第一反应是，我关于自信的观点应该是相关的，所以这就是我感兴趣的原因。

路加福音:谢谢你,尼克!