私は数理論理学、AI検証、大規模システム設計の交差点で仕事をしています。核となる主張はこうです:AIが意思決定を担うようになった領域——都市、政府、自律型マルチエージェントシステム——には、監査人が企業の帳簿を検査するように、AIの出力を検証する独立した検証可能なレイヤーが必要だ、ということです。
私のバックグラウンドは数理論理学と意味論的プログラミングです——Gandy 型不動点定理、P = L 問題、形式体系の多項式計算可能表現などを研究してきました。そこから応用AIインフラへと歩みを進め、大規模言語モデルと形式論理を組み合わせた信頼できるAIの手法、そしてその手法を実装した検証エンジン ENIGMA Axiom を開発しています。
現在は、ドバイの IAIC FZCO を通じて、リスクの高いAIを構築する組織に助言するとともに、信頼できるAIをテーマに研究コミュニティを結集する会議(MathAI、SmartCity、IAIC イベント)や編集・出版イニシアチブを主宰しています。
P = L、Gandy 不動点定理の多項式的類似、多項式計算可能表現。
LLM と形式論理体系の統合。モデル出力の形式的+事実的検証(ENIGMA Axiom)。
仮想都市、デジタルツイン、都市規模の自律AI社会。
タスクベース認知アーキテクチャ。AI+検証可能な記録による行政効率化とシビックインテリジェンス。