观其果知其树：通过编码决策比较法律的形式化

将法律条款形式化有望实现机器可读的法律与自动法律推理，近期大语言模型（LLM）使得直接从法规文本生成形式化成为可能。然而，任何形式化都隐含了解释性选择，其后果难以预测，尤其是当作者为 LLM 时。本文提出一种系统方法，通过不同形式化在个别案件上的推论来比较同一法律条款的多种形式化表达。该方法在节点层面匹配形式化，推导共享接口，并利用 SAT 求解器枚举任意两种形式化存在分歧的边界案例。选定的边界案例被转化为具体事实情境，供法律专家审查。我们将此方法应用于九个前沿 LLM 生成的十个欧盟条款形式化。研究发现，形式化之间的行为差异与其结构一致性基本无关，且转化后的案例揭示了性质截然不同的分歧类型，包括反映法律评论中真实争议的分歧。