証明せよ、第2部：形式論理、Cedarポリシー、そして検証の経済学

自動推論は、ビジネスポリシーを形式論理に変換し、そのルールに照らして検証することで、LLMの出力に検証機能を追加します。これにより、ハルシネーションの検出、コンプライアンス要件の遵守、エージェントの行動制御を実現し、手動QAのわずかなコストで包括的なカバレッジを提供します。

第1部「おそらく正しい」では不十分では、AIを活用したプロダクトを構築するスタートアップに、確率的な安全対策だけでなく決定論的な検証が必要である理由を説明しました。本記事では、その内部の仕組みに踏み込みます。AIスタートアップの技術系共同創業者、エンジニアリングリーダー、またはシニアデベロッパーであれば、自動推論が実際にどのように機能するのか、LLMが応答を生成した際に形式論理がどのようにそれを検証するのか、そしてなぜコスト面においてQAチームを雇うよりもはるかに合理的な選択肢となるのかを学ぶことができるでしょう。

本記事ではAPIコードは扱いません。それについては第3部で説明します。ここでは、皆さんが構築しているものを理解できるよう、概念、形式論理、そして検証パイプラインに焦点を当てます。

確率的アプローチと決定論的アプローチ：根本的な違い

仕組みの詳細に入る前に、この根本的な違いを明確に理解しておくことが重要です。なぜなら、この違いは皆さんが下すあらゆるアーキテクチャ上の意思決定に影響を及ぼすからです。

LLMは確率的なシステムです。

LLMは、学習データから獲得した確率分布に基づいて次のトークンを予測します。温度、Top-k、Top-pといったサンプリングパラメータは、意図的にランダム性を導入します。同じプロンプトを2回実行しても、異なる回答が生成される可能性があります。これは欠陥ではなく機能です。この特性こそが、LLMに柔軟性と創造性を与え、多様な自然言語入力への対応を可能にしています。しかし同時に、個々の出力は確率分布から得られたサンプルに過ぎず、証明された事実ではないことも意味します。

自動推論（AR）は正しいことが保証されています。

自動推論では、ルールの集合と入力が与えられた場合、その結果は単なる最善の推測ではありません。それは証明です。ある主張は、定められたルールに照らして証明可能な形で妥当であるか、証明可能な形で妥当でないか、あるいは不足している情報や曖昧な点が何であるかをシステムが正確に示します。回答が誤っている場合でも、ARは単にそれを指摘するだけではありません。なぜ失敗するのかを正確に示す反例を提示します。出力は確率的なものではなく、数学的に検証可能です。温度の調整は存在しません。サンプリングも存在しません。そこにあるのは、検証可能な証明です。

これは、どちらかのアプローチが「優れている」という話ではありません。LLMは自然言語の理解や人間のような応答の生成に優れています。一方でARは、それらの応答が論理的に正しいかどうかを検証することに優れています。両者を組み合わせることで完全なスタックが成立します。すなわち、LLMが対話を担い、ARが正しさを担保します。このニューラルネットワークと形式論理の組み合わせは、研究者によってニューロシンボリックAIと呼ばれています。

5人規模のスタートアップが最初の100人の顧客にプロダクトをリリースする段階では、この違いは非常に現実的な意味を持ちます。QAチームを抱えるだけの人員はなく、コンプライアンス上のインシデントを吸収できるほどの資金的余裕もありません。形式検証はフォースマルチプライヤーとして機能し、小規模なチームでも大規模な組織と同等の確信を持ってリリースできるようにします。

Amazon Bedrockにおける2つの保護レイヤーは何ですか？

AWSはARを2つのレイヤーで提供しており、それらは多くのAIスタートアップの成熟度カーブにきれいに対応しています。初期段階では、プロダクトはチャットボットやアシスタントであることが多く、LLMが顧客の質問に回答したり、レコメンデーションを生成したり、ガイダンスを提供したりします。この段階では、Amazon Bedrock Guardrailsにおける自動推論が、モデル出力の 内容を定義されたビジネスルール に照らして検証します。

規模が拡大するにつれて、エージェント型ワークフローを構築するようになります。AIが予約を取ったり、返金処理を行ったり、データベースをクエリしたり、外部APIを呼び出したりするようになります。このレイヤーでは、Amazon Bedrock AgentCoreのポリシーがエージェントに許可されるアクションを制御し、ツール実行の前段階でゲートウェイにおいてCedarポリシーによって強制的に適用されます。

