💻 computer science

Neuro-Symbolic AI for Korean Criminal Law: Sentencing Prediction and Document Drafting

本文提出了一种神经符号人工智能框架，该框架将用于语义提取的大型语言模型与用于确定性法定计算的可满足性模理论（SMT）求解器相结合，以增强韩国交通违法行为判刑预测和文书起草的准确性与可靠性，从而减轻纯神经法律系统中固有的幻觉风险。

原作者： Yeonseok Lee

发布于 2026-07-23

📖 1 分钟阅读☕ 轻松阅读

原作者： Yeonseok Lee

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一个这样的世界：计算机就像是才华横溢但有点丢三落四的大厨。它们能在一秒钟内读完一千个食谱，理解一道菜的风味，甚至能为一颗西红柿写下一首优美的诗。这就是人工智能的领域，特别是被称为**大语言模型（LLMs）**的一种类型。这些数字大厨非常擅长理解语言，但它们有一个棘手的习惯：有时在被要求进行精确计算或遵循严格规则时，它们会产生“幻觉”。它们可能会自信满满地告诉你，一颗西红柿的价格是 500 美元，仅仅因为这听起来像是个合理的数字，尽管食谱上明明写着是 5 美元。在现实世界中，这对于写故事来说没问题，但在法庭上——在那里，一个错误可能意味着一个人失去自由或支付错误的罚款——“接近正确”是远远不够的。

这就是**神经符号人工智能（Neuro-Symbolic AI）**发挥作用的地方。你可以把它想象成那位创意十足、丢三落四的大厨与一位极其严谨、恪守规则的会计师之间的联手。大厨阅读凌乱的笔记并理解故事，而会计师则负责计算数学并检查规则，以确保一切都完美契合。这篇论文探讨了如何构建这样一个梦幻组合，来帮助韩国检察官处理成千上万的轻微交通案件（如酒驾），而不至于让他们应接不暇或犯下危险的错误。

问题所在：票据太多，人力不足

在韩国，法律体系为轻微犯罪设有专门的快速通道，称为简易程序（或 guyaksik）。想象一下，在高速公路上，警察抓获了数百名犯有轻微罪行的驾驶员，例如无证驾驶、造成轻微擦碰或饮酒过量。为了避免为每一个案例都举行正式审判，检察官只需审查文件并开具罚单。这很高效，但也产生了一座堆积如山的文书工作。检察官们正淹没在警察报告、酒精测试记录和证人陈述的堆叠之中。他们需要一种方法，将这些凌乱的、手写的或扫描的文件转化为清晰且在数学上完美的法律决策。

陷阱：为什么聪明的计算机也会卡壳

最近，人们尝试使用那些“丢三落四的大厨”型计算机（LLMs）来解决这个问题。这些计算机非常擅长阅读警察报告并说：“啊，这个人的血液酒精含量是 0.12%，并且撞到了隔离栏。”但当被要求根据复杂的法律计算确切的罚款金额时，计算机就开始瞎猜了。它可能会算错数字，或者发明一个并不存在的规则。在刑事法律中，你不能让计算机进行猜测。如果数学错了，司法系统就会崩溃。该论文认为，我们不能依赖这些计算机自行进行计算；它们太容易编造事实了。

解决方案：大厨与会计师的搭档

作者提出了一种神经符号框架（Neuro-Symbolic framework），这是一种高级说法，意指他们将工作拆分为两个截然不同的部分，以获取两者的优点。

第一步：大厨（LLM）
首先，系统获取那些凌乱的、非结构化的文档——比如酒精测试结果或警察的笔记——并将它们输入给 LLM。LLM 的唯一任务是充当“语义提取器”。它阅读故事并提取出重要的事实：“驾驶员的血液酒精含量为 0.12”、“他们撞到了中央隔离带”以及“他们没有前科”。它将这些事实放入一个整齐的结构化列表（如 JSON 文件）中。至关重要的是，LLM 此时不允许进行罚款计算。它只是在收集食材。

第二步：人类检查员（安全检查）
在进行数学计算之前，一名真正的检察官会查看这份清单。系统会高亮显示计算机在原始文档中找到每个事实的具体位置。人类点击按钮表示：“是的，这是正确的，”或者“不，那是错的。”这被称为人机回环（Human-in-the-Loop, HITL）。这确保了计算机不会编造出未经人类验证的事实。只有经过人类批准的事实才能进入下一步。

