Prove It、第 1 部: AI スタートアップにとって「おそらく正しい」だけでは不十分である理由

AI 時代に成功するスタートアップは、最先端のモデルや最大のトレーニングデータセットではなく、信頼によって定義されることになるでしょう。重要な差別化要因は、ユーザーが AI を信頼しているかどうか、「AI が間違った場合にどうなるのか?」という問いに、確率的な保証だけでなく、数学的な確実性をもって答えられるかどうかです。規制が厳しい市場では、モデルの能力だけでなく、検証の重要性が増しています。

あなたはシードラウンドを完了したばかりです。AI を利用した融資アシスタントが先週 Go Live となりました。200 名のベータユーザーがいます。3 日目、顧客がチャットボットから頭金 8% で通常の住宅ローンを組めると伝えられ、そのスクリーンショットを撮影してソーシャルメディアに投稿しました。貴社のポリシーでは頭金は 20% 必要です。

共同創業者が最初にそれを見ました。次に投資家が見ました。そして、最後に弁護士が見ました。

これは架空の話ではありません。これは 2026 年の AI 製品の構築における現実です。2 年前であれば 50 名のエンジニアが必要だった製品を、3 名のチームで提供し、アイデアから MVP までを数か月間ではなく数日間で実現しているのです。

しかし、検証を伴わないスピードは法的責任を引き起こします。生成 AI は、ハルシネーションを生成したり、自社のポリシーに矛盾したり、顧客に明らかに間違った回答を提供したりする製品を、いとも簡単に、危険なほど容易に提供できるようにしてしまいました。「提供した」ことと「信頼できるものを提供した」ことの間にあるギャップこそが、スタートアップが失敗する原因です。

根本原因は構造的なものです。大規模言語モデルは確率的なシステムです。次の可能性の高いトークンを予測することでテキストを生成します。このプロセスには、設計上ランダム性が伴います。温度、サンプリング戦略、トップ k/トップ p パラメータなど、すべてがばらつきを生み出します。同じプロンプトでも、実行ごとに異なる回答が生成されることがあります。これが LLM を創造的かつ有用なものにしている要因です。同時に、正確性が求められるタスクにおいては、根本的に信頼性に欠けるものにしている理由でもあります。お客様のモデルは、不適切な住宅ローンに関する助言をしようとしていたわけではありません。それは、次に最も可能性の高いトークンを予測していたのです。

あらゆる AI スタートアップは、このジレンマを解決しなければなりません: 確率的システムを構築しながら、顧客、規制当局、投資家に正確性の保証を提供するにはどうすればよいのでしょうか?

AI が誤った回答をした場合はどうなるのか

AI が誤ったガイダンスを提供し、顧客がそれに基づいて行動した場合、その結果についての責任はお客様にあります。ヘルスケア AI が数百件の患者とのやり取りにおいて保険適用に関する判断を誤った場合、HIPAA に基づく民事罰は、違反の重大度に応じて違反あたり 137 USD から 68,928 USD であり、最新のインフレ調整後の数値では、違反カテゴリごとの年間上限額は 2,067,813 USD に達します。問題があることに気づく前に、罰金が資金調達総額を超える可能性もあります。GDPR では、重大な違反についての罰金は、2,000 万 EUR または全世界の年間総売上高の 4% のいずれか高い方となります。EU の顧客データを処理するアーリーステージのスタートアップにとって、これは罰金ではなく、事業停止を意味します。非適格者の融資を承認するフィンテックチャットボットは、規制上の責任をもたらします。保険契約の条項を誤って引用する保険ボットは、勝ち目のない契約紛争を引き起こします。

直接的な罰以外にも、二次的なコストが発生します。すなわち、セキュリティレビューに合格できないために破談になる企業との取引、AI の意思決定プロセスを説明できないために停滞する SOC 2 監査、「AI が間違った場合どうなるのか?」と質問するシリーズ A 投資家が満足のいく回答を得られないといったケースが生じます。

プロンプトエンジニアリングと RAG だけでは不十分である理由

LLM を使用して構築するすべてのスタートアップは、同じような安全対策の仕組みを採用しています。すなわち、慎重なプロンプトエンジニアリング、検索拡張生成 (RAG)、ある程度の手動レビューです。これらは優れたプラクティスですが、同時に不十分でもあります。

