top of page
検索

なぜPhysical AIは「AIが正しい」だけでは現場に入れないのか

執筆者の写真: kanna qed
kanna qed
9月15日
読了時間: 9分

——2つの「保証の断絶」をLean 4で形式化した

AIが正しい判断をした。だから、その判断でロボットや設備を動かしてよい。この二つは、同じではありません。Physical AIが研究室から工場・物流・ロボティクスの現場へ出ていくほど、この小さく見える差が大きな問題になります。2026年、国際ロボット連盟（IFR）は、AIと自律化、ITとOTの融合、安全・セキュリティをロボティクスの主要トレンドとして挙げています。AIによる自律化によって、テスト、検証、人間による監督はむしろ複雑かつ重要になるとしています。すでに実装も始まっています。BMWの米国スパータンバーグ工場では、ヒューマノイドロボットFigure 02が10か月で3万台超のBMW X3の生産を支援し、9万個以上の部品を扱いました。BMW自身も、その経験から生産IT、労働安全、生産プロセス管理、工場内物流などを早期から巻き込む重要性を示しています。Physical AIはもう、「AIがロボットを動かせるか」という研究だけではありません。次の問いは、何を確認できたとき、そのAIに現実の仕事を任せてよいのか。です。私たちは、この問題には少なくとも二つの大きな「保証の断絶」があると考えています。


お知らせ / 背景

本記事で扱うフィジカルAIの実行制御・結果検証に関する技術群について、先日5件のPCT国際出願を行いました。あわせて、その基礎となる2つの保証課題を抽象化した数理モデルをLean 4で形式化し、オープンソースとして公開しています。🔗 プレスリリース：GhostDrift、フィジカルAIの実行・結果を検証するAIアシュアランス技術5件を国際出願



断絶1：一つずつ正しくても、つないだ全体が正しいとは限らない

例えば工場で、画像検査AI → 搬送ロボット → 加工設備 → 検査装置という工程があるとします。画像検査AIは正しい。搬送ロボットも仕様通り動く。加工設備も正しい。検査装置も正しい。では、工程全体も正しいでしょうか。必ずしもそうではありません。重要なのは、前の工程が持っていた情報のうち、次の判断に必要な違いが保持されているかです。簡単な形で書くと、現実の状態を s、後工程へ渡す情報を view(s) とします。二つの状態 s と t が、view(s) = view(t)として同じ情報に潰されてしまったとします。しかし、ある動作 a について、

  • 状態 s では実行してよい

  • 状態 t では実行してはいけない

のであれば、後工程は view(s) だけを見ても両者を区別できません。ここには根本的な限界があります。必要な区別を一度失った情報から、後工程だけで正確な判断を復元することはできない。今回公開した Physical AI Verified Composition では、この構造をLean 4で形式化しています。information_loss_impossibility では、異なる判断を必要とする二状態が同じsummaryへ写される場合、そのsummaryだけを使ってsoundかつcompleteな判断を同時に実現できないことを形式化しています。さらに postprocessing_cannot_repair_loss では、そのsummaryを後から加工しても、すでに失われた区別は回復しないことを示しています。これはPhysical AIに限らず、かなり重要な性質です。

「AIをもっと賢くすれば解決する」とは限らない

入力時点ですでに必要な情報が失われているなら、後段により高性能なAIを置いても、その情報そのものは戻ってきません。必要なのは、AIの性能を上げることだけではなく、次の判断に必要な意味を、工程をまたいで失わず渡すことです。逆に公開Leanでは、各工程の局所保証に加えて、前工程の結果を次工程の前提へ接続する明示的な条件が成立すれば、抽象モデル上、有限長の工程について保証を合成できることも形式化しています。つまり、「各装置を検証した」から「工程を検証した」へ。ここには一段別の問題があります。


断絶2：「正しい命令」と「現実に正しく終わった」は違う

