インタビューAIの顕著な欠点の一つは、「幻覚」を起こす性質、つまり現実世界のデータに基づかないもっともらしい答えを作り出す性質です。AWSは、Amazon Bedrock Automated Reasoningチェックを導入することで、この問題に対処しようとしています。
Amazon Bedrock は生成 AI アプリケーション向けのマネージドサービスであり、先月ラスベガスで開催された re:Invent カンファレンスで講演した AWS CEO の Matt Garman 氏によると、このチェック機能は「モデルの錯覚による事実上の誤りを防ぐ…Bedrock はモデルによる事実の記述が正確であることをチェックできる」とのことです。
これはすべて「健全な数学的検証」に基づいていると彼は述べた。
AWS CEO マット・ガーマンが Bedrock の自動推論について語る
これらは大胆な主張です。その背後には何が隠されているのでしょうか？AWS自動推論グループを率い、ユニバーシティ・カレッジ・ロンドンのコンピュータサイエンス教授も務めるバイロン・クック氏は、The Register紙にこう語っています。
多くの人は、プログラマーがメモリ安全性の証明をするように仕向けられていることに気づいていません。Rustの借用チェッカーは本質的に演繹的な定理証明器です。推論エンジンなのですが…
「私は形式推論と、そのためのツールの分野で働いてきました。約10年前からこの種の能力をAmazonに持ち込み、その後AIにも応用されてきました。今では、以前は非常に無名だった私の分野が、突然、無名ではなくなりました。」
AI 幻覚のリスクはどうすれば軽減できるのでしょうか、そしてその問題は解決できるのでしょうか?
「幻覚はある意味では良いことです。なぜなら、それは創造性だからです。しかし、言語モデルの生成においては、その結果の一部は不正確になるでしょう」と彼は言います。
しかし、誰の定義で間違っているのでしょうか？真実とは何かを定義するのは、驚くほど難しいことが分かります。誰もが同意するはずの分野であってもです。
「私は航空宇宙、鉄道のスイッチング、オペレーティングシステム、ハードウェア、生物学の分野で働いてきましたが、これらすべての分野において私が見てきたのは、こうしたツールを構築する際に費やされる時間の大部分は、コーナーケースに当たる具体的な例に基づいて、ドメインの専門家が正しい答えが何であるべきかを議論することに費やされているということです。」
クック氏はさらにこう付け加えた。「もう一つは、解決不可能な問題が存在するということです。これは例えばチューリングによって証明されています。限られた時間内で、常に、権威を持って、100%の正確さで質問に答えられるような手順は存在しません。」
あらゆる言明の領域を細分化しようとすると、比較的形式化しやすいものとそうでないものがあります。良い音楽とは何かを形式化するのは非常に難しく、人々はそれについて何らかの理論を持っているかもしれませんが、おそらく意見が一致していないでしょう。他の分野としては、生物学があります。生物学では、生物システムの仕組みに関するモデルは存在しますが、彼らが行っていることの一部は、それらのモデルを用いて実際のシステムを検証することです。彼らはモデルを改良しようとしているので、おそらくモデルは間違っているでしょう。こうした注意点を踏まえれば、できることはたくさんあります。
AWS自動推論グループを率いるバイロン・クック氏
Cook 氏は、個人の所得明細書に基づいて適切な税コードを決定するといった事例を挙げながら、自動推論ツールについて説明します。
しかし、人間も幻覚を見る…社会として、私たちは何が真実なのか、それをどう定義するのか、そして誰が真実を決めるのかを常に考え続けている。
このツールは、「自然言語の記述を論理に変換し、その領域における妥当性を証明または反証します。どうして間違いが起きるのでしょうか？自然言語から論理への変換には多少の誤りが生じる可能性があります。そして、税法を決定し、それを形式化する人々が間違える可能性もあります。したがって、誤った回答を得る可能性は依然としてありますが、私たちが正しく翻訳し、顧客が[ルール]を正式に定義するのを支援するという前提のもと、数理論理学において正しいことが証明された議論を構築し、顧客が得た回答が正しいと証明することができます。」と彼は言います。
クック氏は、幻覚は「私たちが今後長く付き合っていかなければならない問題です。しかし、人間も幻覚を見るのです。…社会として、私たちは常に何が真実なのか、それをどのように定義するのか、そして誰が真実を決めるのかを少しずつ探求し続けています」と語る。
クック氏に、AIによる幻覚のよく知られた事例についてコメントを求めました。ある弁護士は、Open AIのChat GPTによって考案された判例を引用しました。クック氏によると、それは自動推論ツールが解決できる種類の幻覚ではなかったとのことです。「既知の（訴訟）判例をすべてデータベース化し、形式化することは可能です」と彼は言います。「それが最適な応用方法かどうかはわかりません。」
AIが生成したアルゴリズムが正しいかどうかを知りたいソフトウェア開発者はどうでしょうか？「この製品はプログラマー向けに設計されたものではありません」とクック氏は言います。「しかし、私たちの関心を引いています。私たちが行ってきたのは、実際にはコードの推論です。…私は25年間、プログラムの正しさを証明してきました。これは非常に困難な作業であるため、非常に重要な資産を持つ大企業の領域です。しかし、生成AIは、その参入障壁を大幅に下げ、プログラムについて何を証明したいのかを形式化するのに役立つように思われます。これは非常にエキサイティングですが、それは（自動推論）製品とは別の話です。」
- AWSはAIがあらゆるものを破壊できると述べ、Windowsにもまさにそうなることを期待している。
- LLMパフォーマンスのためのチートコード：投機的デコード入門
- Googleがブラウザを制御できるAIエージェントを開発中との報道
- AIコードヘルパーはパッケージ名を発明するのをやめられない
クック氏のチームは、Amazonでアクセス制御ポリシーが期待通りに機能していることの証明など、他の課題にも取り組んできました。同様に、暗号化、ネットワーク、ストレージ、仮想化についても取り組んできました。コードが数学的に正しいことを証明できることには、有益な副次効果があり、その一つがコードの効率化だとクック氏は語っています。
自動推論ツールがあなたの宿題をチェックしてくれるので、最適化をより積極的に行うことができます。開発者がそのような能力を持たない場合、それは非常に保守的な、いわば防御的コーディングと言えるでしょう。これらのツールがあれば、開発者はそうでなければ非常に恐ろしい最適化を実行できます。私たちは彼らに多くの安全性を与えているのです。
彼は、Rustは証明可能プログラミングに自然に適合していると付け加える。「Rustでプログラミングするということは、実際には定理証明器を使っているということです。多くの人は、プログラマーにメモリ安全性の証明をさせているということを理解していません。Rustの借用チェッカーは、本質的には演繹的な定理証明器です。これは推論エンジンです。開発者はツールを操作しているのです…RustはC言語よりも高速です。その理由は、C言語では不可能だった、そしてJavaや他の言語では決して不可能な、メモリを使った巧妙な処理をRustが実行できるからです。なぜなら、プログラマーに証明をさせているからです。」
Rustは、自動推論技術、型システム、コンパイラを巧みに統合したツールです。さらに、非常に分かりやすいエラーメッセージも備えているため、非常に使いやすいツールとなっています。そのため、特定の種類のプログラムでは、Rustへの移行によって素晴らしい結果が得られています。®
