論文「囚人のジレンマにおける頑健な協力：証明可能性論理によるプログラム均衡」は、友好的AI（FAI）に明示的に関わる研究目標から生まれた理論的進歩の中でも、わかりやすい事例の一つだ。この友好的AI研究の事例から、何を学べるだろうか。成果はどのように得られたのか。アイデアはどう積み重なったのか。誰がどの部分に貢献したのか。どのような相乗効果が重要だったのか。
これらの問いに答えるため、「頑健な協力」の成果に貢献した多くの人に話を聞いた。
話は2011年12月から始めよう。チューリヒでGoogleのエンジニアをしていたウラジーミル・スレプネフが、モスクワのコンピューター科学の大学院生ウラジーミル・ネソフとの共同研究をまとめた「停止オラクルを用いたUDTのモデル」を投稿した。((更新なし意思決定理論そのものが発展してきた経緯は別の話なので、ここでは詳しくは述べない。この経緯を簡潔に知るには、ネソフの「定数プログラムを制御する」の「先行研究」の節と、このコメントが参考になる。ネソフがUDTの発展をごく手短にまとめると、こうなる。「（1）エリエゼル・ユドコウスキーの、TDTについての初期の非形式的な発言と、アンナ・サラモンの記事によって、ある種の状況は通常と異なる依存関係でモデル化すべきだという点が浮上し、適切なモデルをどう選ぶか、つまり依存関係をどう推論するか、という問いが生まれた。（2）ウェイ・ダイのUDTの記事は、その一つの方法を概説していた。しかし当時の私は、それをこの問いへの答えとは理解していなかった。最終的には、2010年5月に、プログラムがプログラムを制御する場合について解明した。意思決定理論のメーリングリストでの議論の後、スレプネフがこの手法を囚人のジレンマ（PD）に適用した。（3）その後、より一般的な手法をスレプネフと私が書きまとめた。スレプネフの記事は技術的な内容が多く、私の記事はより推測的で、理論をよりよく捉える方法を探そうとするものだった。「『できる』の還元はどのようなものになりうるか」「定数プログラムを制御する」「環境全体を介した制御における選好の概念」がそれだ。（4）『見せかけの道徳的論証』をめぐっては、まだ技術的な問題がいくつもあった。ベンジャ・ファレンシュタインのこのコメントと、「UDTにおける自己成就的な見せかけの証明の例」を参照してほしい。（5）一つの解決策は、意思決定アルゴリズムに『チキン・ルール』を加えることだった。私は2011年4月、プログラムがプログラムを制御する場合についてこれを見いだし、意思決定理論のメーリングリストで少し議論した。だが、2011年12月の同じメーリングリストでの別の議論で登場した、停止オラクルを使う設定では、この方法が理論的にはるかに頑健であることがわかった。スレプネフがそれを書きまとめたのが「停止オラクルを用いたUDTのモデル」だ。私も後に「意思決定の予測可能性と対角化法」にまとめた。（6）この対角化の仕掛け、つまりチキン・ルールを使って、スティエノンがオラクルのある場合のPDでの協力を書きまとめた。これは、スレプネフのそれ以前の、オラクルなしのPDの解法よりも理論的に扱いやすかった。（7）この時点で、見せかけの証明の問題を抱えないUDTの形式化と、それをPDのような非自明な問題に適用する実例の両方が揃った」。))この投稿は、初めてと言ってもよい形で、((研究者によっては、スレプネフが2010年8月に投稿した「『できる』の還元はどのようなものになりうるか」こそが、UDTの「最初の形式モデル」を示したと考えるかもしれない。))ウェイ・ダイの更新なし意思決定理論（UDT）の形式モデルを提示し、ニューカム問題に直面したUDTエージェントが「勝つ」ことを示した。ただし、宇宙を表すプログラムと、その中のエージェントを表すサブプログラムが、停止オラクルを使えるならば、という話だ。スタンフォードの数学の大学院生ニサン・スティエノンは、スレプネフの形式化を、ペアノ算術を使って協力を証明する問題に適用し、「意思決定エージェントのように振る舞う算術の式」（2012年2月）にまとめた。((スティエノンの記事は、一段階ではなく二段階の「チキン・ルール」を使うことで、形式化そのものも改善した。))
この二つの記事がUDTの形式化に成功したことに刺激を受け、マディソンで数学のポスドクをしていたパトリック・ラヴィクトワールは、無時間意思決定理論（TDT）の「半形式的な分析」を試みた。TDTは、MIRIの創設者エリエゼル・ユドコウスキーがそれ以前に考案した意思決定理論で、UDTにとっても大きな着想源だった。三つの準備的な記事を経て、ラヴィクトワールは2012年4月に、TDTに多少似たものの形式化に成功したと考えた。
他のTDT／UDT研究者からはあまり反応がなかった。そこで2012年7月、CFARのワークショップに参加するためサンフランシスコのベイエリアを訪れた際、ユドコウスキー、スティエノン、バークレーのコンピューター科学の大学院生ポール・クリスティアーノらを探し出し、TDTを形式化する試みについて話した。その反応は、彼がこのアプローチを続けようと思えるほどには、好意的だった。
2012年8月にスレプネフがベイエリアを訪れたときにも、ラヴィクトワールは自分の研究について話した。スレプネフは、ラヴィクトワールのTDTの形式化の試み――今では「Masquerade」と呼ばれていた――に、レーブの定理に関わる理由で致命的な欠陥があると指摘した。しかし2012年9月、ラヴィクトワールは、Masqueradeが異なる形式体系のあいだを段階的に上がっていくようにして、問題を修正できた。この時点で、「頑健な協力」論文の初期草稿を書き始めた。
スレプネフが最適性についての結果の重要性を強調したため、ラヴィクトワールは同月後半、最適性の概念の候補を考案した。そして10月、その定義ではMasquerade自体が最適ではないことに気づいた。MIRIの2013年4月のワークショップが始まった時点で、状況はおおむねここまで進んでいた。
ワークショップの初めに、ラヴィクトワールは、ほかの参加者にMasqueradeを解説した。Masqueradeに手を加えていくうちに、様相エージェントという概念が生まれた。ラヴィクトワールと、チューリヒのGoogleエンジニア、ミハーイ・バラスは、こうしたエージェント同士が対戦するときの行動を、機械的に検証する方法を探し始めた。最終的に、バラスと、ベイエリアのGoogleエンジニア、マルチェロ・ヘレスホフが、様相エージェント間の相互作用のモデル検査器を開発した。これにより、相手となるエージェントに対してどの選択をするかを、機械的に証明できるようになった。
4月のワークショップの終盤に、クリスティアーノがPrudentBotを開発した。これは、ある意味で現在の論文の「主役」だ。ワークショップ中には、ユドコウスキー、ブリストル大学の大学院生ベンジャ・ファレンシュタインらも貢献した。ラヴィクトワールは、4月のワークショップの成果を草稿に反映し、2013年6月にLess Wrongへ投稿した。
その後、MIRIの2013年9月のワークショップで、南カリフォルニア大学の哲学者ケニー・イーシュワランが、搾取されないエージェントならどれも、ある種のWaitFairBotを相手にすると、いずれ最適化に失敗せざるをえないことを証明するのは、ラヴィクトワールが予想していたより難しいと気づいた。ヘレスホフはこれを補おうとしたが、ささやかな結果のために、証明のために論文のその節が元の姿もわからないほど膨らんでしまったため、ラヴィクトワールは論文から外すことにした。
2013年12月、ファレンシュタインは、二つの様相エージェントの行動が、その様相論理による記述だけに依存することを、論文が十分に示せていないと気づき、一連の修正を加えた。ラヴィクトワールは再び論文を修正し、共著者の同意を得て、2014年1月に修正版をarXivへアップロードした。
では、「頑健な協力」論文の成果には、どのような意味と意義があるのだろうか。少なくとも、ラヴィクトワールの見方はこうだ。
様相エージェントの対戦（modal combat）の意義は、高度な意思決定理論の概念を研究できる小さな模型の宇宙だという点です。少し手を加えれば、脅迫など、ほかの概念の研究にも使えるかもしれません。そしてこの宇宙の中では、直感的に魅力のある超合理性という考え方が、実際にうまく機能します。少なくとも、よいコミュニケーションがあれば、通常必要とされる強制や処罰のコストなしに協力を可能にできること、そして合理的なエージェントのあいだには、単純さと検証可能性へ向かうインセンティブがあることを示す、哲学的なヒントではあります。
実際、これは反復囚人のジレンマのトーナメントに対応する、さらに基礎的なものです。アクセルロッドの反復囚人のジレンマ（IPD）のトーナメントが、「厳しいが公正」の有用性を示し、互恵的利他主義を促す進化上のインセンティブという考えにつながったのと同じように、様相エージェントの対戦は、「超合理性」の論理を示すための有用な実験場だと思います。さらに、この対戦はIPDの特徴を多く含んでいます。推論の段階は、あるエージェントと別のエージェントとの過去のやり取りに、いくらか似ています。そして、アルゴリズムの高度さに比べて、その文法はきわめて単純なのです。