もう一つの断絶は、モデルと現実の間です。AIが、「この部品をA地点へ搬送せよ」という正しい命令を生成したとします。命令は正常に送信された。ロボットからも「完了」が返ってきた。それでも、部品が今回、本当にA地点に存在することまで自動的に証明されたわけではありません。センサーの問題かもしれない。途中で対象物が落下したかもしれない。別の部品を移動したかもしれない。完了通知と物理状態が一致していないかもしれない。この問題は古くからCyber-Physical Systemsでも認識されています。ModelPlexの研究も、検証済みモデルについて成立した保証を現実の実行へ適用するには、その実行がモデルへ適合していることをランタイムで確認する必要がある、という問題を扱っています。私たちが今回公開した Physical AI Outcome Assurance では、この境界をさらに「結果を認定できるか」という観点から形式化しました。


成功と失敗が「同じ証拠」に見えたらどうなるか

ここが今回の形式化で、最も重要な部分の一つです。ある実行について、取得した証拠を e とします。もし、成功した実行履歴と成功していない実行履歴の両方が、同じ証拠 e と矛盾しないのであればどうなるでしょうか。当然ですが、e だけを見て「成功した」と断定することはできません。公開Leanでは、実際に成功と失敗が同じ粗い証拠と両立するケースを構成し、soundな認定器はその証拠について成功認定を差し控えざるを得ないこと、さらに正確な認定器が存在しないことを形式化しています。ここで面白いのは、「何も判断しない」という方法なら、安全側には倒せることです。曖昧なら全部HOLDにする。これは誤った成功認定を避けるという意味ではsoundです。しかし、それでは本当は成功している処理まで止めてしまいます。つまり問題は単なる安全性ではありません。誤って通さないことと、通してよいものを正しく通すことを、どう両立するか。Physical AIをPoCから本番運用へ持っていくには、この両方が必要になります。


そして「後からAIで解析すればいい」でも解決しない

もう一つ重要なのが、後処理です。成功した場合と失敗した場合が、取得時点ですでに同じ証拠になってしまった。その証拠を別のAIへ入れる。特徴量を増やす。別の分類器へ通す。それだけでは、本質的な情報は増えません。公開Leanの postprocessing_cannot_resolve_ambiguous_outcomes は、反対の結果を区別できなかった証拠を後処理しても、その曖昧性そのものは解消できないことを形式化しています。これは先ほどの工程間保証と、実は同じ構造を持っています。

だから重要なのは、巨大なAIモデルを後段に置くことだけではありません。判断に必要な情報を、必要な時点で取得し、失わず、実行と対応付けること。ここにPhysical AIの保証設計があります。


ただし、「必ず実行後に観測しなければならない」という話でもない

ここも重要なので明確にしておきます。私たちの形式化は、「Physical AIでは必ず実行後センサーが必要だ」と主張しているわけではありません。事前の検証と対象範囲のカバレッジによって、対象となるすべての実行について結果がすでに保証されているなら、結果を区別する追加の実行後証拠がなくても認定できる場合があります。公開Leanでも prior_coverage_can_suffice_without_distinguishing_evidence として、このケースを明示的に扱っています。重要なのは、センサーを増やすことではない。今回の実行について、その結論を言うための根拠が本当に足りているかです。


ここから「AIアシュアランス」が必要になる

この二つの断絶を並べると、Physical AIに必要なものが見えてきます。従来の中心的な問いは、「AIは正しい判断をするか」でした。Physical AIでは、その前後にも問いが必要です。その判断に必要な現実を確認できているか。確認した情報が、本当にAIの判断に使われたか。判断した時点と、実際に動く時点で条件は変わっていないか。許可した動作が、現実に実行されたか。目的の状態になったことを確認できたか。確認できていない仕事を、完了扱いして次へ渡していないか。私たちは今回、この問題を現実のPhysical AIへ落とし込む技術として、観測、判断への情報寄与、実行直前条件、物理結果、終了状態に関係する5件のPCT国際出願を行いました。重要なのは、単に「確認記録を残す」ことではありません。確認できなければ、その判断を実行・継続・完了へ進ませない。AIアシュアランスを、監査ログだけではなく、現実の状態遷移そのものへ接続することを目指しています。


Physical AI時代には、品質保証そのものが変わる

