本ブログは 2026 年 8 月 11 日に公開された Amazon Science Blog “ A decade of mathematical certainty: Reflections on the Automated Reasoning Group ” を翻訳したものです。 Automated Reasoning Group の設立から 10 年。数学的論理は学術研究の領域を越え、お客様の数百万のワークロードを守る本番サービスにまで広がりました。これは、システムが単に「おそらく正しい」だけでなく、「正しいと証明できる」ものになり得ることを示しています。 2016 年、Amazon の小さな研究チームが Automated Reasoning Group (ARG) の発足とともに、その存在を世界に向けて発信しました。掲げたビジョンは大胆なものでした。数学的論理を用いて AWS のシステムをテストするだけでなく、正しく動作することを数学的な確実性をもって証明する、というものです。 それから 10 年。ARG は、形式的検証の進歩によってこれまで解決困難だった問題を AWS の規模で緩和できるのかを模索する段階から、AWS のセキュリティと信頼性への取り組みの根幹を成すシステムを構築する段階へと進みました。ARG の本番サービスは、1 日あたり数十億件のクエリを処理しています。 本記事では、最先端の形式的検証とプログラム解析の技術を Amazon 特有の課題にどう適用してきたかを振り返ります。この取り組みの原動力となったのは、現実世界のセキュリティとインフラストラクチャの問題を、AWS の規模で数学的な厳密さをもって解決できるという確信でした。実際、当時研究していたようなツールは、Intel や NASA では既に成果を上げていました。ただ、これらの技術がここまで広範に適用できるようになるとは、十分に予測できていませんでした。 デモから大規模な本番環境へ 2016 年に第 1 回 ARG Demo Day を開催したとき、AWS Security に向けていくつもの野心的なプロジェクトを紹介しました。それぞれが、同じ根本的な問い、すなわち「自分たちのシステムが安全かつ正しいことを数学によってどう証明できるのか」に対する異なるアプローチでした。その日に示された答えは、2026 年の今も AWS とお客様にとって重要な役割を果たし続けるシステムの土台となっています。 Sean McLaughlin は「Automatic tools for reasoning about virtual private clouds (VPC)」と題したプレゼンテーションを行いました。VPC ネットワークの拡大に伴い、設定ミスやセキュリティ脆弱性を特定できる自動推論ソリューションへの需要が高まっていると指摘したうえで、その答えとして示したのが「 Tiros というツール で、簡単に言えば、ネットワークに関する質問に答えてくれるもの」でした。 Tiros は、 Amazon Inspector のネットワークセキュリティ分析機能の基盤となりました。Amazon Inspector は、クラウドでアプリケーションを構築する数百万のお客様にご利用いただいています。Tiros は AWS 内部でも、多くの AWS サービスにおけるコンプライアンス認証の確認やセキュリティ不変条件の遵守チェックを自動化する用途で使われています。現在では、Amazon Inspector と Reachability Analyzer の両方を支えています。この取り組みからは Zelkova も派生しました。Zelkova は 自動推論 を用いて、ポリシーとそれが将来もたらす結果を分析します。 S3 Block Public Access や IAM Access Analyzer をはじめ、数多くのツールが Zelkova を基盤としています。 同様に、その日には、重要なインフラストラクチャを対象とする詳細な自動解析の活用をテーマにしたプレゼンテーションも行われました。これが、TLS ハンドシェイクの正しさや、暗号、ストレージ、仮想化のコードが備えるその他の性質を証明する取り組みへとつながりました。 紹介した小規模なプロジェクトの中にも、その規模をはるかに超える影響をもたらしたものがあります。価値の高いインフラストラクチャに対する演繹的検証の取り組みを発表した当時、その適用範囲は主に暗号プロトコルの最も深い部分に限られていました。しかし今日、その重要性は飛躍的に高まっています。これを後押ししたのが、証明支援システム (proof assistant) の台頭です。証明支援システムとは、ユーザーが形式的な証明を作成するのを助ける自動化ツールで、自動推論 (AR) チームの senior principal scientist である Leo de Moura が作成した Lean などがあります。AWS は現在、こうしたツールを言語モデルと組み合わせることで、より多くの、そしてはるかに大規模なシステムの証明を見つけられるようになりました。実際、 Nitro Isolation Engine について発表した証明 は、まさにそれを裏付けるものです。これは、AWS のポリシーインタープリターの証明や、暗号基盤の正しさを証明する近年の取り組みの基礎にもなっています。 お客様が信頼を寄せる数学的保証 この 10 年間で、ARG の研究プロトタイプは、数百万の AWS のお客様が毎日利用するサービスへと発展しました。 IAM Access Analyzer は Zelkova を利用して、USAA や GoTo といったお客様がリソースへの意図しないアクセスを特定できるよう支援します。セキュリティポリシーが正しく設定されていることをただ期待するのではなく、お客様はポリシーが実際に何を許可しているのかを、数学的な証明という形で確認できます。 2016 年にデモを行った Tiros をベースに構築された Reachability Analyzer は、パケットを 1 つも送信することなく、ネットワークの接続性を把握できるよう支援します。設定をテストするのではなく、考えられるすべてのネットワーク経路を数学的に分析し、宛先に到達できるかどうか、到達できない場合はどのコンポーネントが妨げているのかを示します。 Amazon Bedrock Guardrails の 自動推論チェック は、生成 AI に数学的な検証をもたらします。この機能は、モデルの応答が定義されたポリシーに準拠していることを形式論理で検証し、AI のハルシネーションの防止に役立ちます。検証精度は最大 99% に達します。 これらのお客様向けサービスには共通の基盤があります。いずれも 充足可能性モジュロ理論 (satisfiability modulo theories、SMT) ソルバーなどの自動推論技術を用いてシステムの動作に関する数学的保証を提供し、従来のテストで到達できる範囲をはるかに超えています。 クラウドを支えるインフラストラクチャの正しさの証明 お客様向けのツールは自動推論の実用的な価値を示すものですが、最も困難な取り組みの一部は AWS 内部のインフラストラクチャに向けられてきました。数百万のワークロードが依存しているため、正しさが不可欠なシステムです。 AWS は自動推論を用いて、次に挙げるものをはじめ、インフラストラクチャの多くの部分について正しさを証明してきました。 AWS Nitro Isolation Engine s2n-bignum などの暗号実装 AWS データセンターで動作するブートコード S3 などのストレージシステム とりわけ野心的だったプロジェクトでは、1 秒あたり 10 億回の API コールを処理する認可エンジン全体の正しさを証明し、シームレスに置き換えました。仕様と証明を用い、新しいエンジンを数千兆件に及ぶ本番環境の認可判定に対して検証したのです。 こうした内部検証の取り組みは、クラウドインフラストラクチャの最も基礎的な層に対しても、自動推論が数学的確実性をもたらせることを示しています。 予想外の発見 この 10 年の取り組みでおそらく最も意外だったのは、自動推論はシステムをより安全にするだけでなく、多くの場合、より効率的で保守しやすいものにするという発見です。検証のために厳密な仕様を書く必要が生じると、チームはより単純で洗練された解決策に気付くことがよくあります。 その理由の一つは、自動推論によって可能になる、システム全体を対象としたアプローチにあります。自動推論は、特定のシナリオにおけるシステムの動作を検証することに主眼を置くのではなく、論理を用いて 起こり得るあらゆる シナリオでの動作を検証します。考えられるすべての入力シナリオとその失敗のしかたを洗い出すのではなく、システムがどのように動作すべきかを定義し、その動作に必要な条件を特定します。そして、それらの条件が真であることを数学的証明によって検証します。つまり、システムそれ自体が正しいことを検証できるのです。 この発見は、数学的な厳密さと実践的なエンジニアリングは対立するものではなく、互いに補い合うものだという確信を裏付けました。形式的検証に求められる規律は、そうでなければ見えないままだった単純化の機会をしばしば浮かび上がらせます。 エージェンティック AI を支える基盤の構築 10 年前に始めた研究によって、AWS は AI 開発の次の時代に向けた独自の強みを備えることになりました。分散システムや重要なコードの検証で培った成果は、いまや AI が生成したコードの検証に直接活かせる土台となっています。一方、AWS ポリシーや VPC ネットワークの設定ミスに関する研究は、AI が生成したコンテンツの正しさを検証するのに役立っています。 この進化は、近年のいくつかのローンチに表れています。 Amazon Bedrock Guardrails の自動推論チェック は、深い専門知識を必要とするツールから、ビルダーが毎日使うサービスに直接組み込まれた機能へと歩を進めた、重要な節目です。 Amazon Bedrock AgentCore の Policy は、自動推論を用いてエージェントのアクションに明確な境界を設定し、エージェントが自律的に動作しながらも定められたコンプライアンスの境界内にとどまるようにします。チームは自然言語で、エージェントがアクセスできるツールとデータを指定できます。 AgentCore Gateway と統合すれば、システムはミリ秒単位でポリシーをチェックします。 エージェンティックな開発環境である Kiro では、 要件分析機能 をリリースしました。この機能は自動推論を用いて、コードを書く前にソフトウェア要件に矛盾、あいまいさ、抜け漏れがないことを証明し、コードの正確性を高め、後々のデバッグの繰り返しを防ぎます。Kiro を開発しているチーム自身も、機能を公開する前に、その機能を実装する AI 生成コードが正しく動作するかを自動推論で確認しています。 AI エージェントがより自律的になり、より複雑なタスクを担うようになるほど、その動作に関する数学的保証は決定的に重要になります。AI エージェントが形式仕様を備えたシステムへのコード変更を提案すれば、そのシステムは数学的証明に照らして変更を自動的に検証できます。自動推論は、強力であるだけでなく、安全性と信頼性を証明できる AI システムを構築する道筋をもたらします。 10 年にわたるコラボレーション この取り組みは、築き上げてきた優秀なチームと、重要なインフラストラクチャの保護を AWS に託してくださったお客様なしには実現できませんでした。AWS 全体で、各チームが自動推論の能力を拡大し続けています。 Senior principal scientist の Daniel Kroening が率いる Annapurna のチームは、ハードウェア検証を前進させています。Senior applied scientist の Nadia Labai は、自然言語を形式的な数学的証明へ変換することを AI システムに学習させる自動形式化 (auto-formalization) の研究を切り開いています。Principal applied scientist の Tristan Ravitch が率いる AWS Security のチームは、AWS と Amazon の全アカウントにわたるデータフローを自動的に追跡する Peri をローンチしました。サービスチーム側でのオンボーディングは一切不要です。 これらの取り組みによって、AWS は自動推論の次の 10 年を、最初の 10 年と同じくらい、あるいはそれ以上に変革的なものにする態勢を整えています。 証明してきたこと 10 年を経て、これまで達成してきたことに大きな喜びを感じています。設定エラーの防止から AI システムの動作に関する数学的保証の提供まで、自動推論はあらゆる層で測定可能な価値をもたらすことを証明してきました。そして、数学的な厳密さと実践的なエンジニアリングが手を携えて、お客様が実際に抱える課題を大規模に解決できることを示してきました。 2016 年の最初の Demo Day から今日に至るまでの道のりは、学術的な進歩をお客様が日々頼りにするサービスへと変えていくという AWS の姿勢を体現しています。数学的確実性を通じて信頼の基盤を築いてきました。その基盤は、AI イノベーションの次の 10 年を進むうえで欠かせないものとなるでしょう。 次の 10 年に向けて。 著者について Byron Cook Amazon の vice president 兼 distinguished scientist である Byron Cook は、形式的検証分野のリーダーです。SAT、SMT、記号モデル検査への貢献と、それらを生物システム、コンピュータオペレーティングシステム、プログラミング言語、セキュリティへ応用したことで知られています。Amazon での Byron の自動推論の取り組みは、クラウドにおけるより高い水準の保証と、新しいお客様向け機能をもたらしました。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

