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

arXiv: https://arxiv.org/abs/2511.11954 · HTML: https://mlsanity.com/paper/2511.11954/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 25 references that are in the map.
- First posted on arXiv 15 Nov 2025.

## Builds on (most cited first, 12 of 12)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [LegalBench: A Collaboratively Built Benchmark for Measuring Legal Reasoning in Large Language Models](https://mlsanity.com/paper/2308.11462/) (2023)
- [Neural-Symbolic Computing: An Effective Methodology for Principled Integration of Machine Learning and Reasoning](https://mlsanity.com/paper/1905.06088/) (2019)
- [LawBench: Benchmarking Legal Knowledge of Large Language Models](https://mlsanity.com/paper/2309.16289/) (2023)
- [Can GPT-3 Perform Statutory Reasoning?](https://mlsanity.com/paper/2302.06100/) (2023)
- [A Dataset for Statutory Reasoning in Tax Law Entailment and Question Answering](https://mlsanity.com/paper/2005.05257/) (2020)
- [Large Language Models as Tax Attorneys: A Case Study in Legal Capabilities Emergence](https://mlsanity.com/paper/2306.07075/) (2023)
- [Towards Robust Legal Reasoning: Harnessing Logical LLMs in Law](https://mlsanity.com/paper/2502.17638/) (2025)
- [Fifty Years of Prolog and Beyond](https://mlsanity.com/paper/2201.10816/) (2022)
- [LegalLens: Leveraging LLMs for Legal Violation Identification in Unstructured Text](https://mlsanity.com/paper/2402.04335/) (2024)
- [Equitable Access to Justice: Logical LLMs Show Promise](https://mlsanity.com/paper/2410.09904/) (2024)
- [Logical Lease Litigation: Prolog and LLMs for Rental Law Compliance in New York](https://mlsanity.com/paper/2502.09204/) (2025)

## Abstract (arXiv)

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.