これは事故防止だけの話ではないと思っています。日本の製造業は長い間、

  • 品質

  • 安全

  • 工程管理

  • カイゼン

  • トレーサビリティ

を競争力にしてきました。しかしAIとロボットが判断し、設備が自律的につながる世界では、「ちゃんと作りました」だけではなく、「なぜこの実行を許可できたのか」「なぜこの結果を次工程へ渡せたのか」まで機械的に示せることが、新しい品質保証になる可能性があります。AIの性能競争の次に、AIへ現実の仕事を任せる条件を、どこまで検証可能にできるかという競争が来る。私たちはそこを、Physical AIにおけるAIアシュアランスの重要な技術領域だと考えています。


Lean 4で証明したこと、証明していないこと

最後に、ここは明確に分けます。今回のLean 4形式化は、特定のロボットや工場が安全であることを証明したものではありません。また、5件の国際出願そのものを証明したものでもありません。公開しているのは、

  • どのような情報損失が正確な判断を不可能にするか

  • なぜ失われた区別を後処理では回復できないか

  • どの条件なら局所保証を有限工程へ合成できるか

  • どのような証拠では実行結果を認定できないか

  • どのような条件ならモデル上の保証を対象実行へ移せるか

という、問題の数理的な骨格です。現実の設備へ適用するには、モデルと実機の対応、証拠の真正性、センサー、制御、実行環境などを別途確認する必要があります。だからこそ、「数学で証明できたこと」と「現実について言ってよいこと」を混ぜない。その境界を明示すること自体も、AIアシュアランスの一部だと考えています。


AIが「できる」と言った、その先をつくる

Physical AIによって、AIは画面の中から現実世界へ出てきます。するとAIの誤りは、文章の間違いでは終わりません。モノが動く。機械が動く。工程が進む。次のAIが、その結果を前提にさらに判断する。だから、AIが正しいかだけでは足りない。その判断を、今、現実に実行してよいのか。実行した結果を、本当に次の仕事の前提にしてよいのか。この二つの間を、検証可能にする。私たちはそこに、Physical AIをPoCから現場へ移すための重要な技術課題があると考えています。AIの「精度」を競う時代から、AIに「実行資格」を与えられるかを検証する時代へ。そのための数理と技術を、引き続きつくっていきます。


一次文献・公開資料

  1. GhostDrift Mathematical Institute, “Physical AI Verified Composition”Lean 4による、情報損失・局所保証の合成可能性に関する公開形式化。information_loss_impossibility、arbitrary_length_composition 等を収録。https://github.com/GhostDriftTheory/physical-ai-verified-composition

  2. GhostDrift Mathematical Institute, “Physical AI Outcome Assurance”Lean 4による、証拠の曖昧性、実行結果の認定可能性、事前保証と実測証拠の関係に関する公開形式化。https://github.com/GhostDriftTheory/physical-ai-outcome-assurance

  3. Stefan Mitsch and André Platzer, “ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models,” Formal Methods in System Design, 49, 33–74 (2016).検証済みモデルの保証を現実のCPS実行へ適用するためのruntime validationを扱う先行研究。https://link.springer.com/article/10.1007/s10703-016-0241-z

  4. International Federation of Robotics, “Top 5 Global Robotics Trends 2026” (2026).AI・自律化、IT/OT融合、安全・セキュリティ等を2026年の主要ロボティクストレンドとして整理。https://ifr.org/news/top-5-global-robotics-trends-2026

  5. BMW Group, “First humanoid robot introduced in Plant Leipzig” (2026).Spartanburg工場におけるFigure 02の実生産導入実績と、Physical AIの生産現場への展開についてのBMW Group一次情報。https://www.bmwgroup.com/en/news/general/2026/humanoid-robot-in-leipzig.html

  6. GhostDrift数理研究所「製造AIを、PoCから現場の実行へ。GhostDrift、フィジカルAIの実行・結果を検証するAIアシュアランス技術5件を国際出願」(2026).本記事の背景となる5件のPCT国際出願についての公式発表。https://prtimes.jp/main/html/rd/p/000000008.000182721.html




 
 
 

コメント

bottom of page