本ブログは 2021 年 12 月 1 日に公開された Amazon Science Blog “ A gentle introduction to automated reasoning ” を翻訳したものです。 2021 年、Amazon Science は研究領域のリストに 自動推論 を追加しました。この変更を行ったのは、自動推論が Amazon にもたらしている影響が大きいからです。例えば、Amazon Web Services のお客様は現在、 IAM Access Analyzer 、 S3 Block Public Access 、 VPC Reachability Analyzer といった自動推論ベースの機能を直接利用できます。また、Amazon の開発チームが 自動推論ツールを開発プロセスに統合 し、製品の セキュリティ 、 耐久性 、可用性、品質の水準を高めている例も見られます。 この記事の目的は、自動推論についてまったく知識はないものの詳しく学んでみたいと考えている業界の実務者に向けて、自動推論をわかりやすく紹介することです。この記事を理解するために必要な前提知識は、短い C と Python のコード断片を読めることだけです。途中でいくつかの専門的な概念に触れますが、あくまで堅苦しくない形で紹介するにとどめます。最後に、さらに深く学びたい方のために、一般に公開されているおすすめのツール、動画、書籍、記事へのリンクを紹介します。 まずは簡単な例から始めましょう。次の C 関数を考えてみてください。 bool f(unsigned int x, unsigned int y) { return (x+y == y+x); } 少し時間を取って、次の質問に答えてみてください。 「 f が false を返すことはあり得るか?」 これはひっかけ問題ではありません。論点を明確にするため、意図的に簡単な例を使っています。 網羅的テストで答えを確認するなら、次の二重にネストしたテストループを実行するという方法が考えられます。このループは、unsigned int 型のあらゆる値の組み合わせに対して f を呼び出します。 #include<stdio.h> #include<stdbool.h> #include<limits.h> bool f(unsigned int x, unsigned int y) { return (x+y == y+x); } void main() { for (unsigned int x=0;1;x++) { for (unsigned int y=0;1;y++) { if (!f(x,y)) printf("Error!\n"); if (y==UINT_MAX) break; } if (x==UINT_MAX) break; } } 残念ながら、最新のハードウェアであっても、この二重ループは 非常に長い 時間動き続けます。私はこれをコンパイルして 2.6 GHz の Intel プロセッサ上で 48 時間以上実行したところであきらめました。 なぜテストにこれほど時間がかかるのでしょうか。UINT_MAX は通常 4,294,967,295 なので、検討すべき f の呼び出しは 18,446,744,065,119,617,025 通りあります。私の 2.6 GHz のマシンでは、コンパイルされたテストループは f を 1 秒あたり約 4 億 3,000 万回呼び出しました。それでも、この性能で約 1,844 京通りのすべてのケースをテストするには 1,360 年以上かかります。 上記のコードを業界の実務者に見せると、ほぼ即座に、基盤となるコンパイラ/インタープリタとハードウェアが正しく動作する限り f が false を返すことはないという結論に達します。どのようにしてわかるのでしょうか。コードについて 推論 しているのです。学校で学んだ知識から x + y は y + x と書き換えられることを思い出し、 f は常に true を返すと結論づけます。 Amazon Web Services のユーティリティコンピューティング担当 senior vice president、Peter DeSantis による AWS re:Invent 2021 基調講演。Amazon Web Services の自動推論への取り組みについては 15:49 からご覧ください。 自動 推論ツールは、この作業を私たちの代わりに行います。数学における既知の技法を使って、プログラム (または論理式) に関する問いに答えようと試みるのです。この例であれば、ツールは代数を使って x + y == y + x が単純な式 true に置き換えられることを導出します。 自動推論ツールは、対象領域が無限である場合 (例えば、有限の C の int ではなく非有界の数学的整数の場合) でも、非常に高速に動作することがあります。残念ながら、場合によってはツールが 「Don’t know」 (わからない) と答えることもあります。その有名な例は後ほど見ていきます。 自動推論の 科学 は、本質的にこうした 「Don’t know」 という回答の頻度を可能な限り下げることに焦点を置いています。ツールが 「Don’t know」 と報告する (あるいは試行中にタイムアウトする) 頻度が低いほど、そのツールは有用になるのです。 今日のツールは、かつてのツールでは答えられなかったプログラムやクエリに対しても答えを出せるようになっています。明日のツールはさらに強力になるでしょう。この分野では急速な進歩が続いており、だからこそ Amazon ではそこから得られる価値がますます大きくなっています。実際、自動推論の分野でも、Amazon 流の好循環が独自に形成されつつあると考えています。より多くの入力問題がツールに与えられることでツールが改善され、それがツールのさらなる活用を促すのです。 次に、少し複雑な例です。自動推論とは何かの大まかな輪郭がつかめたところで、次の小さな例では、ツールが私たちの代わりにどのような複雑な問題を扱っているのかを、もう少し現実に近い形で見ていきます。 void g(int x, int y) { if (y > 0) while (x > y) x = x - y; } あるいは、非有界整数を扱う同様の Python プログラムを考えてみましょう。 def g(x, y): assert isinstance(x, int) and isinstance(y, int) if y > 0: while x > y: x = x - y 次の質問に答えてみてください。 「 g は必ず最終的に呼び出し元へ制御を返すか?」 このプログラムを業界の実務者に見せると、たいていはすぐに正しい答えを導き出します。ただし一部の人、特に理論計算機科学の成果を知っている人は、 「これは 停止性問題 の例であり、解けないことが証明されている」 という理由で、この質問には答えられないと誤解することがあります。実際には、 このプログラムを含む 特定のプログラム について、停止するかどうかを推論することは可能です。この点については後で詳しく説明します。 この問題を見たとき、ほとんどの業界の実務者が用いる推論は次のとおりです。 y が正でない場合、実行は関数 g の末尾へ飛びます。これは簡単なケースです。 ループのすべての反復で変数 x の値が減少するのであれば、最終的にループ条件 x > y が成立しなくなり、 g の末尾に到達します。 x の値が常に減少するのは、 y が常に正である場合だけです。そのときにのみ x の更新 (すなわち x = x - y ) が x を減少させるからです。そして y が正であることは条件式によって保証されているため、 x は常に減少します。 経験豊富なプログラマーであれば、通常はこの C プログラムの x = x - y という命令でのアンダーフローを心配するでしょう。しかし、 x の更新前に x > y が成り立っているため、アンダーフローは起こり得ないことに気づきます。 ここまでの 3 つのステップを自分で追ってみたなら、コンピュータプログラムについて推論する際に自動推論ツールが私たちの代わりにどのような思考を行っているかを、とても直感的に理解できたはずです。実際には、ツールが向き合わなければならない厄介な細部が数多くあります (例えば、ヒープ、スタック、文字列、ポインタ演算、再帰、並行性、コールバックなど)。しかし、これらやその他のトピックを扱う技法については数十年分の研究論文があり、そのアイデアを実際に活用するさまざまな実用的ツールも存在します。 自動推論はポリシー (上) とコード (下) の両方に適用できます。いずれの場合も、常に真であることについて推論するのが不可欠なステップです。 重要なポイントは、自動推論ツールは通常、上記の 3 つのステップを私たちの代わりに実行しているということです。ステップ 1 はプログラムの 制御構造 についての推論です。ステップ 2 はプログラム内で 最終的に 真になることについての推論です。ステップ 3 はプログラム内で 常に 真であることについての推論です。 なお、AWS のリソースポリシー、VPC のネットワーク記述、さらには makefile のような設定アーティファクトも、コードとみなすことができます。この視点に立てば、C や Python のコードについて推論するのと同じ技法を用いて、設定の 解釈 に関する問いに答えられます。この着想があるからこそ、IAM Access Analyzer や VPC Reachability Analyzer のようなツールが生まれるのです。 テストは不要になるのか? f と g の例で見たように、自動推論は網羅的テストよりも大幅に高速になる場合があります。今日利用できるツールを使えば、網羅的テストで何世代分もの時間を待つのではなく、 f や g の性質をミリ秒単位で示せます。 では、テストツールを捨てて自動推論に移行してよいのでしょうか。そうとは言えません。テストへの依存を大幅に減らすことはできますが、テストを完全になくせる日は、近いうちには来ないでしょうし、そもそも来ないかもしれません。最初の例をもう一度考えてみてください。 bool f(unsigned int x, unsigned int y) { return (x + y == y + x); } バグのあるコンパイラやマイクロプロセッサが原因で、このソースコードから作られた実行可能プログラムが実際には false を返してしまうかもしれないという懸念を思い出してください。言語のランタイムについても心配する必要があるかもしれません。例えば、C の数学ライブラリや Python のガベージコレクターにバグがあり、プログラムが正しく動作しなくなる可能性もあります。 テストに関して興味深く、しかもしばしば見落とされがちなのは、テストが C や Python のソースコードについて教えてくれるだけではないということです。テストはコンパイラ、ランタイム、インタープリタ、マイクロプロセッサなども同時に検証しています。テストの失敗は、スタック内のいずれのツールに起因していてもおかしくありません。 一方、自動推論は通常、そのスタックのうち 1 つの層 – ソースコードそのもの、あるいは場合によってはコンパイラやマイクロプロセッサ – にのみ適用されます。推論が非常に価値あるものだと感じるのは、検査対象の層について、私たちが 知っている ことと 知らない ことの両方を明確に定義できるからです。 さらに、自動推論ツールが用いる周辺環境のモデル (例えばコンパイラや、対象手続きを呼び出す手続き) によって、私たちの前提が きわめて 厳密なものになります。計算スタックの層を分離することで、時間、労力、費用と、今日および将来のツールの能力をより有効に活用できます。 残念ながら、自動推論を使う際には、ほとんどの場合、 何らかのこと について前提を置く必要があります 。例えば、シリコンチップを支配する物理の原理などです。したがって、テストが完全に置き換えられることはありません。前提をできる限り検証するために、エンドツーエンドテストは今後も行うことになるでしょう。 不可能なプログラム 先に、自動推論ツールが 「yes」 や 「no」 ではなく 「Don’t know」 を返すことがあると述べました。また、永遠に実行を続ける (あるいはタイムアウトする) ために、まったく答えを返さないこともあります。ここでは、ツールが 「yes」 や 「no」 を返すことが できない とわかっている、有名な「停止性問題」のプログラムを見てみましょう。 terminates という名前の自動推論 API があると想像してください。この API は、C 関数が常に停止する場合は 「yes」 を返し、関数が永遠に実行され得る場合は 「no」 を返します。一例として、 こちら で説明されているツールを使えば、このような API を構築できます (著者自身の過去の研究成果です)。停止性判定ツールが何をしてくれるかを理解するために、2 つの基本的な C 関数を考えてみましょう。1 つは (前述の) g です。 void g(int x, int y) { if (y > 0) while (x > y) x = x - y; } もう 1 つは g2 です。 void g2(int x, int y) { while (x > y) x = x - y; } 既に述べた理由により、関数 g は常に呼び出し元へ制御を返すため、 terminates(g) は true を返すはずです。一方、 terminates(g2) は false を返すはずです。例えば g2(5, 0) は決して停止しないからです。 ここで難しい関数が登場します。 h を考えてみましょう。 void h() { if terminates(h) while(1){} } これが再帰的であることに注目してください。 terminates(h) の正しい答えは何でしょうか。答えは「yes」ではあり得ません。「no」でもあり得ません。なぜでしょうか。 terminates(h) が「yes」を返すとしましょう。 h のコードを読めばわかるように、この場合は h のコード内の条件文が無限ループ while(1){} を実行するため、関数は停止しません。したがってこの場合、 terminates(h) の答えは誤りとなります。 h は自分自身に対して terminates を呼び出す形で再帰的に定義されているからです。 同様に、 terminates(h) が「no」を返すとすれば、 h は実際には停止して呼び出し元へ制御を返します。条件文の if の条件が満たされず、else 分岐も存在しないからです。この場合もやはり答えは誤りとなります。だからこそ、このケースでは 「Don’t know」 という答えが避けられないのです。 プログラム h は、決定可能性に関する Turing の 1936 年の有名な論文 や、1931 年の ゲーデルの不完全性定理 で示された例の変種です。これらの論文が教えているのは、停止性問題のような問題は「解けない」ということです。ただしここで 「 解ける 」 とは、解法手続き自体が常に停止し、 「yes」 か 「no」 のいずれかを答え、決して 「Don’t know」 とは答えないことを意味します。しかし、それは私たちの多くが念頭に置いている「解ける」の定義ではありません。多くの人にとっては、ときにタイムアウトしたり、ときおり 「Don’t know」 と返すことはあっても、答えを返すときには必ず正しい答えを返すツールであれば十分なのです。 この問題は飛行機での移動に似ています。過去に墜落事故が起きており、将来も起きるであろうことは確実なので、100% 安全ではないとわかっています。しかし、無事に着陸したなら、そのときはうまくいったと わかる のです。航空業界の目標は、原理的には避けられないとしても、失敗を可能な限り減らすことです。 これを自動推論の文脈に置き換えると、 h のような一部のプログラムについては、 「Don’t know」 という答えをなくせるほどツールを改善することは決してできません。しかし、今日のツールが 「Don’t know」 と答えるものの、将来のツールなら 「yes」 や 「no」 と答えられるようになるケースは他に数多くあります。自動推論の専門家にとっての現代の科学的な課題は、実用的なツールが 「yes」 か 「no」 を返す頻度を可能な限り高めることです。現在進行中の取り組みの一例として、CMU 教授であり Amazon Scholar でもある Marijn Heule 氏による コラッツの停止性問題を解く挑戦 をご覧ください。 もう 1 つ覚えておきたいのは、自動推論ツールが日常的に「計算困難な」問題、例えば 複雑性クラス NP に属する問題を解こうとしているという点です。ここでも、停止性問題で見たのと同じ考え方が当てはまります。自動推論ツールは強力なヒューリスティックを備えており、特定のケースでは計算困難性の問題を回避できることがよくあります。しかし、そうしたヒューリスティックは失敗し得ますし (実際に失敗することもあり)、その結果として 「Don’t know」 という答えや、実用に耐えない長い実行時間が生じます。ヒューリスティックを改善してその問題を最小化することが、この科学の役割です。 用語について 科学文献では、相互に関連するトピックを表すために多くの名称が使われており、自動推論はその 1 つにすぎません。簡単な用語集を示します。 論理 とは、何が真であり何が真でないかを定義するための形式的かつ機械的な体系です。例: 命題論理 や 一階述語論理 。 定理 とは、論理において真である命題です。例: 四色定理 。 証明 とは、定理に対する論理上の妥当な論証です。例: Gonthier 氏による 四色定理の証明 。 機械的定理証明器 とは、多くの場合人間が書き下した証明を機械可読な形で表現したものを検査する半自動推論ツールです。これらのツールはしばしば人間の手助けを必要とします。例: HOL-light 。開発者は Amazon の研究者 John Harrison です。 形式的検証 とは、コンピュータシステムのモデルに定理証明を適用して、システムの望ましい性質を証明することです。例: 検証済み C コンパイラ CompCert 。 形式手法 とは最も広い意味の用語で、単にシステムのモデルについて論理を用いて形式的に推論することを指します。 自動推論 は、形式手法の自動化に焦点を置いています。 半自動推論 ツールとは、ユーザーからのヒントを必要とするものの、論理において妥当な証明を見つけるツールです。 このように、この領域で仕事をする際には呼び名の選択肢がいくつもあります。Amazon では自動推論という呼び方を選びました。自動化とスケールに対する私たちの意欲を最もよく表していると考えているからです。実際には、社内のチームの一部は自動推論ツールと 半 自動推論ツールの両方を使っています。私たちが採用してきた科学者は、完全自動の推論におけるヒューリスティックが失敗しかねない場面でも、半自動推論ツールを使って成功させられることが多いからです。外部のお客様向け機能については、現在は完全自動のアプローチのみを使用しています。 次のステップ この記事では、ごく小さなトイプログラム (例示用の簡単なプログラム) を用いて自動推論という考え方を紹介しました。ヒープや並行性を含む現実的なプログラムの扱い方には触れていません。実際には、自動推論のツールと技法は非常に多岐にわたり、中にはかなり狭い領域もありますが、多種多様な領域の問題を解いています。それらすべてと、この分野の数多くの系統や下位分野 (例えば「充足可能性モジュロ理論 (satisfiability modulo theories、SMT) の求解」「高階論理の定理証明」「分離論理」) を説明するには、数千本のブログ記事と書籍が必要になるでしょう。 自動推論の起源は、コンピュータの初期の発明者たちにまで遡ります。そして論理そのもの (自動推論が解こうとしている対象) には数千年の歴史があります。この記事を簡潔に保つため、ここで筆を置き、さらに読むべき資料の紹介に移ります。なお、この分野を深さ優先で読み進めると細部に迷い込みやすく、始めたときより混乱してしまう可能性があります。1 つの側面だけを深く学ぶのではなく、深さを制限した深さ優先探索のアプローチで、さまざまなツールや技法をそれぞれ少しずつ順に見ていき、次へ進むことをお勧めします。 おすすめの書籍 Handbook of Practical Logic and Automated Reasoning Temporal Verification of Reactive Systems Decision Procedures Model Checking Software Foundations Specifying Systems Introduction to Static Analysis Logic in Computer Science: Modelling and Reasoning about Systems Functional Algorithms, Verified! Handbook of Satisfiability The Calculus of Computation 国際会議・ワークショップ https://etaps.org/2020/tacas https://ijcar2020.org/ https://popl21.sigplan.org/ http://smt-workshop.cs.uiowa.edu/ ツールコンペティション http://termination-portal.org/wiki/Termination_Competition https://sv-comp.sosy-lab.org/2020/ https://smt-comp.github.io/2020/ http://www.satcompetition.org/ ツールの例 AGREE: http://loonwerks.com/tools/agree.html Alloy: https://alloytools.org/ Aprove: https://aprove.informatik.rwth-aachen.de/ BioModelAnalyzer: https://biomodelanalyzer.com/ Boogie: https://github.com/boogie-org/boogie.git CBMC: https://www.cprover.org/cbmc/ Checked C: https://plum-umd.github.io/projects/checkedc.html Checker Framework: https://checkerframework.org/ CoCoSim: https://github.com/NASA-SW-VnV/CoCoSim Coq: https://coq.inria.fr/ CPA Checker: https://cpachecker.sosy-lab.org/ CVC4: https://cvc4.github.io/ Dafny: https://github.com/dafny-lang/dafny Dreal: https://github.com/dreal/dreal4 HOL light: https://www.cl.cam.ac.uk/~jrh13/hol-light/ Infer: https://fbinfer.com Iris: https://iris-project.org/ Isabelle: https://isabelle.in.tum.de/ Java PathFinder: https://github.com/javapathfinder JKind: https://github.com/loonwerks/jkind KeYmaera X: https://keymaerax.org/ Kind2: https://kind.cs.uiowa.edu/ KLEE: https://klee.github.io Lean: https://leanprover.github.io/ MiniSat: http://minisat.se/ Nagini: https://github.com/marcoeilers/nagini P: https://github.com/p-org/P PRISM: https://www.prismmodelchecker.org PVS: https://pvs.csl.sri.com Rosette: http://emina.github.io/rosette/ Rust プログラミング言語: https://www.rust-lang.org/ [Rust でプログラミングすることは、本質的に型システムの中でメモリ破壊が起こらないことを証明していることになります (unsafe 領域を使用していない場合)] Sally: https://github.com/SRI-CSL/sally SAW: https://github.com/GaloisInc/saw-script SeaHorn: http://seahorn.github.io/ SMACK: https://smackers.github.io Soot: http://soot-oss.github.io/soot/ SPIN: http://spinroot.com/spin/whatispin.html T2: https://mmjb.github.io/T2/ TLA+: https://lamport.azurewebsites.net/tla/tla.html Vampire: https://vprover.github.io/ VCC: https://github.com/microsoft/vcc Verifast: https://github.com/verifast/verifast Z3: https://github.com/Z3Prover/z3 自動推論の活用について語る Amazon スタッフへのインタビュー Byron Cook PLDI’20 Ask Me Anything Byron Cook on The CUBE Neha Rungta on The CUBE Neha Rungta が AWS Config ルールにおける制約ベースの推論ツールについて語る Serdar Tasiran CAV’21 Ask Me Anything LogMeIn: How LogMeIn Automates Governance and Empowers Developers at Scale お客様と業界に向けた AWS の講演 Automating Compliance Verification on AWS Using Provable Security 。AWS のコンプライアンス担当 VP である Chad Woolf と、コンプライアンス監査企業 Coalfire の CEO である Tom McAndrew 氏による講演 An AWS Approach to Higher Standards of Assurance w/ Provable Security 、Byron Cook Dive Deep into IAM Access Analyzer 。Andrew Gacek 他による講演 The Evolution of automated reasoning Technology at AWS 。AWS のセキュリティ担当 VP である Eric Brandwine による講演 AWS の CISO 兼セキュリティ担当 VP である Steve Schmidt による、AWS における形式的/制約ベースのツールの開発と活用に関する 講演 AWS re:Invent 基調講演 、CTO ワーナー ヴォゲルス 自動推論の科学コミュニティに向けた AWS の発表 Debugging Network Reachability with Blocked Paths 、CAV’21 Embedded World 2021: Formally Verifying the FreeRTOS IPC Mechanism 、Embedded World ’21 Formal reasoning about the security of Amazon Web Services 、FLoC 2018 基調講演 Formal reasoning about the security of Amazon Web Services 、OOPSLA/SPLASH 2018 基調講演 How I learned to stop worrying and start applying automated reasoning 、FACC’21 (その他の関連発表は FACC のウェブサイト をご覧ください) On automated reasoning for compliance certification 、Formal Approaches to Certifying Compliance (FACC) に関する CAV ワークショップ Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning 、CAV’21 Provable Security at AWS 、USENIX Enigma 2019 [30 分の箇所までスキップしてください]: SideTrail: Verifying Time-Balancing of Cryptosystems Stratified abstraction of access control policies 、CAV’20 Verified Cryptographic Code for Everybody 、CAV’21 What is automated reasoning? How Is it Used at AWS? AWS のブログ記事と解説動画 A simpler way to assess the network exposure of EC2 instances: AWS releases new network reachability assessments in Amazon Inspector AWS CTO による自動推論グループについてのブログ記事: Proving security at scale with automated reasoning AWS CTO が S3 の整合性について語る AWS ポッドキャストのインタビュー: Provable security podcast: Byron interviews Moshe Vardi AWS ポッドキャストのインタビュー: Next Generation Security with automated reasoning, an Artificial Intelligence Technology AWS Config アップデート – S3 バケットをセキュアに管理する新しいマネージド ルール 。IAM ポリシーに対する自動的な制約解決技法を活用した AWS Config のイベント駆動チェックについて解説しています。さらに 詳細はこちら 新しい Amazon S3 暗号化 & セキュリティ機能 。Amazon Web Services の S3 コンソールにおける、ポリシーに関する制約ベースの推論の活用について解説しています ブログ 1 、 2 、 3 : Galois と協力して、Amazon の暗号インフラストラクチャコンポーネントである s2n の正しさを証明した取り組みについて解説しています Chad Woolf (AWS のコンプライアンス担当 VP) が、コンプライアンス認証を簡素化し水準を高めるために自動推論を活用することへの関心について語る Daniel Schwartz-Narbonne が、AWS のブートコードにおける証明可能なセキュリティの実現に自動推論がどのように役立っているかを紹介 How automated reasoning helps us innovate at S3 scale How automated reasoning improves Prime Video experience How AWS SideTrail verifies key AWS cryptography code How AWS uses automated reasoning to help you achieve security at scale Jeff Barr による IoT 設定検証ツールの紹介 新機能 – VPC Reachability Analyzer Zelkova ベースの新しい AWS Config ルール s3-blacklisted-actions-prohibited と bucket-policy-not-more-permissive がリリース Podcast: AI tech named automated reasoning provides next-gen cloud security Amazon Macie で用いられている制約ベースの IAM ポリシー分析の詳細については、 こちら を参照してください Tightening application security with Amazon CodeGuru Using Formal Methods to validate OTA Protocol … その他の AWS ブログ Amazon Scholar として Amazon と協働する大学教授による講義ノート https://courses.cs.washington.edu/courses/cse507/21au/ http://www.cs.cmu.edu/~mheule/15816-f21/ https://www.cs.cmu.edu/~mheule/15217-f21/ とっておきの深掘りトピック 今日私たちが使っている自動定理証明器に見られるアルゴリズムの一部は、1959 年にまで遡ります。この年に Hao Wang 氏が自動推論を用いて証明したのは Principia Mathematica の定理です。 著者について Byron Cook Amazon の vice president 兼 distinguished scientist である Byron Cook は形式的検証分野のリーダーであり、SAT (充足可能性問題)、SMT、記号的モデル検査への貢献と、生物システム、コンピュータのオペレーティングシステム、プログラミング言語、セキュリティへの応用で知られています。Byron が Amazon で進めてきた自動推論の取り組みは、クラウドにおけるより高い水準の保証と、新たなお客様向け機能をもたらしています。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

