Amazon Web Services ブログ

AWS Weekly Roundup: Amazon Bedrock 上の OpenAI GPT-6 Astra、Amazon Quick デスクトップ GA、学生向け Kiro など (2026 年 9 月 14 日)

ニューヨークの 9 月中旬には、特別なエネルギーがあります。パンプキンスパイスラテがたっぷりとあり、気温も下が […]

自動推論による数学的確実性の 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 の自動推論チェックがこれらにどのように取り組んでいるかを解説します。