第3回のALIGNウェビナーでは、2023年に創設された非営利組織Atlas ComputingのCEO、Evan Miyazono博士をお招きしました。形式検証の手法に基づいた安全保証付きのAIの開発を目指すAtlas Computingを創設した狙いや、そしてMiyazono氏が長年取り組んできたメタサイエンス的視点から見たAI Safety分野の今後の発展の見通しについて伺いました（動画はこちら）。

日時：2024年5月24日（金）10:00 am-11:00 am （日本時間）
参加者：オンラインで20名ほど

以下は、Evanさんによるトークの翻訳です。

Evan Miyazono博士講演の翻訳（一部抜粋）

（※質疑・ディスカッションパートは省略）

皆さん、ご参加ありがとうございます。今日は「scoped safeguarded AI tools（特定分野にフォーカスした安全保証付きAIのためのツール）」についてお話します。

安全保証付きAIのためのツールとは

まず動機についてです。AIに関しては期待もあれば、心配すべきこともたくさんあります。しかし、過小評価されていると思うのは、今日のAIシステムは、まだ簡単な要求に対して簡単な答えを返してくれる段階にあるということです。この段階では、答えをレビューして、自分が求めているものかどうかを判断できます。しかし、これからのAIは、ますます複雑な要求に対し複雑な答えを出すようになるでしょう。そのとき、得られた回答が本当に望んでいるものかをレビューできるのでしょうか。私たちのレビュー能力が向上することはあまり期待できません。

しかも、これは私たちが「超知能」のリスクに直面するずっと前に起こる話です。ソフトウェアの生成、低分子合成経路の生成など、今日、商業的に大規模にAIが活用されている分野で、ごく短期間に起こり得る問題です。

安全性を示す一般的な方法は、制御された条件下でテストを行うことです。これは続けるべきだと思います。しかし私にはこのやりかたが「安全柵を押せるだけ押して壊れないかをテストする」ことに似ているようにも見えます。そう思うと、もっと良い方法はないものかと考えたくなるのは自然でしょう。

そこで私たちは、AIエージェントをある一つのブラックボックスとみなすのではなく、AIが人間によるレビューが可能な「中間出力」を生成すべきだと考えています。AIシステムが「非公式な仕様書」のようなものを生成し、ボタンを押すと解候補が出力されて人間がレビューするという従来の方式ではなく、仕様作成のアシスタントを用意するのです。この仕様アシスタント（specification assistant）は、「どうなったら失敗か」を表現する規準（criteria）の集合を言語で生成するのを助けてくれます。ソリューション生成システムは、この規準のいずれにも抵触しない解候補を、その証明（proof）とともに出力し、軽量なソリューションチェッカーが、解と証明の有効性と、解が実際に仕様を満たしていることを検証します。これが、私たちが解こうとしている問題の概要です。

私は何をしてきたか

簡単に、これまでやってきた他の仕事についてお話します。私の博士の研究は、光量子インターネットのためのスケーラブルな固体レーザー型光量子メモリの構築でした。その後、より短期的なインパクトを目指したいと思い、当時最も野心的なスタートアップであったProtocol Labsに入社しました。そこで私たちは型破りな資金調達に成功し、助成金プログラムを作ることになりました。

「最高の助成金プログラムとは何か？」という問いへの答えは、「より速く、より安く、より多くのよい科学を進めること」になります。速さと安さは簡単に定量化できる一方、「より多くのよい科学とは何か？」を定量化しようとなると、公共財の評価方法や価値について非常に興味深い疑問につながります。そこで、私たちが構築していたツールを一般化し、そこから得た概念を使って、全く新しい調整システム（coordination system）を構築したらどうかと考えました。

Network Goodsというベンチャースタジオをやっていた時のお気に入りスライドがこれです。ここでは、「人類は革命的な調整システムを発明してきた」という主張をしています。「文明は、考えなくても実行できる重要なオペレーションを増やすことで進歩する（A.N. ホワイトヘッド）」。私はこの考え方がとても好きです。

これらの発明のどれか一つについて、それが生まれる前の世界を想像できるでしょうか。また、それを思いつき、世に出すまでにどれほどの苦労があったでしょうか。これらの発明のされ方が、予期せぬ様々な影響や被害をもたらす可能性があることがわかるでしょう。私たちはこれらをインスピレーションとして、より意図的に、インパクトが予期できるような新しい革命的な調整システムを構築できないかと考えました。

そして、公共財やコモンズへの資金提供を改善する方法に関する、3つの非営利団体、2つの営利団体、そしてオープンソースコミュニティを立ち上げました。このベンチャー・スタジオから生まれたプロジェクトの一つが、An Open Agency Architectureです。

