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

本论文提出了一种神经符号框架，该框架整合了法定本体、规则提取以及基于求解器的推理，以确保 CalFresh 的自动化资格认定决定与法律规则保持一致，从而实现可追溯且可质疑的程序问责。

要点

想象一个负责决定谁有资格获得食品援助的政府机构。当他们向申请人发出“拒绝”通知时，会附上一封信函说明原因。通常，这些信函使用令人困惑的法律术语写成。申请人阅读后，可能会觉得“听起来合乎情理”，但实际上无法核实政府是否正确地遵循了规则。由于缺乏验证所需的法律工具，他们只能被迫信任这封信。

本文提出了一种新的“数字裁判”来核查这些信函。其工作原理可分解为以下简单概念：

问题：官僚体系的“黑箱”

将政府的决策过程想象成一个黑箱。你输入个人信息，系统输出一个决定。有时，这个黑箱是一个计算机程序；有时，是一个遵循复杂规则手册的人类。问题在于，寄给你的“解释信函”表面上可能看起来没问题，但背后可能正在暗中违反规则。

目前，我们依赖“可解释性”——试图让计算机的推理过程变得可见。但作者认为，在法律环境中，仅仅看到推理过程是不够的。你需要可审计性。你需要知道解释是否真正符合法律，就像核对收据是否与所购物品一致一样。

解决方案：“翻译器”与“规则检查器”

作者构建了一个名为神经符号框架的系统。你可以将其想象为一个由两人组成的协作团队：

1. 翻译器（“神经”部分）：
   想象一个超级聪明的机器人，它阅读杂乱复杂的政府法律（用英语书写）以及寄给申请人的杂乱解释信函。该机器人的任务是将这些人类语言翻译成计算机能完美理解的严格数学语言。这就像将一首诗翻译成精确的数学方程组。

   • 在论文中： 他们使用大型语言模型（LLM）将诸如“你的收入必须低于 2000 美元”这样的法律条文转化为形式化规则：如果 收入 > 2000，则 不符合资格。

2. 规则检查器（“符号”部分）：
   一旦法律和解释信函被转化为数学方程，一个严格的逻辑机器（称为 SMT 求解器）便会介入。这台机器不进行猜测，而是进行计算。它会问：“这封解释信函是否在数学上证明了该决定的合理性？”

   • 如果信函说“你因收入过高而被拒绝”，而数学计算显示你确实收入过高，机器会输出SAT（可满足/有效）。这意味着解释站得住脚。
   • 如果信函说“你因收入过高而被拒绝”，但数学计算显示你并未收入过高，机器会输出UNSAT（不可满足/无效）。这意味着解释是谎言或错误，即使对人类来说听起来似乎合理。

现实世界测试：CalFresh

该团队在加利福尼亚州的食品援助项目CalFresh上测试了此系统。他们选取了 50 个真实案例，其中人们的福利被拒绝或削减。

• 设置： 他们将实际法律、申请人的事实（收入、家庭规模）以及政府寄出的官方信函输入系统。
• 结果： 系统成功发现了“法律不匹配”。在一次测试中，他们通过欺骗系统，将“拒绝”决定改为“批准”，但保留了相同的解释（其中称该人收入过高）。系统立即发出UNSAT警报，指出解释与新决定相矛盾。
• “铁证”： 当系统发现错误时，它不仅仅说“错误”。它会指出违反法律的具体页码和段落。这就像裁判不仅吹哨，还直接指出球员违反规则的具体规则书页。

为何这很重要

作者认为，我们需要停止仅仅尝试“解释”AI 如何思考，转而开始审计其产生的法律理由。

• 现有方式： “这是计算机说‘不’的原因。它是基于它学到的模式。”（这在法庭上难以反驳）。
• 新方式： “这是信函。我们的系统已将其与法律进行核对，发现其违反了第 63-409.111 条。”（这在法庭上易于反驳）。

核心结论

本文并不声称要取代政府或做出最终决定。相反，它构建了一个数字安全网。它确保当政府向你发送一封说“不”的信函时，该信函确实是一个合法的法律理由，而不仅仅是一个令人困惑的借口。它将“解释”从一份你必须信任的纸张，转变为你可以验证的证据。

关键要点： 在公共福利领域，解释不仅仅关乎清晰；它关乎法律上的真实性。该系统就是用来核查真相是否真正被陈述出来的工具。

技术摘要

技术摘要：面向公共部门人工智能问责的神经符号框架

1. 问题陈述

公共机构日益依赖自动化决策（ADM）系统来管理福利获取权限。尽管这些系统承诺提高效率，但它们往往缺乏透明度，导致申请人难以理解或质疑资格认定结果。当前可解释人工智能（XAI）的研究方法侧重于模型可解释性、保真度或用户信任。然而，在法律和行政语境中，解释的首要功能并非仅仅为了被理解，而是作为可在对抗性或准司法环境中被质疑的法律依据。

identified 的核心问题在于，现有解释（例如“行动通知”）对人类读者而言可能看似合理，却未能引用正确的法律依据，或错误陈述法定条件。目前缺乏技术基础设施来验证这些论证性文件是否相对于 governing statutes 具有法律有效性。现有的审计方法通常侧重于决策层面的合规性或模型行为，而忽视了解释本身的法律完整性。这一缺口阻碍了申请人和监督机构有效评估某项决定是否满足法定标准及程序规范。

