形式策略的语义差分：反合一如何把真实行为分歧从语法噪声中分离

当自动化策略生成流程把同一条自然语言需求翻译成两份形式化策略时，审查者面对的第一个问题不是哪份对，而是它们到底哪里不同。文本差异工具在这里系统性失效：交换两个合取项的顺序、把外部目的地改写为非内部、用等价谓词替换另一个，都会让大量行标记为变更，而真正改变授权行为的差异——比如把And换成Or——可能淹没在噪声中。

AWS机器学习博客介绍了一个名为semi-persistent的开源引擎，它用反合一（anti-unification）计算形式策略的语义差分。反合一来自Plotkin 1970年的经典工作，目标是找到两个表达式的最大特定公共模式。引擎在等价图（e-graph）上运行，等价图追踪已知相等的表达式，用户通过声明代数律（如合取的结合律、交换律、幂等律）和领域规则（如外部目的地等价于非内部）来告诉引擎哪些语法变化不改变含义。

引擎的输出是一个单一术语，其中共享结构只出现一次，每处分歧被标记为Variants节点，节点内保留两个候选的完整子树。选择每个Variants节点的第一子树可以重建候选A，选择第二子树可以重建候选B。这意味着反合一结果是两个输入的无损合并：不是丢弃信息，而是把相同部分折叠、把不同部分保留并定位。

博客用一个具体例子展示了这如何工作。需求是：敏感数据发往外部目的地必须加密。候选A写成sensitive(data)且external(dst)蕴含encrypted；候选B写成非internal(dst)且sensitive(data)蕴含audited。文本差异会标记条件重排、谓词改写和结论不同。引擎先报告两处分歧：一处在条件（external对非internal），一处在结论（encrypted对audited）。用户把领域事实声明为rewrite规则——external等价于非internal——饱和后重新差分，条件分歧消失，只剩结论分歧：候选B审计而需求要求加密。一个Variants节点精确指向需要审查的位置。

在更复杂的例子中，一份跨Region复制策略的两种编码有五个文本差异。三个是纯语法：合取项重排、等式参数交换、approvedRegion展开为两个具体Region。声明And为结合交换幂等、Eq为交换后，前两个被吸收；加一条领域rewrite把approvedRegion等价于两个Region的析取后，第三个也被吸收。剩余两处分歧是真实行为差异：一份编码在机密对象条款中用Or替代了And（允许加密或同账号之一即可，而非两者都要求），另一份在大小阈值上用严格小于替代了小于等于（恰好等于阈值的对象走不同路径）。语义差分把五处文本变更压缩为两处可审查的语义分歧，压缩比从0.59降到0.40。

方法有明确边界。它不证明任何候选正确：两份翻译可以犯同一个错误，共享的错误不会显示为分歧。它依赖用户声明的代数和rewrite：如果领域知识不完整，真实等价仍会残留为Variants节点。搜索本身也可能不完备——当使用默认蒙特卡洛搜索而非精确求解时，返回结果标注为budget而非exact，意味着可能还有更小的公共模式未被找到。引擎不评估策略、不查询SMT求解器、不判断哪份翻译匹配需求；它只组织信息，把审查注意力引导到真正可能改变行为的位置。

对于使用大语言模型自动生成形式化策略的团队，这个方法的实际价值在于：生成多个候选后，不需要人工逐行比对，也不需要依赖模型自身的判断。语义差分给出一个确定性的、可重复的审查起点——先看Variants节点标记的位置，用schema验证、replay、示例输入输出或人工判断来逐一解决。

引擎以Apache-2.0许可开源，需要Rust工具链构建，输入是S表达式文件。博客提供了多个可运行的策略例子，覆盖Cedar、Dogwood、OpenShell和CEL四种策略格式的候选翻译比较。