このDavid Dalrymple（通称davidad）氏の記事は、同氏のAI safety分野への最初の貢献として、読むに値するものです。このアイデアが、英国のARIA（高等研究発明局）のSafeGuarded AIプログラム（訳注：ALIGNによる解説記事）につながり、英国政府は5900万ポンドの資金を投入してこれを加速させています。これについては後ほどもう少しお話します。

Atlas Computingは何をしているのか？

Atlas Computingでは、上述したように、要求の複雑さとレビューの難しさが増していく状況を踏まえ、個別の特定領域で何ができるのかを検討しています。

実は私は普段、汎用知能の危険性についてはほとんど考えていません。限定された領域におけるAIのリスクへの対処が私の主眼なのです。ただし、後で、これらを繋ぎ合わせて一般知能のリスクをカバーするような安全ネットのようなものが作る話もできればと思います。

何かを作ることはレビューすることよりも簡単です。たとえばコード生成では、ソフトウェアの脆弱性を修正するよりも、ウイルスや悪用プログラムを作る方が簡単です。同じく、病気を根本的に治すよりも、新しい病原体を作る方がおそらく簡単でしょう。法律に関しても、少なくとも米国は訴訟社会なので、人々が抜け道を利用して法律を悪用する方が、AIを使って法的曖昧性を解消するよりも速いだろうと予想されます。社会でレビューが行われているあらゆる分野において、AIの能力が人間を抜き去ってしまう場面が見つかるはずです。私たちのレビューシステムは次第にパンクしていってしまうでしょう。

もう一つのポイントは、レビューを行う際に使われるスケーラブルな代理指標がうまくいかないということです。「どんな指標も、目標として使われるようになると、もはや良い指標ではなくなる」というグッドハートの法則が知られています。たとえば経済的利益を、エージェントの行動の良さの代理指標として使うことを想像すると、これは非常に恐ろしいものになります。ある種の資本主義の暴走に陥ってしまうでしょう。

したがって、私たちの方針は、Open Agency ArchitechtureやSafeGuarded AIと同様に、最適化の対象を完全にコード化せず、アライメントを目指すのではなく、よりシンプルな問題を解くことで「これらのことはするな、これが制約だ」と言えるようにしよう、というものです（”Don’t try to wholly encode optima – just enable specifying constraints”）。

AIの出力が守るべきルールを設定するツールを作ること。これは様々な分野で応用できます。我々はこれを、1）リスクへの注意喚起、2）仕様言語の生成、3）仕様言語を使って出力を検証するツールの作成という段階を踏むものと考えています。

まず初めにサイバーセキュリティとバイオセキュリティに取り組んでいるのは、これらのリスクと機会の領域が短期的に到来する可能性があると思われるからです。ソフトウェア生成と低分子設計という具体例で説明したいと思います。

ソフトウェア生成では、Coq、Dafny、Leanなどの既存の仕様言語を使用することを想定しています。例えば、ユーザーが FortranコードやCコードをアップグレードしたいとします。そのコードをAIベースの仕様生成器に送り込みます。

――なお、ここで言っておきますが、ここで1つの箱で書いているものは、それ自体がコンピュータサイエンスの一分野における壮大な目標（holy grail problem）です。しかし、かたやAGI（汎用人工知能）を構築しようとしている人たちがいることを考えれば、これは野心的な取り組みではあるとはいえ、まだ実現可能性が高いとも言えます。そのためには大規模な政府系の研究施設や、ヒトゲノム計画のように多くの人々が集まって行うプロジェクトが必要となる可能性があります。あるいは国際宇宙ステーションも、各国が協力して一国では作れなものを構築している好例でしょう。さらに、この挑戦は明らかに全員にとって利益のあるものです。共財へのファンディングやガバナンスメカニズムに興味を持ってきた私が、私がこの問題に取り組む理由がわかるかと思います。

話を戻します。Fortranコードの一部を仕様生成器に投入すると、その生成器はLeanを使ってそのコードが何をするものであるべきかを説明した仕様を生成します。この仕様を検証し、レビューを行い、その後ソリューション生成器に送ります。ソリューション生成器は、プログラムとともにそれが仕様を満たしていることの証明を生成します。そして、それをソリューションチェッカーが確認できます。

