Implementing Computational Law in Wolfram Language for the Governance of Artificial Intelligence

技術要約：人工知能のガバナンスに向けた、Wolfram言語における計算論的法の実装

問題提起
本論文は、内部的な推論プロセスが不透明な（「ブラックボックス」である）人工知能システムをいかに統治するかという課題に取り組んでいる。従来の解釈可能性に関する研究は、AIが「なぜ」特定の結論に至ったのかを理解することを目指しているが、著者は、効果的なガバナンスには推論プロセスそのものを理解する必要はないと主張する。代わりに、ガバナンスには、システムが何を義務付けられ、何を許可され、何を禁止されているかを明示的に記述し、コンプライアンスを検証することが必要である。

核心的な困難は、法の媒体にある。人間の言語は本質的に曖昧で、情報の欠落があり、文脈依存的であり、機械による直接実行には適していない。大規模言語モデル（LLM）は法的テキストを流暢に読み書きできるが、それらは人間特有の曖昧さを継承したまま、不透明に解釈を行う。本論文は、計算論的法（法的推論を実行可能なコードへと形式化すること）が、この曖昧さを回避する経路を提供すると仮定している。これにより、AIシステムは法を「解釈」するのではなく、法を直接「実行」することが可能になる。

手法
本論文は、体系的な評価研究ではなく、探索的な実装研究である。以下の3つのアプローチを採用している。

1. 形式化の実装： 著者は、DAPRECO知識ベースの背後にある形式論である「再帰的入出力（Reified I/O）論理」をWolfram言語内で実装した。この実装は以下を網羅している：

   • I/Oペア： ノルム（規範）を書き換えルール（入力 $\to$ 出力）として表現する。
   • 公理： 古典的な義務論理に見られるパラドックスを扱うための、入力の強化（SI）、出力の弱体化（WO）、出力の結合（AND）、入力の選言（OR）、および集約的累積的推移性（ACT）といった論理演算の実装。
   • ノルムの型： 規制的ノルム（義務と許可）と構成的ノルム（「署名された契約」$\to$「従業員である」といった制度的事実を定義するもの）の区別。
   • 再帰化（Reification）： 抽象的なイベントや状態を記号的なオブジェクト（例：Transfer["Alice", "Book", "Bob"]）に変換することで、再帰的な構成と構造的検査を可能にする。
   • 時間演算子： 時間的スコープを扱うための再帰的時間演算子（RexistAtTime）の実装。
   • ABox/TBoxの分離： 知識表現を管理するために、原子的事実（ABox）と定義およびルール（TBox）を分離する。

2. LLM翻訳実験： 著者は、GPT-4（2024年1月版）が英語の法的記述を、実装されたWolfram言語の形式へと翻訳できるかどうかをテストした。モデルにはコードのフレームワークと公理が提供され、4つの異なる法的記述の翻訳を依頼した。出力されたコードは実行され、意図した論理に照らして手動で検証された。

3. ケーススタディ（Fluffy）： 「計算論的契約」の下で動作するAIエージェント（ロボットの警備犬「Fluffy」）のデモンストレーション。この契約は独立した文書ではなく、エージェントの動作コードに直接組み込まれている。エージェントのセンサーデータ（カメラ映像、距離計算など）は、記号的なルールに直接入力され、その行動に対する監査可能な記号的根拠（例：Obligation[Stop]、Permission[UseTaser]）を生み出す。

主な貢献

1. Reified I/ologyのWolfram実装： 法的ノルム、再帰的な出来事、および時間演算子をどのように表現・操作できるかを示す、DAPRECO形式論の動作する実装。
2. LLMの失敗モードのカタログ： 法的テキストをコードへと翻訳する際のGPT-4の失敗に関する詳細な報告。本研究では、4つの具体的な失敗パターンを特定した：
   • 関数の幻覚（Hallucinated Functions）： モデルが存在しないAPI関数を捏造する。
   • 時間の欠落（Temporal Omission）： 明示的にプロンプトを与えない限り、必要な時間的スコープを含めることに失敗する。
   • 形式論の逸脱（Formalism Drift）： モデルが特定の論理形式を放棄し、一般的なプログラミングパターンへと回帰する。
   • サイレントな意味論的エラー（Silent Semantic Errors）： 最も重大な失敗モード。コードはエラーなく実行され、一見もっともらしく見えるが、誤ったノルムをエンコードしている（例：表面距離ではなく3D距離をチェックしている、あるいは義務を適用する対象を間違えている）。これらのエラーは、判別能力のないテストケースに対しては「正しい」出力を生成するため、初期の人間によるレビューを通過してしまうことが多い。
