本ブログは 2025 年 8 月 4 日に公開された Amazon Science Blog “ Three challenges in machine-based reasoning ” を翻訳したものです。 自然言語から構造化された言語への変換、真理の定義、そして確定的な推論は、自動推論において依然として中心的な課題です。しかし、Amazon Web Services の新しい自動推論チェック (Automated Reasoning checks) は、これらすべてに対処するのに役立ちます。 生成 AI の登場により、自動推論の分野に携わってきた私の 30 年以上のキャリアの中で、ここ数年は最も刺激的な時期になっています。なぜでしょうか。コンピュータ業界、さらには一般の方々までもが、論理の分野に携わる私たちが長年情熱を注いできたアイデアについて、今や熱心に語るようになったからです。言語、構文、意味論、妥当性、健全性、完全性、計算複雑性、さらには決定不能性といった課題は、かつては学術的で難解すぎて、多くの人々には縁のないものでした。しかし、状況は一変しました。これらのテーマに触れ始めたばかりのみなさん、ようこそ。ぜひ足を踏み入れてください。一緒に取り組めることを楽しみにしています。 本記事では、AI システム (例えばチャットボットのような生成 AI ベースのシステム) で正しい推論を実現する際に、最も厄介だと私が考える 3 つの側面を紹介します。Amazon Bedrock Guardrails の自動推論チェック機能をリリースした背景には、まさにこれらの難題がありました。とはいえ、まだ道半ばです。これらの問題には本質的な難しさがあるため、私たちはコミュニティとして (そして自動推論チェックのチームとして)、この先も長年にわたってこれらの難題に取り組み続けることになるでしょう。 難題 1: 自然言語から構造化された言語への変換 人間は通常、厳密さに欠けるあいまいな言葉でやり取りしています。多くの場合、文脈からあいまいさを解消する情報を補って理解できます。本当に重要な場面では、「～という意味でしょうか」と互いに確認し合うこともあります。しかし、本当に確認すべき場面であっても、そうしないこともあります。 これはしばしば混乱と対立の原因になります。ある雇用主が、従業員向け福利厚生の受給資格を「フルタイム換算 (FTE) 0.2 以上の雇用契約を有していること」と定義しているとしましょう。ここで私が「手術を受けた家族の回復を支えるために昨年休みを取った期間を除き、自分の時間の 20% を仕事に費やしています」と伝えたとします。私はこの福利厚生を受ける資格があるでしょうか。「自分の時間の 20% を仕事に費やしている」という発言は、雇用契約のもとで、労働時間の 20% に相当する時間を働いているという意味なのでしょうか。 私の発言には複数の合理的な解釈が成り立ち、解釈によって受給資格の結論が変わります。自動推論チェックでは、相補的ないくつかのアプローチを用いて、自然言語とクエリ述語の間の変換を複数回試みます。これはインタビューでよく使われる手法と同じです。同じ情報を異なる方法でたずね、事実が一貫しているかどうかを確かめるのです。自動推論チェックでは、形式論理体系のソルバーを使って、異なる解釈が等価であるかどうかを証明または反証します。変換結果が意味のレベルで食い違っていれば、自動推論チェックを利用するアプリケーションは、ユーザーに確認を求めることができます (例: 「フルタイムの 20% 以上の雇用契約があることを確認していただけますか」)。 自動推論チェックは、大規模言語モデルを使用して、自然言語を形式言語へ変換した複数の候補を生成します。変換結果の間に食い違いがあれば自動推論チェックがそれを指摘し、お客様は自然言語による対話を通じて解消できます。 難題 2: 真理の定義 いつも驚かされるのは、ルールの意味について複数の人が合意することがいかに難しいかという点です。複雑なルールや法律には微妙な矛盾が潜んでいることが多く、誰かがその解釈について合意を形成しようとするまで見過ごされることがあります。例えば、英国の 1988 年著作権・意匠・特許法 (Copyright, Designs and Patents Act 1988) には本質的な矛盾があります。著作権の対象となる著作物を著作者自身の知的創作から生じたものと定義する一方で、人間の創造的な関与を必要としない著作物にも保護を与えているのです。この不整合は、AI が作品を生成する現代において、とりわけ目立つものになっています。 2 つ目の問題は、私たちがルールを絶えず変え続けているように見えることです。例えば、米国連邦政府の日当 (per diem) の額は毎年変更されるため、その値に依存するシステムは常に保守が必要になります。 最後に、自分が従うべきルールのコーナーケースをすべて深く理解している人はほとんどいません。運転中のイヤホン装着を例に考えてみましょう。米国では、アラスカ州のように違法な州、フロリダ州のように片方のイヤホンだけなら合法な州、そしてテキサス州のように問題なく合法な州があります。友人や同僚に非公式に聞いてみたところ、直近で車を運転した場所において、運転中のヘッドホン装着が合法かどうかを自信を持って答えられた人は、ごくわずかでした。 自動推論チェックは、税法、人事ポリシー、その他のルール体系といったお客様の関心領域において何を真理とするかを定義できるよう支援し、さらにルールの変更に合わせてその定義を継続的に洗練する仕組みを提供することで、これらの難題に対処します。生成 AI ベースのチャットボットが登場したとき、私たちの多くが想像力をかき立てられたのは、複雑なルール体系を自然言語のクエリで一般の方々にも利用できるようにする、という発想でした。将来、チャットボットは「日本の東京で運転中に U ターンできますか」といった質問に、端的でわかりやすい回答を返せるようになる可能性があります。真理を定義するという難題に取り組むことで、自動推論チェックはその回答の信頼性を確保するのに役立ちます。 自動推論チェックのユーザーインターフェイス。 難題 3: 確定的な推論 ルールの集合 (これを R と呼びます) と、検証したい文 ( S ) があるとします。例えば、 R はシンガポールの交通規則、 S はシンガポールの交差点での U ターンに関する質問だとしましょう。 R と S は、ブール変数をさまざまに組み合わせることで、コンピュータが理解できるブール論理へエンコードできます。 R と S のエンコードに必要なのはわずか 500 ビット、およそ 63 文字だとしましょう。ごく小さな情報量です。しかし、ルール体系のエンコードがテキストメッセージに収まるほど小さくても、チェックすべきシナリオの数は天文学的な規模になります。理論上は、2 500 とおりの組み合わせをすべて検討しなければ、 S が真であると断定することはできません。今日の高性能なコンピュータは、まばたきをする間に数億回の演算を実行できます。しかし、世界中のコンピュータをこの猛烈な速度で宇宙の始まりから動かし続けていたとしても、2 500 とおりの可能性をすべてチェックし終えるには、今日に至ってもなお程遠いでしょう。 ありがたいことに、自動推論のコミュニティは SAT (充足可能性問題) ソルバーと呼ばれる高度なツール群を開発してきました。これによって、この種の組み合わせのチェックが可能になり、すべてではないものの、多くのケースで驚くほど高速に実行できます。自動推論チェックは、文の妥当性を検証する際にこれらのツールを活用しています。 残念ながら、あらゆる問題を SAT ソルバーの強みが生きる形でエンコードできるわけではありません。例えば、あるルール体系に次の規定があるとしましょう。 「2 より大きいすべての偶数が 2 つの素数の和であるならば、源泉徴収税率は 30% とし、そうでなければ 40% とする」 。問題は、源泉徴収税率を知るには 2 より大きいすべての偶数が 2 つの素数の和であるかどうかを知る必要があるのに、それが真かどうかを現時点で誰も知らないという点です。この命題はゴールドバッハ予想と呼ばれ、1742 年以来の未解決問題です。とはいえ、ゴールドバッハ予想の答えはわからなくても、それが真か偽のいずれかであることは確かです。したがって、源泉徴収税率は 30% か 40% のいずれかでなければならない、と確定的に言えます。 自動推論チェックを利用するお客様が、自動推論チェック自身の判定結果に依存するポリシーを定義できるかどうかを考えてみるのも面白いところです。例えば、次のルールをポリシーとしてエンコードすることは可能でしょうか。 「アクセスは、自動推論チェックが『許可されない』と判定した場合、かつその場合に限り許可される」 。この場合、正しい答えは存在しません。このルールは自身のチェック手続きを再帰的に参照することで矛盾を生み出しているからです。ここでできる最善の対応は「不明 (Unknown)」と答えることです (実際、このケースで自動推論チェックが返す答えも「不明」です)。 訳注: 2026 年 9 月時点の Amazon Bedrock ユーザーガイドでは、自動推論チェックの検証結果は VALID、INVALID、SATISFIABLE、IMPOSSIBLE、TRANSLATION_AMBIGUOUS、TOO_COMPLEX、NO_TRANSLATIONS の 7 種類として定義されており、「不明 (Unknown)」という結果値はありません。ポリシーの矛盾により判断できない場合は IMPOSSIBLE が返されます。参照: 自動推論チェックの概念 – Amazon Bedrock 自動推論チェックのようなツールが、こうした文に対して「真」も「偽」も返せないという事実は、1931 年に Kurt Gödel によって初めて示されました。Gödel の結果からわかるのは、自動推論チェックのようなシステムは無矛盾性と完全性を同時に満たせず、どちらかを選ばなければならないということです。AWS は無矛盾性を選びました。 自然言語を構造化された論理へ変換すること、絶えず変化し、時には矛盾するルールのもとで真理を定義すること、確定的な推論の複雑さに立ち向かうこと。この 3 つの難題は、健全な推論を備えた AI システムを構築する際に直面する単なる技術的ハードルにとどまりません。いずれも、私たちの技術の限界と、人間が作る仕組みの複雑さの両方に深く根ざした問題です。 2025 年 8 月 6 日の Amazon Bedrock Guardrails における自動推論チェックのリリースを機に、AWS は相補的なアプローチを組み合わせてこれらの難題に取り組んでいます。具体的には、あいまいな自然言語から論理述語へ変換するためのクロスチェック手法を適用すること、お客様によるルール体系の開発と保守を支援する柔軟なフレームワークを提供すること、そして確定的な回答が得られないケースを慎重に扱いながら高度な SAT ソルバーを活用することです。これらの難題に対する製品の性能を高めていく中で、AWS は技術を前進させるだけでなく、Gödel の不完全性定理から、変化し続ける法律やポリシーの枠組みのあり方に至るまで、推論そのものを形作ってきた根本的な問いへの理解も深めています。 健全な推論を提供するというコミットメントを踏まえれば、AI 分野における今後の道のりは険しいものです。その挑戦を受けて立ちます。 著者について Byron Cook Amazon の vice president 兼 distinguished scientist である Byron Cook は、形式的検証分野のリーダーであり、SAT、SMT、記号モデル検査への貢献と、それらを生物システム、コンピュータのオペレーティングシステム、プログラミング言語、セキュリティへ応用した実績で知られています。Byron が Amazon で進めてきた自動推論の取り組みは、クラウドにおけるより高い水準の保証と、お客様向けの新機能の実現につながっています。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

