一种用于基于ASP的合规推理的规范性中间表示

# 基于ASP合规推理的规范化中间表示

**来源：** https://arxiv.org/html/2506.04619

###### 摘要

我们提出MONIR——一种用于基于ASP的合规推理的模态化输出规范中间表示（Modalized-Output Normative Intermediate Representation）。其核心片段具有分阶段操作语义，而MONIR-ASP则提供了可执行的编译实现，并支持外部函数、时态规则和稳定模型推理的扩展。我们以中国ADAS法规和标准为基础实例化该框架，并构建了一个LLM辅助的处理流程。实验对提取质量以及模块化和增量式ASP求解的效率进行了评估。

## 引言

技术标准的合规检查需要对规范条款进行可执行且可解释的表示。这一任务颇具挑战性，因为标准往往将事实条件与模态性、例外、补偿、冲突和不确定性相结合。尽管LLM能够从文本中提取结构化规则，符号推理仍需要一个稳定的中间表示。回答集编程（ASP）[Brewka et al. 2011](https://arxiv.org/html/2606.04619#bib.bib8) 是完成这一任务的合适后端。近期研究也报告了求解器在合规检查任务中的出色表现 [Robaldo et al. 2024](https://arxiv.org/html/2606.04619#bib.bib9)。然而，直接在ASP中对标准进行编码往往会将条件、模态性、目标、豁免和违规等角色隐藏在实现谓词中，使得LLM生成的规则库难以检查、修复和解释。

本文提出MONIR，即模态化输出规范中间表示（Modalized-Output Normative Intermediate Representation）。MONIR部分受到条件规范的输入-输出视角 [Makinson and van der Torre 2000](https://arxiv.org/html/2606.04619#bib.bib1) 的启发，但并不旨在成为完整的道义逻辑。它是一种受限的中间语言，用于连接LLM辅助的规范提取与基于ASP的合规推理。MONIR规则将规范适用的条件与其产生的模态化目标分离，并将豁免视为规则级别的输出，而非道义模态。

参见图1：所提框架的整体工作流程。自然语言标准被转换为MONIR规则库，而配置表单被编译为ASP事实。MONIR-ASP通过模块化和增量式求解执行推理任务，并输出违规情况、冲突、未知状态、解释和合规状态。

[图1](https://arxiv.org/html/2606.04619#Sx1.F1) 展示了整体工作流程。规范提取通道将标准条款映射为MONIR规则；事实准备通道将配置表单映射为ASP事实。所得对象被编译为MONIR-ASP，其中命题模块和规范模块可在ASP模块定理 [Oikarinen and Janhunen 2006](https://arxiv.org/html/2606.04619#bib.bib11) 下分别进行评估和更新。当用户确认的更新到达时，系统复用未受影响的模块结果，并通过多步ASP求解 [Gebser et al. 2019](https://arxiv.org/html/2606.04619#bib.bib10) 重新求解受影响部分。

本文作出三项贡献。第一，定义MONIR-core，包括其语法、可接受条件、分阶段操作语义及基本元理论性质。第二，给出MONIR-ASP，即MONIR的可执行ASP实现，并支持外部命题函数、时态编码以及超越核心片段的稳定模型语义扩展。第三，实现了一个LLM辅助的ADAS合规检查流程，并对提取质量和求解效率进行评估。

## 预备知识

本节回顾本文所使用的背景知识：用于基于规则推理的ASP，以及用于将法规文本映射为结构化规则的LLM辅助提取。

### 回答集编程

回答集编程（ASP）是一种声明式框架。项（term）是常量、变量或函数项。若项中不含变量，则称其为基项（ground term）。若 $p$ 是一个 $n$ 元谓词符号，$t_1, \ldots, t_n$ 是项，则 $p(t_1, \ldots, t_n)$ 是一个原子。对于基程序 $\Pi$，令 $\mathsf{At}(\Pi)$ 为 $\Pi$ 中出现的所有基原子的集合。解释是集合 $X \subseteq \mathsf{At}(\Pi)$。

一条正常规则 $r$ 的形式为：

$$a_0 \leftarrow a_1, \ldots, a_m, \mathsf{not}\ a_{m+1}, \ldots, \mathsf{not}\ a_n.$$

其中 $\mathsf{not}$ 表示失败即否定（negation as failure）。记 $H(r) = \{a_0\}$，$B^+(r) = \{a_1, \ldots, a_m\}$，$B^-(r) = \{a_{m+1}, \ldots, a_n\}$。完整性约束是头部为空的规则，写作：

$$\leftarrow B.$$

它消除满足 $B$ 的解释。

对于基正常程序，稳定模型语义由Gelfond–Lifschitz归约 [Gelfond and Lifschitz 1988](https://arxiv.org/html/2606.04619#bib.bib7) 定义。给定解释 $X$，$\Pi$ 关于 $X$ 的归约为：

$$\Pi^X = \{H(r) \leftarrow B^+(r) \mid r \in \Pi,\ B^-(r) \cap X = \emptyset\}.$$

$\Pi$ 的稳定模型集合记为 $\mathsf{SM}(\Pi)$，定义为：

$$X \in \mathsf{SM}(\Pi)\ \text{当且仅当}\ X \text{ 是 } \Pi^X \text{ 的 } \subseteq\text{-极小模型。}$$

对于非基程序 $\Pi$ 和输入事实 $F$，基化得到 $\mathsf{gr}(\Pi, F)$，求解计算 $\mathsf{SM}(\mathsf{gr}(\Pi, F))$。

为支持分阶段和模块化计算，我们使用ASP模块 [Oikarinen and Janhunen 2006](https://arxiv.org/html/2606.04619#bib.bib11)。模块是元组 $\mathcal{P} = \langle R, I, O, H \rangle$，其中 $R$ 是规则集，$I$、$O$、$H$ 分别是两两不相交的输入、输出和隐藏签名。$R$ 中的头部原子属于 $O \cup H$。对于 $V \subseteq I$，令 $R[V] = R \cup \{a \leftarrow \mid a \in V\}$。$\mathcal{P}$ 在 $V$ 下的稳定模型为：

$$\mathsf{SM}(\mathcal{P}, V) = \{X \in \mathsf{SM}(R[V]) \mid X \cap I = V\}.$$

两个模块 $\mathcal{P}_1 = \langle R_1, I_1, O_1, H_1 \rangle$ 和 $\mathcal{P}_2 = \langle R_2, I_2, O_2, H_2 \rangle$ 可连接（joinable），若满足：

1. $O_1 \cap O_2 = \emptyset$；
2. $H_1 \cap \mathsf{At}(\mathcal{P}_2) = \emptyset$ 且 $H_2 \cap \mathsf{At}(\mathcal{P}_1) = \emptyset$；
3. 正依赖图中不存在同时包含 $O_1$ 和 $O_2$ 中输出原子的强连通分量。

此处，正依赖图使用从头部到正体部原子的有向边；条件3禁止跨模块的正递归，但允许负依赖。令 $\mathcal{P}_1 \sqcup \mathcal{P}_2$ 表示两个可连接模块的合成。两个局部结果 $X_1$ 和 $X_2$ 相容（记作 $X_1 \sim X_2$），当且仅当它们在共享可见原子上一致：

$$X_1 \cap \mathsf{At}(\mathcal{P}_2) = X_2 \cap \mathsf{At}(\mathcal{P}_1).$$

模块定理支持对可连接模块分别求解并合并相容的稳定模型。

### LLM辅助提取

大语言模型（LLM）通常被表述为自回归生成模型。给定上下文 $C$，参数化为 $\theta$ 的LLM按照以下概率生成输出序列 $y = (y_1, \ldots, y_T)$：

$$p_\theta(y \mid C) = \prod_{t=1}^{T} p_\theta(y_t \mid C, y_{<t}).$$

---

$$\mathsf{AtLeast}^X_0(\vec{x}) = \top, \quad \mathsf{AtLeast}^X_k(\vec{x}) = \bot \text{ 对于 } k > m,$$

$$\mathsf{Card}^X_{[l,u]}(\vec{x}) = \mathsf{AtLeast}^X_l(\vec{x}) \wedge \neg \mathsf{AtLeast}^X_{u+1}(\vec{x}).$$

基数在MONIR-core中没有独立的计数语义，其值由固定求值器 $\eta$ 作用于显式的 $\mathsf{AtLeast}$ 翻译所赋予。因此，不同的正则求值器可能对基数的未知值传播策略有所不同。

对命题集合 $\mathcal{P}$ 的输入解释是一个对 $I = \langle I^+, I^- \rangle$，满足 $I^+ \cap I^- = \emptyset$，并诱导：

$$\nu_I(p) = \begin{cases} \mathbf{t} & p \in I^+, \\ \mathbf{f} & p \in I^-, \\ \mathbf{u} & p \notin I^+ \cup I^-. \end{cases}$$

###### 定义4（可接受规则库）

设 $\mathcal{B} = \langle R_P, R_N \rangle$ 为一个良构的MONIR-core规则库。若存在映射 $\lambda_P: R_P \to \mathbb{N}$ 和 $\lambda_N: R_N \to \mathbb{N}$，使得以下条件成立，则称规则库 $\mathcal{B}$ 是**可接受的**（admissible）：

1. **（F-分层）** 对所有 $\rho, \rho' \in R_P$，若 $\mathsf{At}(\mathsf{head}(\rho')) \cap \mathsf{At}(\mathsf{body}(\rho)) \neq \emptyset$，则 $\lambda_P(\rho') < \lambda_P(\rho)$。
2. **（N-分层）** 对所有 $r, r' \in R_N$，若 $\mathsf{state}(s, \mathsf{id}(r')) \in \mathsf{St}(\mathsf{body}(r))$ 对某个 $s \in \mathcal{S}$ 成立，则 $\lambda_N(r') < \lambda_N(r)$。
3. **（E-可接受性）** 对所有 $r, r' \in R_N$，若 $\mathsf{out}(r) = \mathsf{exempt}(\mathsf{id}(r'))$，则 $\lambda_N(r) < \lambda_N(r')$。

F-分层防止命题规则体依赖于在同一或更高事实层次中推导的事实。N-分层使得依赖状态的规范规则只能读取在更低规范层次中固定的状态。E-可接受性强制执行非追溯豁免：豁免必须在目标规则被评估之前生成。

事实翻译 $\llbracket \cdot \rrbracket_F$ 通过以下方式扩展共享情形：

$$\llbracket \mathsf{count}_{[l,u]}(\ell_1, \ldots, \ell_m) \rrbracket_F = \mathsf{Card}^F_{[l,u]}(\ell_1, \ldots, \ell_m).$$

$\kappa$ 在 $I$ 下的事实值记为：

$$\nu_I^F(\kappa) = \eta(\llbracket \kappa \rrbracket_F, \nu_I).$$

###### 定义5（事实闭包）

设 $\mathcal{B} = \langle R_P, R_N \rangle$ 可接受，$I$ 为输入解释，$\lambda_P$ 为见证事实分层。对每个已占用的层次 $k$（按递增顺序），令：

$$R_P^k = \{\rho \in R_P \mid \lambda_P(\rho) = k\}.$$

---

**C1.** 若自动车道保持系统（ALKS）处于激活状态，且驾驶员未响应接管请求，系统**应**启动最小风险操作。

**C2.** 若C1适用且至少两个风险条件成立，则C3**应**适用。

**C3.** 当C3适用时，系统**应**满足所需的安全操作条件。

交叉引用被展开为事实触发：

$$c_1:\ \mathsf{alks\_active} \wedge \mathsf{tor\_timeout} \leadsto \mathsf{c1\_applies},$$

$$c_2:\ \mathsf{c1\_applies} \wedge \mathsf{count}_{[2,3]}\!\left(\begin{array}{l}\mathsf{shoulder\_unavailable},\\ \mathsf{obstacle\_ahead},\\ \mathsf{low\_visibility}\end{array}\right) \leadsto \mathsf{c3\_applies}.$$

对应的规范规则为：

$$n_1:\ \mathsf{c1\_applies} \Rightarrow \mathsf{O}(\mathsf{mrm}),$$

$$n_2:\ \mathsf{c3\_applies} \Rightarrow \mathsf{O}\!\left(\mathsf{count}_{[2,3]}\!\left(\begin{array}{l}\mathsf{reduce\_speed},\\ \mathsf{stay\_in\_lane},\\ \mathsf{audio\_warn}\end{array}\right)\right).$$

豁免可禁用原本适用的规则：

$$n_3:\ \mathsf{emergency\_evasion} \Rightarrow \mathsf{exempt}(n_2).$$

仅当 $n_3$ 在 $n_2$ 之前被评估时，此规则才是可接受的。

规范冲突在聚合阶段被检测：

$$n_4:\ \mathsf{obstacle\_ahead} \Rightarrow \mathsf{O}(\neg\mathsf{stay\_in\_lane}).$$

若某条激活规则同时要求 $\mathsf{stay\_in\_lane}$，则签名目标 $+\mathsf{stay\_in\_lane}$ 与 $+(\neg\mathsf{stay\_in\_lane})$ 在 $\perp_O$ 下冲突，从而影响 $\mathsf{HC}^*$ 和 $\mathsf{status}^*$。

未知证据通过规则状态表示：

$$n_5:\ \mathsf{heavy\_rain} \Rightarrow \mathsf{O}(\mathsf{reduce\_speed}).$$

若 $\mathsf{heavy\_rain}$ 为真且 $\mathsf{reduce\_speed}$ 在 $I^*$ 中未知，则 $\mathsf{state}(\mathsf{unknown}, n_5) \in \Sigma^*$。若 $\mathsf{heavy\_rain}$ 未知，则 $\mathsf{state}(\mathsf{pending}, n_5) \in \Sigma^*$，且 $n_5$ 不产生有效输出。

###### 示例2（违规与分阶段补救）

考虑如下一个程式化的碰撞响应需求：

> 若检测到前方碰撞风险，系统**应**发出碰撞警告。若警告未发出，系统**应**启动紧急制动。若紧急制动未启动，系统**应**请求最小风险操作并记录事件。

其表示为：

$$n_6:\ \mathsf{collision\_risk} \Rightarrow \mathsf{O}(\mathsf{collision\_warn}),$$

$$n_7:\ \mathsf{state}(\mathsf{violated}, n_6) \Rightarrow \mathsf{O}(\mathsf{emergency\_brake}),$$

$$n_8:\ \mathsf{state}(\mathsf{violated}, n_7) \Rightarrow \mathsf{O}(\mathsf{mrm\_log}).$$

规则 $n_6$ 是主要义务，$n_7$、$n_8$ 是补救性义务。可接受性要求 $\lambda_N(n_6) < \lambda_N(n_7) < \lambda_N(n_8)$。

局部补救结果从 $\Sigma^*$ 中读取。若 $\mathsf{collision\_warn}$ 为假且 $\mathsf{emergency\_brake}$ 为真，则：

$$\mathsf{state}(\mathsf{violated}, n_6) \in \Sigma^*,$$

$$\mathsf{state}(\mathsf{fulfilled}, n_7) \in \Sigma^*.$$

聚合状态仍为 $\mathsf{violated}$，而追踪记录中记录了一条已履行的补救义务。