Cedarポリシーはエージェントが何を実行できるかを制御します。しかし、ARチェックAPIをエージェントのツールキットとして公開することもでき、エージェント自身が実行前に中間的な結論を検証できるようにします。エージェントはポリシーに対してApplyGuardrailを呼び出し、その結果を確認し、ユーザーを介さずに自己修正を行います。複数ステップのワークフローを計画しているエージェントは、その提案した手順が制約に違反していないかを確認したり、前提の矛盾を検出したり、導出された値が入力から正しく導かれているかを検証したりできます。これによりARは境界チェックから推論パートナーへと役割が変わります。つまり、エージェントはゲートで止められるだけでなく、そもそもゲートに向かうこと自体を避けるようになります。

両者の比較は以下の通りです：

ARチェックとAmazon Bedrock AgentCoreのポリシーは、アプリケーションの異なるレイヤーを保護します。

• ARチェックは、AIが何を言っているかを検証します。つまり、この住宅ローンの適格性に関する回答は、あなたの融資基準に照らして正しいか、ということです。
• Amazon Bedrock AgentCoreのポリシーは、AIが 何を実行できるかを制御します。つまり、このエージェントは返金を実行したり、顧客のアカウントを照会したりする権限があるか、ということです。

現在構築している内容によっては、どちらか一方から、あるいは両方から始めることになります。

• MVPがポリシーに関する質問に回答するチャットボットである場合、最初の統合対象はARチェックになります。
• 予約を行い、金銭を移動させるエージェントを提供する場合、ポリシーは初日から必須です。

ほとんどのスタートアップは、最終的に両方を併用するようになります。

ARチェックの仕組み：ビジネスルールを形式論理としてエンコードする方法

ARへの入力はポリシーであり、そのポリシーは既存のドキュメントから始まります。

フィンテックのスタートアップであれば、それは融資基準書かもしれません。ヘルスケア分野では、臨床プロトコルやHIPAA対応手順である場合があります。保険業界では、引受基準ガイドラインに相当します。これらの文書は、AIが何を言うべきか、何を言うべきでないかを定義しています。これらはすでに法務部門のレビューを受けており、投資家もデューデリジェンスの過程で確認しています。ARは、こうした既存の資産を実行可能なルールへと変換します。つまり、ゼロから新しいものを構築するのではなく、すでに存在するものを有効化しているのです。

Amazon Bedrockにポリシードキュメント（PDF、Markdown、またはプレーンテキスト）をアップロードすると、システムは2つの要素を抽出します。それは変数とルールです。

変数は、あなたのドメインにおける概念を表します。各変数には名前、型、そして説明があります。例えば、住宅ローンの適格性ポリシーでは次のようになります：

変数の記述は、精度において最も重要な要素です。曖昧な記述は、LLMにその変数が何を意味するのかを推測させてしまいます。一方で、その概念が何を意味するのか、ユーザーがそれをどのように呼んでいるのか、そしてポリシードキュメント上でどのように現れるのかを説明する詳細な記述は、LLMが自然言語を正しい形式変数へと対応付けるために必要なコンテキストを提供します。ここにこそ、スタートアップビルダーとしてのドメイン知識が最も重要に働く部分があります。

ルールは、変数間の関係を表現する形式論理式です。これらはSMT-LIB構文のサブセットを使用し、ほとんどはif-then（含意）形式に従います：

住宅ローンのポリシードキュメントをアップロードすると、Bedrockの内部ではこのような内容が生成されます。コンソール上でこれらのルールを確認し、システムが意図を正しく捉えているか検証することはできますが、SMT-LIBを手で記述するわけではありません。あなたはポリシーを自然言語で記述し、システムがそれを形式論理へと変換します。

2段階の検証プロセス

ARポリシーを設定し、それをガードレールに紐付けた後（詳細は第3部で説明します）、アプリケーションがApplyGuardrailに送るすべてのLLMレスポンスは、2段階の検証プロセスを通過します。この分離を理解することは極めて重要です。なぜなら、どこにリソースを投下すべきかを判断する指針になるからです。

ステップ 1: 翻訳

システムは、ポリシーで宣言されている変数を用いて、ユーザーの質問とLLMの回答の両方に含まれる自然言語を、単なる代入ではなく、「earning >= 180 & earning <= 220」のような形式論理の述語へと変換します。このとき重要になるのが変数の説明です。

例えば、「3万米ドルの頭金で35万米ドルの住宅を購入する顧客は、従来型住宅ローンの適格要件を満たす」という回答があった場合、変換ステップでは次のように出力されます：downPaymentAmount = 30000、purchasePrice = 350000、mortgageType = CONVENTIONAL。

