Latest / 1 More Paper / A Neuro-Symbolic Framework for Legal Accountability in Public-Sector AI — Sunny & Sivan-Sevilla (2026)
Transcript
- You’re listening to “A Neuro-Symbolic Framework for Legal Accountability in Public-Sector AI,” by A.D. Sunny and I. Sivan-Sevilla. Published in 2026. Abstract. Automated decision-making systems are increasingly used by public agencies to govern access to welfare. Accountability in these settings is not achieved through access to model internals, but by the explanations provided to applicants i.e. documents that function as legal justifications and sites of contestation. Little work has been done to examine whether such explanations are legally valid. This paper examines explanation-level accountability in public-sector AI systems by designing and implementing a neuro-symbolic framework to assess automated welfare eligibility determinations. We deploy a Large Language Model (LLM) to encode statutory eligibility rules into a formal ontology and use satisfiability-based verification to assess whether benefits explanations comply with the governing law. Applying this approach to California’s CalFresh program, we analyze explanations and observe if our system detects legal mismatches. Our findings show that formal verification reveals violations of statutory requirements even when explanations appear reasonable or complete to human readers. We argue that explanation-level verification offers a distinct and necessary complement to existing approaches of algorithmic auditing and accountability, shifting attention from model behavior to the legal integrity of justificatory artifacts. We call for a shift from interpretability to auditability of public algorithms, as government explanations must do more than reveal statistical associations; they should articulate the legal basis for a decision so that affected individuals, oversight bodies, and administrative reviewers can assess whether the justification satisfies statutory criteria and procedural norms. Introduction. Government agencies have increasingly turned to automation to maintain service delivery. The rapid ad-vancement of artificial intelligence and machine learning has accelerated this shift, encouraging the adoption of automated decision systems for welfare benefits with the promise of efficiency and consistency. At the same time, integrating machine learning into public-benefit decision making introduces serious risks. Advanced predictive systems are often opaque, making it difficult or even impossible to understand how eligibility decisions are made. Decisions that cannot be explained cannot be meaningfully challenged, restricting applicants’ rights to contest errors that may deny them essential support. Authors’ Contact Information: Allen Daniel Sunny, University of Maryland, College Park, MD, USA, the email address; Ido Sivan-Sevilla, The Hebrew University of Jerusalem & University of Maryland, Jerusalem, Israel, the email address. FAccT ’26, Montreal, QC, Canada Automated eligibility systems, whether predictive, rule-based, or hybrid, produce determinations whose internal logic is often inaccessible to the individuals they affect. Eligibility criteria are expressed in complex legal language, and it is unrealistic to expect applicants to hold the knowledge needed to assess their eligibility explanations. At the same time, the reasoning behind automated determinations is rarely surfaced in the explanations provided to applicants. This disconnect means that explanations provided to applicants may appear plausible yet fail to reference the required legal authority or may misstate the conditions under which benefits should be granted. Notices of action, benefit determination letters, and similar administrative texts serve as the interface through which state authority is exercised and made contestable. These explanations must document how statutory criteria were applied, signal the legal basis for eligibility or denial, and structure the procedural rights of individuals who seek review or appeal. This governance framing stands in contrast to much of the explainable AI literature, which treats explanations as tools for interpretability, debugging, or user trust. XAI methods typically optimize for fidelity to model behavior or user comprehensibility. Legal and institutional review evaluates explanations according to a different criterion: traceability to authoritative sources of law, coherence with procedural rules, and suitabil-ity for contestation in adversarial or quasi-judicial settings. Interpretability is a necessary condition for accountability, but it is not sufficient in legal contexts, and bridging this gap requires moving from explaining models to auditing justifications. Such a shift requires formal representations of legal rules, mechanisms that map explanation content to those rules, and procedures that determine whether stated justifications satisfy applicable statutory requirements. Without a shared legal structure, neither applicants nor administrators can determine whether an automated decision is justified under the law. This gap highlights a fundamental accountability problem: explanations must be legally valid and not just interpretable, if automation is to preserve due-process rights in public-benefit administration. Previously, a similar formalization of welfare distribution was conducted by Escher and Banovic (2020). Their method, however, focused on the validity of benefits screening tools rather than the explanations provided to applicants. Our work addresses a distinct governance function: rather than producing eligibility determinations, we evaluate whether justifications already issued are legally adequate, supporting contestation and appeal rights that existing technical infrastructure rarely enables. To address this gap, we build a neuro-symbolic framework to evaluate the legal accountability of public benefits programs and demonstrate its validity on California’s SNAP program (CalFresh). We rely on literature about formal knowledge representation, ontology extraction, and neuro-symbolic frameworks (Section 2), describe our methodology and architecture (Section 3), and report model accuracy against the CalFresh case study (Section 4). We discuss our results (Section 5) and conclude (Section 6) with a call for a shift towards explanations-based public algorithmic accountability. 2 Literature Review: Legal Reasoning for Welfare Distributions via Neuro-Symbolic Frameworks To automatically verify the legal basis for public benefit distributions, the paper brings together literature about knowledge representation (of the law) and ontology extraction and construction via formal methods. The paper uses Large Language Models (LLMs) to represent the law and builds the relevant ontology at scale, to then put everything together through a neuro-symbolic framework for legal verification of welfare distribution. Knowledge representation is applied through an ontology, defined as a formal specification of how entities within a domain are categorized and related to one another. It articulates a shared conceptualization of reality, defining the classes (types of things), relations (how those things connect), and axioms (constraints that must hold true) that together describe a domain’s structure. Gruber defines an ontology as “an explicit specification of a conceptualization”, positioning ontologies as a bridge between human semantic categories and the formal structures required for computational reasoning in legally regulated domains. Over time, several representational standards have emerged to encode such knowledge structures, ranging from the Resource Description Framework (RDF), which expresses knowledge as subject–predicate–object triples, to the Web Ontology Language (OWL), which builds on RDF to support richer logical semantics based on Description Logic. From these standards, the field of representation of legal knowledge has emerged, seeking to separate the structure of legal concepts from the logic of their application. The emergence of legal knowledge representation happened through the development of ontologies which are formal, machine-readable vocabularies of legal entities and relations. Frameworks such as LKIF-Core (Legal Knowledge Interchange Format), LegalRuleML, and other OWL-based models introduced dependencies between rules. These ontological frameworks allowed legal knowledge to be represented with greater precision and interoperability, allowing reasoning engines to perform tasks such as compliance checking, conflict detection, and inference of legal consequences. In doing so, they transformed legal texts from static documents into structured knowledge bases that could be computationally queried and analyzed. This formalization provided a foundation for a new class of reasoning systems: once legal rules were expressed as explicit logical statements, they could be subject to automated verification and consistency checking. A related institutional effort is the Rules as Code movement, which advocates encoding legislation as machine-executable specifications at the drafting stage to improve administrative clarity and automation. The construction of ontological vocabulary against the way rules are expressed is a major challenge. Legal ontologies have traditionally been built through manual expert analysis — a process that is labor-intensive, difficult to maintain as statutes evolve, and prone to inconsistency when multiple analysts encode the same domain. Recent work has explored automating this process by extracting ontological structure directly from legal text. Concept extraction pipelines segment statutory provisions into minimal eligibility-relevant clauses and identify legally operative terms through noun-phrase extraction, named entity recognition, or embedding-based similarity matching. Extracted concepts can then be organized into hierarchical class structures that reflect the normative organization of the source legislation, with de-duplication enforced through semantic similarity thresholds to prevent redundant or overlapping representations. A key challenge in this process is maintaining alignment between extracted concepts and their authoritative legal sources. Without explicit traceability — linking each ontology term to a specific statutory citation — the resulting vocabulary risks becoming disconnected from the legislation it is meant to represent. This concern is particularly acute in welfare administration, where eligibility depends on precise statutory conditions and where misalignment between the ontology and the governing law could produce verification errors that harm affected individuals. Embedding-based methods offer a partial solution by enabling both de-duplication and structural validation. By projecting extracted concepts into a shared semantic space, it becomes possible to assess whether legally distinct eligibility domains — income, residency, citizenship — remain separable in the representation, a necessary condition for accurate downstream rule retrieval and verification. Importantly, representing legal knowledge in formal structures is a necessary but insufficient condition for accountability. Reasoning systems operationalize these representations by evaluating whether specific facts, claims, or decisions satisfy encoded legal constraints. Satisfiability Modulo Theories (SMT) provide the foundational computational mechanism for this task. SMT solvers extend propositional logic with domain-specific theories — including arithmetic, temporal relations, and string comparison — enabling evaluation of both qualitative and quantitative legal conditions. For example, determining whether a household’s income satisfies statutory thresholds while residency verification obligations are jointly met, requires reasoning across multiple constraint types simultaneously. Systems such as Regorous integrate legal ontologies with SMT-based constraint solving to perform process-level compliance auditing, while other approaches employ logical reasoners to infer legal consequences or detect rule conflicts. Judson et al. demonstrate how SMT-based oracles can investigate the reasoning behind automated decisions, combining formal verification with decision traceability. Collectively, this body of work shows that symbolic reasoning can render the structure of law computationally tractable for compliance tasks. Still, a common limitation persists: existing reasoning systems rely on exhaustive manual rule enumeration, require expert maintenance, and remain disconnected from unstructured natural-language texts that constitute the operative interface between agencies and affected individuals. Large Language Models (LLMs) have introduced new possibilities for bridging natural-language legal texts and formal representations. Unlike earlier rule-based extraction methods that required hand-crafted templates or expert annotation, LLMs can process statutory language at scale and generate candidate logical formalizations from unstructured text. Recent work has explored ’LLM-Plus-Solver’ architectures in which neural models extract candidate rules or explanations from natural language, and symbolic solvers check the satisfiability of those claims. These pipelines have been applied to visual reasoning, scientific discovery, and automated theorem proving, demonstrating that neural interpretations can be systematically tested against external logical constraints rather than accepted at face value. In legal domains specifically, LLMs have been used to identify legally operative concepts, clause boundaries, and exceptions from regulatory texts, while related approaches combine rule extraction with constraint validation — for example, LLM + Z3 or LLM + Prolog pipelines — verifying whether the logic behind a textual explanation is complete and consistent. The reliability of LLM-based formalization, however, is critically dependent on the prompting strategy. Uncon-strained generation frequently produces narratively plausible but syntactically invalid or semantically drifted outputs. Directed symbolic prompting — in which the model is explicitly instructed to produce solver-compatible logic using a controlled vocabulary — has been shown to dramatically improve formalization success rates, while vanilla and undirected approaches yield unreliable results even from frontier models. These findings position LLMs not as autonomous legal reasoners but as extraction and translation components within larger verification pipelines — capable of scaling the formalization of statutory text, provided their outputs are validated against independent symbolic constraints. The different components above can come together via Neuro-symbolic frameworks. Neuro-symbolic AI integrates neural learning with symbolic reasoning, combining the flexibility of data-driven methods with the formal guarantees of logic-based systems. In settings where behavioral errors carry significant consequences and correctness must be formally established, this integration enables outputs to be verified rather than merely interpreted. Foundational architectures such as Logic Tensor Networks and DeepProbLog incorporate logical constraints directly into neural inference, ensuring that predictions respect domain-specific structure rather than relying on unconstrained statistical associations. More recent approaches connect LLMs to external verification systems, creating pipelines in which neural components generate structured representations and symbolic components evaluate them. In these architectures, the division of labor is deliberate: neural methods handle the variability and scale of natural-language inputs, while symbolic methods provide the deterministic reasoning required for verification and traceability. In legal domains, this paradigm aligns directly with the requirements of procedural accountability. Neural systems can extract legally operative concepts and translate statutory clauses into formal constraints, while symbolic solvers verify whether these constraints are jointly satisfiable under given case facts. The resulting systems can detect not only that an inconsistency exists but also which specific legal provisions are implicated — transforming verification outputs into governance-relevant accountability signals. Despite these advances, no existing neuro-symbolic system has been designed to verify the legal adequacy of the explanations that public agencies issue to affected individuals. Current approaches focus on decision-level compliance or rule-level consistency, but do not address whether the justificatory artifacts — notices of action, eligibility explanations, benefit determination letters — satisfy the statutory requirements that authorize them. This gap between decision verification and explanation verification defines the specific contribution of the paper. A Neuro-Symbolic Framework for Legal Accountability in Public-Sector AI 3 Methodology: Building a System to Automatically Verify the Legality of Public Welfare Distributions 3.1 Data Sources The Supplemental Nutrition Assistance Program (SNAP) is the largest food-assistance program in the United States, providing monthly benefits to low-income households based on statutory eligibility criteria including income, residency, citizenship, resources, and student status. Still, not all eligible individuals receive their benefits. Errors in determination put applicants at risk of losing access to basic subsistence needs. In California, SNAP operates under the name CalFresh. Eligibility determinations are governed by the Cali-fornia Manual of Policies and Procedures (MPP) Division 63, which translates federal and state requirements into detailed administrative rules. When a decision is made, counties must issue a Notice of Action (NOA) explaining the legal basis for an approval, denial, reduction, or termination of benefits. Because internal decision processes may be automated or otherwise opaque, the NOA is often the only publicly visible justification for how eligibility rules were applied. It serves as the central accountability mechanism through which applicants can understand, challenge, or correct decisions affecting their access to food. Our designed neuro-symbolic framework requires two types of input: A statutory corpus encoding the legal rules that govern eligibility, and Real-world case data containing the agency’s explanation, the determination outcome, and the factual circumstances of the applicant. The first provides the legal standard against which explanations are evaluated; the second provides the explanations and case facts to be verified. We draw each from a separate publicly available source. The statutory corpus comes from the CalFresh regulations in MPP Division 63, published by the California Department of Social Services. These span chapters on eligibility criteria, benefit computation, and administrative procedures, and are stored as separate document files on the California Department of Social Services (CDSS) website. We downloaded, read, assembled, and cleaned them into a unified JSON structure for downstream processing. This corpus serves as the ground truth for ontology construction of the law. Case data was drawn from the CDSS State Hearings Division Decision Registry, a public database of administrative appeal decisions. Each record documents a contested CalFresh eligibility determination and includes the agency’s original justification, the claimant’s grounds for challenge, and the adjudicatory outcome. We downloaded individual hearing decisions as PDFs, cleaned them, and used Python-based extraction scripts with named entity recognition to reconstruct three elements from each case: The explanation quoted from the agency’s Notice of Action, The eligibility determination, and Case-related facts presented by the claimant. Because original case files were not directly available, these reconstructed elements serve as the system’s input data. We selected 50 cases spanning five statutory eligibility dimensions — income, residency, citizenship, resources, and student status — to ensure coverage of the five primary categories invoked in CalFresh determinations. 3.2 Overall Architecture Our architecture has four stages: Ontology construction, Terminological Box (TBox) encoding, Assertion Box (ABox) construction, and Satisfiability Modulo Theories (SMT)-based verification, as shown in Figure 1. Ontology construction derives a controlled legal vocabulary and statute-based constraints from the governing law of CalFresh. These are assembled into the TBox, which encodes stable, case-invariant legal requirements. In parallel, administrative explanations and case facts are structured into the ABox, capturing what the agency claims as a justification for a particular determination. The verification layer evaluates whether the TBox and ABox are jointly satisfiable using the SMT. A ’SAT’ outcome means the explanation is coherent under the governing law i.e. it can function as a legally admissible justification. An ’UNSAT’ outcome means no such interpretation exists, signaling that the explanation fails to justify the determination under the law (but not that the eligibility decision itself was wrong). When an inconsistency is detected, the solver extracts an unsatisfiable core i.e. a minimal subset of constraints responsible for the conflict and maps them back to their corresponding legal provisions. The output is not a binary verdict, but a statute-grounded accountability signal identifying which legal clause is violated by the explanation. Simply put, the ontology and TBox define what the law requires, the ABox captures what the explanation claims, and SMT verification determines whether those claims hold up. 3.3 Ontology Construction Statutes and administrative explanations are written in natural language and cannot be checked directly for logical consistency. We therefore construct a formal ontology; a controlled vocabulary of the concepts, relationships, and constraints that govern eligibility decisions to serve as the foundation for verification. Rather than modeling an entire legal domain, the ontology targets the core elements that structure real-world determinations: threshold conditions, status categories, verification requirements, and exclusion rules. The design prioritizes traceability to authoritative sources and consistency across cases over legal completeness. The ontology’s architecture draws on the LKIF-Core (Legal Knowledge Interchange Format) framework, from which we adopted class naming conventions and structural patterns for representing legal knowledge. The key insight guiding construction is that the structure of the statute itself provides the skeleton of the ontology: the MPP Division 63 regulations are already organized around eligibility dimensions (income, residency, citizenship, resources, student status), and each section specifies the conditions, thresholds, and exceptions that apply within that dimension. We used this statutory structure as the top-level class hierarchy. Within each statutory section, we used named entity recognition to extract noun-verb keyword pairs. Nouns identified candidate classes and individuals (e.g., "household," "gross income," "sponsor," "verification document"), while verbs identified candidate relationships and properties (e.g., "exceeds," "resides in," "is exempt from"). To prevent redundancy, each candidate term was embedded using the embedding model Qwen3-Embedding-8B and compared against existing ontology entries via cosine similarity; terms exceeding a similarity threshold of 0.85 were merged with their existing counterpart rather than added as duplicates. 3.4 TBox: Legal Knowledge and Statutory Constraints The TBox represents the normative structure of the domain. It consists of two parts: a legal ontology that defines the key concepts used in decision-making, and a set of statute-derived rules that specify when a determination is legally permitted or prohibited. Together, these components define the space of legally valid justifications against which individual explanations are evaluated. The construction of the TBox follows the pipeline shown in Figure 2. The process begins with the regulatory corpus, which serves as the authoritative source of legal requirements. These texts are segmented law by law, preserving the statutory structure of the source material. We then use named entity recognition to extract legally operative noun-verb pairs from each law identifying conditions, thresholds, obligations, and exclusions. These extracted elements are mapped to the controlled ontology vocabulary using cosine similarity against existing entries, ensuring that the same legal concepts are represented consistently across rules and cases. Using this shared vocabulary, a large language model, OpenAI’s o1 is prompted to translate each statutory provision into a formal logical rule (see Appendix for prompt strategy). These rules express the normative structure of the law in solver-ready form, including implications, necessary conditions, and disqualifying grounds. Each rule is stored together with a citation to its source provision, preserving a direct link between formal constraints and their legal authority. This construction process yields a case-invariant TBox: the ontology and rules remain fixed across cases and define the general standards of legal coherence. Individual explanations are later evaluated by instantiating these standards with case-specific facts in the ABox and checking whether the asserted reasoning satisfies the constraints encoded in the TBox. 3.5 ABox: Case Assertions and Explanatory Claims The ABox represents the case-level content of a determination. It encodes two types of information: (i) factual predicates describing the case, and (ii) the claims made by the explanation, including the asserted outcome and the conditions offered in its support. Explanations are mapped into the same controlled predicate vocabulary used by the TBox so that justificatory claims can be evaluated in a consistent and verification-ready form. The ABox is built using the pipeline shown in Figure 3. As described in Section 3.1, each case is reconstructed from Allen Daniel Sunny and Ido Sivan-Sevilla a hearing decision record containing the agency’s original explanation, the eligibility determination, and the factual circumstances presented by the claimant. The construction of the ABox proceeds in three steps: First, the justificatory rules cited in the case are fetched from the existing TBox. Because the TBox already encodes the full set of statute-derived constraints, the ABox does not re-derive legal rules. It retrieves the specific provisions that the explanation invokes. This ensures that the same formal representation of the law is used on both sides of the verification. Second, the agency’s explanation is translated into the same statutory logic used by the TBox. OpenAI’s o1 is prompted to encode the explanation’s reasoning as solver-ready implication statements (see Appendix for prompt strategy). Although these take the form of logical rules, they do not represent statutory requirements, they capture what the explanation claims would justify the outcome. Third, the case file is assembled from the hearing decision record itself. Factual predicates such as the applicant’s circumstances including income or household size are extracted from the claimant’s testimony and case details documented in the hearing decision. These facts, together with the retrieved TBox rules and the translated explanation logic, form a self-contained ABox representing a single case, ready for verification against the TBox constraints. 3.6 Solver: Formal Verification and Accountability Output The solver takes the legal rules from the TBox and the case assertions from the ABox and evaluates their joint satisfiability using an SMT solver. Every explanation is treated as a set of testable claims: the asserted determination (eligible or not eligible) and the conditions offered as reasons. Verification asks whether these claims are consistent with the statutory constraints that apply. A SAT result means the explanation and determination are coherent under the law and can function as a legally admissible justification. An UNSAT result means the explanation cannot be made consistent with the legal rules — not that the eligibility decision itself was wrong, but that the justification fails. To support audit, appeal, and oversight, the solver tracks which legal rules are involved in each check. When an inconsistency is detected, the system extracts an unsatisfiable core i.e. a minimal subset of constraints responsible for the conflict and maps them back to their corresponding provisions in the MPP. The output is not a vague error but a statute-grounded accountability signal, identifying which specific legal requirements the explanation failed to meet. This makes results actionable for review, appeals, and compliance work. 4 The CalFresh Case Study of Public Algorithmic Governance We trace a single case through the full pipeline to illustrate how the system operates (See Figure 6 in the Appendix). The case involves a one-person household in San Diego County whose CalFresh benefits were terminated (See Figure 7 in the Appendix). The agency’s Notice of Action states: “CalFresh benefits terminated because gross income exceeds the gross income limit for a household of one.” TBox: The relevant statutory provision is MPP §63-409.111, which establishes the gross income eligibility standard: a household with gross income in excess of the standard is ineligible. During TBox construction, this provision was segmented, its operative terms (GrossIncome, GrossIncomeLimit, HouseholdSize) were extracted via NER and mapped to the ontology vocabulary, and o1 translated it into the solver-ready rule: Implies(GrossIncome > GrossIncomeLimit(HouseholdSize), Not(ApplicantEligible)) This rule is stored with its citation to §63-409.111. ABox: The case file is assembled from the hearing decision record. Construction follows the three steps de-scribed in Section 3.5. First, the explanation text—“CalFresh benefits terminated because gross income exceeds the gross income limit for a household of one”—is processed using NER to extract its operative noun-verb pairs. This yields the key terms: “gross income,” “exceeds,” “gross income limit,” “household of one,” and “termi-nated.” Each term is embedded using Qwen3-Embedding-8B and matched to the ontology vocabulary via cosine similarity, mapping them to the controlled predicates: GrossIncome, GrossIncomeLimit, HouseholdSize, and ApplicantEligible. Second, o1 translates the explanation’s reasoning into solver-ready logic using the matched ontology terms: Implies(GrossIncome > GrossIncomeLimit(HouseholdSize), Not(ApplicantEligible)) This captures what the explanation claims would justify the outcome. The relevant TBox rule citing MPP §63-409.111 is retrieved—in this case, the explanation’s logic and the statutory rule take the same form, indicating close alignment between the agency’s stated reasoning and the governing law. Third, factual predicates are extracted from the hearing decision record: household size of 1, gross earned income of $728.11, unemployment insurance benefits of $1,950.30, yielding total gross income of $2,678.41 against a gross income limit of $2,082.00. These, together with the translated explanation logic and the retrieved TBox rule, form the complete ABox for this case. SMT Verification: The solver evaluates the TBox rule and the ABox assertions jointly. The explanation asserts that gross income exceeds the limit for a household of one, and the determination is termination. The solver returns sat—the explanation is coherent with the cited statutory provision and can function as a legally admissible justification. To test accountability detection, we invert the determination to “eligible” while holding the explanation constant. The solver now returns unsat: an explanation citing excess income cannot justify an approval. The unsatisfiable core identifies MPP §63-409.111 as the implicated provision—exactly the statute on which the original explanation was grounded. This demonstrates the full accountability loop: the system detects the inconsistency and traces it back to the specific law that was violated. 4.1 Empirical Examination of the Explanations-based Algorithmic Accountability Framework We evaluate the proposed accountability artifact across two layers of the pipeline: representation fidelity and Verification and Retrieval of Laws. Together, these analyses assess whether the system can function as accountability infrastructure—carrying legal norms into a computable form, detecting inconsistency between explanations and the governing laws, and localizing statutory responsibility when such inconsistencies arise. 4.1.1 Representation Adequacy of the Legal Ontology. We first assess whether the legal ontology provides sufficient structure to support explanation verification. To inspect coverage and internal organization, we embed ontology concepts using a sentence-level embedding model and project them into two dimensions with UMAP (Figure 5). This visualization is descriptive, it does not affect verification or rule execution. However, it allows us to confirm that the primary statutory dimensions relevant to eligibility form coherent, separable groupings in the representation. As seen in figure 5, across the evaluated CalFresh cases, the ontology captures the primary statutory dimensions invoked in administrative explanations, including income eligibility, residency verification, citizenship status, household composition, resources, and student status. These dimensions align with the categories routinely cited in Notices of Action and eligibility determinations. All cases in our evaluation could be encoded using this vocabulary without resorting to ad hoc predicates, indicating that the representation provides adequate coverage for the accountability task. This result establishes a necessary precondition for verification: legal requirements can be carried into a formal system in a way that supports consistency checking and statutory traceability. Importantly, this assessment does not claim doctrinal completeness or legal finality. It demonstrates that the ontology is fit for purpose as infrastructure for explanation-level accountability. 4.1.2 Verification and Retrieval of Laws. We evaluate whether the accountability artifact can (i) detect when an explanation no longer provides a legally admissible justification for a decision and (ii) localize the statutory provisions implicated when such inconsistency arises. Together, these tests assess the system’s capacity to function as accountability infrastructure for audit, appeal, and oversight. The evaluation focuses on a controlled subset of cases in which each determination is grounded in a single statutory provision, enabling unambiguous attribution of legal responsibility. For each case, we construct a paired evaluation. In the baseline condition, the explanation is assessed together with its original determination and the relevant statute-derived constraints. In these instances, the solver consistently returns SAT, indicating that the explanation and outcome are jointly coherent under the encoded legal requirements. A Neuro-Symbolic Framework for Legal Accountability in Public-Sector AI FAccT ’26, June 25–28, 2026, Montreal, QC, Canada To construct negative instances, we reverse the eligibility determination while holding the explanation constant. This produces a deliberate legal contradiction: the same explanation now purports to justify the opposite outcome despite being grounded in a single statutory rule that does not support that determination. This design isolates the accountability function of the artifact by varying only the decision claim rather than introducing speculative factual perturbations. Under this condition, the solver returns UNSAT whenever the explanation lacks a valid statutory basis for the inverted determination. These UNSAT outcomes do not indicate that the applicant is factually ineligible; rather, they signal that the justification fails as a legal basis for the asserted decision. In institutional terms, the system evaluates not whether the decision is substantively correct, but whether the explanation is legally admissible. Detection alone, however, is insufficient for accountability. When the solver returns UNSAT, the artifact also localizes legal responsibility by identifying which statutory provisions are implicated. Each statute-derived rule is asserted with a unique identifier corresponding to its source in California’s Manual of Policies and Procedures. We extract an unsatisfiable core over these tracked constraints, yielding a subset of statutory provisions that cannot be jointly satisfied with the explanation and asserted determination. Using the paired single-law cases described above, we evaluate whether the system returns the statute on which the original explanation was based. Because each negative instance is constructed from a case grounded in a single statutory provision, the expected outcome is unambiguous: a legally inconsistent explanation should implicate that same provision when the determination is inverted. Across negative cases, the returned unsatisfiable cores consistently include the expected statute identifier. Moreover, the cores remain compact, typically implicating a small number of provisions rather than producing diffuse attributions. This indicates that the artifact does not merely detect inconsistency but localizes it with sufficient precision to support institutional accountability processes. To characterize performance, we report two complementary measures: (i) the proportion of negative cases yielding UNSAT outcomes, indicating detection reliability and (ii) the inclusion rate of the expected statute identifier in the returned set of implicated provisions, indicating attribution accuracy. Together, these measures capture the system’s capacity to transform formal verification outcomes into governance-relevant accountability signals. FAccT ’26, June 25–28, 2026, Montreal, QC, Canada 4.2 SAT and UNSAT results We evaluate the proposed accountability artifact on a set of 50 administrative cases, constructing a paired incoherent instance for each by inverting the asserted determination, yielding 100 total evaluation instances. Table 1 reports category-level results on a balanced subset of these cases across five statutory dimensions of eligibility. For each category, ten underlying cases are evaluated in both coherent (SAT) and incoherent (UNSAT) form, producing twenty evaluation instances per category. Across all categories, the system consistently distinguishes legally coherent from incoherent explanations. In coherent cases, verification returns satisfiable outcomes, indicating that the stated justifications align with statutory requirements. In incoherent cases, the solver reliably identifies inconsistencies and retrieves the laws implicated in the explanation. Overall solver behavior remains stable across domains, demonstrating consistent verification under both positive and negative conditions. Performance in retrieving relevant laws, measured by F1 score on UNSAT cases, varies by category in ways that reflect differences in legal structure. Categories governed by more determinate rules, such as citizenship and residency, exhibit higher retrieval accuracy, while domains characterized by greater contextual nuance, such as income and student status, show lower but still substantial performance. These patterns suggest that the framework is sensitive to the normative complexity of different legal dimensions rather than reflecting uniform system behavior. Taken together, these results show that the proposed framework supports explanation-level legal account-ability along three dimensions: it (i) distinguishes coherent from incoherent justifications, (ii) retrieves the statutory bases of inconsistency when they arise, and (iii) does so consistently across heterogeneous eligibility categories. Rather than optimizing for predictive accuracy, the evaluation demonstrates that the system fulfills its intended institutional role, which is transforming explanations into auditable, legally grounded objects of review. All code, prompts, ontology artifacts, and evaluation data are available at the linked source. 5 Discussion The results of this study suggest that explainability in public administration must be reframed as a problem of accountability infrastructure. By treating explanations as normative claims that must be reconciled with statutory requirements, we shift evaluation from model-centric notions of interpretability or bias, to institution-centric notions of governance. This re-framing aligns explanations with their actual role in administrative practice: they are instruments through which legal authority is exercised, contested, and can be corrected. Neuro-symbolic architectures also reflect a broader design principle, in highly regulated domains, automation should prioritize verifiability over autonomy. It is important to note that the accountability gap we address does not depend on the presence of machine learning in the eligibility pipeline. Many public benefits systems, including CalFresh, rely on rule-based decision trees or hybrid workflows in which automated screening is combined with caseworker discretion. The opacity of these systems comes from institutional complexity i.e. layered regulations, frequent policy changes, and administrative processes that are difficult for applicants to observe or reconstruct. Whether a determination is produced by a predictive model or a deterministic rule engine, the explanation issued to the applicant must independently satisfy statutory requirements. Our framework evaluates this explanatory layer regardless of the upstream decision mechanism, making it applicable across the full spectrum of automation in public-sector administration. The designed capability can be used by multiple institutional actors within the eligibility decision life cycle. For agencies, it offers a mechanism for internal compliance checking prior to issuing determinations. For oversight bodies, it provides a structured basis for reviewing contested decisions. For affected individuals and advocates, it opens the possibility of appeals grounded not only in narrative disagreement but in formalized legal inconsistency. In each case, accountability shifts from abstract ethical principles to operational standards tied to the governing laws. Based on evaluation results, agency staff can review their explanations to applicants, public benefits attorneys can seek justice for their clients, and our tool can be routinely used to evaluate the CalFresh program or other programs on a regular basis (rather than upon a specific challenge). The assessments provided by our tool can be monitored by the state comptroller or agency reviewers, who can fine tune the tool upon changes in benefits eligibility criteria. We envision our framework as a foundational base layer atop which further bands of verification can be composed. For example, privacy-preserving verification modules that formally check whether explanations inadvertently disclose sensitive applicant attributes, or group fairness auditors that assess whether the consistency of reasoning holds equitably across demographic subgroups. By anchoring these higher-order concerns to a verified legal-semantic base, each successive band inherits the formal guarantees established below it rather than operating in isolation. Ultimately, this work suggests a broader agenda for responsible AI in the public sector. Rather than focusing exclusively on improving model-level explainability, future research should attend to the institutional pathways through which explanations acquire meaning and force. Accountability-centered design asks different questions: not only “can users understand this explanation?” but “can institutions act on it?” and “can it sustain contestation, audit, and review?” By demonstrating that explanation verification can be operationalized through a neuro-symbolic architecture, this paper offers a concrete step toward that agenda. The contribution is a new kind of infrastructure, one that embeds legal accountability into the technical substrate of public-sector AI. In doing so, it reframes explainability as a governance challenge and positions accountability as a first-class design objective rather than an afterthought. 6 Limitations While the proposed accountability artifact demonstrates the feasibility of explanation-level legal verification, several limitations shape the scope and interpretation of these results. Scope of Legal Formalization. First, the system relies on a task-specific formalization of statutory requirements. Welfare law contains open-textured standards, discretionary judgments, and contextual exceptions that cannot be fully captured in symbolic rules or ontological structures. The encoded constraints reflect those aspects of the statute that are routinely invoked in administrative justifications, but they do not constitute a complete or authoritative representation of the law. As a result, the artifact should be understood as supporting accountability for formalized components of legal reasoning, not as a substitute for holistic legal judgment. Dependence on Structured Explanations. Second, the effectiveness of the system depends on the availability of explanations that can be reliably mapped to the controlled predicate vocabulary. Although neural extraction components mitigate this constraint by enabling scalable processing of unstructured text, errors in extraction or misalignment between explanation language and the ontology can propagate into the verification stage. In practice, this means that the artifact’s outputs are only as robust as the quality of the structured representations it receives. Evaluation via Controlled Cases. Third, the evaluation emphasizes controlled case constructions—particularly single-law determinations and paired inversions—to enable clear attribution of legal responsibility. While this design is appropriate for testing detection and localization capacity, it does not model the full complexity of real-world administrative decision-making, where multiple statutes, discretionary factors, and procedural consid-erations often interact. The results therefore demonstrate the system’s capability for accountability verification rather than its performance under all institutional conditions. Non-Uniqueness of Legal Localization. Fourth, the localization of statutory responsibility is based on unsatisfiable cores returned by the solver. Such cores are not guaranteed to be unique, and different minimal sets of constraints may explain the same inconsistency. Consequently, the artifact should not be interpreted as identifying the singular “true” violated law, but rather as surfacing a principled subset of implicated provisions that warrant institutional attention. This reflects a broader feature of formal verification: it supports accountability by narrowing the space of legal concern, not by resolving interpretive disputes. Institutional Integration and Adoption. Finally, the artifact has been evaluated as a technical system rather than as part of a deployed administrative workflow. Its real-world impact depends on how it would be integrated into agency practices, oversight regimes, and appeal processes. Questions of organizational uptake, legal admissibility, and procedural legitimacy remain open and require empirical study beyond the scope of this paper. Taken together, these limitations clarify the intended contribution of the work. The proposed system does not aim to automate legal judgment or guarantee the substantive correctness of administrative decisions. Instead, it offers a proof-of-concept for how neuro-symbolic methods can support accountability infrastructure, making the legal adequacy of explanations visible, reviewable, and contestable within institutional processes. 7 Conclusion Automated decision systems increasingly mediate access to public benefits, rights, and services. In these settings, explanations are not just technical artifacts but are legal instruments that shape accountability, contestation, and procedural fairness. This paper has argued that evaluating explanations solely in terms of interpretability is insufficient for public-sector AI. What is required instead is an infrastructure that makes explanations legally verifiable. We introduced a neuro-symbolic accountability artifact that operationalizes this shift. By translating statutory requirements into formal constraints and evaluating administrative explanations against those constraints, the A Neuro-Symbolic Framework for Legal Accountability in Public-Sector AI system reframes explainability as a problem of governance rather than transparency alone. Across a multi-layer evaluation we show that explanation-level accountability can be made computationally tractable without automating legal judgment or replacing institutional discretion. The contribution of this work is a new kind of technical substrate for public administration: one that embeds legal accountability into the design of AI-enabled processes. By making the legal adequacy of explanations visible, inspectable, and contestable, the proposed artifact supports emerging practices of algorithmic auditing, oversight, and rights-preserving AI deployment. More broadly, this work points toward an accountability-centered paradigm for responsible AI. Rather than treating explainability as an end in itself, future systems should be designed around the institutional roles that explanations are meant to serve—supporting review, appeal, and governance in domains where automation carries legal and social consequences. Neuro-symbolic approaches offer a promising path toward this goal, by strengthening the conditions under which automated systems remain answerable to the law. 8 Public Repository All work including the constructed ontology and the formal generated rule set can be found in the linked source. 9 Acknowledgments We thank Professor Gabriel Kaptchuk (Department of Computer Science) and Professor Jessica Vitak (College of Information) at the University of Maryland, College Park for their guidance and support. 10 Generative AI Usage Statement The authors used generative AI tools (ChatGPT) during manuscript preparation for limited purposes of language editing, clarity improvements, and structural refinement of text drafted by the authors. No generative AI system was used to produce the substantive content, arguments, analysis, or results of this paper. The authors take full responsibility for the originality, accuracy, and integrity of the work. SUMMARY. San Diego County correctly proposed to discontinue the claimant’s CalFresh benefits effective July 31, 2020, where the claimant’s countable income exceeded the gross income limit for a CalFresh household size of one. FACTS The claimant's CalFresh Program household consists of one person. There is not anyone in the household who is disabled or over the age of 60. San Diego County issued a Notice of Action on June 30, 2020 advising the claimant that his CalFresh Program benefits were discontinued effective July 31, 2020 because the household's monthly gross income exceeded the maximum allowable for a one person household. On July 6, 2020, the claimant requested a hearing, disputing the county’s proposed discontinuance. As the claimant timely filed his hearing request, the claimant is receiving Aid Paid Pending the release of this decision. The claimant acknowledged that he may owe back the Aid Paid Pending if the county’s action is determined to be correct. A hearing was held telephonically on September 16, 2020. The claimant and the county representative appeared at the hearing. The county representative submitted a Statement of Position. (Exhibit 1) The county representative testified to the following: -The claimant applied for CalFresh benefits on April 14, 2020. The applicable semi-annual period is April 2020 to October 2020. -The claimant works for Target and is paid bi-weekly. Based on information reported by the claimant, the county anticipated that he would work 14 hours per week. He was being paid $12.00 per hour, so his income was calculated as follows: $12.00 x 14 hours = $168.00 weekly x 2 = $336.00 bi-weekly. This was converted to a monthly amount by multiplying by the appropriate factor ($336.00 x 2.167 = $728.11 monthly). -The county received a Payment Verification System (PVS) report dated June 11, 2020 showing that the claimant had been approved for Unemployment Insurance Benefits (UIB) of $900.00 bi-weekly. The claimant received his first payment on April 27, 2020. Per All County Letter 13-17, PVS reports are considered Verified Upon Receipt (VUR) and require mid-period action. Fig. 7. Hearing Document (Page 1/3) State of California CDSS State Hearings Division -The claimant’s Unemployment Insurance Benefits were converted to a monthly amount by multiplying by the appropriate factor ($900 x 2.167 = $1,950.30). -The claimant continued to work at Target while receiving Unemployment Insurance Benefits. -The household’s total income is $2,678.41. This exceeds the limit to have Modified Categorically Eligibility (MCE) status as the claimant is over 200% Federal Poverty Level. The claimant’s income also exceeds the CalFresh gross income limit for one person of $1,354.00. Therefore, he is ineligible for CalFresh benefits for this reason. The county's determination was as follows: The claimant testified to the following: -He did not dispute that he was still receiving his same earned income from Target and biweekly UIB of $900.00. The claimant testified that he was told that his UIB would not be countable income. The claimant testified that his UIB may be terminating this month. The claimant was informed that he may reapply for CalFresh benefits at any time. LAW All the regulations cited herein are set forth in the Manual of Policies and Procedures (MPP), unless otherwise specified. Except for categorically eligible households and households with an elderly or disabled household member(s), the counties shall determine eligibility for CalFresh Program benefits pursuant to the maximum gross income standards as promulgated and updated by the United States Department of Agriculture. Effective October 2019 through September 202 the gross income standard for a one-person household as set forth in Handbook §63-1101.31 is $1,354.00. A household with income in excess of the standard is ineligible to receive CalFresh Program benefits. (§63-409.111) Effective October 2019 to September 2020 the gross income standard for a one-person household with Modified Categorical Eligibility as set forth in Handbook §63-1101.31 is $2,082.00, which is 200% of the Federal Poverty Level. A household with income in State of California CDSS State Hearings Division excess of the standard is ineligible to receive CalFresh Program benefits. (§63-409.111) (All County Information Notice No. I-54-19, August 21, 2019) Unemployment Insurance Benefits (UIB) Unearned income includes annuities, pensions, retirement or veteran's or disability benefits; worker's or unemployment compensation; social security benefits; striker's benefits (except compensation for picketing); foster care payments for CalFresh household members; "and any deemed income from a sponsor who has signed an I-864 and/or I-864A paid to a sponsored noncitizen". (Man. Pol. Pro. § 63-502.142, as Rev. effective February 21, 2002); 7 C.F.R. § 273.9(b) (ii)) CalFresh Income Reporting Threshold Households determined eligible with gross income at or below 130 percent of the FPL are required to report changes in income when the household’s gross income exceeds 130 percent of the FPL, both during the SAR payment period and at recertification and submission of the SAR 7. The CalFresh IRT for a household of one is $1,354.00. (ACIN I-54-19, August 21, 2019) Prospective Budgeting The prospective budgeting system uses anticipated income/prospective budgeting to determine a recipient’s benefits. Prospective budgeting requires the county to use income that the recipient reasonably anticipates it will receive during the certification period. (All-County Letter No. 03-18, April 29, 2003, All County Letter No. 12-25, May 12, 2012) Income is “reasonably anticipated” when the recipient and CWD determines it is reasonably certain that the recipient will receive a specified amount of monthly income in the certification period. If the amount of income that will be received or when it will be received is uncertain, the portion of the AU/household’s income that is uncertain shall not be counted. This definition applies to earned and unearned income. (All County Letter No. 12-25, May 17, 2012; All County Letter No. 13-17, March 22, 2013, p. 7) If the AU/household’s monthly income fluctuates or they expect the income received in the Data Month to change in the upcoming months of the certification Period, the county must attempt to find out the amount of income the AU/household reasonably expects to receive, in order to determine what income, if any, can be reasonably anticipated and used in the next SAR Payment Period’s benefit calculation. Only that portion of income that the AU/household reasonably anticipates it will receive can be used in the benefit calculation. If, for example, a recipient has fluctuating income, but agrees that she usually makes at least a minimum of $200 a month, the minimum anticipated income can be anticipated. If however, a recipient can’t anticipate an amount or if she will get You are a legal reasoning assistant that converts legal clauses into formal logic rules compatible with the Z3 SMT solver. Use only the ontology variables provided below. Represent the eligibility conclusion as ApplicantEligible. Syntax Requirements: – Express each rule as a single logical implication – Use first-order logic operators: Implies, And, Or, Not, Equals – Use only ontology variable names exactly as listed – Output only JSON with the field: “hasLogic” – Do not include natural language explanations Ontology Concepts: {ontologyconcepts} Clause: “{inputclause}” Output format: { “hasLogic”: “<first-order logical implication>” } Fig. 10. Prompt template for rule formalization. This template is used for both TBox and ABox construction. For TBox, {inputclause} is a statutory provision from the MPP. For ABox, {inputclause} is the agency’s explanation from the Notice of Action. Fig. 11. Excerpt of the ontology in JSON format, showing two of nine domains. Each concept includes a type for solver compatibility and a citation linking it to the governing statute. Definitions omitted for space. Fig. 12. Excerpt of the TBox rule set showing three rules across income, residency, and student eligibility domains. Each rule preserves its statutory citation, the ontology predicates it operates on, and the solver-ready logic. The full rule set can be examined in the attached github repository.