A Neuro-Symbolic Framework for Accountability in Public-Sector AI

This thesis proposes a neuro-symbolic framework that integrates a statutory ontology, rule extraction, and solver-based reasoning to ensure automated eligibility decisions for CalFresh align with legal rules, thereby enabling traceable and contestable procedural accountability.

The Gist

Imagine a government office that decides who gets food assistance. When they say "no" to an applicant, they send a letter explaining why. Usually, these letters are written in confusing legal jargon. The applicant reads it, thinks, "That sounds reasonable," but they can't actually check if the government is following the rules correctly. They are stuck trusting the letter because they don't have the legal tools to verify it.

This paper proposes a new "digital referee" to check those letters. Here is how it works, broken down into simple concepts:

The Problem: The "Black Box" of Bureaucracy

Think of the government's decision-making process as a black box. You put your information in, and a decision comes out. Sometimes, the box is a computer program; sometimes, it's a human following a complex rulebook. The problem is that the "explanation letter" sent to you might look good on the surface, but it could be secretly breaking the rules.

Currently, we rely on "interpretability"—trying to make the computer's thinking visible. But the authors argue that in a legal setting, just seeing the thinking isn't enough. You need auditability. You need to know if the explanation actually matches the law, like checking if a receipt matches the items you bought.

The Solution: A "Translator" and a "Rule Checker"

The authors built a system called a Neuro-Symbolic Framework. You can think of this as a two-person team working together:

1. The Translator (The "Neural" Part):
   Imagine a super-smart robot that reads the messy, complex government laws (written in English) and the messy explanation letters sent to applicants. This robot's job is to translate that human language into a strict, mathematical language that computers can understand perfectly. It's like a translator turning a poem into a precise set of math equations.

   • In the paper: They used a Large Language Model (LLM) to turn laws like "You must earn less than $2,000" into a formal rule: If Income > 2000, Then Not Eligible.

2. The Rule Checker (The "Symbolic" Part):
   Once the laws and the explanation letters are turned into math equations, a strict logic machine (called an SMT solver) steps in. This machine doesn't guess; it calculates. It asks: "Does the explanation letter mathematically prove the decision?"

   • If the letter says, "You are denied because you earn too much," and the math shows you do earn too much, the machine says SAT (Satisfiable/Valid). The explanation holds up.
   • If the letter says, "You are denied because you earn too much," but the math shows you don't earn too much, the machine says UNSAT (Unsatisfiable/Invalid). The explanation is a lie or a mistake, even if it sounds plausible to a human.

The Real-World Test: CalFresh

The team tested this system on CalFresh, California's food assistance program. They took 50 real cases where people had their benefits denied or cut.

• The Setup: They fed the system the actual law, the applicant's facts (income, family size), and the official letter the government sent.
• The Result: The system successfully found "legal mismatches." In one test, they tricked the system by changing a "Denied" decision to "Approved" but kept the same explanation (which said the person earned too much). The system immediately screamed UNSAT, pointing out that the explanation contradicted the new decision.
• The "Smoking Gun": When the system found a mistake, it didn't just say "Error." It pointed to the exact page and paragraph of the law that was violated. It's like a referee not only blowing the whistle but pointing to the specific rulebook page the player broke.

Why This Matters

The authors argue that we need to stop trying to just "explain" how AI thinks and start auditing the legal justifications it produces.

• Current Way: "Here is why the computer said no. It's based on a pattern it learned." (This is hard to fight in court).
• New Way: "Here is the letter. Our system checked it against the law and found it violates Section 63-409.111." (This is easy to fight in court).

The Bottom Line

This paper doesn't claim to replace the government or make the final decisions. Instead, it builds a digital safety net. It ensures that when the government sends you a letter saying "No," that letter is actually a valid legal reason, not just a confusing excuse. It turns the "explanation" from a piece of paper you have to trust, into a piece of evidence you can verify.

Key Takeaway: In the world of public benefits, an explanation isn't just about being clear; it's about being legally true. This system is the tool that checks if the truth is actually being told.

Technical Summary

Technical Summary: A Neuro-Symbolic Framework for Legal Accountability in Public-Sector AI

1. Problem Statement

Public agencies increasingly rely on automated decision-making (ADM) systems to govern access to welfare benefits. While these systems promise efficiency, they often lack transparency, making it difficult for applicants to understand or challenge eligibility determinations. Current approaches to Explainable AI (XAI) focus on model interpretability, fidelity, or user trust. However, in legal and administrative contexts, an explanation's primary function is not merely to be understood, but to serve as a legal justification that can be contested in adversarial or quasi-judicial settings.

The core problem identified is that existing explanations (e.g., Notices of Action) may appear plausible to human readers yet fail to reference the correct legal authority or misstate statutory conditions. There is a lack of technical infrastructure to verify whether these justificatory artifacts are legally valid against governing statutes. Current auditing methods often focus on decision-level compliance or model behavior, neglecting the legal integrity of the explanations themselves. This gap prevents applicants and oversight bodies from effectively assessing whether a decision satisfies statutory criteria and procedural norms.

2. Methodology

The authors propose a neuro-symbolic framework designed to automatically verify the legal adequacy of welfare eligibility explanations. The system shifts the focus from interpreting model internals to auditing the justifications provided to applicants. The architecture consists of four primary stages:

