AI時代の本当のインフラは何か――内閣府AX構想と形式検証

kanna qed

13 分前

読了時間: 7分

2026年10月26日、内閣府の人工知能戦略専門調査会（第7回）は、「信頼できるAIで社会全体を駆動するAX（AIトランスフォーメーション）」を議論した。[1]資料が扱うのは、AIを導入する方法だけではない。AIが行政手続を進め、企業間で判断し、現実の設備や物流を動かすとき、何を根拠に、その判断を採用し、実行させてよいのかという問題である。ここで、AI時代のインフラについて見方を変える必要がある。AIは新しいインフラである。しかし、AIを信頼して動かすための基盤は、AIの高度化だけでは完成しない。 その中核を担い得るのが、従来から存在する「形式検証（Formal Verification）」である。そして重要なのは、AIが形式検証を置き換えるのではなく、AIの進化によって、形式検証をより広範な業務で利用できる可能性が開かれ始めていることだ。

1. 何が変わったのか――AIが形式検証の利用障壁を下げる

形式検証は、システムや判断規則が、明示された条件のもとで必要な性質を満たすことを、数学的・論理的に確かめる技術である。AI以前から、ソフトウェアやハードウェアの信頼性確保に活用されてきた。問題は、現実の業務要件を厳密な仕様に落とし込み、証明や検査につなげるまでに、高い専門性と労力が必要だったことだ。この状況に変化が生まれている。

ACL 2025 の研究は、自然言語の要求から形式仕様・検証可能な証明へ至る過程を分解し、複数の形式言語でLLMの能力と限界を評価した。[2]
Microsoft Research は、検証済みRustシステムから抽出した849件の証明課題でAIエージェントを評価し、最良の組合せが80％超を完了したと報告した。これは特定のベンチマークにおける結果であり、あらゆる実務の証明を自動化できたという意味ではない。[3]
Google DeepMindのAlphaProof は、Leanによる検証可能な環境を使い、高度な数学的証明を探索する能力を示した。[4]
ICML 2025のAlphaVerus は、検証器のフィードバックを使ってプログラムを改善し、形式的に検証されたコードを生成する手法を報告した。[5]

これらが示すのは、「AIが数学的な正しさの最終判定者になった」ということではない。AIが仕様化・証明探索・コード生成を支援し、独立した検証器が定められた性質の成立を確認するという分業が現実の研究課題として進んでいる、ということだ。AIが形式検証を不要にするのではない。形式検証の利用可能性を、AIが押し広げようとしている。

2. 内閣府AX構想は、実行前の適合性判定を求めている

今回の内閣府資料で特に注目したいのは、資料P.40の「法令AX」である。[1]そこでは、法令や審査基準をAI・情報システムが利用できるよう Rules as Code として整備し、AIが行政手続を行う前に法的適合性を判定する仕組みが示されている。例えば、AIが補助金の申請を支援する場合を考えよう。AIが「要件を満たすと思う」と答えるだけでは足りない。適用する規則は何か。必要な証拠はあるか。誰が申請を承認したか。許された範囲を超える処理ではないか。こうした問いに答えなければ、AIの提案を実際の手続に移せない。さらに資料P.39・P.42では判断過程の検証可能性と人・AIの責任分担、P.56ではID・権限管理・API・電子署名・監査ログ等を含む実行基盤が議論されている。[1]ここは慎重に区別したい。Rules as Code、通常の条件判定、形式検証は同義ではない。 ルールをコード化しても、そのルールに矛盾や抜け道がないことまで証明されるわけではない。また、内閣府が形式検証や特定の民間技術の採用を決定したわけではない。 ただし政府が提示した「実行前に条件を確かめる」という課題に対して、形式検証が貢献し得ることは明確である。

3. 「生成→検証→実行」が、次のアーキテクチャになる

AIが自律的に外部ツールを使う時代には、従来の「AIが生成したら実行する」という構成そのものを見直す必要がある。ACMの専門誌 Communications of the ACM に掲載されたErik Meijer氏の論考「Guardians of the Agents」は、AIが生成したワークフローを実行前に形式的に検証するという設計を提案している。[6] これは実運用全般での安全性を実証した研究ではなく、重要なアーキテクチャ上の提案である。その基本構図は、次のように整理できる。人間 → AI → 形式検証・証拠検査 → 実行許可 → 実行・記録

