NIK WEAVER在理性机构的悖论上

路加福音Muehlhauser： 在韦弗（2013）你讨论了理性代理的一些悖论。你可以大致解释这些“悖论”是什么，因为可能不是熟悉可证明逻辑的人？

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

它们都与基本的Löbian困难有关如果你在一个固定的公理系统S中推理，并且你知道某个命题a在S中是可证明的，你通常不能推断出a是正确的。亚博体育苹果app官方下载这可能是你我愿意做出的推论，但如果你试图把它构建成一个正式的系统，那么这个系统就会变得不一致。亚博体育苹果app官方下载所以，对于一个理性的行为人来说，在一个特定的公理系统中进行推理，知道一个证明的存在不如有一个证明。亚博体育苹果app官方下载

这导致了一些非常令人沮丧的后果。让我们说我想建立宇宙飞船，但首先我需要确保它不会爆炸。我有一个关于如何证明这一点的想法，但它非常乏味，所以我写了一个程序来解决证明的细节并验证它是否正确。好消息是，当我运行该程序时，它会通知我，它能够成功填写详细信息。坏消息是我现在知道船不会爆发的证据，但我仍然不知道这艘船不会爆发！我将不得不检查自己的证据，按行线排队。这是完全浪费时间，因为我知道程序正常运作（我们可以假设我已证明这一点），所以我知道这条线通过线验证将要查看，但我仍然必须这样做。

你可能会说我已经被严重编程。无论谁写下我的源代码都应该让我接受“船舶不会爆炸”作为建造船舶的充分理由。这可以是一般规则：对于任何语句A，让“存在”许可证许可证许可证的所有操作。我们与Löb的定理不相矛盾 - 我们仍然无法推断出A的证据 - 但我们通过规定知道有足够好的证据来说，我们很紧张。但仍有问题。想象一下，我可以证明如果riemann假设是真的，那么船不会爆炸，如果它是假的，那么船不会爆炸。然后我在我知道的情况下任何一个a是真的或者有一个证据是真的，但我不知道哪一个。所以即使有了更自由的许可条件，我仍然无法建立我可爱的宇宙飞船。

卢克：论文第2节发展了一种通过概念解决这种问题的方法保证断言．这是如何运作的？

n:“保证断言”是一个哲学术语，在数学设置中，指的是可以用完美的理性论证断言的陈述。我的想法是，这个概念可以帮助解决Löbian类型的问题，因为它在某些方面比形式证明更好。例如，在任何一致的公理系统中，都有命题A(n)，它具有这样的性质:对于每一个n值，我亚博体育苹果app官方下载们都可以证明A(n)，而对于“对于所有n, A(n)”的命题没有单一的证明。然而，如果每个A(n)都有保证，那么“对所有n, A(n)”也有保证，这种情况总是存在的。

因此，我介绍了一个谓词框（a）以表达“a是保证的”，并且给出了合适的公理化（这是一个小微妙），我表明我们可以随时推断出框（a）知道禁用A.We still can’t infer A — Löb’s theorem is not violated — but, along the lines I suggested earlier, we can program our agents to accept Box(A) as licensing the same actions that A licenses. Thus, it suffices to prove that the statement “the ship won’t blow up” is warranted. If you go this route then all the paradoxes seem to disappear. If an agent is able to reason about warranted assertibility, then it gets to perform all the actions it intuitively ought to be allowed to perform.

卢克：篇篇文章中，你写道：

［尤多科夫斯基和赫里肖夫(2013)这涉及到一个理性的代理，它正在寻求……将行为的执行委托给另一个代理……同样的问题也出现在一个智能机器的案例中，它正在考虑修改自己的源代码(比如，为了让自己更智能)。在这样做之前，它会想要确定它修改后的状态将会正确地推理，也就是说，它在修改后证明的任何定理都应该是真的。这就遇到了熟悉的Löbian困难，即代理甚至不能确认其预修改推理的正确性。

