AIガバナンスのためのWolfram言語による計算法学の実装

本論文は、AIシステムのガバナンスを目的として、Wolfram LanguageでReified Input/Output Logic（DAPRECO知識ベースの背後にある形式論理）を実装した研究である。具体的には、I/O公理、義務、許可、構成規範、再化された事象、時間演算子を実装し、GPT-4が英語の法的文をこの形式論理に翻訳できるかをテストしている。さらに、計算契約に基づいて動作するAIガードドッグのケーススタディを通じて、形式化されたルールが契約から具現化エージェントの運用コードに直接拡張され、シンボリックで監査可能な行動の正当化を生成することを示している。最終的に、計算法律をガバナンスツールとして使用できると主張し、プログラム的に実行可能な法律を形式化することを望ましい目標としている。

先行研究では、Reified Input/Output LogicやDAPRECO知識ベースが存在するが、Wolfram Languageでの実装は新しい。また、大規模言語モデル（GPT-4）を用いて法的文を形式論理に翻訳する試みは、その失敗パターン（幻覚関数、時間スコープの省略、形式からの逸脱、コードが実行され一見妥当だが規範を誤ってエンコードするケース）を報告している点で独自性がある。さらに、形式化されたルールを具現化エージェントの運用コードに直接統合し、シンボリックな監査可能な正当化を生成するケーススタディは、実用的なガバナンス応用を示している。

手法の核心は、Reified Input/Output Logicの公理をWolfram Languageで実装することである。具体的には、I/O公理、義務、許可、構成規範、再化された事象、時間演算子をコード化する。また、GPT-4を用いて英語の法的文を形式論理に翻訳するテストでは、翻訳の失敗パターンを分析している。ケーススタディでは、AIガードドッグが計算契約の下で動作し、形式化されたルールをエージェントの行動決定に直接組み込み、シンボリックな正当化を生成する。

有効性の検証は、GPT-4による翻訳テストとケーススタディを通じて行われた。翻訳テストでは、GPT-4が法的文を形式論理に翻訳する際の失敗（幻覚関数、時間スコープの省略、形式からの逸脱、コードが実行され一見妥当だが規範を誤ってエンコードするケース）を報告している。ケーススタディでは、AIガードドッグが計算契約の下で動作し、形式化されたルールがエージェントの行動を適切に制約し、監査可能な正当化を生成することを示している。

議論としては、AIシステムの推論を完全に検査できなくても、ガバナンスにはシステムが何を義務付けられ、許可され、禁止されているかを述べ、遵守をチェックすればよいという主張がある。また、GPT-4の翻訳失敗は、大規模言語モデルを形式論理への翻訳に使用する際の課題を示している。さらに、計算法律をガバナンスツールとして使用することの可能性と、プログラム的に実行可能な法律を形式化する目標について議論している。

要旨からは、次に読むべき論文として具体的なものは挙げられていないが、関連する研究として、Reified Input/Output Logicの元となったDAPRECO知識ベースに関する論文や、Input/Output Logicの基礎を築いた研究が考えられる。また、AIガバナンスにおける形式手法の応用に関する研究も関連する。