こんにちは！Girls Meet STEM in AWS 運営メンバーの守田です。2026 年 8 月 21 日、AWS は中高生女子の皆さんを 2026 年に開設したばかりの麻布台ヒルズの新オフィスにお迎えし、「自分のアイデアを AI アプリにする」体験をお届けしました。私は普段、アマゾン ウェブ サービス ジャパン合同会社 (以下、AWS) でソリューションアーキテクトとして働いています。 イベント概要 AWS は「Girls Meet STEM」に参加し、東京都港区の麻布台ヒルズの新オフィスにてイベントを開催しました。 「Girls Meet STEM」は、公益財団法人山田進太郎 D&I 財団が大学や企業と協力して実施するツアー形式のプログラムです。中高生女子が STEM（科学・技術・工学・数学）分野で働く人や学ぶ学生、実際の現場に触れることで、将来の可能性を広げる機会を提供します。 今回は 34 名の中高生の方々にご参加いただきました。「AWS ってどんなビジネスをしている会社？」「クラウドってなに？」といった紹介から始まり、生成 AI 体験ワークショップ、オフィスツアー、AWS 社員によるパネルディスカッションを実施しました。特に生成 AI 体験ワークショップに関しては、AI と会話することが当たり前になっている皆様に、もう一歩踏み込んで、 AI を”使う”側から、自分のアイデアを形にする”作る”側へ という体験をお届けしました。 プログラム詳細 1. 生成 AI 体験ワークショップ 〜 自分のアイデアをアプリにする 〜 ワークショップでは、AWS の有志を中心に開発された生成 AI アプリケーション「 Generative AI Use Cases (GenU) 」の「ユースケースビルダー」機能を使いました。ユースケースビルダーは、タイトル・説明・プロンプトテンプレート（AI への指示文）を入力するだけで、コードを書かずに自分だけの AI アプリを作れる機能です。裏側では Amazon Bedrock を通じて生成 AI モデルが動いています。 当日は、まず参加者の方々に「どんな AI アプリがあったら、自分や身のまわりの人が嬉しいか？」を考えてもらいました。テーマが決まったら、ユースケースビルダーにタイトルと説明を入力し、AI への指示となるプロンプトテンプレートを自分の言葉で書いてアプリを作成。完成したアプリを実際に動かして、思ったとおりの答えが返ってくるかを確かめ、うまくいかなければプロンプトを書き直して何度も試す——という流れで、自分だけの AI アプリを一から作り上げていきました。 このワークショップのポイントは、 「AI に何をさせたいかを自分で設計する」 という点です。生成 AI を利用する際は出力を受け取るだけですが、アプリを作る際は、入力項目の定義とプロンプト（AI への指示）の設計を自分で行う必要があります。参加者の皆さんには、この設計プロセスを通じて、アプリ開発の基本的な考え方を体験いただきました。 参加者の方々は、自身の興味や日常からテーマを設定し、テスト対策アプリ、恋愛相談に乗ってくれるアプリ、ファッション相談アプリ、読書感想文作成アプリなど、身近な悩みを解決するアプリを動く形へ落とし込んでいきました。「自分でアプリを作るのは難しいと思っていたが、実際に自分が使いたくなるようなアプリが作れてとても楽しかった」といった声もいただきました。 ユースケースビルダーの基本的な使い方や画面イメージについては、 GenU の開発ガイド で詳しくご紹介しておりますので、あわせてご覧ください。 昨年からのアップデート — 「考えを”図”にしてくれる AI」 今年、参加者から好評だったのが、 生成 AI が文章を”図”に変換してくれる 体験です。GenU のユースケースビルダーは画像の出力ができず、テキスト出力が主ですが、フロントエンドが Markdown 内の mermaid コードブロックを検出し、SVG としてレンダリングする仕組みが備わっています。例えば、「興味を入力すると将来の職業をおすすめしてくれるアプリ」を作った場合、マインドマップ形式で職業を表示することが可能です。 「職業おすすめ AI」のプロンプトテンプレート 先ほど例に挙げた「興味を入力すると将来の職業をおすすめしてくれるアプリ」は、次のようなプロンプトテンプレートで作成できます。難しい設定は必要なく、「新規作成」からタイトル・説明・プロンプトテンプレートの 3 つを入力するだけです。 プロンプトテンプレートには次のように記述しました。 あなたは中高生の進路相談にのるキャリアアドバイザーです。 以下の「興味のある分野」をもとに、関連する職業と必要なスキルをマインドマップで提案してください。 <興味のある分野> {{text:興味のある分野}} </興味のある分野> 作成したアプリで「興味のある分野」に「IT」と入力して実行すると、関連する職業のジャンルから具体的な職種、必要なスキルまでが枝分かれしたマインドマップが表示されます。 図の左上に「図を表示」「コードを表示」の切り替えボタンがあり、 生成 AI が実際に出力した Mermaid のテキストをその場で確認できます 。描画された図は SVG や PNG としてダウンロードすることも可能です。「画像が生成された」ように見えるものが、実際にはテキストから描かれていることが、この切り替えで一目でわかります。 Mermaid （マーメイド）はテキストで図を記述するためのダイアグラム記述言語で、生成 AI が出力しているのは画像ではなく、あくまでこの記述テキストです。参加者にとって Mermaid 形式は見慣れない内容ですが、画像以外にも図を表示する手法があるという観点に気づいた参加者の方もいました。 マインドマップに続いて、タイプ別のおすすめ職業や「今からできること」といった文章も出力されます。図と文章を組み合わせることで、全体像を俯瞰しながら具体的な行動まで確認できる構成になります。 2. オフィスツアー 〜 「働く場所」のイメージが変わる 〜 会場となった麻布台ヒルズの新オフィスをめぐるツアーを実施しました。このオフィスのデザインは日本の四季と伝統的な庭園文化にインスピレーションを得ており、働く人の活力と創造性を高める工夫が随所に散りばめられています。 参加者からは「パソコンがずらっと並んだ部屋を想像していたけれど、全然違って驚いた」「オフィスが綺麗で驚いた」「季節を意識したり、トンボをイメージしたライトなど、建物の工夫が面白かった」といった声が寄せられました。 3. AWS 社員によるパネルディスカッション 〜 進路の「軸」を見つける 〜 AWS で活躍する 4 名の女性社員が登壇し、学生時代の経験や、文理・進路の選択、なぜ今の仕事を選んだのかについてお話ししました。参加者の中には、文理の選択やなりたい職業について悩んでいる方が多くいらっしゃいました。そこで、AWS 社員も同じような悩みを抱えていたこと、そしてどのような興味をたどって今の仕事に行き着いたのかをお話しすることで、進路を考えるヒントを持ち帰っていただく時間となりました。「将来のことはほとんど決められていなくて不安でしたが、いろいろな経歴を経て今の職に就いた社員の方のお話を聞いて、自分なりのやりたいことの軸を見つけていけたらいいなと思いました。」といった感想もいただきました。 参加者の声 「自分好みの生成 AI を作ることができること、いままであまりよく知らなかった職業を知ることができたこと、会社員の方の高校時代のおはなしなど、とても学びが多い時間でした。今回の経験が自分の将来に必ず役に立つと感じました。」 「理系と文系を行き来した方のお話から、モチベーションと自分の中での軸があれば、自分の夢が叶うことがわかりました。」 「プログラミングに興味があり、日常で聞いていた AWS についても知れました。現役社員さんのお話は、進路を決める時にすごくためになりました。社内ツアーで社内を見せていただくことで想像もでき、少し楽しみになりました。」 参加者をサポートした AWS メンバーの声 「アプリを作れたという成功体験に、参加者が喜んでいました。『すごい！』という素直な感想が出たり、うまくいかなかったらサイクルを回すという試行錯誤ができたりと、良い経験になっていたと思います。」 「グループワークでは、進路相談などの雑談も一緒にできました。皆さんやりたいことがたくさんあって素晴らしかったです。」 昨年 2025 年夏に開催した Girls Meet STEM in AWS の様子は、 昨年の開催報告ブログ でご紹介しています。あわせてご覧ください。 著者について 守田 凜々佳 (Morita Ririka) Amazon Web Services Japan G.K. のソリューションアーキテクトとして、ISV/SaaS 業界のお客様を中心に、AWS をご利用になるお客様を技術面でサポートしています。好きなサービスは Amazon Quick です。週末はヴァイオリンの演奏を楽しんでいます。