1979年、マイケル・ラビンは、自分の暗号方式を逆に解いて暗号文を復号できるのは、攻撃者が n を素因数分解できる場合に限ることを証明した。十分に大きな n では、この素因数分解は計算上困難なので、ラビンの暗号方式は、十分に大きな n を使う限り「安全性が証明可能」だと言われた。
それ以来、この種の「証明可能安全性」を持つ暗号アルゴリズムを作ることは、暗号学の大きな目標となってきた。((ラビンの方式のように、セキュリティ要件が形式的に記述され、システムがそれらを満たすと証明されている場合、その暗号方式は安全性が証明可能だとされる。ウィキペディアを参照。))そして、この基準を満たす新しい暗号アルゴリズムは、ときに「安全性が証明可能」として売り込まれる。
残念ながら、「証明可能安全性」という言葉は、いくつかの理由で誤解を招きうる。((安全性の帰着は、それでも有用でありうる（Damgård 2007）。私が言いたいのは、この言葉が、とりわけ専門家でない人に誤解を与えうる、ということだけだ。))((詳細や、この用語に関するほかの問題は、コブリッツとメネゼスのAnother Lookというサイトと、そこからリンクされた論文、特にKoblitz & Menezes（2010）を参照。))
第一に、 ラビン流の安全性証明は、実際には安全性そのものを証明していない。証明しているのは、その暗号方式を破る効率のよいアルゴリズムがあれば、その基盤となる、計算上困難と仮定されている問題――たとえば整数の素因数分解――を解く効率のよいアルゴリズムも得られる、ということだ。そして、それらの基盤となる問題は、計算上困難だと 仮定 されてはいるが、実際に困難だと 証明 されているわけではない。したがって、「安全性証明」の「証明」は、数学で通常使われる「証明」とは意味が異なる。数学での証明は、証明された命題から、使っている数学体系の公理に至るまで、演繹的な道筋をたどれるものだからだ。
第二に、 システムの形式的なセキュリティ要件は、攻撃者がシステムを破るためにできることや、攻撃者が利用できる情報のすべてを、捉えきれていないかもしれない。たとえば、Rabin（1979）の発表からほどなくして、RSAのRに当たるロン・リベストは、攻撃者がラビンの暗号方式の利用者をだまし、攻撃者自身が選んだ暗号文を復号させられるなら、方式全体を破ることがはるかに容易になると指摘した。((Williams（1980）を参照。))別の例では、Bleichenbacher（1998）が、攻撃に失敗した後に返ってくるエラーメッセージを巧みに利用すると、初期のRSA暗号方式への攻撃を成功させられることを示した。
一般に、安全性証明は、暗号方式の物理的な実装から得られる情報を利用するサイドチャネル攻撃を考慮していないことが多い。たとえば、現実のコンピューターは、暗号処理を実行するとき、必ず電力を消費し、電磁波を放射する。場合によっては、その消費電力や電磁波を統計的に分析することで、暗号方式を破ることができる。
第三に、 安全性証明に限らず、数学的証明そのものが間違っていることがある。たとえば、Boldyrevaほか（2007）は、OMSと呼ばれる新種のデジタル署名を作り、同様の機能を持つほかの方式より効率がよく、より安全だと主張した。しかしその後、Hwangほか（2009）は、この「安全性が証明可能」なOMSプロトコルが、簡単に破れることを示した。実は、Boldyrevaらの定理5.1の4ページにわたる証明に、見逃されていた誤りがあったのだ。((Koblitz & Menezes（2010）を参照。数学的証明の誤りのほかの例については、Branwen（2012）、Kornai（2013）を参照。))
実のところ、最も強い意味で「安全性が証明可能」なシステムは、一つもありえない。（1）形式的なセキュリティ要件が適切に定められていると100%確信することも、（2）安全性証明そのものに誤りがないと100%確信することも、できないからだ。
同様に、コンピューターシステムには「安全性が証明可能」という説明が付くことがある。これは通常、形式的に定められた安全性の基準に照らして、ソフトウェアの全部または一部が形式検証されているためだ。((「安全性が決定的に重要なシステムにおける透明性」も参照。))しかし、ここでも忘れてはいけない。（1）安全性の形式仕様が、私たちの大切にしていることをすべて捉えていると100%確信することは決してできないし、（2）複雑な数学的証明、つまり形式検証に誤りがないと100%確信することも決してできない。
同じ理屈は、AGIの「友好性」にも当てはまる。友好的AI研究で知られている未解決問題について、解決策らしきものが見つかったとしても、最も強い意味で「友好性が証明可能」なAGIを作れるということにはならない。（1）「友好性」の形式仕様が、私たちの大切にしていることをすべて捉えていると100%確信することも、（2）形式的な推論に誤りがないと100%確信することも、決してできないからだ。実際、「友好性の仕様を定める」問題は、「セキュリティの仕様」や「安全性の仕様」の問題より、はるかに難しそうだ。友好性を適切に定めるには、哲学が大きく関わり、人間は哲学が苦手なことで知られているからである。
したがって、「証明可能なセキュリティ」「証明可能な安全性」「証明可能な友好性」と呼ばれることのあるアプローチが、セキュリティ、安全性、友好性を100%保証するのだと誤解してはいけない。((この誤解があまりに多いため、MIRIのスタッフは「友好性が証明可能」といった表現を避けるようにしている。MIRI研究員のエリエゼル・ユドコウスキーは、「友好性が証明可能」なAGIを提唱しているとよく批判される。だが、彼自身がその表現を使った例を、私は見つけられなかった。過去に使ったことが ある とすれば、物理世界での振る舞いについての証明ではなく、AGIの内部構造についての何らかの証明を持つこと――それがない場合より、友好性への確信を強められるようにすること――を指していた可能性が高そうだ。
2014年10月16日追記： ある読者が、この混乱の一因になったかもしれないユドコウスキーの文章を、いくつか教えてくれた。2008年10月の記事では、「正しさが証明可能な友好的AI」という表現を使っていたが、その意味は説明していなかった。同じく2008年10月のブログのコメントでは、「正しく自己改良することが証明可能な友好的AI」という表現も使っていた。2008年12月の記事では、こう書いている。「知性への深い洞察を持つプログラマーが、効率的で計画された経路に沿って、決定論的な精密さで自らを改変できる知性を直接作る。つまり、正しいと証明可能な、あるいは破局的でないと証明可能な自己改変だ。友好的AIを作れるほど狙いを絞り込む方法として、私に見えるのはこれだけだ」。そして最後に、2005年9月のメーリングリストのコメントで、友好的AIについて「証明可能」という言葉を使うとき、通常何を意味しているのかを、より明確に説明している。
既知のどのアルゴリズムも、単独では、宇宙の年齢に相当する時間をかけてもCPU設計の正しさを証明できない。しかし、人間が選んだ*補題*があれば、機械によって*検証された*正しさの証明を得ることができる。公理系における証明の重要な性質は、確実であることではない。私たちが知っている限りでも、形式的に証明できる範囲でも、その体系が無矛盾でない可能性は残るからだ。重要なのは、その体系が無矛盾*ならば*、1万ステップの証明も10ステップの証明と同じだけ信頼できる、という性質だ。独立した失敗の原因はない。AIが少なくとも人間の数学者に匹敵する効率、計算上の扱いやすさ、規模への対応力で演繹的推論を行えるなら、正しさが証明可能なCPUと同様、正しさが証明可能な書き換えも扱えるようになると期待している。AI完全な問題かって？ もちろんだ。でも忘れないでほしい。私たちはAIを設計しようと*している*のだ。
))むしろ、 これらのアプローチが目指すのは、ほかの条件が同じなら、あるシステムのセキュリティ、安全性、「友好性」について、それがない場合よりも強い確信 を得ることだ。
特に、友好的AIほど複雑なものについての私たちのメッセージは、こうだ。「正しいと証明すれば、うまくいくかもしれない。正しいと証明しなければ、確実にうまくいかない」。((これは、AGIシステムの 全体 を形式検証できるはずだ、あるいは、その必要がある、と言っているわけではない。一つの可能性は、初期のAGIが、Fisherほか（2013） のような 階層型の自律エージェントになり、その「最上位」の制御層だけが、何らかの形式的な正しさの証明に適した形で作られる、というものだ。))
人間はしばしばリスクゼロの解決策を求める。しかし、コンピューターのセキュリティ、安全性、友好性には、リスクゼロの解決策は存在しない。一方で、形式的証明の価値を無視すべきでもない。それは、利用できるほかのどの方法よりも精密で、たとえばテストを補うものとして有用だ。((Kornai（2012）、Muehlhauser（2013）、Damgård（2007）も参照。))
そして、自己改良するAGIを作るとなれば、その友好性について、できるだけ強い確信を持ちたい。自己改良するAGIは、単に「安全性が決定的に重要なシステム」なのではなく、世界の存亡に関わるシステムだ。友好性の研究は難しい。しかし、何が懸かっているかを考えれば、その価値はある。((この記事への意見を寄せてくれたルーイ・ヘルムとエリエゼル・ユドコウスキーに感謝する。))