pith. sign in

arxiv: 2604.14607 · v2 · submitted 2026-04-16 · 💻 cs.AI

GDPR Auto-Formalization with AI Agents and Human Verification

Ha Thanh Nguyen , Wachara Fungwacharakorn , Sabine Wehnert , May Myo Zin , Yuntao Kong , Jieying Xue , Micha{\l} Araszkiewicz , Randy Goebel
show 1 more author
Ken Satoh
This is my paper

Pith reviewed 2026-05-10 11:09 UTC · model grok-4.3

classification 💻 cs.AI
keywords GDPRlegal formalizationAI agentshuman-in-the-loopLLMverificationdataset constructionlegal reasoning
0
0 comments X

The pith

Structured verification and targeted human oversight are essential for reliable AI formalization of GDPR provisions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper investigates automatic formalization of GDPR rules by large language models inside a human-in-the-loop framework. LLM agents in a multi-agent setup generate legal scenarios, formal rules, and atomic facts, while separate verification modules check representational, logical, and legal correctness with human reviewers. The process produces a high-quality dataset and examines both successful and problematic cases. Results indicate that legal nuance and context-sensitive reasoning make full automation unreliable without structured human input. A sympathetic reader would care because accurate formal legal representations could support compliance tools, automated reasoning, and clearer privacy regulation.

Core claim

A role-specialized multi-agent LLM workflow with iterative feedback generates legal scenarios, formal rules, and atomic facts from GDPR provisions, paired with independent verification modules that assess representational, logical, and legal correctness through human review, yielding a dataset whose analysis of cases demonstrates that structured verification and targeted human oversight remain essential for reliable legal formalization especially under legal nuance and context-sensitive reasoning.

What carries the argument

A multi-agent LLM workflow with iterative feedback for generating scenarios, rules, and facts, coupled with independent human-in-the-loop verification modules for representational, logical, and legal correctness.

If this is right

  • High-quality datasets for GDPR formalization become feasible through this hybrid generation and verification process.
  • AI agents can reliably handle initial generation of legal elements but require human checks for nuance and context.
  • Similar workflows could extend to formalizing other regulatory texts beyond GDPR.
  • Legal formalization systems must incorporate targeted oversight to handle context-sensitive reasoning.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The approach could lower the manual effort needed to build formal models for privacy compliance checking.
  • Testing the same pipeline on other data-protection laws would reveal how general the need for human oversight is.
  • Further automation of verification criteria might reduce human burden if measured against edge-case legal disputes.
  • Integration with existing legal databases could provide ground truth for scaling the dataset construction.

Load-bearing premise

LLM agents can produce scenarios, rules, and facts accurate enough that human verification is effective without becoming overly burdensome.

What would settle it

A collection of GDPR articles where formalizations approved by the human verification process later fail when checked against real legal precedents or expert legal analysis.

Figures

Figures reproduced from arXiv: 2604.14607 by Ha Thanh Nguyen, Jieying Xue, Ken Satoh, May Myo Zin, Micha{\l} Araszkiewicz, Randy Goebel, Sabine Wehnert, Wachara Fungwacharakorn, Yuntao Kong.