2.1 Data Sources

• Statutory Corpus: The California Manual of Policies and Procedures (MPP) Division 63, governing the CalFresh (SNAP) program.
• Case Data: 50 administrative appeal decisions from the California Department of Social Services (CDSS) State Hearings Division. These records include the agency's original explanation, the determination outcome, and the factual circumstances presented by the claimant.

2.2 System Architecture

The framework operates through a pipeline that separates legal rules from case-specific assertions:

1. Ontology Construction:

   • A controlled legal vocabulary is derived from the MPP regulations using Named Entity Recognition (NER) and embedding-based similarity matching (using Qwen3-Embedding-8B).
   • The ontology targets core eligibility dimensions: income, residency, citizenship, resources, and student status.
   • This structure ensures traceability to authoritative sources and prevents redundancy.

2. TBox (Terminological Box) Encoding:

   • Represents the normative structure of the law (case-invariant rules).
   • Statutory provisions are segmented, and operative terms are extracted.
   • A Large Language Model (LLM), specifically OpenAI's o1, is prompted to translate these provisions into formal, solver-ready logical rules (e.g., implications, necessary conditions).
   • Each rule is linked to its source citation (e.g., MPP §63-409.111).

3. ABox (Assertion Box) Construction:

   • Represents case-level content (facts and explanatory claims).
   • The agency's explanation is translated into the same logical format as the TBox using the LLM.
   • Factual predicates (e.g., household size, income amounts) are extracted from the hearing records.
   • The ABox combines the retrieved TBox rules invoked by the explanation, the translated explanation logic, and the specific case facts.

4. SMT-Based Verification:

   • A Satisfiability Modulo Theories (SMT) solver evaluates the joint satisfiability of the TBox (legal rules) and the ABox (case assertions).
   • SAT Outcome: The explanation is coherent with the governing law and can function as a legally admissible justification.
   • UNSAT Outcome: The explanation is inconsistent with the law. The solver extracts an unsatisfiable core—a minimal subset of constraints responsible for the conflict—and maps them back to specific statutory provisions.

3. Key Contributions

• Shift from Interpretability to Auditability: The paper argues for a paradigm shift where public algorithmic accountability is measured by the legal validity of explanations rather than just model interpretability.
• Neuro-Symbolic Verification Pipeline: A novel integration where neural components (LLMs) handle the extraction and translation of unstructured legal text and explanations, while symbolic components (SMT solvers) provide deterministic verification and traceability.
• Explanation-Level Accountability: Unlike previous work that formalized screening tools (e.g., Escher and Banovic, 2020), this framework evaluates the justificatory artifacts (notices of action) issued to applicants, supporting rights to contest and appeal.
• Statute-Grounded Signals: The system does not merely flag errors; it produces actionable accountability signals by identifying exactly which statutory provisions are violated by an explanation.

4. Results

The framework was evaluated on 50 CalFresh cases across five eligibility categories (Student Status, Income, Residency, Citizenship, Resources). For evaluation, the authors created paired instances by inverting the eligibility determination while keeping the explanation constant to test for legal contradictions.

• Verification Accuracy: The system achieved an overall 97.7% accuracy in distinguishing between legally coherent (SAT) and incoherent (UNSAT) explanations.
• Localization Precision: When an inconsistency was detected (UNSAT), the system successfully localized the specific statutory provision implicated.
  • Localization F1 Score: Varied by category, ranging from 0.51 (Income) to 0.83 (Citizenship), with an overall average of 0.977 for the UNSAT cases where localization was applicable.
  • Categories with more determinate rules (Citizenship, Residency) showed higher retrieval accuracy than those with contextual nuance (Income, Student Status).
• Case Study: In a specific case where a benefit termination was justified by "gross income exceeds the limit," the system confirmed the explanation was SAT. When the determination was inverted to "eligible" while keeping the same explanation, the system correctly returned UNSAT and identified MPP §63-409.111 as the violated provision.

5. Significance and Claims

The authors claim that this work offers a proof-of-concept for embedding legal accountability into the technical substrate of public-sector AI.

• Institutional Scaffolding: The system is designed not to replace administrative discretion or automate legal judgment, but to act as "institutional scaffolding" that strengthens oversight and contestability. It automates the verification of justifications, not the decisions themselves.
• Governance over Transparency: The paper reframes explainability as a governance challenge. It posits that for public algorithms, explanations must do more than reveal statistical associations; they must articulate the legal basis for a decision to satisfy due-process rights.
• Applicability: The framework is applicable regardless of whether the underlying decision engine is predictive, rule-based, or hybrid, as it evaluates the explanatory layer issued to the applicant.
• Limitations: The authors modestly note that the system relies on a task-specific formalization of statutes and cannot capture open-textured standards or discretionary judgments fully. The evaluation used controlled, single-law cases to ensure clear attribution, meaning real-world complexity involving multiple interacting statutes may present additional challenges. The system is a technical tool for accountability infrastructure, not a substitute for holistic legal judgment.

In conclusion, the paper demonstrates that explanation-level legal accountability can be made computationally tractable through neuro-symbolic methods, providing a mechanism for agencies, oversight bodies, and individuals to assess whether automated justifications satisfy statutory requirements.