MIRI的研究指南金宝博娱乐

,内特苏亚雷斯

---

如果人类想要开发出比人类更聪明的具有积极影响的人工智能，我们必须迎接三个艰巨的挑战。首先，我们必须设计出比人类更聪明的系统金宝博官方高度可靠，这样我们就有理由相信系统会满足特定的目标或偏好。金宝博官方第二，设计必须是宽容，使系统在面对不可避免的人为金宝博官方错误时，能够在线修改和修正。第三，系统必须实际学习金宝博官方有益的目标或偏好。

MIRI目前的研究项目集中在了金宝博娱乐解如何原则上应对这些挑战．可靠推理的某些方面我们甚至在理论上都还不了解;即使在简化的环境中，我们也无法解决有限理性的问题。作为第一步，我们的研究重点是在简化的环境中寻找解决方案。因此，我们的现代研究看起来更像是纯数学，金宝博娱乐而不是软件工程或实际的机器学习。

本指南简要概述了我们的研究重点，并提供资源，将帮助您获得每个学科领金宝博娱乐域的前沿。本指南不打算证明这些研究主题;金宝博娱乐关于我们的方法的进一步动机，请参阅文章“美里的方法，还是要我们的技术议程和支持文件．

注(2016年9月):本研究指南是基于我们的金宝博娱乐代理基金会议程．截至2016年，我们还有一个机器学习聚焦议程．关于我们认为有前途的、本指南没有涉及的研究方向的更多信息，请参阅该文件。金宝博娱乐

如何使用本指南

本指南适用于有抱负在相关主题领域的研究人员。金宝博娱乐如果您已经是AI专业人员或经验丰富的数学家，请考虑跳到我们的现有的出版物反而。（我们的技术议程是一个很好的起点。)本指南适用于那些想要成为MIRI研究人员的学生，以及其他领域想要跟上我们工作的专业人士。金宝博娱乐

金宝博娱乐研究人员通常会通过两种途径中的一种加入我们的团队。首先是参加MIRI研讨会，并亲自与我们建立关系。您可以使用这种形式申请参加研究研讨会。金宝博娱乐要注意的是，车间之间经常有相当长的时间，而且它们的能力有限。

第二种方法是独立地在我们的研究议程上取得一些进展，并让我们知道你的结果。金宝博娱乐您可以使用我们的在线表单在你的工作上申请帮助或投入，但是开始贡献的最快的方法是阅读智能代理基础论坛(IAFF)，注意人们正在处理的开放问题，并解决一个。然后你可以把你的结果作为关联在论坛上。

（2019年3月更新错误和错误AI对齐论坛现在是我们公开讨论人工智能校准问题的场所，取代了IAFF。查看这篇文章的顶部，以获得对这部分建议的其他更新。)

研究论坛的主要目的是让已经在同一页面上的研究人员讨论未金宝博娱乐经修饰的部分结果。因此，论坛上的帖子可能相当不透明。本研究指南金宝博娱乐可以帮助您快速了解IAFF上正在讨论的开放问题。它还可以帮助你发展必要的技能，使你有资格参加研讨会，或找到方法，在其他机构的人工智能校准中解决开放性问题。

本指南首先介绍了一些基础学科的建议，在尝试这种类型的研究之前，了解这些学科是很重要的，比如概率论。金宝博娱乐在那之后，它会被分解成一系列的主题区域，并提供论文的链接，让你了解该领域的最新技术。

这不是一个线性指南:如果你想成为一个MIRI研究员，我建议首先确保你理解了基础，然后选择一个你感兴趣的主题，深入该金宝博娱乐领域。一旦你很好地理解了一个主题，你就可以在IAFF上尝试在这个主题领域做出贡献。

对于本指南中的所有材料，请不要为了磨而磨。如果你已经了解了材料，那就跳过它。如果其中一个活跃的研究领域不能吸引你的兴趣金宝博娱乐，切换到另一个。如果你不喜欢推荐的课本，找一本更好的，或者干脆跳过。这个指南应该作为一个工具，让你知道你可以在哪里做出贡献，而不是作为实现目标的障碍。

最基本的

重要的是要有一些流利的基本数学概念，然后直接进入我们积极的研究主题。金宝博娱乐我们所有的研究领域都很金宝博娱乐好地服务于计算，逻辑和概率论的基本理解。下面是一些帮助你入门的资源。

