通过他们的成果，你就会了解他们：通过他们编码的决定来比较法律的形式化

形式化的法律条款有望实现机器可访问的法律和自动法律推理，而最近的 LLM 使得直接从法定文本生成此类形式化变得很有吸引力。然而，任何形式化都会产生隐含的解释选择，其后果很难预测，特别是如果 LLM 是作者的话。我们提出了一种通过对个案的推论来系统地比较同一法律条款的不同形式的方法。给定一个规定的多个形式化，我们在节点级别匹配它们，从匹配中为每对派生一个共享接口，并使用 SAT 求解器枚举任何两个形式化不一致的边缘情况。然后将选定的边缘案例表述为具体的事实场景，供法律专家检查并采取行动。我们将我们的方法应用于由九个前沿 LLM 生成的十个欧盟条款的形式化。我们发现，形式化之间的行为分歧本质上与其结构一致性无关，并且口头案例揭示了性质上不同类型的分歧，包括反映法律评论中真正争议的分歧。