Amazon Bedrockの自動推論チェックが生成AIのコンプライアンスを変える方法
Amazon BedrockのAutomated Reasoning checksは、生成AIの出力を数学的検証で形式的に証明し、規制産業におけるコンプライアンス課題を解決する技術を提供している。
キーポイント
規制産業におけるコンプライアンス課題
医療、金融、保険などの規制産業では、AI出力の手動レビューや外部コンサルタントへの依存が非効率であり、確率的なLLM-as-a-judgeアプローチでは監査可能な保証が得られない。
Automated Reasoning checksの技術的特徴
Amazon Bedrock Guardrailsの機能として、形式的検証（formal verification）を基盤に、AI生成出力を定義されたルールと制約に対して数学的に検証し、証明可能で監査可能な結果を提供する。
従来手法との根本的差異
確率的システム同士の検証（LLM-as-a-judge）ではなく、数学的論理に基づく形式的検証により、ルール違反があれば具体的に特定し、全てのルールとの整合性を証明できる。
実用事例と適用範囲
6つの産業分野の顧客が採用しており、保険請求のカバレッジ判断など、誤った回答が規制上の結果をもたらす場面で、形式的に検証された監査可能なAI出力を生成している。
影響分析・編集コメントを表示
影響分析
この技術は、生成AIの企業導入における最大の障壁の一つである規制コンプライアンスを、数学的証明によって解決する画期的なアプローチを提供する。確率的な出力検証から形式的検証への移行は、金融、医療、保険など厳格な規制下にある産業でのAI採用を加速させる可能性が高い。
編集コメント
AIの実用化において避けて通れないコンプライアンス課題を、数学的アプローチで根本から解決しようとする試みは、業界の成熟度を示す重要なマイルストーンと言える。
Amazon BedrockにおけるAutomated Reasoning checksが生成AIのコンプライアンスをどのように変革するか
規制業界のコンプライアンスチームは、手動レビューに数週間を費やし、外部コンサルタントに多額の費用を支払っても、AIの出力に形式的な証明がない場合、監査上の抜け穴に直面します。Amazon Bedrock GuardrailsのAutomated Reasoning checksは、確率的なAI検証を数学的検証に置き換えることでこの課題に対処し、AIが生成した判断を証明可能な正しさを持つ監査可能な結果に変えます。
本記事では、確率的なAI検証が規制業界においてなぜ不十分なのか、そしてAutomated Reasoning checksが形式的検証 (formal verification)を用いて数学的に証明された結果をどのように提供するかをご説明します。また、6つの業界にわたる顧客が、この技術を用いて形式的に検証された監査可能なAI出力をどのように生成しているか、そして使い始める方法についてもご紹介します。
コンプライアンスの課題
規制業界は、重大なコンプライアンスの課題に直面しています。病院は放射線安全規制を遵守し、金融機関はEU AI Actに基づいてAIリスクを分類しています。保険会社は、誤った回答が規制上のペナルティにつながる補償範囲の質問に対応しています。手動レビュー、高額なコンサルタント費用、そして既存のプロセスではスケーラビリティが追いつきません。
生成AIやエージェント型ソリューションを構築する多くのチームは、LLM-as-a-judgeパターンを採用しています。これは、第2のLLMを使用して最初のモデルの出力を評価する手法です。直感的には理解しやすいものの、このアプローチには根本的な限界があります。すなわち、確率的なシステムが別の確率的なシステムを検証するだけでは、規制業界が必要とする形式的で監査可能な保証を提供できません。
自動推論チェックが定義されたルールと制約のセットに対して証明可能なコンプライアンスをどのように提供するか
Amazon Bedrock GuardrailsのAutomated Reasoning checksは、数学的論理に基づいた形式的検証手法 (formal verification methods)を適用し、定義されたルールと制約のセットに対してAIが生成した出力を検証します。すべてのリクエストに対して、証明可能な正しさと監査可能な評価が得られます。
以下の例を考えてみましょう。AIアシスタントが顧客に対し、保険請求は補償対象であると伝えます。LLM-as-a-judgeアプローチでは、第2のモデルがその回答を検証し「正しそう」と判断します。一方、Automated Reasoning checksでは、システムがその回答がポリシーのすべてのルールと一致することを数学的に証明します。ルールが違反されている場合、どのルールがどのように違反されたかを正確に特定します。
image
図1：自動推論の分類体系。定理証明、型システム、モデル検査、抽象解釈、記号実行、SMTソルビング、SATソルビングを含む。SATおよびSMTソルビングは、Automated Reasoning checksの基盤を形成します。
- *
自動推論（Automated reasoning）は、与えられた前提から論理的結論を自動的に導き出すアルゴリズムを開発する分野です。これは、形式検証（formal verification）（システムが仕様を満たすことを数学的に証明する）、充足可能性ソルビング（satisfiability solving）（論理式が充足可能かどうかを判定する）、および数学的論理学（mathematical logic）における数十年にわたる研究の成果を基盤としています。
これらの基盤技術は、ハードウェア設計の検証、暗号プロトコルの妥当性証明、および安全クリティカルなソフトウェアが仕様をどの箇所で違反しているかを特定するために用いられてきました。現在、Automated Reasoning checksはこれらを生成AIに応用しています。
このチェック機能は、ニューラルネットワーク（neural networks）と論理推論を組み合わせ、定義されたルールや制約に対してAIの出力を検証します。これにより、確率的応答（probabilistic responses）を形式的に検証され監査可能な成果物へと変換します。AWSは、AIアプリケーションを保護するお手伝いをするため、複数のresponsible AIツールの一つとしてAutomated Reasoning checksを提供しています。
Automated Reasoningポリシーの設定方法と検証の実際の動作について詳しく知りたい場合は、Amazon BedrockのAutomated Reasoningチェックで生成AIのハルシネーションを最小限に抑えるをご覧ください。
image
図2: Amazon BedrockにおけるAutomated Reasoning checksの4つのステップ（ポリシーエンコーディング、出力変換、形式検証エンジン、結果生成）を示すプロセス図。
業界別アプリケーション
医療、金融、エネルギー、保険、教育などの分野の組織は、Automated Reasoning checksを用いてAIの出力を検証し、監査対応可能な証拠に基づいてコンプライアンスに関する判断を説明しています。
運用エンジニアリング：Amazon Logistics
Amazon Logisticsチームは、すべての判断に対して形式的なコンプライアンス検証を受けながら、エンジニアリングのレビュー時間を約8時間から数分に短縮しました。Amazon LogisticsのSustainability Engineeringチームは、Amazonの配送ステーションネットワーク全体にElectric Vehicle Charging Points（EVCPs）を展開する取り組みを主導しています。各設置提案は、地域固有の規制と社内技術仕様を満たす必要があります。従来、各レビューには約8時間を要し、専門家がエンジニアリングパラメータを手動で照合する必要がありました。
AWSと連携して、チームはAutomated Reasoningチェックを基盤とした生成AI支援の設計レビューポータルを構築しました。このポータルは、明示的に定義された変数、型、条件を含む正確な論理規則など、技術仕様をAutomated Reasoningポリシーに変換します。提案書から抽出されたエンジニアリングパラメータを形式数学的推論を用いて検証します。Amazon BedrockのClaudeは、文書インテリジェンスレイヤーを駆動し、構造化されていない提案書からデータを抽出して構造化します。
“当社の専門家は意思決定者であり続け、ツールの動作を完全に把握でき、すべての推奨事項を追跡、検証、確認できるという確信を持っています。”
– ポウラ・ガルシア・カラスコ、シニアサステナビリティエンジニア、AMZL
専門家は現在、退屈なパラメータの一致作業ではなく、エンジニアリング判断に注力しています。Amazon Logisticsのケーススタディはこちら
ファイナンスサービス：Lucid MotorsとPwC
Lucid Motorsは予測生成を数週間から1分未満に短縮し、わずか10週間で企業全体に14のAIユースケースを展開しました。電気自動車メーカーであるLucid Motorsは、PwCおよびAWSと連携し、AIネイティブな財務予測・分析ソリューションを構築しました。財務チームはよくある課題に直面していました。数週間の手動作業を要する予測サイクルにより、急速に変化する市場状況への対応能力が制限されていたのです。
PwCとAWSは共同で、Amazon Bedrock上で機械学習（ML）ベースの予測エージェントを構築しました。チームはAutomated Reasoningチェックを形式検証レイヤーとして適用し、モデルの出力が事前に定義された財務ルールと制約に準拠していることを数学的に検証しました。このアプローチは、確率的AI単独では見逃す可能性がある論理的矛盾を検出します。
財務チームは現在、レポートを数週間待つのではなく、リアルタイムでビジネス意思決定に積極的に貢献しています。
“PwCおよびAWSとの連携により、Lucidはクラウド環境をイノベーションのプラットフォームに変革しています… PwCチームは予測ツールを迅速に構築し、手動作業の所要時間を数週間から1分未満に削減しました。”
– アディティヤ・バヘティ、ビジネス財務責任者、Lucid
教育：First Education & Technology Group (FETG)とPwC
FETGはルール設定作業を最大80%削減し、継続的なコンプライアンスオーバーヘッドを50%削減し、応答レイテンシを8〜13秒から1.5秒に最適化しました。MarsLadder AI学習システムの運用者であるFirst Education & Technology Group (FETG)は、PwCおよびAWSと連携し、学生向け生成AIに対する責任あるAIガバナンスレイヤーを構築しました。従来のモデレーションアプローチ、キーワードフィルター、確率的分類器は、文脈や意図が重要なSafer Technologies 4 Schools (ST4S)フレームワークを確実に適用できませんでした。
PwCは、Automated Reasoning checks（自動推論チェック）を決定論的検証レイヤーとして実装し、データ保護と学生の安全をカバーする10の形式論理ルールにST4S原則を翻訳しました。このシステムは、学習者に届く前にすべてのAI生成応答を検証し、確率的な判断に代わって数学的に証明可能なコンプライアンスを実現します。
本ソリューションは、数学的に証明可能なコンプライアンス証拠を提供し、教育規制当局がST4Sフレームワークへの準拠を求める際に必要とする機能です。Explore the PwC case study on Responsible AI in Education.
More industries adopting Automated Reasoning checks
規制業界全体で組織も、コンプライアンスを強化するためにAutomated Reasoning checksを採用しています。
- Financial services (EU AI Act): EU AI Act（EU人工知能法）に基づいてAIリスクを分類する組織は、Automated Reasoning checksを使用して、一貫性のない手動レビューから、形式的に検証可能で監査準備が整ったコンプライアンスワークフローへ移行しています。PwCとAWSがAutomated Reasoningで責任あるAIを構築する方法をご覧ください。
- Energy and utilities: 電力事業者は、North American Electric Reliability Corporation（NERC）およびFederal Energy Regulatory Commission（FERC）の規制要件に対してAI生成の停電分類を検証し、各dispatch（配電判断）決定の背後に形式検証を設けます。このユースケースに関するPwCとのre:Inventトークをご覧ください。
- Pharmaceuticals and life sciences: プロフェッショナルサービス企業は、AI駆動のマーケティングコンテンツに対して数学的に検証可能な検証レイヤーを構築し、コンテンツ主張が承認されたソース資料に基づいていることを検証します。
- Insurance: 保険会社は、ポリシー言語に対して形式的に推論を行う顧客向けチャットボットを構築し、確率的な近似値ではなく検証可能なカバレッジ（補償）決定を提供します。
Conclusion
本投稿では、Amazon Bedrock GuardrailsのAutomated Reasoning checksが、監査準備が整った証拠とともに数学的に証明可能な検証をどのように提供するかをご理解いただきました。規制業界でコンプライアンスアシスタントを構築するチーム、または既存のAIワークフローに形式検証レイヤーを追加するチームにとって、この技術は確率的な信頼性から数学的証明への道筋を提供します。
Automated Reasoning checksは、retrieval-augmented generation（検索拡張生成）用のKnowledge Bases for Amazon Bedrock、コンプライアンス追跡用のAWS Audit Manager、モデルガバナンス用のAmazon SageMaker AIなど、他のAWS responsible AI（責任あるAI）機能と補完し合います。
準備はできましたか？
- Get started：設定ガイドについては、How Automated Reasoning checks documentationをご覧ください。
ハンズオンチュートリアルについては、How to minimize generative AI hallucinations with Automated Reasoning checksをご覧ください。
- チャットボットは、How Automated Reasoning checks feedbackを用いて回答を反復的に書き換え、検証可能な正解に達するまでユーザーに確認質問を行うことができます。
- 始め方については、How Automated Reasoning checks rewriting chatbot reference implementationをご覧ください。
- エージェントは、自然言語で専門知識を持つ担当者（subject matter experts）を伴走させながらHow Automated Reasoning policyの改善プロセス全体を案内できます。このようなエージェントのオープンソースサンプルをご覧ください。
- 顧客事例の閲覧：Amazon Logistics case study | PwC Responsible AI in Education case study | AWS Responsible AI resources
- Amazon Bedrock機能の詳細：Amazon Bedrock Guardrails | Amazon Bedrock AgentCore
- AIライフサイクル全体におけるガイダンスと責任あるAI（Responsible AI）のベストプラクティス：AWS Well-Architected Responsible AI Lens
How Automated Reasoning checksがcompliance use casesをどのように支援できるかについてご議論いただくには、AWSアカウントチームまでお問い合わせください。準備として、AIの出力に対して形式検証（formal verification）が求められる上位3つのcompliance workflowsを特定してください。
image
図3：Reference architecture for compliance checks with Amazon Bedrock Automated Reasoning.
- ユーザーはAmazon CloudFrontを介してアプリケーションにアクセスし、ReactフロントエンドはAmazon Simple Storage Service（Amazon S3）の静的ホスティングから提供されます。
- Amazon Cognitoがユーザーを認証し、JWTトークンを発行します。CloudFrontは下流のリクエストに対して認証を強制します。
- ユーザーは、リージョン、施設タイプ、ライセンスカテゴリを指定してコンプライアンスチェックリクエストを送信します。CloudFrontはリクエストをAWS Lambdaにルーティングします。
- Lambdaは、リージョン、施設タイプ、ライセンスカテゴリをキーとして使用してAmazon DynamoDB Rules Engineにクエリを実行し、適用される正確な規制ルールを返します。
- Lambdaはルールをプロンプトに注入し、Amazon Bedrockを呼び出します。Knowledge Baseは、Amazon S3に保存された検証済みの規制ドキュメントから、検索拡張生成（RAG: Retrieval-Augmented Generation）のコンテキストを提供します。
- 生成されたコンプライアンスチェックリストはAmazon Bedrock Automated Reasoning Checks（ARC: 自動推論チェック）に送信され、ルールが形式論理モデルにコンパイルされて各項目が数学的に検証されます。この検証は確率的なものではなく、証明可能なものです。
- 検証済みの項目はAmazon S3に保存され、ユーザーに戻されます。無効な項目はモデルによる補正再生（最大3回の再試行）をトリガーします。対象外の項目は推論付きで自動的に除外されます。
- 2番目のDynamoDBテーブルには顧客の施設プロファイルが保存されており、各リクエストでデータを再アップロードすることなく、IDで病院を検索できます。
- Amazon EventBridge Schedulerは、構成可能なスケジュールでLambdaウェブクローラーをトリガーし、政府の規制ウェブサイトからポリシー変更をスクレイピングします。
- スクレイピングされたコンテンツはAmazon Bedrock Policy Diff Agentに送信され、変更箇所が検出されます。更新されたルールはDynamoDBに書き込まれ、新しいドキュメントがKnowledge Baseに再インデックスされます。
- ARC検証証明付きのコンプライアンスレポートはDynamoDBに保存され、監査証跡、フィルタリング、ダウンロードのためにReports Tabからアクセス可能です。
謝辞
*この取り組みに貢献したSuresh Kanan、Tonny Ouma、Laurie Kasper、Stefano Bulianiに特別感謝いたします。
著者について
image
Nafi Diallo
Nafi DialloはAmazon Web Servicesのシニア自動推論アーキテクトであり、信頼性の高いAIソリューションのためのAIセキュリティ、形式検証、ガードレール実装を専門としています。彼女はAmazon Bedrock上で生成AIおよびエージェントシステムの信頼性を評価し改善する豊富な経験を持っています。Nafiはまた
原文を表示
Compliance teams in regulated industries spend weeks on manual reviews, pay for outside consultants, and still face audit gaps when AI outputs lack formal proof. Automated Reasoning checks in Amazon Bedrock Guardrails address this by replacing probabilistic AI validation with mathematical verification, turning AI-generated decisions into provably correct, auditable results.
In this post, you’ll learn why probabilistic AI validation falls short in regulated industries and how Automated Reasoning checks use formal verification to deliver mathematically proven results. You’ll also see how customers across six industries use this technology to produce formally verified, auditable AI outputs, and how to get started.
The compliance challenge
Regulated industries face high-stakes compliance challenges. Hospitals navigate radiation safety regulations. Financial institutions classify AI risk under the EU AI Act. Insurance carriers answer coverage questions where incorrect responses carry regulatory consequences. Manual review, costly consultants, and legacy processes don’t scale.
Many teams building generative AI or agentic solutions reach for a large language model (LLM)-as-a-judge pattern: using a second LLM to evaluate the first model’s outputs. While intuitive, this approach carries a fundamental limitation: one probabilistic system validating another cannot provide the formal, auditable guarantee that regulated industries require.
How Automated Reasoning checks deliver provable compliance against a defined set of rules and constraints
Automated Reasoning checks in Amazon Bedrock Guardrails apply formal verification methods, grounded in mathematical logic, to validate AI-generated outputs against a defined set of rules and constraints. You get a provably correct, auditable assessment for every request.
Consider the following example. An AI assistant tells a customer their insurance claim is covered. With an LLM-as-a-judge approach, a second model reviews that answer and says “looks right.” With Automated Reasoning checks, the system mathematically proves the answer is consistent with every rule in the policy. If rules are violated, it identifies exactly which ones and why.
Figure 1: Automated Reasoning taxonomy, including Theorem Proving, Type Systems, Model Checking, Abstract Interpretation, Symbolic Execution, SMT Solving, and SAT Solving. SAT and SMT solving form the foundation of Automated Reasoning checks
- *
Automated reasoning develops algorithms that automatically derive logical conclusions from given premises. It draws on decades of research in formal verification (mathematically proving a system meets its specification), satisfiability solving (determining whether a logical formula can be satisfied), and mathematical logic.
These same foundations verify hardware designs, prove cryptographic protocols sound, and pinpoint exactly where safety-critical software violates its specification. Automated Reasoning checks now apply them to generative AI.
The checks combine neural networks with logical reasoning to validate AI outputs against defined rules and constraints, transforming probabilistic responses into formally verified, auditable artifacts. AWS offers Automated Reasoning checks as one of several responsible AI tools to help you safeguard your AI applications.
For a detailed walkthrough of how to configure Automated Reasoning policies and see verification in action, see Minimize generative AI hallucinations with Amazon Bedrock Automated Reasoning checks.
Figure 2: Automated Reasoning checks in Amazon Bedrock, showing the 4-step process: Policy Encoding, Output Translation, Formal Verification Engine, and Result Generation.
Industry applications
Organizations across healthcare, finance, energy, insurance, and education use Automated Reasoning checks to verify AI outputs and explain compliance decisions with audit-ready evidence.
Operational engineering: Amazon Logistics
The Amazon Logistics team reduced engineering review time from approximately 8 hours to minutes while receiving formal compliance verifications on every determination. Amazon Logistics’ Sustainability Engineering team leads the deployment of Electric Vehicle Charging Points (EVCPs) across Amazon’s delivery station network. Each installation proposal needs to meet region-specific regulations and internal technical specifications. Previously, each review required a subject matter expert to spend approximately 8 hours manually cross-referencing engineering parameters.
Working with AWS, the team built a generative AI-assisted design review portal powered by Automated Reasoning checks. The portal translates technical specifications into Automated Reasoning policies, including precise logical rules with explicitly defined variables, types, and conditions. It validates engineering parameters extracted from proposals using formal mathematical reasoning. Claude in Amazon Bedrock powers the document intelligence layer, extracting and structuring data from unstructured proposals.
“Our experts remain the decision-makers, with complete visibility into how the tool operates and the confidence that every recommendation can be traced, verified, and validated.”
– Paula Garcia Carrasco, Sr. Sustainability Engineer, AMZL
Subject matter experts now focus on engineering judgment rather than tedious parameter matching. Learn more in the Amazon Logistics case study
Financial services: Lucid Motors and PwC
Lucid Motors reduced forecast generation from weeks to less than one minute and scaled 14 AI use cases across the enterprise in only 10 weeks. Lucid Motors, the electric vehicle manufacturer, partnered with PwC and AWS to build an AI-native finance forecasting and analytics solution. The finance team faced a familiar challenge: forecasting cycles that took weeks of manual effort, limiting their ability to respond to rapidly changing market conditions.
Together, PwC and AWS built machine learning (ML)-based forecasting agents on Amazon Bedrock. The team applied Automated Reasoning checks as a formal verification layer to mathematically validate that model outputs adhered to predefined financial rules and constraints. This approach catches logical inconsistencies that probabilistic AI alone might miss.
The finance team now actively shapes business decisions in real time rather than waiting weeks for reports.
“Together with PwC and AWS, Lucid is turning its cloud environment into a platform for innovation… PwC’s team rapidly built forecasting tools to reduce manual efforts from weeks to less than a minute.”
– Aditya Baheti, Head of Business Finance, Lucid
Read the Lucid Motors case study.
Education: First Education & Technology Group (FETG) and PwC
FETG achieved up to an 80% reduction in rule-setup effort, a 50% reduction in ongoing compliance overhead, and response latency optimized from 8–13 seconds to 1.5 seconds. First Education & Technology Group (FETG), operator of the MarsLadder AI learning system, partnered with PwC and AWS to build a responsible AI governance layer for student-facing generative AI. Traditional moderation approaches, keyword filters, and probabilistic classifiers failed to reliably enforce the Safer Technologies 4 Schools (ST4S) framework where context and intent matter.
PwC implemented Automated Reasoning checks as a deterministic validation layer, translating ST4S principles into ten formal logic rules covering data protection and student safety. The system verifies every AI-generated response before it reaches a learner, replacing probabilistic judgment with mathematically provable compliance.
The solution provides mathematically provable compliance evidence, a capability that education regulators require for adherence to the ST4S framework. Explore the PwC case study on Responsible AI in Education.
More industries adopting Automated Reasoning checks
Organizations across other regulated industries also adopt Automated Reasoning checks to strengthen compliance:
- Financial services (EU AI Act): Organizations classifying AI risk under the EU AI Act use Automated Reasoning checks to move from inconsistent manual review to formally verifiable, audit-ready compliance workflows. Learn how PwC and AWS build responsible AI with Automated Reasoning.
- Energy and utilities: Utility operators verify AI-generated outage classifications against North American Electric Reliability Corporation (NERC) and Federal Energy Regulatory Commission (FERC) regulatory requirements, with formal verification behind each dispatch decision. Watch the re:Invent talk with PwC on this use case.
- Pharmaceuticals and life sciences: Professional services firms build mathematically verifiable validation layers for AI-driven marketing content, verifying that content claims are grounded in approved source materials.
- Insurance: Insurance carriers build customer-facing chatbots that reason formally over policy language, providing verifiable coverage determinations rather than probabilistic approximations.
Conclusion
In this post, you learned how Automated Reasoning checks in Amazon Bedrock Guardrails deliver mathematically provable verification with audit-ready evidence. For teams building compliance assistants in regulated industries or adding a formal verification layer to existing AI workflows, this technology provides a path from probabilistic confidence to mathematical proof.
Automated Reasoning checks complement other AWS responsible AI capabilities, such as Knowledge Bases for Amazon Bedrock for retrieval-augmented generation, AWS Audit Manager for compliance tracking, and Amazon SageMaker AI for model governance.
Ready to get started?
- Get started: Explore the Automated Reasoning checks documentation for setup guidance.
For a hands-on walkthrough, see How to minimize generative AI hallucinations with Automated Reasoning checks.
- Your chatbot can iteratively rewrite its answers using Automated Reasoning checks feedback, asking the user clarifying questions until it reaches a provably correct answer.
- To get started, see the Automated Reasoning checks rewriting chatbot reference implementation.
- An agent can walk a subject matter experts through the entire process of improving the Automated Reasoning policy in natural language; See our open-source sample of such an agent.
- See customer results: Amazon Logistics case study | PwC Responsible AI in Education case study | AWS Responsible AI resources
- More about Amazon Bedrock features: Amazon Bedrock Guardrails | Amazon Bedrock AgentCore
- Guidance and responsible AI best practices across AI lifecycle: AWS Well-Architected Responsible AI Lens
To discuss how Automated Reasoning checks can support your compliance use cases, contact your AWS account team. To prepare, identify your top 3 compliance workflows where AI outputs require formal verification.
Figure 3: Reference architecture for compliance checks with Amazon Bedrock Automated Reasoning.
- User accesses the application via Amazon CloudFront, which serves the React front end from Amazon Simple Storage Service (Amazon S3) static hosting.
- Amazon Cognito authenticates the user and issues a JWT token. CloudFront enforces authentication on downstream requests.
- User submits a compliance check request specifying their region, facility type, and license category. CloudFront routes the request to AWS Lambda.
- Lambda queries the Amazon DynamoDB Rules Engine using region, facility type, and license category as the key. Returns the exact applicable regulatory rules.
- Lambda injects the rules into a prompt and calls Amazon Bedrock. The Knowledge Base provides retrieval-augmented generation (RAG) context from verified regulatory documents stored in Amazon S3.
- The generated compliance checklist is sent to Amazon Bedrock Automated Reasoning Checks (ARC), which compiles the rules into a formal logic model and mathematically verifies each item. This verification is provable, not probabilistic.
- Verified items are stored in Amazon S3 and returned to the user. Invalid items trigger corrective regeneration with the model (max 3 retries). Out-of-scope items are auto-excluded with reasoning.
- A second DynamoDB table stores customer facility profiles so hospitals can be looked up by ID without re-uploading data on every request.
- Amazon EventBridge Scheduler triggers a Lambda web crawler on a configurable schedule to scrape government regulatory websites for policy changes.
- Scraped content is sent to the Amazon Bedrock Policy Diff Agent, which detects what changed. Updated rules are written to DynamoDB and new documents are re-indexed into the Knowledge Base.
- Compliance reports with ARC verification proofs are stored in DynamoDB and accessible via the Reports Tab for audit trails, filtering, and downloads.
Acknowledgement
*Special thanks to Suresh Kanan, Tonny Ouma, Laurie Kasper and Stefano Buliani who contributed to this work.*
About the authors
Nafi Diallo
Nafi Diallo is a Senior Automated Reasoning Architect at Amazon Web Services, specializing in AI safety, formal verification, and guardrails implementation for trustworthy AI solutions. She brings deep experience evaluating and improving the reliability of generative AI and agentic systems on Amazon Bedrock. Nafi also
関連記事
AWSがS3 Filesを導入、S3バケットへのファイルシステムアクセスを実現
AWSはS3 Filesを発表し、ユーザーがAmazon S3バケットをマウントして標準ファイルシステムインターフェースでデータにアクセスできるようにした。アプリケーションは標準ファイル操作で読み書きでき、システムが自動的にS3リクエストに変換するため、コンピュートサービスがS3に保存されたデータを直接扱える。
AWSが自動インシデント調査のためのDevOpsエージェントを一般提供開始
AWSは、開発者と運用者がAWS環境での問題のトラブルシューティング、デプロイメントの分析、運用タスクの自動化を支援する生成AI搭載アシスタント「DevOps Agent」の一般提供を開始した。
Amazon Bedrockの詳細なコスト帰属機能の導入
AWSがAmazon Bedrockの推論コストをIAMプリンシパルごとに自動的に帰属する機能を発表した。これにより、コストの内訳把握、コスト最適化、財務計画が容易になる。