Semantic diffing of formal policies with anti-unification

本文介绍一种基于反统一（anti-unification）的语义差异分析方法，用于比较形式化策略的含义差异，而非仅关注语法变化。该开源引擎通过 e-graph 跟踪已知等价的表达式，并利用代数定律和领域规则识别等价性。在自动形式化场景中，大语言模型可能生成不同形式化版本，语义差异分析可展示其共通与分歧部分，帮助审查关键差异。