人間は、目的、守るべき条件、責任、権限を定める。
AIは、複雑な要求を整理し、仕様・計画・行動の候補を生成する。
形式検証は、判断規則やワークフローが必要な性質を満たすか、明示した前提のもとで確かめる。
証拠検査・実行制御は、個別の事実、承認、権限、有効期限、実行内容を確認し、満たされなければ実行させない。
実行後の記録は、何を根拠に許可し、実際に何が起きたのかを追跡可能にする。

この区別は理論だけの話ではない。Amazonが開発した認可ポリシー言語 Cedar は、Leanで言語設計上の重要な性質を証明し、実際の認可判断に用いる仕組みとして実装されている。[7] もっとも、個々の認可判定のたびにLeanで定理証明を実行するわけではない。検証された規則と、実行時の判定を適切につなぐことが重要なのだ。ここには、決定的な違いがある。「AIが正しそうだと言った」ことと、「定められた条件を満たしたので実行してよい」ことは別である。

4. フィジカルインターネットでは、すでに同じ問題が見えている

この構図は、先日公開した記事「『つながる物流』から『任せられる物流』へ――フィジカルインターネットに形式検証・AI・責任OSが必要な理由」でも述べた。[8]複数企業が物流網を共有するとき、AIは配送計画を最適化できる。しかし、その計画が効率的であっても、すべての参加企業が受け入れられるとは限らない。納品時間は守られるか。混載条件は満たされるか。必要な承認はそろっているか。計画変更後に古い許可が使われていないか。これらは、最適化の点数とは別に守らなければならない条件である。形式検証を用いれば、例えば「必要な承認がなければ参加を許可しない」「失効した承認では実行できない」といった判断規則の性質を確認できる。個々の配送計画については、現実の証拠とその時点の条件を別途検査する必要がある。異なる企業の条件を同一にするのではなく、異なる条件が守られたことを共通の方法で検証する。 これが、企業間の協調を「つながる」段階から「任せられる」段階へ進める鍵になる。内閣府資料P.57でも、2027年度予算要求に関連する取組として、造船・物流交通領域におけるフィジカルAIの安全性評価手法の確立が挙げられている。[1] これは政策上の接点を示すものであり、予算の成立や形式検証の採用を意味しない。

5. 形式検証を、AI時代の「信頼のインフラ」に

もちろん、形式検証だけで現実世界の安全性がすべて証明できるわけではない。証明する仕様が実際の要求を正しく表しているか。センサーや帳票の証拠は真正か。検証済みの判断と実際に動くシステムが一致しているか。条件が変わったとき再検査できるか。これらは別途、技術と運用で扱わなければならない。それでも、AIの判断能力が向上するほど、その判断を、どの条件で社会が採用してよいかを検証する仕組みの価値は高まる。私たち株式会社AIアシュアランスは、形式検証を中核として、判断の採用条件、証拠、実行許可、責任記録を接続する技術を開発している。また、広島AIアシュアランス協議会（HAAC）では、広島AIプロセスの理念を、第三者が確認できる具体的な採用条件と証拠につなぐ Hiroshima AI Assurance Protocol（HAAP） を民間から提案している。これは政府やG7による公式な技術指定・認証ではない。目指すのは、AIモデルを一つに統一することではない。異なるAI、企業、業務規則が共存しても、判断の採用・実行条件を検証できる共通の方法を整えることである。現時点で公開PoCや形式モデルが示すのは、定義された条件・検証範囲における成立性であり、あらゆる実運用の安全性ではない。だからこそ、検証対象、証拠の範囲、未解決事項を明示する必要がある。

おわりに

「AIを社会のインフラにする」という言葉だけでは、肝心な問いが残る。そのAIの判断を、何に基づいて信頼し、誰が許可し、どこまで実行させるのか。形式検証は、この問いに答えるための重要な基盤技術である。そしてAIの進歩は、かつて専門家の限られた領域に閉じがちだった形式検証を、より広い産業で使うための条件を変え始めている。AIが進化したから形式検証が不要になるのではない。AIが進化したからこそ、形式検証を社会の広い領域で使える可能性が生まれている。次の競争力を決めるのは、AIをどれだけ賢くできるかだけではない。そのAIに、どこまでの仕事を、どのような根拠で信頼して任せられるかである。