入力された自然言語を論理へ変換するためにLLMを使用しているという事実が、このシステムが最大99パーセントの検証精度を主張している理由です。翻訳の正確性を保証するために、私たちは1つのLLMだけに依存しているわけではありません。代わりに、異なる温度設定を持つ複数のLLMを並列で使用し、同じ翻訳を実行します。冗長な翻訳結果が意味的に等価である場合にのみ、検証結果を得ることができます。翻訳が一致しない場合は、代わりに入力の2つの解釈を含むAMBIGUOUS（曖昧）な結果を返します。LLMはこのフィードバックを利用して回答の曖昧性を解消したり、ユーザーに明確な質問をしたりすることができます。カーネギーメロン大学の条件付きQAデータセットと照合してシステムをベンチマークしたところ、システムがVALIDと判定したケースの99%以上で、そのフラグが正しいことが確認されました。方法論の詳細については、このホワイトペーパーをご覧ください。

ステップ 2: 検証

充足可能性理論付き （SMT）ソルバーは、変換された代入がすべてのポリシールールを満たしているかどうかを評価します。このステップは定義上、数学的に健全です。翻訳が正しければ、検証は証明可能に正しいものとなります。

住宅ローンの例では、ソルバーは downPaymentPercentage = (30000 / 350000) * 100 = 8.57% を計算し、この値をルール (=> (< downPaymentPercentage 20.0) (not (= mortgageType CONVENTIONAL))) と照合します。その結果、8.57 < 20 であることを確認し、mortgageType = CONVENTIONAL は論理的に無効と判断します。システムは、どのルールがどのように違反されたかを示す完全なトレース付きで、無効の結果を返します。

スタートアップビルダーにとっての実務的なポイントは何でしょうか。翻訳の品質は、より良い変数の説明によって自分たち でコントロールできるということです。一方で、検証の計算そのものについては心配する必要はありません。あなたはドメインを適切に記述することに投資し、あとはソルバーがすべてを処理します。

結果は何を意味するのか？

ARチェックは単に「合格」または「不合格」を返すだけではありません。何が起こったのか、次に何をすべきかを正確に示す構造化された所見を返します。各所見は次のいずれかの種類です：

これは重要です。 ARチェックは検出モードで動作します。検出結果とフィードバックは返されますが、応答が妨げられることはありません。アプリケーションは結果を検査して、提供するか、書き直すか、説明を求めるか、安全なデフォルトに戻すかを決定します。これにより、すべての応答を数学的に検証しながら、ユーザーエクスペリエンスを完全に制御できます。このパターンの実例として、オープンソースのリライトチャットボットの実装を参照してください。この実装では、AR の調査結果を LLM にフィードバックして自動的に修正する方法が示されています。

AgentCoreポリシー：AIエージェントの決定論的な境界

スタートアップ企業がエージェント型アプリケーションを構築している場合、つまりAIが複数ステップのワークフローを調整し、ツールを呼び出し、ユーザーに代わってアクションを実行する場合、信頼の問題は従来とは異なります。問題となるのはAIが何を言うかだけではなく、AIが何をするかです。

ヘルスケア、フィンテック、またはリーガル領域のスタートアップにおいては、「エージェントが予期しないことを行った」という説明は、コンプライアンスや規制の観点から許容されません。必要なのは、エージェントの振る舞いに対する証明可能な境界であり、その境界はプロンプトインジェクションによって操作された場合や、推論エラーを起こした場合であっても維持されなければなりません。

Amazon Bedrock AgentCoreにおけるポリシーは、ゲートウェイ境界におけるすべてのエージェントとツールのやり取りに対して強制される認可レイヤーによって、この問題を解決します。ポリシーはCedarで記述されます。CedarはAWSによって開発された認可言語であり、ARによって検証可能です。Cedarポリシーは、誰（プリンシパル）が、どのリソースに対して、どのような条件のもとで、何（アクション）を実行できるかを定義します。一致する許可がない限り、いかなるツール呼び出しもゲートウェイを通過することはできません。ポリシーはCedarで直接記述することもできますし、ルールを自然言語で記述してシステムにCedarを生成させることもできます。

ポリシーがデプロイされる前に、自動推論がセマンティック検証を実行 し、以下のような問題を検出します：

• 特定のプリンシパル／アクション／リソースの組み合わせに対して、すべてのリクエストを許可してしまう過度に緩いポリシー
• すべてを拒否してしまう過度に制約的なポリシー
• 無効なポリシー（Permitが何も許可せず、Forbidが何も禁止しないケース）

この強制（エンフォースメント）は、規制産業のスタートアップにとって特に重要な2つの原則に従います：

1. デフォルト拒否： ポリシーによって明示的に許可されていないアクションはすべてブロックされます。エージェントは、あなたが許可していないことは一切実行できません。
2. Forbidは常にPermitに優先する： 他のポリシーがどのように設定されていても、上書きされることのないハードストップルールを設定できます。