......在[Yudkowsky＆Herreshoff（2013）的第4节中，两个建筑呈现出无限的独立作用代理的序列，每个结构都可以为激活下一个的可证明的理由提供可提供的理由，但其中没有其中的演绎权均不低于最初规定的水平。结构是聪明的，但它们具有非标准的味道。可能这是不可避免的，除非问题描述是以某种基本的方式改变。在本节的剩余部分中，我们介绍了另一种解决方案，它使用非标准的分数推理。

您能否描述您继续展示的解决方案 - 就缺乏可证明逻辑中缺乏背景的人可能能够理解，至少以直观的方式？

n我试试看!首先，关于我所说的似乎只有非标准的解决方案是可能的，我应该提到现在已经有了由于Herreshoff，Fallenstein和Armstrong造成的定理这使得这个想法更加精确。重点是，我不清楚应该允许建立一个自己的副本，并把我的目标委托给它，因为害怕它会做同样的事情，并无穷无尽地(“拖延问题”)。

现在，回到我的宇宙飞船榜样，让B成为船不会爆炸的声明。断言的基本特征是，我们有一个普遍的法律，即暗示框（a），但我们没有交谈。因此，BOX（B）比B“弱”，我的提议是我们应该允许我们的代理人接受BOX（B）授权B所做的相同行动（建造宇宙飞船）。这有助于Löbian问题，因为B可证明的声明并不意味着B，但它确实暗示了盒子（b）。

但是如果框(B)已经足够好了，为什么不接受更弱的框(B)呢?或盒(盒(盒(B))) ?我写一下Box^k(B)对于k个盒子的一般表达式。将任务委托给继任者的想法是，如果我愿意接受Box^9(B)，那么我应该愿意建立一个不能接受Box^9(B)但可以接受Box^8(B)的继任者。我可以推断，如果我的继任者证明了Box^8(B)，那么Box^8(B)也是可证明的，因此Box^9(B)是正确的，这对我来说已经足够好了。然后我的继任者应该会很高兴地得到一个证明Box^7(B)所需的后续模型，以此类推。所以我们可以用这种方法创建有限链，而不用做任何非标准的事情。

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

卢克现在我来问一下这类研究的一般情况。亚博体育官网你认为这类研究如何发挥作用的模型是什么?亚博体育官网它与当前构建实际软件代理的方法相距甚远。

n：是的，这是非常理论的，毫无疑问。一个模型是纯数学，其实际上是我的背景。在纯粹的数学中，我们正在研究没有任何直接实际应用的问题的大部分时间。我认为经验表明，这种工作偶尔会变得非常重要，而大多数情况下都没有，但很难预测哪些方向会被淘汰出局。

或者，你知道，也许我们都生活在尼克博斯特罗姆说的那样的模拟中。在这种情况下，我们试图弄清楚如何帮助机器使自己更聪明的事实可能是对这种模拟性质的线索。

卢克:你认为有哪些“有希望的途径”可以让我们通过这些理性代理的“悖论”来取得额外的进展?

n： 我不知道。如果你在谈论呼吸障碍，我觉得我们当前的问题描述中缺少了重要的东西。在现在可以使用的指示中，我的偏好是为了Benja Fallenstein的参数多态性。但我也认为我们应该在寻找修改问题描述的方法。

卢克:您对理性代理的悖论感兴趣的根源是什么?

n：我一直在考虑周围真相和循环的问题大约五年。（我刚检查过：我的最早的纸2009年5月发表在《数学arXiv》上。)这是纯粹的理论工作，来自于对数学和逻辑基础的兴趣。

我参与理性代理机构的悖论埃利泽·尤多科夫斯基和马塞洛·赫里肖夫关于洛比安障碍的论文．事实上，我认为我从那篇论文中得到了“理性代理的悖论”这个术语。当我读到它的时候，我的第一反应是我关于断言性的想法应该是相关的，所以这就是我感兴趣的原因。

卢克:谢谢你,尼克!