近日，一篇题为《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。