予約スケジューリングエージェントを構築しているヘルスケアスタートアップを考えてみましょう。AgentCoreポリシーを使うことで、患者が自分自身の記録のみにアクセスできること、予約の取得が営業時間内に制限されること、返金額がポリシーによって上限設定されることを強制できます。これらのルールは、エージェントへのプロンプト内容、コード内に存在するバグ、あるいはユーザーがどれだけ創造的なリクエストをしてきたとしても変わりません。これらの強制はゲートウェイ境界で行われ、エージェントの外側で完全に実行されます。

自動推論は、手動QAと比べてどのくらいコストがかかりますか？

自動推論の経済性を理解するには、現在ほとんどのチームが採用しているベースライン、つまりモデル出力に対する手動QAレビューと比較することが有用です。

古い方法:手動 QA

AIの出力をレビューする担当者は、時間あたり約50件のインタラクションを処理でき、総コストベースでは約40米ドル/時間となります。月間10万件の顧客インタラクションを扱うスタートアップの場合、すべてのインタラクションをレビューすると月額80,000米ドルのコストがかかります。10％のサンプリングに抑えたとしても月額8,000米ドルかかり、残りの90％については依然として未検証のままです。レビュー担当者1人あたりの年間コストが80,000〜150,000米ドルであることを考えると、5〜10人のチームでは年間400,000〜1,500,000米ドルになります。多くのスタートアップにとって、これはAIが正しいかどうかを確認するために費やされるかなり大きな資金です。

新しい方法：自動推論

ARチェックは検証リクエストごとに課金されます。（正確な価格はBedrockの料金ページで確認する必要があり、レートは変動する可能性があります。）手動レビューとは異なり、すべてのインタラクションをサンプリングではなくすべて検証できます。Amazon Bedrock Guardrailsでは、検証単位としてテキストユニットを使用しており、1テキストユニットは1,000文字です。以下は、典型的なスタートアップにおける例です：

想定

計算

上記の月間10万インタラクションを処理するスタートアップの例を用いると、各インタラクションの出力が約200トークンであると仮定した場合、ARチェックを検証に使用するコストを容易に見積もることができます。Amazon Bedrock Guardrailsでは使用量をテキストユニットで測定しており、1テキストユニットは1,000文字です。1トークンあたり平均4文字と仮定すると、各インタラクションは約800文字となり、したがって0.8テキストユニットとなります。

各0.8テキストユニットの100,000インタラクションを検証すると、月間合計は80,000テキストユニットになります。ARチェックの価格が1,000テキストユニットあたり0.17ドルの場合、単一ポリシーにおける月額コストは13.60米ドルとなります。複数のポリシーを適用した場合、コストは線形に増加します。それでも、複数ポリシーを適用した場合でも、総コストは手動レビューと比較して圧倒的に低く抑えられます。

コンプライアンスの観点からの計算はさらに説得力があります。HIPAA違反の1カテゴリだけでも、現在のインフレ調整後の数値では年間最大2,067,813米ドルのコストが発生する可能性があります。AIが毎日数千件の患者インタラクションを処理するヘルスケアスタートアップにとって、未検証の出力による規制リスクは存続に関わるレベルのものです。この文脈では、ARはソフトウェアのコストというよりも、リスク管理のための統制手段として機能します。

開発者にとって最も近いアナロジーは、Rustの借用チェッカーです。Rustはメモリ破損をコンパイル時に検出し、コードが本番環境に到達する前に防ぎます。ARはポリシー違反を検証時に検出し、顧客に届く前に防ぎます。問題が実害を引き起こす前に検出することは、後から修正するより常にコストが低くなります。

トレードオフとして、AR検証は各レスポンスにレイテンシを追加し、またリライトが必要な場合にはフラグが立った出力に対してLLMが2回実行されることになります。しかし多くのアプリケーションにおいては、そうしたコストは、誤った出力がもたらす運用上・法的・評判上の影響と比べればごく小さいものです。

同じ主張は投資家にも強く響きます。AIの出力が正式なビジネスポリシーに対して体系的に検証されていると言えることは、単なるプロダクト機能ではありません。それはリスクがプロアクティブに管理されていることの証明です。こうした具体的で検証可能な主張こそが、スタートアップのリスクプロファイルを強化します。

次に何が来るのか？

第 3 部「ステップバイステップの実装プレイブック」では、概念からコードへと進みます。既存のドキュメントから AR ポリシーを作成し、それをガードレールにデプロイする方法、ApplyGuardrail API と統合する方法、検出結果をプログラム的に処理する方法、AgentCore Gateway を通じて AgentCore ポリシーをセットアップする方法、監査証跡を構築する方法を学びます。数理的な検証について読む段階から、本番でのリリースまでに必要なすべてを扱います。