Amazon Web Services ブログ

自動推論による数学的確実性の 10 年: Automated Reasoning Group が歩んだ道

Automated Reasoning Group (ARG) の発足から 10 年の歩みを振り返ります。自動推論による形式的検証は研究プロトタイプから、Amazon Inspector、IAM Access Analyzer、Reachability Analyzer といったお客様向けサービスへと発展しました。Nitro Isolation Engine や暗号実装、認可エンジンの正しさを証明した内部の取り組み、Amazon Bedrock Guardrails の自動推論チェックによる生成 AI のハルシネーション防止、そして Amazon Bedrock AgentCore や Kiro でのエージェンティック AI への展開まで、システムを「おそらく正しい」だけでなく「正しいと証明できる」ものにする数学的確実性の価値を紹介します。

エージェント型 AI による ERP ビジネスプロセス運用の変革

大量のトランザクションを扱う企業にとって、ERP システムにおける手作業の例外処理は、重要なビジネスプロセスの遅延やお客様満足度・収益認識への影響を招くボトルネックとなります。本記事では、Accenture が Amazon Bedrock や Amazon Bedrock AgentCore、Strands Agents SDK、AWS Lambda、Amazon RDS、AWS Step Functions といった AWS サービスを用いて構築した、エージェント型 AI ソリューションをご紹介します。このソリューションは、Direct Ship（直送）請求業務の例外管理を、手作業から自律的でエージェント主導の解決へと転換し、展開からわずか 5 週間で業務上の摩擦の軽減、課題解決の加速、売上の実現の向上を実現しました。SAP S/4HANA との統合により、対話型の Digital Assistant がリアルタイムの運用データへのアクセスと文脈に沿った解決策の推奨を提供します。

自動推論に立ちはだかる 3 つの難題

自動推論の分野に 30 年以上携わってきた著者が、生成 AI で正しい推論を実現するうえで最も厄介だと考える 3 つの難題を紹介します。あいまいな自然言語から構造化された論理への変換、絶えず変化し、時には矛盾するルールのもとでの真理の定義、そして SAT (充足可能性問題) ソルバーでも越えられない計算量の壁やゲーデルの不完全性定理が示す確定的な推論の限界です。これらは単なる技術的ハードルにとどまらず、技術の限界と人間が作る仕組みの複雑さの両方に根ざした問題です。Amazon Bedrock Guardrails の自動推論チェックがこれらにどのように取り組んでいるかを解説します。

はじめての自動推論

Amazon Science の研究領域に新たに加わった自動推論について、予備知識のない方に向けてわかりやすく解説します。簡単な C と Python のコード例を使い、網羅的テストでは 1,300 年以上かかる検証を自動推論がミリ秒で示せる理由、テストが今後も必要な理由、停止性問題ゆえに「Don’t know」という答えが避けられない事情、論理・定理証明・形式手法といった関連用語の違いを説明します。IAM Access Analyzer や VPC Reachability Analyzer など AWS での活用例と、学習用の書籍・ツールの一覧も紹介します。

セキュリティにおける AI の現在地: 信頼構築に最も重要な指標の測定

セキュリティ業務で AI を活用する際、脆弱性を発見できるかだけでなく、安全なコードを誤検出しないかが信頼の鍵になります。本記事では、実際の脆弱性と誤検出を見分ける能力を測る初のベンチマーク Deception Benchmark を紹介します。16 のプログラミング言語、70 を超える CWE カテゴリの 14,822 サンプルで 12 モデルを評価した結果、FPR (偽陽性率) と FNR (偽陰性率) の両方を 10% 未満に抑えられた構成はありませんでした。設計手法と結果、実務への示唆を詳しく解説します。

← Older posts