你不需要按列出的顺序阅读这一部分的书。选择任何有趣的内容，在必要时不要犹豫，在研究领域和基础知识之间来回跳转。金宝博娱乐

集理论 大多数现代数学是在集合理论中形式化的，这里列出的教科书和论文也不例外。这使得集合理论成为一个很好的起点。 第1-18章 可计算性和逻辑 可计算性理论(以及对角化带来的限制)是理解机器能做什么和不能做什么的基础。 1 - 4章 概率论 概率理论是对理性机构的理解的核心。在不确定性下，一些熟悉推理在我们所有活跃的研究领域都至关重要。金宝博娱乐 1 - 5章 概率推断 这本书将帮助充实的理解如何推理可以完成使用概率世界模型。 统计数据 流利地使用统计模型将有助于为我们的“高级机器学习对齐“研金宝博娱乐究议程。先熟悉一下概率推理是个好主意。 机器学习 强烈推荐，制定对机器学习的实用熟悉Andrew Ng的Coursera课程(课堂讲稿这里）。对于ML的更为理论介绍，请尝试了解机器学习． 人工智能 虽然我们的很多工作都是理论上的，但现代人工智能领域的知识对于我们把这项工作放在具体情境中来说是很重要的。

理解VNM理性的概念也很重要，我建议从中学习维基百科的文章但也可以从原书籍．冯·诺依曼和摩根斯特恩表明，任何服从几个简单一致性公理的代理行为都具有效用函数所描述的偏好。虽然有些人认为，为了构建可靠的智能代理，我们可能最终需要放弃VNM的合理性，但VNM框架仍然是我们拥有的描述任意强大代理行为的最有表现力的框架。(例如，参见正交性的论文和仪器收敛的论文从博斯特罗姆的“有超常智慧的意志。VNM合理性的概念贯穿于我们所有积极的研究领域。金宝博娱乐

现实世界模型

如果您的智慧比人类系统不可靠，您可以正式化有益目标。金宝博官方甚至原则上，我们还没有理解的良好推理。它可能通过建立使用算法的实用系统来获得洞察力，这些系统似乎工作的算法，即使他们工作的原因尚未理解：通常，在实际应用的次唤金宝博官方醒之后，理论理解就遵循。然而，我们考虑这种方法在设计具有潜力的系统时，我们将在尝试创建实际的高层系统之前手头有一般情报理论，更安全。金宝博官方

由于这个原因，我们的许多积极的研究主题集中在我们还不知道如何解决的一般智金宝博娱乐力部分，甚至在原则上。例如，考虑以下问题:

我有一个计算机程序，被称为“宇宙”。宇宙中只有一个函数是未定义的。你的工作是给我提供一个适当类型的计算机程序来完成我的宇宙程序。然后，我会运行我的宇宙程序。我的目标是给你的代理打分根据它对原始宇宙程序的了解程度。

我怎么能这么做?所罗门诺夫的归纳推理理论为理论解决方案提供了一些启示:它描述了一种从观察中做出理想预测的方法，但仅在预测者生活在外部环境的情况下。所罗门诺夫归纳法产生了许多思考归纳推理的有用工具(包括柯尔莫哥洛夫复杂性、普遍先验和AIXI)，但如果主体是宇宙的一个子过程，由宇宙计算，那么问题就明显变得更加困难了。

在主体嵌入环境的情况下，归纳问题就变得模糊了:什么算“学习宇宙程序”?根据什么样的环境分布应该对代理进行评分?在“主体”和“环境”的边界变得模糊的情况下，什么构成理想归纳?这些都是归化归纳法的问题。

1. 苏亚雷斯’”形式化现实世界的两个问题模型"进一步激发了归化归纳法的问题这与一般智力理论的构建有关。

2. “牵牛星”的“索罗门归纳法的直观解释“解释了Solomonoff的归纳推理理论，这是了解归化诱导的开放问题时的重要背景知识。

3. Bensinger的“归化诱导(系列)更详细地探讨归化归纳法的问题。

解决归化诱导的问题需要更好地了解现实世界模型：什么是“可能的现实”？关于环境的哪种前沿是理想的代理商使用？这些问题的答案不仅必须允许良好的推理，他们必须在世界模型方面允许规范人体目标。

例如，在Solomonoff归纳中(以及在Hutter的AIXI中)，图灵机被用来对环境建模。假设我们唯一看重的是钻石(碳原子与另外四个碳原子共价结合)。现在，假设我给你一台图灵机。你能告诉我里面有多少钻石吗?

为了设计一个追求其世界模型中特定目标的代理，代理必须有某种方法来识别其世界模型(图灵机)中我们的目标(碳原子)的本体。这个“本体识别”问题在“形式化现实世界模型的两个问题”(链接上)中讨论，由De Blanc首先介绍:

4. 德布兰科的“人工主体价值体系的本体论危机金宝博官方“询问如何使代理商的目标变得更加强大，以便在本体的变化。如果代理从物理学的原子模型开始（其中碳原子在本体基础上），那么这可能并不难。但是，当代理商建立物理核模型时会发生什么（其中原子由中子和质子构成）？如果“碳识别器”是硬编码的，则该代理可能无法识别这个新的世界模型中的任何碳，并且可能奇怪地开始行动（寻找隐藏的“真正碳”）。该代理程序如何设计，以便在对本体论危机中成功地用“碳原子”识别“六个质子原子”？

决策理论

说我给你以下内容：（1）描述宇宙的计算机程序;（2）描述代理人的计算机程序;（3）代理商可用的一组行动;（4）宇宙已经进入的状态历史记录的一组偏好。我在识别这些偏好方面识别代理的最佳动作。例如，您的输入可能是：

def Universe(): outcomes = {Lo, Med, Hi} actions = {1,2,3} def Agent(): worldmodel = {Lo: One, Hi: Two, Med: Three} return worldmodel[Hi] territory = {One: Lo, Two: Med, Three: Hi} return territory[Agent()]

def Agent(): worldmodel = {Lo: 1, Hi: 2, Med: 3} return worldmodel[Hi]

action = {1, 2, 3}

嗨> Med > Lo

(请注意代理是如何嵌入到环境中的。)这是另一个我们不知道如何回答的问题，即使是在原则上。这似乎很简单:只需迭代每个行动，找出如果代理采取该行动会得到什么结果，然后选择导致最佳结果的行动。但事实上,在这个思想实验,代理是一个确定的子流程确定的计算机程序:有一个行动,代理将输出,并要求“会”如果一个确定的确定性项目的一部分的东西它不做是不明确的。

为了评估如果主体采取了不同的行动“会发生什么”，必须构建一个“反事实环境”(主体做了它没有做的事情)。令人满意的反事实推理理论还不存在。即使在理论上，即使我们对宇宙和我们的偏好有充分的了解，并拥有无限的计算能力，我们仍然不知道如何识别嵌入在其环境中的代理所能采取的最佳行动。

解决这个问题需要更好地理解反事实推理;这是决策理论的领域。

决策理论 彼得森的教科书概括地解释了规范性决策理论的领域。对于更快速的调查，更侧重于纽库姆式问题，参见米尔豪泽的“决策理论常见问题解答．” 博弈理论 决策理论中的许多开放性问题都涉及到多智能体设置。我听说过塔德里斯的教科书，但我自己还没有读过。斯科特·亚历山大的也有可能博弈论概论“LessWrong。 1 - 5章 (如果热情+ 6 - 9) 只是逻辑 多智能体设置的玩具模型可以在这样的环境中进行研究，在这样的环境中，智能体的行动基于它们能够证明的关于同一环境中其他智能体的事情。我们目前的玩具模型大量使用可证明性逻辑。

现有的反事实的推理方法在短期内都是令人不满意的(在这个意义上他们系统地实现贫困结果在一些问题上好的结果是可能的)和长期(在这个意义上使用坏反设事实将变为无效来代理推理,金宝博官方根据那些破碎的反事实，决定他们不应该修复所有的缺陷)。我的演讲”你为什么不富有?这两个问题都简要地谈了一下。为了了解更多，我建议使用以下资源:

1. 苏亚雷斯和法伦斯坦的"走向理想化的决策理论，并进一步激发与MIRI研究计划相关的决策理论问题。金宝博娱乐本文讨论了两个现代决策理论的缺点，并讨论了决策理论中指向执行反事实推理的新方法的一些新见解。

如果“走向理想化的决策理论”进展太快，这一系列的博客文章可能是一个更好的起点:

2. Yudkowsky的“真正的囚徒困境解释了为什么合作并不是自然而然的‘正确’或‘好的’选择。

3. 苏亚雷斯’”因果决策理论并不令人满意，用囚徒困境来说明决策算法之间非因果联系的重要性。

4. Yudkowsky的“纽科姆的问题与理性的遗憾“专注于”获胜“的决策理论，不仅仅是似乎直观合理的决策理论。苏亚雷斯’”介绍类纽康姆问题的内容类似。

5. 苏亚雷斯’”纽康姆式的问题是常态“注意人类代理概率地根据常规基础逐步模范彼此的决策标准。

Miri的研究金宝博娱乐导致了“更新决策理论”（UDT）的发展，这是一种解决上述许多缺点的新决策理论。

6. 迈克的“预测困境中的问题类别优势总结了UDT对其他已知决策理论的主导地位，包括永恒决策理论(TDT)，另一个主导CDT和EDT的理论。

7. Fallenstein的“具有逻辑语句之上的具体优先级的UDT模型提供了一种概率形式化。

但是，UDT绝不是解决方案，并且在以下地方讨论了自己的许多缺点：

8. Slepnev的“UDT中自我实现伪证明的一个例子解释了UDT是如何由于伪造证据而获得次优结果的。

9. Benson-Tilsen的“已知搜索顺序的UDT是一个有点令人不满意的解决方案。它包含了一个具有已知证明搜索顺序的UDT的形式化，并演示了使用一种称为“与宇宙对抗”的技术以避免虚假证明的必要性。

为了研究多智能经纪人的设置，帕特里克·瓦特奥尔已经开发出了莫代尔代理商框架，这也使我们能够在决策理论领域进行一些新的进展，使我们在决策理论领域进行一些新的进展：

10. Barasz等人的"囚徒困境中的稳健合作“允许我们考虑代理商，它们只根据自己的能力来决定是否相互合作证明关于彼此的行为。这可以防止无限倒退;事实上，两个行为人的行为只能根据他们对另一个行为人的行为的证明，可以在二次时间内使用可证明性逻辑的结果来确定。

逻辑的不确定性

想象一个黑匣子，有一个输入溜槽和两个输出溜槽。一个球可以放入输入滑槽，它将从两个输出滑槽之一出来。在黑盒子里面是一个Rube Goldberg机器，它把球从输入槽带到一个输出槽。

一个不知道盒子里是哪个Rube Goldberg机器的完美概率推理者也不知道盒子会如何运作，但如果他们能知道盒子里是哪个机器，那么他们就会知道哪个滑道会带走球。这个寻欢环境不确定．

一个现实的推理者可能知道盒子里是哪台机器，可能知道机器是如何工作的，但可能缺乏推断出机器将在哪里犯错的能力。这个寻欢逻辑上不确定。

概率论假定逻辑无所不知;它假定推理者知道他们所知道事物的所有结果。在现实中，有限理性者在逻辑上并不是无所不知的:我们可以精确地知道盒子里装的是哪台机器，机器是如何工作的，只是没有时间推断出球是从哪里出来的。我们在逻辑的不确定性下进行推理。

在逻辑不确定性下进行推理的正式理论还不存在。当涉及到构建一个高度可靠的普遍智能系统时，获得这种理解是极其重要的:无论何时，一个代理推理复杂系统、计算机程序或其他代理的行为，它必须在至少一点逻辑不确定性下运行。金宝博官方

要了解这门学科的现状，必须对概率论有扎实的了解;考虑扩充前几章我们与樵夫，第1、5、6、9章，然后研究以下论文:

1. 苏亚雷斯和法伦斯坦的"在逻辑不确定性下推理的问题“提供一般介绍，解释了逻辑不确定性领域，激励其与Miri的研究计划的相关性。金宝博娱乐

2. Gaifman的“关于一阶计算的措施他在许多年前就研究过这个问题。Gaifman主要关注一个相关的子问题，即对一个正式系统的不同模型的概率分配(假设一旦模型已知，该模型的所有结果都已知)。金宝博官方我们现在尝试这种方法扩大到一个更完整的概念逻辑的不确定性(推理程序可以知道模型是什么但不知道模型)的影响,但通过Gaifman仍是有用的历史背景和理解周围的困难逻辑的不确定性。

3. Hutter等人的"表达逻辑中句子的概率主要研究逻辑不确定性的问题，假设访问无限的计算能力(和许多级别的停止oracle)。理解Hutter的方法(以及用无限的计算能力可以做些什么)有助于充实我们对难题所在的理解。

4. Demski的“合理的先验概率“提供可计算地近似的逻辑。在Demski之后，我们的工作主要侧重于创建逻辑句子的可近似概率分布，因为精炼和近似逻辑事先的行为非常类似于在逻辑不确定性下的推理行为。

5. global的“非全知、概率推理和元数学基本上遵循这种方法。本文提供了一些关于逻辑先验生成的早期实际考虑，并强调了一些悬而未决的问题。

视频反思

人工智能问题的独特之处在于，一个足够先进的系统将能够比人类程序员做更高质量的科学和工程。金宝博官方一个先进的系统的许多可能的危险和好处源于它能够引导自身到更高水平的能力，可能导致金宝博官方智力爆炸．

如果一个智能体通过递归自我完善实现了超智能，那么结果系统的影响完全取决于初始系统可靠地推理出比自己更智能的智能体的能力。金宝博官方一个系统可以使用什么样的推理方法来证明一个更加智能的系统的行为具有极高的可信度金宝博官方?我们称这种推理为“文根式反思”，以弗诺·文奇(1993)，他指出，一般来说，不可能精确预测比推理者更聪明的代理者的行为。

一个进行文根式反思的推理者必须进行推理抽象关于更智能的代理。这几乎肯定需要某种形式的高度自信的逻辑不确定推理，但是代替一个工作理论的逻辑不确定，证明推理(使用形式逻辑)是研究抽象推理的最好的形式主义。因此，对Vingean反思的现代研究需要以形式逻辑为背景:

一阶逻辑 MIRI现有的用于研究自修正agent的玩具模型很大程度上基于这一逻辑。理解一阶逻辑的细微差别对于使用我们开发的工具来研究能够在类似系统中接近自信的形式系统是至关重要的。金宝博官方

我们通过构建能够在高度相似的系统中获得某种形式信任的代理的玩具模型来研究Vingean反射。金宝博官方要了解这一领域的前沿，请阅读以下论文:

1. 《Fallenstein & Soares》Vingean反思:自我改进代理的可靠推理介绍了Vingean反思的领域，并激发其与MIRI的研究项目的联系。金宝博娱乐

2. Yudkowsky的“拖延悖论在Löbian障碍(一个由于“自信”太少而产生的问题)和不可靠之间行走的微妙界线上，需要更多的细节来获得令人满意的解决方案很多自信。

3. Christiano等人。的“概率逻辑中真理的可定义性描述了一个早期的尝试，即创建一个能够对自身进行推理，同时避免自我参照悖论的正式系统。金宝博官方它成功了，但最终被证明是不可靠的。我的预排本文可能有助于将其放入更多的背景中。

4. 《Fallenstein & Soares》自我改进时空嵌入智能中的自我参照问题“描述了我们的简单建议 - 验证者模型，用于研究产生略微改进的自己或”瓷砖“自己的代理商。本文演示了一种玩具场景，其中声音代理可以成功地铺设到（例如，高度信心）其他类似药剂。

可订正

随着人工智能系统在智能和能力方面的发展，它们的一些可用选金宝博官方项可能允许它们抵制程序员的干预。我们称一个人工智能系统是“可金宝博官方矫正的”，如果它与它的创造者所认为的纠正性干预进行合作，尽管理性的行为主体会抗拒关闭它们或修改它们偏好的尝试。

这一研究领域基本上是全新的，金宝博娱乐所以要想跟上进度，只需阅读一篇或两篇论文:

1. 苏亚雷斯等人的"可订正介绍了该领域的总体情况，以及一些未解决的问题。

2. 阿姆斯特朗的“在冷漠中学习才是正确的价值“讨论一种在其最大化的实用功能之间漠不关心的一种潜在方法，这是朝向允许自我修改的代理的一小步。

我们目前在可纠正性方面的工作主要集中在一个称为“关机问题”的小子问题上:您如何构建一个在按下关机按钮时就关机的代理，并且该代理没有导致或阻止按下按钮的动机?在这个子问题中，我们目前关注的是效用无关的问题:你如何构建一个代理，它允许你切换它最大化的效用函数，而不给它激励来影响转换是否发生?即使我们对效用无关问题有一个满意的解决方案，这也不会对关闭问题产生一个满意的解决方案，因为似乎仍然很难以一种不受反常实例化影响的方式充分指定“关闭行为”。Stuart Armstrong写了几篇关于“减少影响”规范的博客文章AGIs:

3. ”驯化减少了ai的影响”
4. ”减少影响AI:没有后台通道”

这些最初的尝试还不是一个完整的解决方案，但它们应该能让您快速了解我们目前对这个问题的理解。

值的学习

由于我们对我们的价值观的理解是模糊和不完整的，可能是将值加载到强大的AI中最有希望的方法是指定代理的标准学习我们的价值观不断。但这也带来了一些有趣的问题:

假设您构建一个培训集，其中包含许多充满幸福人类的成果（标有“好”）和充满悲伤人类的其他结果（标记为“坏”）。从这个数据来看，最简单的概括可能是人类真的就像人形微笑 - 事情：然后这个代理人可以试图建立许多微小的animatronic快乐的人。

价值学习必须是在线进程：系统必须能够识别歧义并向用户提出有关这些歧义的查询。金宝博官方它不仅必须识别它不知道如何分类的情况（例如它不能判断脸是否看起来快乐或悲伤），但也确定训练数据没有提供任何信息的维度(例如，当你的训练数据永远不会显示充满了看起来快乐、被贴上无用标签的人形机器人的结果时)。

当然，光有模糊性识别是不够的:你不希望一个系统,花前三周要求澄清金宝博官方人类是否仍然值得在不同海拔高度时,或当风吹,最后(运营商停止后注意)问是否重要的是人形的东西是自己的意志。

为了让代理可靠地学习我们的意图，代理必须构造和细化其操作符的模型，并使用该模型通知其查询和更改其首选项。要了解有关这些问题和其他问题的更多信息，请参见以下内容:

1. 苏亚雷斯’”价值学习问题“提供与价值学习相关的一些公开问题的一般概述。

2. 杜威的“了解什么是有价值的进一步探讨了价值学习的难度。

3. 这正交性的论文认为价值学习不会被默认解决。

4. 麦卡斯基尔的“规范的不确定性“提供讨论规范性不确定性的框架。被警告，全部工作，同时包含许多洞察力，很长。你可以逃脱掠夺零件和/或跳过一些，特别是如果你对其他积极研究的其他领域更兴奋。金宝博娱乐

其他工具

掌握在任何主题中都可以是一个非常强大的工具，尤其是在数学领域，看似不相交的主题实际上是深切的。许多数学领域都有这样的财产，如果你非常了解它们，那么无论你去哪里都很有用。考虑到这一点，虽然下面列出的主题是不需要理解Miri的主动研究，但对这些主题中的每一个的理解构成了数学工具箱中的额外工具，通常在进行新的研究时经常证明非常有用。金宝博娱乐

离散数学 教科书可用在线．大多数数学研究的不是连续结构就是离散结构。许多人发现离散数学更直观，对离散数学的扎实理解将帮助您快速掌握许多其他数学工具的离散版本，如群论、拓扑学和信息论。 线性代数 线性代数是数学中随处可见的工具之一。对线性代数的扎实理解将在许多领域有帮助。 类型理论 集合理论通常作为现代数学的基础，但它不是唯一可用的候选。类型理论也可以作为数学的基础，并且在许多情况下，类型理论更适合于手头上的问题。类型理论还弥补了计算机程序和数学证明之间的理论差距，因此通常与某些类型的人工智能研究有关。金宝博娱乐 范畴论 类别理论研究许多数学结构在非常高的抽象中。这可以帮助您注意不同分支的数学分支模式，并使您的数学工具从一个域转移到另一个域。 拓扑 拓扑学是另一门在数学中随处可见的学科。对拓扑学的深刻理解在许多意想不到的地方都很有帮助。 可计算性和复杂性 MIRI的数学研究正致力金宝博娱乐于最终与计算机程序相关的解决方案。对计算机的能力有一个良好的直觉往往是必不可少的。 节目验证 程序验证技术使程序员能够确信特定的程序将根据某些规范实际执行。(当然，仍然很难验证规范是否描述了预期的行为。)虽然MIRI的工作目前并不关心验证真实世界的程序，但了解现代程序验证技术能做什么和不能做什么是非常有用的。

了解任务

为什么首先要做这种研究?金宝博娱乐

超智 本指南在很大程度上假设你已经参与了MIRI的任务，但如果你想知道为什么这么多人认为这是一个重要而紧迫的研究领域，金宝博娱乐超智提供良好的概述。 合理性:从AI到僵尸 这本电子巨著汇编了六卷论文，解释了MIRI对人工智能观点背后的许多哲学和认知科学。 不平衡 对微观经济学和认识论的讨论，他们承担了对社会误解和盲点的讨论，包括被忽视的研究机会。金宝博娱乐试图回答基本问题，“雄心勃勃的项目何时可以实现不寻常的目标希望成功？”