近日，一篇題為《Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries》的論文引起了廣泛關注。該論文由Alan L. McCann撰寫，提出了一種基於機器校驗的形式化方法，用於對AI工作流架構實施結構化的效果級治理。研究使用Rocq 8.19中的互動樹（Interaction Trees）定義了治理運算元G，該運算元能夠中介所有效果指令，包括記憶體訪問、外部呼叫和預言機（LLM）查詢。整個形式化開發包含36個模組、約12,000行Rocq程式碼和454個定理，且沒有引入任何未證明的引理。
論文的核心貢獻在於證明了治理與計算表達性之間的正交性。具體而言，研究者確立了七個關鍵屬性：（P1）受治理的圖靈完備性；（P2）受治理的預言機表達性；（P3）可判定性邊界，其中治理謂詞是全的且在布林組合下封閉，而語義程式屬性仍是非平凡且不可判定的；（P4）允許執行的目標保持性；（P5）原始能力（計算、記憶體、推理、外部呼叫、可觀察性）的表達最小性；（P6）包含非對稱性，表明結構治理嚴格包含內容級過濾；（P7）語義透明性，即在所有治理允許的執行中，受治理解釋與未受治理解釋在觀察上等價（僅考慮治理事件）。這些結果強有力地證明了治理和計算表達性是正交的維度：治理約束程式的效果邊界，同時對內部計算保持語義透明。
這一工作為AI系統的安全治理提供了理論基礎，使得在不犧牲計算能力的前提下，能夠對AI工作流進行細粒度的效果控制。論文的正式版本可在arXiv上獲取，編號為2605.01030。