プロンプトエンジニアリングはヒューリスティックであり、証明可能なものではありません。モデルが適切に動作するよう促す指示を作成しますが、モデルがそれに従う保証はありません。新しいモデルバージョンにアップグレードしたり、新しいエッジケースに対応するためにシステムプロンプトを調整したりすると、以前は安全だった動作が、気づかないうちに安全ではなくなってしまう可能性があります。つまり、強制力のない暗黙の取り決めに基づいて安全性を築いていることになります。

RAG は、取得したドキュメントに基づいてモデルを構築することで、ハルシネーションの可能性を低減します。これは確かに改善点です。しかし、モデルは依然として、取得したコンテキストを無視したり、誤って解釈したり、選択的に使用したりする可能性があります。RAG は確率分布をより良い回答の方向にシフトさせますが、誤った回答の可能性を排除するものではありません。「大抵は正しい」というのは、コンプライアンス戦略とは言えません。

手動 QA は、企業の成長に合わせてスケールしません。積極的なサンプリング (やり取りの 10% をチェック) を行っても、90% は未検証のままです。月間 10 万件の顧客とのやり取りを処理するスタートアップにとって、出力のサンプルチェックを行うレビュアーを雇うには、年間数十万 USD のコストがかかります。これは、シードステージのチームには確保できない人員であり、チェックしていない 90% については、適切であることを願うしかありません。この費用は一度きりのものではありません。顧客の質問の表現方法は時間とともに変化します。モデル自体も、お客様の知らないうちに変化します。以前は信頼できた動作も、定期的なモデル更新後に劣化する可能性があります。先月はうまく機能した慎重な指示も、来月は気づかないうちに失敗している可能性があります。QA プロセスは継続的に評価および再テストし、適応させる必要があり、一度解決すれば済む問題ではなく、常にコストがかかるものとなっています。

共通しているのは、これらのアプローチはすべてリスクを軽減するものの、確実性を提供しないということです。投資家から「AI は誤った出力を生成する可能性がありますか?」とたずねられた場合、これらのツールだけでは正直な答えは「ほとんどの場合、おそらくそうではありません」となります。しかし、それではシリーズ A の資金調達を成功させることも、規制当局を納得させることもできません。

自動推論とは

自動推論とは、システムが何を行うか、何を行わないかについての保証を提供するために数学的論理を用いるコンピュータサイエンスの分野です。データからパターンを学習する機械学習とは異なり、自動推論は、数学的論理、定理証明、制約充足を用いて、あらゆる可能な入力の無限空間において特定の特性が成り立つことを証明します。

この違いは非常に重要です。機械学習モデルが「この出力は 95% の確率で正しいです」と言う場合、それは統計的な主張です。一方、自動推論システムが「この出力は有効です」と言う場合、それは定義されたすべての制約を出力が満たすという数学的な証明を構築したことを意味します。信頼区間は存在しません。証明が存在するか、存在しないかのどちらかです。

自動推論は大規模言語モデル (LLM) の代替ではありません。チャットボットは、顧客の質問を理解し、自然な応答を生成するために、依然として言語モデルを必要とします。自動推論が提供するのは、その上に構築された検証レイヤーです。すなわち、LLM が生成し、自動推論が検証するのです。

これらが組み合わさることで、創造性と正確性が共存する完全なスタックが形成されます。AI は、会話的で、役に立ち、高速であり続けることができます。同時に、自動推論により、定義したビジネスおよびコンプライアンスの制約内にとどまることが保証されます。

AWS が自動推論を利用している方法

AWS は長年にわたって、スタートアップ (および他のすべての企業) が利用するインフラストラクチャを保護するために、本番で自動推論を利用してきました。

• Zelkovaは、AWS IAM Access Analyzer の基盤となる自動推論エンジンであり、Satisfiability Modulo Theories (SMT) ソルビングを使用して、IAM および Amazon Simple Storage Service (Amazon S3) ポリシーが意図どおりに機能することを数学的に検証し、手動レビューでは検出できない、意図しないアクセスパスを検出します
• 現在 CNCF Sandbox プロジェクトである Cedar は、自動推論で検証できるようゼロから構築された最初の認可ポリシー言語であり、Amazon Verified Permissions を支えています
• 初の形式的に検証されたクラウドハイパーバイザーである Nitro Isolation Engine は、約 26 万行の機械による検証済みの証明で Amazon Elastic Compute Cloud (Amazon EC2) のテナント分離を保証します
• AWS のオープンソース TLS ライブラリである s2n-tls は、形式的証明を用いて、その暗号化オペレーションがタイミングサイドチャネル攻撃に耐えることを検証します