第三步：会计师（Z3 求解器）
现在，经过验证的事实会被交给“会计师”，这是一个被称为 Z3 满足性模理论（SMT）求解器的软件。这不是一个瞎猜的机器；它是一个数学证明引擎。它接收人类批准的事实，并将其运行通过**《2026 年交通违法行为量刑指南》**的严格规则。

如果血液酒精含量在 0.08 到 0.20 之间，计算机必须将其归类为“类型 3”。
如果驾驶员撞到了隔离带，计算机必须增加一项“加重情节”。
然后，它进行实际的数学运算，以确定罚款范围。

因为这一部分是纯粹的逻辑和数学，所以它不可能产生幻觉。如果规则规定罚款在 5,000,000 到 8,000,000 韩元之间，那它输出的结果必然完全一致。如果数学逻辑不通（例如，如果人类不小心批准了两个相互矛盾的事实），会计师会停止运行并提示：“错误！出问题了，”然后将案件发回给人类进行修正。

结果：一份完美的起草文件

一旦会计师得出了最终数字，系统最后一次回到“大厨”（LLM）那里。这一次，LLM 被给予了确切的数学结果，并被要求撰写最终的法律文件，例如简易起诉书请求。LLM 会按照规范的法律格式撰写文件，但它直接从会计师的结果中复制罚款金额。它不进行任何计算，只是在讲述故事。

这对未来意味着什么

论文表明，这种方法在理论上是行得通的，并且创建了一个既快速又安全的流程。它表明，通过让“富有创造力”的 AI 远离“数学”，并让人类检查其工作，我们可以在不冒出错风险的前提下，实现法律系统枯燥环节的自动化。

作者谨慎地指出，这目前是他们设计并进行逻辑测试的一个框架。他们还没有将其推广到韩国的每个警察局。然而，他们计划开发完整的软件并使用真实数据进行测试。如果成功，这个系统最终不仅可以处理酒驾，还可以处理其他轻微犯罪，如简单殴打、轻微盗窃或网络侮辱，从而在确保每一笔罚款都经过数学精准计算的同时，帮助检察官清理他们的案头。这是一种让计算机承担繁重体力活，同时让把控方向盘的权利始终留在人类手中的方式。

技术摘要：面向韩国刑事法律的神经符号人工智能（Neuro-Symbolic AI）

1. 问题陈述

韩国刑事司法系统高度依赖简易程序（guyaksik）来加速处理大量轻微违规案件，特别是涉及简单酒驾（DUI）、无证驾驶和轻微交通事故等交通违法行为。虽然这种机制提高了司法吞吐量，但也给检察官带来了沉重的行政负担，因为他们必须手动将非结构化法律文件（如酒精检测日志、警察报告、审讯记录）转化为确定性的法定结果。

大型语言模型（LLMs）的最新进展已展示了从密集法律文本中进行语义提取的强大能力。然而，将纯 LLM 用于**法律判决预测（LJP）**存在根本性的局限性：

概率性质： LLM 基于概率生成文本，这并不适用于法定罚金计算所需的严格算术和基于规则的推理。
幻觉风险： 在要求完全确定性的法律语境下，当面对复杂的数学约束或特定的法定阈值时，LLM 经常产生“幻觉”。
缺乏形式化验证： 纯神经架构无法在数学上证明判决结果的有效性，因此不足以直接应用于对随机误差容忍度极低的司法应用场景。

2. 方法论

作者提出了一种神经符号框架，旨在将非结构化法律事实与形式化验证相连接。该架构将任务严格划分为神经语义理解和符号逻辑推理，并组织为五个模块的流水线：

模块 1：原始数据摄取

系统摄取异构且具有复杂布局的证据文件（DUI 情况说明、酒精检测结果、审讯记录和事故报告）。它采用一种结合了自定义基于规则的 OCR 和双向编码器文本分割的混合布局感知摄取协议，将叙述部分从表格索引和元数据中分离出来，并将其转换为干净的文本流。

模块 2：LLM 提取

LLM 作为语义解析器，用于提取核心案件要素（犯罪类型、连续变量如血液酒精浓度 (BAC) 以及离散分类变量）。

