面向 AI 工作流架构的效果透明治理：语义保持、表达最小性与可判定性边界

我们提出了一种在 Rocq 8.19 中进行机器验证的结构化受控 AI 工作流架构形式化，并证明了在不降低内部计算表达力的前提下，可以对效果层级进行治理。我们使用交互树（Interaction Trees）定义了一个治理算子 G，用于调解所有效果化指令，包括内存访问、外部调用以及 oracle（LLM）查询。我们的开发采用 0 个已接受引理，包含 36 个模块、约 12,000 行 Rocq 代码和 454 个定理。我们确立了七项性质：（P1）受控图灵完备性、（P2）受控 oracle 表达力、（P3）在治理谓词为全称且闭合于布尔合成的可判定性边界内，语义程序属性仍保持非平凡且不可判定、（P4）允许执行的目标保持、（P5）原始能力（计算、内存、推理、外部调用、可观测性）的表达最小性、（P6）结构化治理严格包含内容级过滤的子sumption 非对称性、以及（P7）语义透明性：在所有允许治理的执行上，受控解释与未受控解释在观察等价性（除治理唯一事件外）下保持一致。这些结果表明，治理与计算表达力是正交的两个维度：治理约束程序的效果边界，同时在内部计算语义上保持透明。