LLM-Assisted Formalization Enables Deterministic Detection of Statutory Inconsistency in the Internal Revenue Code

📄 arXiv: 2511.11954v1 📥 PDF

作者: Borchuluun Yadamsuren, Steven Keith Platt, Miguel Diaz

分类: cs.AI

发布日期: 2025-11-15

备注: 29 pages, 3 appendices with Prolog code and full codebase available at: https://github.com/borchuluun/section121-inconsistency-detection

💡 一句话要点

提出LLM辅助的形式化方法，用于确定性地检测美国国内税收法中的法规不一致性

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 符号逻辑 法规一致性检测 形式化方法 神经符号计算

📋 核心要点

  1. 现有基于LLM的方法在处理法律法规等长文本时，面临分层处理和深度结构化推理的挑战，尤其是在检测法规不一致性方面。
  2. 论文提出一种混合神经符号框架，结合LLM（GPT-4o/GPT-5）和符号逻辑（Prolog），将法规条文形式化为Prolog规则，辅助LLM进行推理。
  3. 实验结果表明，该方法能够确定性地检测美国国内税收法中的法规不一致性，验证了LLM辅助形式化在法规一致性检测方面的有效性。

📝 摘要（中文）

本研究介绍了一种混合神经符号框架，该框架能够确定性地检测复杂法律中的法规不一致性。我们以美国国内税收法（IRC）为例，因为其复杂性使其成为识别冲突的沃土。我们的研究通过将大型语言模型（LLM）与符号逻辑相结合，为检测不一致的条款提供了一种解决方案。基于LLM的方法可以支持合规性、公平性和法规起草，但特定于税务的应用仍然很少。一个关键的挑战是，这些模型在分层处理和深度结构化推理方面存在困难，尤其是在长文本上。本研究通过使用GPT-4o、GPT-5和Prolog的实验来解决这些差距。首先使用GPT-4o将第121条翻译成Prolog规则，并在SWISH中对其进行改进。然后将这些规则纳入提示中，以测试Prolog增强提示是否提高了GPT-4o的不一致性检测能力。GPT-4o，无论是单独使用自然语言提示还是使用Prolog增强提示，仅在三种策略中的一种中检测到不一致性（33%的准确率），但其推理质量不同：自然语言提示实现了100%的规则覆盖率，而Prolog增强提示实现了66%，表明法规分析不完整。与概率提示相反，混合Prolog模型产生了确定性和可重复的结果。在GPT-5的指导下进行改进，该模型形式化了IRC部分的竞争性解释，并成功检测到一个不一致区域。验证测试证实，Prolog实现是准确的、内部一致的、确定性的，并且能够自主识别不一致性。这些发现表明，以符号逻辑为基础的LLM辅助形式化能够实现透明且可靠的法规不一致性检测。

🔬 方法详解

问题定义：论文旨在解决复杂法律法规（如美国国内税收法IRC）中法规不一致性难以检测的问题。现有方法，特别是基于LLM的自然语言处理方法，在处理长文本、进行深度结构化推理和保证结果确定性方面存在局限性，容易出现推理错误和不一致的结果。

核心思路：论文的核心思路是将LLM的自然语言理解能力与符号逻辑的精确推理能力相结合。通过LLM将法规条文转换为形式化的Prolog规则，利用Prolog的确定性推理引擎进行一致性检测。这种混合方法旨在克服LLM在长文本推理和结果确定性方面的不足，同时利用LLM的知识获取和规则生成能力。

技术框架：整体框架包含以下几个主要阶段：1) 使用GPT-4o将IRC Section 121翻译成Prolog规则。2) 在SWISH环境中对Prolog规则进行精炼和调试。3) 将Prolog规则集成到提示中，用于增强GPT-4o的不一致性检测能力。4) 使用GPT-5指导Prolog模型的改进，形式化IRC部分的竞争性解释。5) 使用验证测试确认Prolog实现的准确性、内部一致性和确定性。

关键创新：最重要的技术创新点在于LLM辅助的形式化方法，它将LLM的自然语言处理能力与符号逻辑的确定性推理能力相结合，实现了透明且可靠的法规不一致性检测。与传统的基于规则的系统相比，该方法可以自动从自然语言法规中提取规则，降低了人工构建规则的成本。与纯粹基于LLM的方法相比，该方法能够提供更可靠和可解释的结果。

关键设计：关键设计包括：1) 使用GPT-4o进行初始的规则生成和翻译。2) 使用SWISH环境进行规则调试和验证。3) 设计合适的提示，将Prolog规则集成到LLM的推理过程中。4) 使用GPT-5进行规则改进和竞争性解释的形式化。5) 设计验证测试，评估Prolog实现的准确性、内部一致性和确定性。

📊 实验亮点

实验结果表明，GPT-4o在自然语言提示下实现了100%的规则覆盖率，但在不一致性检测方面的准确率仅为33%。而混合Prolog模型能够产生确定性和可重复的结果，成功检测到IRC部分的不一致区域。验证测试证实，Prolog实现是准确的、内部一致的、确定性的，并且能够自主识别不一致性。这些结果表明，LLM辅助的形式化方法在法规不一致性检测方面具有显著优势。

🎯 应用场景

该研究成果可应用于法律法规的合规性检查、法规草案的审查和修订，以及智能合同的验证等领域。通过自动检测法规中的不一致性，可以提高法律法规的质量，降低合规风险，并促进法律领域的智能化发展。未来，该方法可以扩展到其他领域的复杂规则系统，如金融监管、医疗指南等。

📄 摘要（原文）

This study introduces a hybrid neuro-symbolic framework that achieves deterministic detection of statutory inconsistency in complex law. We use the U.S. Internal Revenue Code (IRC) as a case study because its complexity makes it a fertile domain for identifying conflicts. Our research offers a solution for detecting inconsistent provisions by combining Large Language Models (LLMs) with symbolic logic. LLM-based methods can support compliance, fairness, and statutory drafting, yet tax-specific applications remain sparse. A key challenge is that such models struggle with hierarchical processing and deep structured reasoning, especially over long text. This research addresses these gaps through experiments using GPT-4o, GPT-5, and Prolog. GPT-4o was first used to translate Section 121 into Prolog rules and refine them in SWISH. These rules were then incorporated into prompts to test whether Prolog-augmented prompting improved GPT-4o's inconsistency detection. GPT-4o, whether prompted with natural language alone or with Prolog augmentation, detected the inconsistency in only one of three strategies (33 percent accuracy), but its reasoning quality differed: natural-language prompting achieved 100 percent rule coverage, while Prolog-augmented prompting achieved 66 percent, indicating more incomplete statutory analysis. In contrast to probabilistic prompting, the hybrid Prolog model produced deterministic and reproducible results. Guided by GPT-5 for refinement, the model formalized the IRC section's competing interpretations and successfully detected an inconsistency zone. Validation tests confirm that the Prolog implementation is accurate, internally consistent, deterministic, and capable of autonomously identifying inconsistencies. These findings show that LLM-assisted formalization, anchored in symbolic logic, enables transparent and reliable statutory inconsistency detection.