约束： LLM 在结构上受到限制，必须将每个提取的要素直接映射到其精确的文本来源（“参考文本”），以强化法律三段论并确保溯源性。
输出： 提取的实体被填充到一个中间 JSON Schema 中，作为概率提取与确定性逻辑之间的桥梁。

模块 3：人机回环（HITL）验证

为了确保法律合规性和正当程序，在进行任何计算之前，引入了一个强制性的验证阶段。

界面： 分屏 UI 同时显示结构化的 JSON 输出以及带有高亮参考文本的原文档。
机制： 所有提取的变量默认设为 is_valid_by_human = false。法律从业者必须显式验证每个要素，将其切换为 true。
数据溯源： 只有经过人类显式验证的参数才会转发至求解器，从而确保系统作为决策支持工具而非自主决策者运行。

模块 4：逻辑转换与 Z3 SMT 求解器

这是核心的神经符号桥梁。经过验证的 JSON 字段被映射到 Z3 可满足性模理论（SMT）求解器中的形式化状态变量（布尔标志和整数约束）。

公理建模： 将 《2026 年交通犯罪量刑指南》 公式化为数学公理。例如，BAC 阈值被建模为条件约束（例如， $0.08 \le BAC < 0.20 \implies Crime\_Category = 3$ ）。
区间推导： 求解器评估减轻和加重情节的布尔数组，通过求和来确定量刑区间（基础、减轻或加重）。
强制监禁逻辑： 求解器检查复合逻辑约束（例如，如果前科 $\ge 3$ 或加重情节占主导地位），以用强制监禁建议覆盖罚金计算。
可满足性检查： 在输出结果之前，Z3 执行 SAT 检查，以确保不存在逻辑矛盾（例如，一个案件不能既是“减轻”又是“加重”）。如果检测到 UNSAT 状态，流水线将返回 HITL 界面进行冲突解决。

模块 5：可视化与文档生成

来自 Z3 求解器的确定性输出被转化为可操作的产物：

量刑树可视化： 系统将逻辑决策路径（从 BAC 分类到最终罚金）渲染为可视化树，提供可解释的审计追踪。
文档起草： 使用严格结构的提示词，LLM 生成符合法律规范的文件（警察调查报告、移送意见书和简易起诉书请求）。至关重要的是，罚金额度是逐字从 Z3 求解器输出中注入的，以防止 LLM 进行重新计算或产生数字幻觉。

3. 主要贡献

本文概述了三个主要贡献：

神经符号流水线设计： 一个将非结构化警察和检察记录转化为确定性法律结果的框架，特别通过将 LLM 隔离在语义提取阶段，来降低罚金计算过程中的幻觉风险。
人机回环（HITL）验证： 一种透明的方案，将提取的法律变量锚定到来源参考文本，在保持检察官最终法律权威的同时，确保了人类监督和可解释性。
形式化法律逻辑框架： 构建了一个使用 Z3 SMT 求解器的逻辑框架，用于计算与 2026 年量刑指南一致的精确量刑范围，以数学证明取代概率生成。

4. 结果与主张

本文并未呈现经验性能指标（例如在测试集上的准确率百分比），因为研究重点在于该架构的理论构建与逻辑映射。相反，作者基于设计提出了以下主张：

确定性： 通过将法定计算交给定理证明器，系统保证了量刑结果不会出现 LLM 固有的随机误差。
鲁棒性： SAT 检查机制确保逻辑矛盾在生成判决前被检测并解决，从而防止无效的法律结果。
问责制： HITL 集成确保了系统作为一个可验证的辅助工具，解决了“黑箱”AI 模型固有的透明度问题。

5. 意义

作者将这项工作定位为高风险环境下法律判决预测（LJP）的一次必要演进。通过承认 LLM 在算术和严格规则遵循方面的不足，本文提出了一种混合方法，既利用了神经网络的语义优势，又依靠符号逻辑处理法律的“硬”约束。

其意义在于，它有可能在不损害司法公正的前提下，缓解韩国轻微检察案件的行政瓶颈。该框架提供了一条实现自动化起草简易起诉书（yaksik-gongsojang）的路径，同时确保每一个数学结果都基于经过形式化验证、经由人类验证的事实。作者指出，虽然目前侧重于交通犯罪，但该架构具备扩展到其他轻微犯罪（如简单殴打、诽谤、轻微盗窃）的可扩展性，这些犯罪同样以简易程序结案。