ここで、「仕様をレビューするのと同じように、コードをレビューすればいいのではないか」という疑問が生じるかもしれません。コードを生成したことがある人なら誰でもわかるように、「配列のインデックスがメモリ割り当ての境界を超えないようにする」とか、「これらの数値は決して0を超えないようにする」とか、「この合計は常に100でなければならない」といった項目は仕様書では一行で確認することができます。形式手法の数学的厳密さにより、これが真であることが証明できれば、その部分のレビューは解決されたことになります。これにはコード全体を理解する必要はありません。そして、このシステムの残りの部分は、ソフトウェアを検証する他のどの手法を用いた時よりも信頼できるものとなります。

生化学の例では、最初のステップは、AlphaFoldのような生成能力を競うコンペティションを開催することです。このコンペティションを通じて、既知のすべての代謝経路とすべての予測される相互作用のセットが得られます。そして、この情報から別のAIシステムが LD 50（半数致死量）などの毒性指標を生成し、この分子が体内に入ることをどれほど心配しなければならないかがわかります。

ここにはたくさんの科学的知見が必要でしょう。ただ、一度これを手に入れることができれば、非常に強力なツールになります。ユーザーが自然言語を使って「この経路を修飾する／代謝経路サイクルの一部を修飾する薬を設計してください、ただし有害な影響を避けてください」と要求したときに、修飾するとはどういう意味で、有害とはどういう意味かを客観的に定量化・形式化できるツールは非常に価値があります。これがあれば、それをin vitroあるいはin vivo、in silicoでテストし、実際に分子が望ましい特性を持っていることを検証できます。

「望まないものを仕様で制約する」という目標は、「最大化すべき値を符号化する」ことに比べて、ガバナンスプロセスと非常に適合性がある点で優れています。仕様（specification）をつくるという考え方は、国際条約や国や地方自治体の法制度、さらには個人的な目標を設定する方法などと合致しています。仮にこれを最適化問題にしようとすると、これらすべての仕様を組み合わせなければなりません。すると、計算が非常に難しくなったり、ある最適化関数が別の最適化関数の制約の効果を打ち消したりしてしまう可能性が出てきます。これは破局的リスク（catastrophic risks）に対する安全を考えるうえで望ましいことではありません。

長期的な目標としては、「検証可能なガバナンスが可能なAI」（verifiably governable AI）の国際標準化団体を設立し、さまざまな組織が協力してツールを構築することが考えられます。

なお、Atlas Computing が非営利団体であるのはなぜかと疑問に思うかもしれません。私たちは営利目的のスタートアップのように運営されている非営利団体ですが、非営利団体である理由は、このアーキテクチャがAIをガバナンスする最良の方法だと考えているからです。これは競争優位性ではなく、誰もがアクセスできるものでなければなりません。仮に、私たちが営利企業を設立するのであれば、私、または私の代わりを務める人物が、設立した翌日に競合他社をこのアーキテクチャに参入させるためのガバナンス要件を持たなければなりません。なぜなら、安全を達成するためには、誰もが最高の安全ツールを使用することが不可欠だと考えているからです。

Guaranteed-Safe AIというジャンル

これまで、私が取り組んでいることと、分野ごとにどのようにアプローチしているかをお話してきました。これらは実は「安全保証付きAI（Guaranteed-Safe AI）」と呼ばれる大きな枠組みの一つの試みであると言えます。

Guaranteed-Safe AIのアーキテクチャの概要は次のとおりです。AIシステムは、提案された行動の影響をシミュレーションするための世界モデル（world model）を持ち、そのモデルのなかで安全な状態を指定する仕様（specification）を作ることができ、さらに検証プログラム（verifier）によって出力が仕様通りであることを確かめることができます。もしこれが全く馴染みがないようでしたら、著名な著者たちによる重要な論文（Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems）を参照してください。

davidadのSafeGuarded AIプログラムも紹介しましょう。これもGuaranteed-Safe AIに含まれるアプローチです。私がかつて Protocol Labsでdavidadと一緒に働いていた頃、よくやっていたことの一つは、彼のアイデアを実装しやすく、ユーザーが理解しやすいように整理することでした。彼の論文は非常に素晴らしいのですが、このような複雑な図表が使われています。

私はこれをもっとシンプルに書き換えました。元の図と色分けを一致させながら、ボックスの数を大幅に減らしています。

私たちがつくっているものとdavidadのプログラムとの関係について触れておきます。両者は当面はリンクしないだろうと予想していますが、私の取り組みを「Safeguarded AIのUX開発と顧客獲得」と考えることもできます。ですので、やがて「ユーザー各位、これまで使っていただいたver 2.5を、Safeguarded AI のver 3.0に置き換え、既存のシステムと同じ機能に加え、さらに多くの機能を利用できます」と言う日が来ることも容易に想像できます。davidadの研究プログラムが終了したときに、我々の実装が完了していれば非常に有用であることがお分かりいただけると思います。システムのユーザー数は、研究とは独立して増加していくべきだと思います。