Figure 1
Figure 1. Figure 1: Overview of the verification-centered generation and validation pipeline. [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
read the original abstract

We study the overall process of automatic formalization of GDPR provisions using large language models, within a human-in-the-loop verification framework. Rather than aiming for full autonomy, we adopt a role-specialized workflow in which LLM-based AI components, operating in a multi-agent setting with iterative feedback, generate legal scenarios, formal rules, and atomic facts. This is coupled with independent verification modules which include human reviewers' assessment of representational, logical, and legal correctness. Using this approach, we construct a high-quality dataset to be used for GDPR auto-formalization, and analyze both successful and problematic cases. Our results show that structured verification and targeted human oversight are essential for reliable legal formalization, especially in the presence of legal nuance and context-sensitive reasoning.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript describes a role-specialized multi-agent LLM workflow for GDPR auto-formalization in which agents generate legal scenarios, formal rules, and atomic facts, followed by independent human verification modules assessing representational, logical, and legal correctness. The authors construct a dataset from this process and analyze successful and problematic cases, concluding that structured verification and targeted human oversight are essential for reliable legal formalization in the presence of legal nuance and context-sensitive reasoning.

Significance. If the central claim holds, the work would usefully illustrate the practical limits of autonomous LLM formalization in regulated domains and supply a reusable dataset plus case analysis for hybrid legal-AI pipelines. The emphasis on human-in-the-loop verification aligns with emerging needs in trustworthy AI for law. However, the absence of quantitative metrics, dataset statistics, error rates, or baseline comparisons currently limits the strength of this contribution.

major comments (2)
  1. [Abstract] Abstract and results description: the assertion that 'structured verification and targeted human oversight are essential' is not supported by any comparative evidence. No automated-only baseline, ablation study, or inter-rater reliability data is reported to show that removing the human modules measurably reduces legal correctness.
  2. [Results] The workflow description provides no quantitative metrics (dataset size, success/failure rates, error distributions) or concrete examples of how correctness was measured, leaving the necessity claim dependent on qualitative observation of nuance rather than differential performance data.
minor comments (1)
  1. Clarify the exact verification criteria and rubrics used by human reviewers; the current description of 'representational, logical, and legal correctness' is high-level and would benefit from explicit rubrics or examples.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback emphasizing the need for stronger quantitative support. We address each major comment below and have revised the manuscript to incorporate additional metrics and clarifications while preserving the focus on the hybrid workflow.

read point-by-point responses

  1. Referee: [Abstract] Abstract and results description: the assertion that 'structured verification and targeted human oversight are essential' is not supported by any comparative evidence. No automated-only baseline, ablation study, or inter-rater reliability data is reported to show that removing the human modules measurably reduces legal correctness.

    Authors: We agree that direct comparative evidence would strengthen the claim. The manuscript relies on qualitative analysis of problematic cases to illustrate where legal nuance requires human input. In the revised version, we have added inter-rater reliability statistics among human reviewers and expanded the discussion of verification outcomes. A full ablation removing all human modules was not performed in the original study, as the work centers on the hybrid pipeline; we have noted this as a limitation and included preliminary observations from automated-only runs where available. revision: partial

  2. Referee: [Results] The workflow description provides no quantitative metrics (dataset size, success/failure rates, error distributions) or concrete examples of how correctness was measured, leaving the necessity claim dependent on qualitative observation of nuance rather than differential performance data.

    Authors: We have revised the Results section to include the dataset size, success and failure rates across the three verification modules, and categorized error distributions (e.g., by type of legal ambiguity or context dependency). Concrete examples of correctness measurement are now provided, including the specific criteria and scoring used by human reviewers for representational, logical, and legal correctness. These additions make the evaluation process transparent and support the necessity of oversight with data. revision: yes

Circularity Check

0 steps flagged

No significant circularity in empirical workflow and dataset study

full rationale

The paper is an empirical workflow description and dataset construction study. It details a multi-agent LLM process for generating scenarios, rules, and facts, followed by human verification of representational, logical, and legal correctness, then analyzes the resulting dataset and problematic cases. No mathematical derivations, equations, fitted parameters, or self-referential predictions exist that could reduce outputs to inputs by construction. The claim that structured verification and human oversight are essential follows from observed patterns in the constructed data rather than any definitional loop, self-citation chain, or ansatz smuggling. Self-citations, if present, are not load-bearing for any formal result. The work is self-contained as a descriptive empirical report with no circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

This is an applied empirical study of an AI workflow for legal text processing with no mathematical or theoretical derivations, so it introduces no free parameters, axioms, or invented entities.

pith-pipeline@v0.9.0 · 5454 in / 1153 out tokens · 69577 ms · 2026-05-10T11:09:12.904910+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

  1. [1]

    Mario Alviano, Matteo Capalbo, Georg Gottlob, Irfan Kareem, Fabrizio Lo Scudo, and Sebastiano Piccolo. 2025. A Preliminary Evaluation of Open-Source LLMs for Datalog-Based Semantic Parsing in the ASVIN Project. InJoint Proceedings of the Workshops and Doctoral Consortium of the 41st International Conference on Logic Programming (ICLP-WS-DC 2025) co-locate...

    work page 2025

  2. [2]

    Mario Alviano, Lorenzo Grillo, Fabrizio Lo Scudo, and Luis Angel Rodriguez Reiners. 2025. Integrating Answer Set Programming and Large Language Models for Enhanced Structured Representation of Complex Knowledge in Natural Language. InProceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2025, Montreal, Canada, A...

    work page doi:10.24963/ijcai.2025/482 2025

  3. [3]

    Julien Breton, Mokhtar Mokhtar Billami, Max Chevalier, Ha Thanh Nguyen, Ken Satoh, Cassia Trojahn, and May Myo Zin. 2025. Leveraging LLMs for legal terms extraction with limited annotated data.Artificial Intelligence and Law(2025), 1–27

    work page 2025

  4. [4]

    Li Dong and Mirella Lapata. 2016. Language to Logical Form with Neural Attention. InProceedings of the 54th Annual Meeting of the Association for Compu- tational Linguistics, ACL 2016, August 7-12, 2016, Berlin, Germany, Volume 1: Long Papers. The Association for Computer Linguistics. doi:10.18653/V1/P16-1004

    work page doi:10.18653/v1/p16-1004 2016

  5. [5]

    Norbert E Fuchs, Kaarel Kaljurand, and Tobias Kuhn. 2008. Attempto controlled english for knowledge representation. InReasoning Web: 4th International Sum- mer School 2008, Venice, Italy, September 7-11, 2008, Tutorial Lectures. Springer, 104–124

    work page 2008

  6. [6]

    2012.The concept of law

    Herbert Lionel Adolphus Hart. 2012.The concept of law. OUP Oxford

    work page 2012

  7. [7]

    Elias Horner, Cristinel Mateis, Guido Governatori, and Agata Ciabattoni. 2025. From Legal Texts to Defeasible Deontic Logic via LLMs: A Study in Automated Semantic Analysis.arXiv preprint arXiv:2506.08899(2025)

    work page arXiv 2025

  8. [8]

    Andrew JI Jones and Marek Sergot. 1992. Deontic logic in the representation of law: Towards a methodology.Artificial Intelligence and Law1, 1 (1992), 45–64

    work page 1992

  9. [9]

    Manuj Kant, Sareh Nabi, Manav Kant, Roland Scharrer, Megan Ma, and Marzieh Nabi. 2025. Towards Robust Legal Reasoning: Harnessing Logical LLMs in Law. CoRRabs/2502.17638 (2025). arXiv:2502.17638 doi:10.48550/ARXIV.2502.17638

    work page doi:10.48550/arxiv.2502.17638 2025

  10. [10]

    Robert Kowalski. 2020. Logical English. InProceedings of Logic and Practice of Programming (LPOP)

    work page 2020

  11. [11]

    Robert Kowalski, Jacinto Dávila, and Miguel Calejo. 2022. Logical English as a Programming Language for the Law. InProceedings of Programming Languages and the Law 2022

    work page 2022

  12. [12]

    Ho-Pun Lam and Mustafa Hashmi. 2019. Enabling reasoning with LegalRuleML. Theory and Practice of Logic Programming19, 1 (2019), 1–26

    work page 2019

  13. [13]

    Le, Kenneth D

    Chen Liang, Jonathan Berant, Quoc V. Le, Kenneth D. Forbus, and Ni Lao. 2017. Neural Symbolic Machines: Learning Semantic Parsers on Freebase with Weak Supervision. InProceedings of the 55th Annual Meeting of the Association for Computational Linguistics, ACL 2017, Vancouver, Canada, July 30 - August 4, Volume 1: Long Papers, Regina Barzilay and Min-Yen K...

    work page doi:10.18653/v1/p17-1003 2017

  14. [14]

    Junnan Liu. 2025. Few-Shot Natural Language to First-Order Logic Translation via Code Generation. InProceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL 2025 - Volume 1: Long Papers, Albuquerque, New Mexico, USA, April 29 - May 4, 2025, Luis Chiruzzo,...

    work page 2025

  15. [15]

    Daniel Mendoza, Christopher Hahn, and Caroline Trippel. 2024. Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers. InFormal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, Nina Narodytska and Philipp Rümmer (Eds.). IEEE, 1–11. doi:10.34727/2024/ISBN.978-3-85448-065-5_17

    work page doi:10.34727/2024/isbn.978-3-85448-065-5_17 2024

  16. [16]

    Denis Merigoux, Nicolas Chataing, and Jonathan Protzenko. 2021. Catala: a programming language for the law.Proceedings of the ACM on Programming Languages5, ICFP (2021), 1–29

    work page 2021

  17. [17]

    Ha-Thanh Nguyen and Ken Satoh. 2026. PYTHEN: A Flexible Framework for Legal Reasoning in Python.arXiv preprint arXiv:2603.15317(2026)

    work page arXiv 2026

  18. [18]

    Donald Nute. 2001. Defeasible logic. InInternational Conference on Applications of Prolog. Springer, 151–169

    work page 2001

  19. [19]

    Monica Palmirani, Michele Martoni, Arianna Rossi, Cesare Bartolini, and Livio Robaldo. 2018. Pronto: Privacy ontology for legal reasoning. InInternational Conference on Electronic Government and the Information Systems Perspective. Springer, 139–152

    work page 2018

  20. [20]

    2013.Logical tools for modelling legal argument: a study of defeasible reasoning in law

    Henry Prakken. 2013.Logical tools for modelling legal argument: a study of defeasible reasoning in law. Vol. 32. Springer Science & Business Media

    work page 2013

  21. [21]

    Damith Premasiri, Tharindu Ranasinghe, Ruslan Mitkov, Mo El-Haj, and Ingo Frommholz. 2025. Survey on legal information extraction: current status and open challenges: D. Premasiri et al.Knowledge and Information Systems67, 12 (2025), 11287–11358

    work page 2025

  22. [22]

    Livio Robaldo, Cesare Bartolini, Monica Palmirani, Arianna Rossi, Michele Mar- toni, and Gabriele Lenzini. 2020. Formalizing GDPR provisions in reified I/O logic: the DAPRECO knowledge base.Journal of Logic, Language and Information 29, 4 (2020), 401–449

    work page 2020

  23. [23]

    Ken Satoh, Kento Asai, Takamune Kogawa, Masahiro Kubota, Megumi Naka- mura, Yoshiaki Nishigai, Kei Shirakawa, and Chiaki Takano. 2010. PROLEG: an implementation of the presupposed ultimate fact theory of Japanese civil code by PROLOG technology. InJSAI international symposium on artificial intelligence. Springer, 153–164

    work page 2010

  24. [24]

    Sergot, Fariba Sadri, Robert A

    Marek J. Sergot, Fariba Sadri, Robert A. Kowalski, Frank Kriwaczek, Peter Ham- mond, and H Terese Cory. 1986. The British Nationality Act as a logic program. Commun. ACM29, 5 (April 1986), 370–386

    work page 1986

  25. [25]

    David M Sherman. 1987. A Prolog model of the income tax act of Canada. In Proceedings of the 1st international conference on Artificial intelligence and law. New York, NY, USA, 127–136

    work page 1987

  26. [26]

    Georg Henrik Von Wright. 1951. Deontic logic.Mind60, 237 (1951), 1–15

    work page 1951

  27. [27]

    Adam Wyner. 2015. From the language of legislation to executable logic programs. InLogic in the theory and practice of lawmaking. Springer, 409–434

    work page 2015

  28. [28]

    Yuan Yang, Siheng Xiong, Ali Payani, Ehsan Shareghi, and Faramarz Fekri

    work page

  29. [29]

    Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation. InProceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2024, Bangkok, Thailand, August 11-16, 2024, Lun-Wei Ku, Andre Martins, and Vivek Srikumar (Eds.). Association for Computational Linguist...

    work page doi:10.18653/v1/2024.acl-long.375 2024

  30. [30]

    Zelle and Raymond J

    John M. Zelle and Raymond J. Mooney. 1996. Learning to Parse Database Queries Using Inductive Logic Programming. InProceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, AAAI 96, IAAI 96, Portland, Oregon, USA, August 4-8, 1996, Volume 2, William J. Clancey and...

    work page 1996

  31. [31]

    Zettlemoyer and Michael Collins

    Luke S. Zettlemoyer and Michael Collins. 2005. Learning to Map Sentences to Logical Form: Structured Classification with Probabilistic Categorial Gram- mars. InUAI ’05, Proceedings of the 21st Conference in Uncertainty in Ar- tificial Intelligence, Edinburgh, Scotland, July 26-29, 2005. AUAI Press, 658–

    work page 2005

  32. [32]

    https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_ id=1209&proceeding_id=21

    work page

  33. [33]

    Good Cases

    May-Myo Zin, Sabine Wehnert, Yuntao Kong, Ha-Thanh Nguyen, Wachara Fungwacharakorn, Jieying Xue, Michał Araszkiewicz, Randy Goebel, Ken Satoh, and Le-Minh Nguyen. 2026. Can Legislation Be Made Machine-Readable in PROLEG?arXiv preprint arXiv:2601.01477(2026). Nguyen Ha Thanh et al. A Human Verification and Detailed Findings The human verification stage was...

    work page arXiv 2026