スタートアップデベロッパーにとって重要なのは、Amazon Bedrock と Amazon Bedrock AgentCore を通じて利用できる数学的検証の手法は、研究プロトタイプではないということです。これらは、AWS が S3 の耐久性、EC2 の分離性、AWS サービスへのすべての TLS 接続のセキュリティを保証するために使用するのと同じエンジニアリングの専門領域に基づいています。最近まで、この専門領域にアクセスするには、形式手法の PhD 取得者で構成される社内チームを構築する必要があり、これは研究室の予算を持つ組織にのみ許された贅沢でした。Bedrock と AgentCore は、従量制料金で利用できる API コールとしてこれを実現します。

スタートアップが自動推論を活用する方法

スタートアップチームは、その同じ数学的検証の専門領域を、AI の信頼性に関する問題の異なる側面に対応する 2 つの製品を通じて直接利用できるようになりました。

Amazon Bedrock ガードレールの自動推論チェックは、SMT ベースの形式論理 (Zelkova と同じアプローチ) を使用して、LLM の出力内容がビジネスルールに準拠していることを検証します。まず、融資基準、ヘルスケアプロトコル、コンプライアンスルールなど、ビジネスに必要なポリシーを定義します。その後、システムはそれらを形式論理に変換し、あらゆる LLM 応答をこれらのルールに照らして検証します。何かがポリシーに矛盾している旨をモデルが示した場合、システムはそれを検知し、どのルールに違反したのか、およびその理由を正確に通知します。

この記事の冒頭に記載した住宅ローンのシナリオでは、システムは頭金 8% の誤りを検出し、LLM が回答をユーザーに提供する前に、その回答を書き換えるための正しい値を提案していたでしょう。

Amazon Bedrock AgentCore のポリシーは、Cedar (認可のためのオープンソースのポリシー言語) を使用して、AI エージェントのアクションに決定論的な境界を強制適用します。AI がツールを呼び出すことによって重要な意思決定を行うエージェンティックアプリケーションを構築している場合 (機密データへのアクセス、外部システムへの書き込み、ユーザーのためのアクションの実行など)、ポリシーは、ゲートウェイ境界でエージェントからツールへのあらゆるリクエストをインターセプトし、実行前に Cedar ポリシーに照らして評価します。この強制適用は決定論的です。エージェントの推論とは独立して動作し、プロンプトインジェクション、ハルシネーション、またはエージェントコードのバグによって回避されることはありません。ヘルスケア、フィンテック、または法律分野のスタートアップにとって、これは、数学的に検証されたポリシーを利用して、エージェントができることとできないことを規制当局に正確に伝えることができることを意味します。

AWS の形式手法ポートフォリオに含まれる他のシステム (Nitro Isolation Engine、s2n-tls、s2n-quic、Dafny) は、間接的にメリットをもたらします。実行するすべての EC2 インスタンスは形式的に検証された分離機構で動作し、すべての TLS 接続は形式的に検証された暗号化を使用します。AgentCore の Bedrock ガードレールおよびポリシーは、形式手法をアプリケーションコードに直接組み込む場所です。

2 つのレイヤー、1 つの原則: 確率的信頼に基づく形式的な数学的検証

このシリーズの次回の内容

これは 3 部構成シリーズの第 1 部です。「第 2 部: 形式論理、Cedar ポリシー、そして検証の経済性」では、自動推論ポリシーの仕組み、ビジネスルールがどのように形式論理となるのか、検証パイプラインがどのようなものか、数学的検証と手動 QA チームの経済性について、詳細に解説します。「第 3 部: ステップバイステップの実装プレイブック」では、Bedrock ガードレール AR チェックと AgentCore のポリシーをスタックに統合するための、本番ですぐに使用できるコードパターンを含む実践的なガイドを提供します。