3. Fluffyケーススタディ： 計算論的契約がエージェントの動作コードに直接拡張できることを示す概念実証であり、法的テキストと機械の挙動の間の溝を埋めつつ、記号的な監査証跡を生み出すものである。
4. ガバナンスの枠組み： 「AIのガバナンス（機械の挙動を制御すること）」と「AIにおけるガバナンス（人間の開発者を制御すること）」の概念的な区別を行い、計算論的法が前者に対するツールであることを主張している。

結果

• 実装： Wolfram言語は、複雑な選言、再帰的な否定、入れ子になった義務を含む、Reified I/ologyの形式的要件を正常に処理した。しかし、著者は、完全な形式化の結果（例：「金髪か、さもなくば結んでいるか」のルール）は非常に複雑になり、法務実務家にとって読解不能になることを指摘しており、人間の言語と形式論理の間の隔たりを浮き彫りにしている。
• LLMの性能： GPT-4は、候補となるコードを迅速に生成する能力を示し、修正に対しても良好に反応した。しかし、自律的な形式化エージェントとしては機能しなかった。翻訳された4つの記述のうち3つにサイレントな意味論的エラーが含まれており、これらは本論文の作成過程で初めて検出された。本研究は、LLMは候補を生成するための「生産性ツール」としては有効であるが、実行可能なテストケースを用いた厳格な人間による検証が必要であると結論付けている。
• ケーススタディ： Fluffyエージェントは、リアルタイムのセンサーデータに基づいてルールを正常に実行し、様々なシナリオに対して正しい義務論的出力（義務/許可）を生成した。しかし、本研究では、エージェントを検証するために使用された「テストハーネス」自体にバグが含まれていたことも明らかになり、検証レイヤー自体も精査されなければならないという知見を補強した。

意義と主張
本論文は、計算論的法が「AIにおけるガバナンス（人間の開発者を規制すること）」ではなく、「AIのガバナンス（機械の挙動を制御すること）」のための実行可能な技術的ルートであることを主張している。

• 監査可能な正当化： ルールをコードに直接組み込むことで、AIシステムは自身の行動に対して記号的で監査可能な正当性を提示できるようになり、不透明な「ブラックボックス」の決定を、透明な規範的記録へと置き換えることができる。
• 執行メカニズム： 機械に対する執行は、物理的な罰則ではなく、エネルギー（電気）や情報（計算予算、データアクセス）の制御を通じて達成できると示唆している。計算論的契約は、運用の挙動を経済的ペナルティ（例：低評価による計算リソースの制限）に直接結びつけることができる。
• 形式化の限界： 著者は、すべての法を形式化することが目的ではないと明言している。「合理的である」「善意に基づく」といった多くの法的概念は、形式化を拒む「開かれた質感（open texture）」を持っている。目的は、「形式化が可能であり、プログラムとして実行可能であるべき法」、例えば税制、金融コンプライアンス、安全性が極めて重要な機械操作などを形式化することである。
• パイプライン・アプローチ： 本論文は、LLMが翻訳案をドラフトし、形式システムがそれを検証し、人間が裁定するという分業を提案している。サイレントな意味論的エラーのリスクから、LLMを自律的な形式化ツールとして扱うことは否定している。

本論文は、技術的な仕組みとしての実行可能な法は存在するものの、その展開への道筋には、技術的課題（衝突解決、検証済みライブラリ）、法的課題（コードベースの法に関する基準）、および制度的課題（実行可能な契約に対する規制上の承認）を解決する必要があると結論付けている。最終的な目標は、人間の判断を置き換えることではなく、規制とイノベーションのバランスを機械の速度で維持できるほど鋭いツールを提供することである。