← 研究の方向性

オープンソース・ゲーム理論

AIシステムからなる社会を想像するなら、その社会が協働と協力を育み、欺瞞と不信を最小限に抑えるものであってほしい。1つの理想像では、個別のアラインメント問題は解決されており、各個人・政府・企業などの主体は、自らの価値観を忠実に代弁するAIシステムを持っている。だがそのような世界でさえ、これらのシステムは互いに交渉しなければならない。このゲーム理論的な問題をどうモデル化し、どのように推論すればよいだろうか。

1つのアプローチは、人間の脳とは違って、AIシステムはそのコードを検査できるおかげで高い透明性とアクセス可能性を持つ、という事実を利用する。そこで、互いのソースコードを読めるAIシステムの世界をモデル化することは理にかなっている。「あなたが協力するなら、私も協力する!」という考えを、厳密かつ形式的なものにしようと試みるのだ。

形式的には、ある OtherBot と出会い、自身のソースコードの中で次の計算を行う FairBot を考えよう: OtherBotが私に協力することを証明できる場合、かつその場合に限り、私はOtherBotに協力する。

ここで少し立ち止まる価値がある。というのも、自分自身のソースコードを直接参照することは、技術的には不可能だからだ。この種の自己言及はよく研究されている。すべての計算可能関数を枚挙しておき、数 $f$ に対して、「 $f$ に対応する関数の上で $O$ が協力するという証明が存在する場合、かつその場合に限り $O$ に協力するプログラム」を $FairBot(f)$ と書けばよい。するとクリーネの再帰定理(Kleene's recursion theorem)により、対応する関数がちょうど $FairBot(f)$ となるような $f$ が得られる。これにより FairBot は、無限後退なしに完全に厳密に規定される。

FairBot が搾取されることは決してない。裏切る相手に対して協力することは決してないからだ。しかし、これだけでは不十分である。常に裏切ることでも同じ性質は得られてしまう。FairBot が自分自身に対して協力するというのが、Robust Cooperation in the Prisoner's Dilemma の定理である。

定理 (レープの定理)。 $□$ を、十分に強い形式的理論における証明可能性を表すものとする。その理論が $□P \to P$ を証明するならば、その理論は $P$ を証明する。様相論理の記法で同値に書けば:

□(□P → P) → □P.

FairBot が自分自身と協力することを見るには、 $Q$ を $FairBot(FairBot) = C$ という言明とすればよい。FairBot のソースコードにより、 $□Q \to Q$ が証明できる。 $Q$ にレープの定理を適用すれば、結論が得られる。

以下では、FairBot を DUPOC (Defect Unless Proof Of Cooperation、協力の証明がなければ裏切る) と呼ぶことにする。

より興味深い相互作用

より興味深いエージェントを定義することもできる。CUPOD は相手が裏切ることを証明できない限り協力し (Cooperate Unless Proof Of Defection)、DUPOC は相手が協力することを証明できない限り裏切る。これらのロボットが互いに対してどう振る舞うかは、すぐには明らかでない。CUPOD も DUPOC も、FairBot に対しては協力する。

定理 (CUPODとDUPOCの自己対戦)。 Cooperative and uncooperative institution designs の有界設定において、十分大きなすべての証明長の上界 $k$ に対して、

outcome(DUPOC(k), DUPOC(k)) = (C,C)

かつ

outcome(CUPOD(k), CUPOD(k)) = (D,D).

これは直観に反する。CUPOD のほうが優しいロボットに見えるのに、自分自身に対しては裏切るのだ。完全に形式的ではないものの、直観の源になりうる見方はこうだ: CUPOD が自分自身と協力するのは、「協力しない」ことの証明が存在しない場合である。しかし証明体系の無矛盾性を仮定すると、何かの証明が存在しないことを示すことは決してできない。

このことは、DUPOC 対 CUPOD を考えるとよりはっきり現れる。CUPOD が何らかの相手に対して協力することをPA(ペアノ算術)の中で証明することは不可能である。それを証明するには、その相手についての裏切りの証明が存在しないことを証明しなければならない。無矛盾性を仮定すると、PAは任意の言明について「その証明が存在しない」ことを証明できない。PAは自身の無矛盾性を証明できないからである。したがって DUPOC は CUPOD が協力するという証明を見つけられず、裏切る。対称的に、CUPOD は DUPOC に対して協力する。

ほかにも PrudentBot や CIMCIC (Cooperate If My Cooperation Implies Cooperation、自分の協力が相手の協力を含意するなら協力する) といったボットがあり、その挙動は定義の微妙な言い回しに左右される。詳細と未解決問題については Cooperative and uncooperative institution designs を参照。

1つの問題は、プログラムの停止が保証されないことである。証明の探索は永遠に終わらないかもしれないからだ。そこで、 $FairBot(k)$ のような有界版を考えることができる。これは、相手が協力することの長さ $k$ 以下の証明を見つけられる場合、かつその場合に限り協力する。「 $φ$ の長さ $k$ 以下の証明が存在する」ことを $□ k φ$ と書く。

定理 (パラメトリック有界レープの定理)。 $p(k)$ を自由変数を1つ持つ論理式とし、 $f(k)$ を、漸近的に少なくとも $log(k)$ 程度で増大する計算可能な増加関数とする。もし

⊢ ∀k > k₁ (□_f(k)p(k) → p(k)),

ならば、ある $k̂$ に対して、

⊢ ∀k > k̂, p(k).

この定理を使うと、十分大きな $k$ について、 $CUPOD(k)$ は自分自身に対して裏切り、 $DUPOC(k)$ は自分自身と協力することが証明できる。しかし、次の問題は未解決である (Critch et al., Open Problem 3 を参照)。

問題。 十分大きな $k$ に対して、 $DUPOC(k)$ 対 $CUPOD(k)$ の帰結はどうなるか? 同値な言い方をすれば、

outcome(DUPOC(k), CUPOD(k)) = (D,C)

は最終的に真となるか?

これが明らかでない理由は、この問題を展開すると $X \Leftrightarrow \neg□ k \neg□ k X$ のような形になるからである。何かの短い証明が存在しないことを求めているため、ゲーデルの第二不完全性定理を単純に適用することはできない。論文には、同じ趣旨の問いがさらにいくつか挙げられている。

さらに読むために

Robust Cooperation in the Prisoner’s Dilemma: Program Equilibrium via Provability Logic
搾取を避けながら頑健に協力する、証明ベースのエージェントを構成する。
Cooperative and Uncooperative Institution Designs
驚くべき例と具体的な未解決問題の集成を通じて、オープンソース・ゲーム理論を発展させる。
Parametric Bounded Löb’s Theorem and Robust Cooperation of Bounded Agents
レープ流の協力を、有限の証明探索リソースしか持たないエージェントに適応させる。
Characterising Simulation-Based Program Equilibria
相手についての言明を証明する代わりに、相手をシミュレートすることで構築されるプログラム均衡を研究する。
Prisoners’ Dilemma with Costs to Modeling
他のプログラムについて推論することにわずかなコストがかかるだけでも、協力の均衡がどう変わるかを検討する。