こんにちは、エンジニアの澤田です。 前回の記事 では、Rust で RgbColor 構造体を使って演算子オーバーロードをやってみましたが、今回はその RgbColor を使ってグラデーションを表現するイテレータを作ってみたいと思います。 私はイテレータを普段の業務であまり意識せずに使っていましたが、イテレータのインターフェースを実装することで理解を深めたいと思い、試してみました！ ※rustc と cargo はバージョン 1.97.1、edition 2024 を使用しています。 イテレータとは イテレータを一言でいうと、 次の要素を1つずつ返してくれるもの です。 配列のように

はじめに この記事は、BASE夏のブログリレー7日目の記事です。 BASE Dept Order SectionでエンジニアをしているCapi(かぴ)です。 本記事では有志でチームを組んで進めているBASEのWebアプリケーションセキュリティ施策の一環で脅威モデリングを行ったのでそのご紹介です。脅威モデリングに興味のある方の参考になれば嬉しいです。 最初にこの記事で伝えたいこと3つを事前に共有しておきます。 目的をもって脅威モデリングを導入する 小さく始めて継続することを意識する 脅威モデリングに時間はかかったが、得るものは多かった 脅威モデリング実施の背景 過去のインシデント履歴 BASEでも過去に決済周りのインシデントが発生しています。決済のインシデントはユーザーにも会社にも影響が大きく、恒久対応のプロジェクトが立ち上がったこともありました。ただ、いずれも「発生してから気づく」受け身の対応でした。そこで、自分たちで決済周りを事前に検査し、原因を特定し、修正まで行える能動的な体制を作りたいと考えました。 OWASP SAMMのスコア改善 以前OWASP SAMMというフレームワークを使い、ソフトウェア開発ライフサイクル全体におけるセキュリティ対策成熟度を数値化しました。その結果として、"セキュリティ基準の明文化"や"アプリケーションの継続的なセキュリティ評価実施"の項目のスコア改善を目指すことにしました。 今後も追加開発が行われシステムが複雑化していくことを予想し、早めの対策を打ちたいと考えました。 脅威モデリング実施前の準備 先行事例調査 脅威モデリングをどう行い、どう活かしていくのかの具体事例が知りたかったためまずは先行事例を調査しました。主に企業のテックブログを参考にさせていただきました。 脅威モデリングを始めてみました - セキュリティリスク分析の第一歩 Luup社 メルカリの脅威モデリングプロセス mercari社 事例を調査する中で気づいたのは「想像以上に日本語の事例がインターネットで公開されていないこと」です。脅威モデリングに関する情報はたくさん公開されているのですが、具体的な事例紹介は少なかったです。 手法を学ぶ STRIDE、Attack Treeを学びました。 STRIDEは脅威を6種類に分類して網羅的に洗い出す手法、Attack Treeは特定の攻撃目標に至る経路や条件をツリー状に分解する手法です。 最終的にはじめての脅威モデリングだったので多くに手を出さず、情報が手に入りやすい(インターネットでの情報が多い)ものを採用したいという理由で STRIDE を使うことに決めました。 STRIDEに関してはMicrosoft社をはじめ大手のサイバーセキュリティ企業が公開している資料がありました。 Microsoft Threat Modeling Tool の脅威 また、Attack Treeは今後導入していきたいものとして概要のみ押さえました。 Monthly Research 「脅威分析の役割と手法の紹介」 脅威モデリングに対して共通認識を持つ 前提として最初に「重要箇所から小さくはじめて少しずつ範囲を広げていく」をチームで合意しました。当時のドキュメントにある意思決定内容にも「小さくはじめる」、「できる範囲から実施し、継続する」というのを残しました。 当時の社内意思決定ドキュメントより引用 最初から完璧を目指さない dfdを完璧にしないと脅威モデリングができないわけではありません。わかる範囲で実施し、継続することが大事です。 引用文に出てくるdfdは Data Flow Diagram(データフロー図) のことで、システムにおけるデータの流れを表した図のことです。データの流れからシステムの機能を洗い出します。 脅威モデリングの設計 セキュリティインシデントが発生した場合にユーザー影響、会社への影響が大きい箇所から優先的に脅威モデリングを行いたいと考え、まず下記2シナリオを選びました。 カート機能のクレジットカード決済 カート機能で購入者アカウントにログインした状態でのクレジットカード決済 BASEにはいろんな決済手段、決済時のオプションがありますが今回は一番オーソドックスなものを選びました。「まずはシンプルな決済手段から」というのをチームで合意を取っていたためです。 また、洗い出す脅威を絞りました。今回はSTRIDEを選んだため最大6種類の脅威が存在します。今回はその中からS、T、Iに絞りました。チームでクレジットカード決済でよく発生しそうなものは何かを話し合い決めました。また、多くの脅威を洗い出そうとすることで脅威モデリングの時間が伸びてしまうことを防ぐためです。 略字 脅威 日本語 脅威の内容 侵害されるセキュリティ特性 今回の対象 S Spoofing なりすまし 他人や他システムになりすまして正規の利用者・サービスとして振る舞う 真正性(Authentication) ○ T Tampering 改ざん データや通信、コードを不正に書き換える 完全性(Integrity) ○ R Repudiation 否認 行った操作や取引を後から「やっていない」と否定できてしまう 否認防止(Non-repudiation) 次回 I Information Disclosure 情報漏洩 権限のない相手に情報が渡ってしまう 機密性(Confidentiality) ○ D Denial of Service サービス拒否 サービスを利用できない状態に追い込む 可用性(Availability) 次回 E Elevation of Privilege 権限昇格 本来持たない権限を取得して操作を行う 認可(Authorization) 次回 DFD作成 今回は脅威モデリングの対象範囲にしたカート機能のクレジットカード決済処理の範囲のみDFDを作成しました。 DFD作成が脅威モデリング準備で一番時間がかかりました。カート機能がBASEのコア機能でありたくさんのシステムコンポーネントが関わっているため図解するための現状理解が難しかったためです。 DFD作成では生成AI(Claude Code)を活用し、時間短縮を目指しました。 カート機能をClaude Codeに読み込ませDFDをMermaidで出力 MermaidをFigJamにインポート Mermaid Live Preview でもMermaidを表示し、見比べながらFigJam側の図を整える FigJamのインポートには Mermaid to FigJam というプラグインを使いました。 FigJamにインポートしたのは脅威モデリング中、付箋を貼るだけで脅威を残せる形にしたかったためです。 脅威モデリング実施 進め方 アプリケーションエンジニア2人で時間を合わせ、オンラインで行いました。 シナリオごとにDFDを追う シナリオを追いながら気になったところに付箋を貼る 貼った付箋に対して議論する、深掘って追加の付箋を貼る ※進め方の補足 付箋はSpoofing（なりすまし）を緑、Tampering（改ざん）を赤、Information Disclosure（情報漏洩）をオレンジにして貼りました DFDをAIに出力してもらった関係上、実際の動きと異なる部分がいくつか見つかりました。DFDの不安な箇所は既存のUMLを参照したり実際にコードを読みました。 脅威モデリングで出てきた脅威 詳細をご共有することはできないため割愛しますが、SとTとIどれも同じくらい見つかりました。 下の表にそれぞれいくつ付箋が貼られたのかを数えてまとめています。 脅威 数 Spoofing（なりすまし） 8 Tampering（改ざん） 9 Information Disclosure（情報漏洩） 7 システム間の接続部分に付箋が集中しました。 新しい決済手段を実装するときに意識すること、守るべきことを明文化していく素材を手に入れられました。 わかったこと 脅威モデリングの難易度 取り組み当初は「1シナリオ1時間あれば十分」と見積もっていました。しかし、実際に取り組むと、DFD作成に2時間半、脅威の洗い出しに4時間、合計6時間半かかりました。時間を食うのはシナリオ選定ではなく、図解と脅威の洗い出しでした。 はじめてで慣れていなかったとはいえ他の業務と兼務してやり切るのは難易度が高いことがわかりました。 シナリオ2つを選んだのも原因です。今後は余裕を持って1つずつ確実に進めます。 自分たちのシステム認識と実態のズレ 脅威モデリングを行う前、カート機能に関わるのはアプリケーション(フロントエンド)、アプリケーション(バックエンド)、外部サービス1つ(決済代行サービス)、DBくらいだと想定していました。 しかし、DFDを作って脅威モデリングを進めるうちに、想定外のものが次々と出てきました。 把握しきれていなかった内部システムとの接続 1つ 把握しきれていなかった外部システムとの接続 1つ アプリケーションが参照しているデータソース 2つ 想定していたコンポーネント数と同じだけ、知らないものがありました。 画面だけ見ると単純な決済処理でも、内部では多くのコンポーネントと通信が関わっています。脅威モデリングそのものも大事ですが、DFDを作成し正しく整理していくだけでも学びは多かったです。 継続するために行ったこと。今後やること。 DFD、脅威モデリング結果の記録 今回のDFD、脅威モデリング結果は社内の誰もが閲覧できるFigJamに残せました。 また、DFDの作り方や脅威の分類も図解することで今回脅威モデリングを行ったメンバー以外の人が脅威モデリングを始める土台を準備できました。 次の脅威モデリング対象を決める BASEのカートには他にもたくさん機能があります。今回の脅威モデリングや直近の開発プロジェクトを考慮し、今後下記シナリオの脅威モデリングをやりたいと考えています。 使用率の高いクレカ以外の外部決済手段 かんたん海外販売のカート機能 セキュリティ要件の作成 現在、脅威モデリングを元にセキュリティ要件を作成しています。今後、カートの追加開発をする時に「ここだけは守ってほしい」ことを明文化していきます。 セキュリティツール導入のPoC 脅威モデリングで出した脅威に対し、自分たちでテストを行い、テスト結果をレポートにして早期防止に繋げる仕組みを作りたいと考えています。 その仕組みを作るためにDASTツール、IASTツールの導入PoCを進めています。 おわりに 今回は脅威モデリング未経験者が調査から実践までやってみた経験、学びを共有させていただきました。 BASEでは機能開発はもちろん非機能要件について考える課題があり、その課題に挑戦する機会もあります。ご興味あればぜひ採用情報をご覧ください。 binc.jp 明日はwakanaさんによる社内のサービスレベル活動推進に関する記事です！ 参考資料 OWASP SAMM OWASP Threat Modeling Process 脅威モデリングを始めてみました - セキュリティリスク分析の第一歩 メルカリの脅威モデリングプロセス 脅威モデリングをソリューション化させるまでの歩み Newton Consulting「STRIDEモデル」 Microsoft Threat Modeling Tool の脅威 脅威モデリングとは｜実施手順と成功のためのポイントを解説 Monthly Research 「脅威分析の役割と手法の紹介」 DFD