私の一つの主張は、こうした方法はアライメント問題を回避できる可能性があるというものです。このアーキテクチャを使えば、人間とアラインしていないAIも有用に利用できる可能性があります。すべての価値を信頼したり埋め込む必要がなく、民主的な方法で複数の人々の価値を引き出す必要もありません。

AI Safetyに対する「オープンワールド」のアプローチ

メタサイエンス的な観点から、2つ話したいことがあります。私は、科学の科学（science of science）について考えること、つまり科学をシステムとして科学的な視点で捉えることが好きだからです。未発達なアイデアですが、考えてみると面白いと思うかもしれないことを述べてみます。

1つ目は、「クローズドワールドの発想」と「オープンワールドの発想」の対比です。クローズドワールドの想定は、基本的に「述べられていなければ、偽である」というものです。知識グラフやリレーショナルデータベースを例に考えるとわかりやすいのですが、ある人のノードに対して「○○の子ども」というエッジがなかったり、「子どもの名前」という項目がないのであれば、その人は子供を持たないと考える。利点としてはデータがすっきりする反面、暗黙の仮定が多いという課題もあります。

オープンワールドはこれとは反対で、「述べられていないことは、真かもしれないし、偽かもしれない」と想定します。

例えば「すべてのAIコンテンツに電子透かし（watermark）を入れよう」というのは、クローズドワールドの想定です。電子透かしがないものは人間が生成したものだと考えるためです。一方で、オープンワールド側の例としては、Andrew Critch氏が提唱した「WordSig」があります。これは、QRコードと公開鍵基盤を使って動画がディープフェイクでないことを確認できるようにするものです。これは、電子透かしのアプローチを補完するものだと思います。クローズドワールドはリスクの出所を隔離するのに対し、オープンワールドはリスクとは何かを定義して直接対処する。前者はアライメント、後者はSafeGuarded AIとも少し重なるところがあります。

社会技術的問題としてのAI Safety

2つ目に関して、まずこのブログ記事：Shallow review of live agendas in alignment & safetyを紹介します。これはAI Safety分野を知るための出発点としては、素晴らしいものだと思います。（このブログ記事には分類体系が示されており、私たちのアプローチは「妄想的なエンドツーエンド（galaxy-brained end-to-end）理論的ソリューション」という区分に分類されており、やや困惑しつつも面白く思っていました。）

技術的な解決策だけでなく、さまざまなアプローチを比較することは非常に興味深いと思います。ほとんどの重要な問題は社会技術的（sociotechnical）な問題です。あるいは「Wicked problem（厄介な問題）」という用語があります。1970年代頃の論文で提起された、世の中には解決した状態がどうなのかを定義するのが不可能な問題があるという考え方です。AIのアライメントはこのカテゴリーに入ると思います。しかし、社会技術的な問題に対して、AI Safetyアプローチの多くは技術的な解決策、ガバナンスによるアプローチの多くは社会的な解決策になっていると思います。私が最も成功する可能性があると思うのは、社会技術的な問題に対する社会技術的な解決策、つまり社会的解決策が技術的な側面とうまく連携した場合（social solution that interfaces well the technical side）か、技術的な解決策が社会的側面とうまく連携した場合（technical solution that interfaces well with the social side）だと思います。

実世界の責任の仕組みは、示唆に富んでいます。たとえば、カリフォルニア州議会で可決されるかもしれない法案（SB1047）では、モデルのトレーニングを開始する前に、安全とセキュリティのプロトコルを実装しなければならないという文面になっています。このプロトコルは、悪影響が起こらないようにするための合理的な保証を提供するものです。これは、建築基準法や防火安全基準、電気製品の登録などと同じような仕組みです。つまり、監督機関がバッテリーが機器内で爆発しないことを保証し、爆発した場合にはリコールが行われるようにしています。このように、私たちはうまいシステムをもっています。しかし、従来のリスク評価や責任の検証方法は、まるで安全柵を押してその強度を確かめているように思えます。必要なのは、もしかしたらSafeGuarded AIではなく、あるいは形式検証や何らかの防御、リスク軽減策ですらない可能性はありますが、AIリスクに対する解決策やツール、システムとして採用されるものは、既存の社会構造に最も適合したものになるはずです。

（講演録ここまで）

【開催記録】ALIGN Webinar #3 Dr. Evan Miyazono (Atlas Computing)