用大模型+逻辑编程，精准发现税法条文中的矛盾之处。
LLM-Assisted Formalization Enables Deterministic Detection of Statutory Inconsistency in the Internal Revenue Code
- 结合大模型与逻辑编程，将税法条文转化为可验证规则。
- 在3种策略中仅1种准确识别矛盾（33%正确率），但结果可复现。
- 适合法律科技、政策分析者，提升法规一致性审查效率。
本研究提出一种混合神经符号框架，实现对复杂法律条文的确定性不一致检测。以美国《国内税收法典》（IRC）为案例，因其结构复杂，是发现冲突的理想领域。通过结合大型语言模型（LLM）与符号逻辑，解决传统模型在层次化处理和深层结构推理上的不足。实验使用GPT-4o、GPT-5与Prolog进行验证：先由GPT-4o将第121节转换为Prolog规则，并在SWISH中优化；再以这些规则增强提示，测试其对不一致检测的影响。结果显示，无论采用自然语言或带Prolog增强的提示，GPT-4o仅在三种策略中正确识别一次（33%准确率），但自然语言提示达100%规则覆盖，而增强提示仅66%，表明分析更不完整。相比之下，混合式Prolog模型产生确定且可复现的结果。经由GPT-5引导优化后，模型成功形式化了竞争性解释并识别出不一致区域。验证表明，该实现准确、内部一致、确定且能自主发现矛盾。研究证明，基于符号逻辑的大模型辅助形式化方法，可实现透明可靠的法定不一致检测。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。