2. 方法论

作者提出了一种神经符号框架，旨在自动验证福利资格解释的法律充分性。该系统将焦点从解读模型内部机制转移到审计向申请人提供的理由上。其架构包含四个主要阶段：

2.1 数据源

• 法规语料库：加利福尼亚州政策与程序手册（MPP）第 63 部分，规范 CalFresh（SNAP）项目。
• 案例数据：来自加利福尼亚州社会服务部（CDSS）州听证会分部的 50 起行政上诉裁决记录。这些记录包括机构原始解释、裁决结果以及申请人陈述的事实情况。

2.2 系统架构

该框架通过一个将法律规则与特定案例主张分离的管道运行：

1. 本体构建：

   • 利用命名实体识别（NER）和基于嵌入的相似度匹配（使用 Qwen3-Embedding-8B），从 MPP 法规中提取受控的法律词汇。
   • 该本体针对核心资格维度：收入、居住地、公民身份、资产和学生身份。
   • 此结构确保了对权威来源的可追溯性，并防止冗余。

2. TBox（术语框）编码：

   • 表示法律的规范结构（案例不变规则）。
   • 对法定条款进行分段，并提取操作性术语。
   • 提示大型语言模型（LLM），具体为 OpenAI 的 o1，将这些条款转化为形式化的、可供求解器处理的逻辑规则（例如蕴含关系、必要条件）。
   • 每条规则均链接至其来源引用（例如 MPP §63-409.111）。

3. ABox（断言框）构建：

   • 表示案例级内容（事实与解释性主张）。
   • 利用 LLM 将机构的解释转换为与 TBox 相同的逻辑格式。
   • 从听证记录中提取事实谓词（例如家庭规模、收入金额）。
   • ABox 结合了由解释所调用的检索到的 TBox 规则、转换后的解释逻辑以及具体的案例事实。

4. 基于 SMT 的验证：

   • 可满足性模理论（SMT）求解器评估 TBox（法律规则）与 ABox（案例断言）的联合可满足性。
   • SAT 结果：解释与 governing law 一致，可充当法律上可采纳的理由。
   • UNSAT 结果：解释与法律不一致。求解器提取一个不可满足核心——即导致冲突的最小约束子集——并将其映射回具体的法定条款。

3. 主要贡献

• 从可解释性转向可审计性：本文主张范式转变，即公共算法的问责制应通过解释的法律有效性而非仅仅是模型可解释性来衡量。
• 神经符号验证管道：一种新颖的集成方式，其中神经组件（LLM）负责提取和翻译非结构化法律文本及解释，而符号组件（SMT 求解器）提供确定性验证和可追溯性。
• 解释级问责：与以往形式化筛查工具的研究（如 Escher 和 Banovic, 2020）不同，本框架评估向申请人发出的论证性文件（行动通知），支持质疑和上诉的权利。
• 基于法规的信号：该系统不仅标记错误，还通过确切指出解释违反了哪些法定条款，生成可操作的问责信号。

4. 结果

该框架在 50 个 CalFresh 案例上进行了评估，涵盖五个资格类别（学生身份、收入、居住地、公民身份、资产）。为进行评估，作者在保持解释不变的情况下反转资格认定，创建了配对实例以测试法律矛盾。

• 验证准确率：该系统在区分法律上一致（SAT）与不一致（UNSAT）的解释方面，整体达到了**97.7%**的准确率。
• 定位精度：当检测到不一致（UNSAT）时，系统成功定位了所涉的具体法定条款。
  • 定位 F1 分数：因类别而异，范围从0.51（收入）到0.83（公民身份），在适用定位的 UNSAT 案例中，整体平均值为0.977。
  • 规则更为确定的类别（公民身份、居住地）比具有语境细微差别的类别（收入、学生身份）显示出更高的检索准确率。
• 案例研究：在一个具体案例中，福利终止的理由是“总收入超过限额”，系统确认该解释为 SAT。当将认定结果反转为“符合资格”而保持解释不变时，系统正确返回 UNSAT，并识别出 MPP §63-409.111 为被违反的条款。

5. 意义与主张

作者声称，这项工作为将法律问责制嵌入公共部门人工智能的技术基础提供了概念验证。

• 制度支撑：该系统的设计目的并非取代行政自由裁量权或自动化法律判决，而是作为“制度支撑”，加强监督和可争议性。它自动化的是理由的验证，而非决策本身。
• 治理优于透明度：本文将可解释性重新框架化为治理挑战。它提出，对于公共算法，解释必须超越揭示统计关联；它们必须阐明决策的法律依据，以满足正当程序权利。
• 适用性：无论底层决策引擎是预测性、基于规则的还是混合型的，该框架均适用，因为它评估的是向申请人发出的解释层。
• 局限性：作者谦逊地指出，该系统依赖于针对特定任务的法规形式化，无法完全捕捉开放纹理的标准或自由裁量判断。评估使用了受控的单一法律案例以确保归因清晰，这意味着涉及多个相互作用法规的现实世界复杂性可能会带来额外挑战。该系统是问责基础设施的技术工具，而非整体法律判决的替代品。

总之，本文证明，通过神经符号方法，解释级的法律问责制在计算上是可行的，这为机构、监督机构和个体提供了一种机制，以评估自动化理由是否满足法定要求。