在自回归强化学习策略中注入LTLf约束的神经符号方法

# 自回归强化学习策略中LTLf约束的神经符号注入
来源：https://arxiv.org/html/2606.08312
\\copyrightclause

本文版权归作者所有。依据知识共享署名4.0国际许可协议（CC BY 4.0）允许使用。

\\conference

逻辑、学习、伦理决策与大语言模型的统计与知识融合联合研讨会（SKILLED-LLMs 2026）

[orcid=0009-0005-9247-1786, [email protected] ]

[orcid=0009-0004-9547-7115, [email protected] ]

[orcid=0000-0002-5639-6038, [email protected] ]

[orcid=0000-0002-9116-251X, [email protected] ]

Matteo MancanelliElena UmiliFabio Patrizi

（2022年）

###### 摘要

本文研究了在有限迹线性时序逻辑（LTLf\\textsc{LTL}_{f}）表达的时序扩展任务约束下的离线强化学习（RL）。近期，基于Transformer的方法（如轨迹Transformer（Trajectory Transformers）和决策Transformer（Decision Transformers））被用于将RL建模为序列建模问题。然而，这些方法仅针对奖励进行优化，未考虑高层次的时间需求。本文提出一个神经符号框架，将LTLf\\textsc{LTL}_{f}背景知识注入到此类基于Transformer的RL策略中。我们的方法将LTLf\\textsc{LTL}_{f}公式编译为确定性有限自动机（DFA），并通过可微表示和基于逻辑的损失函数将其整合到学习过程中。具体而言，我们从DFA进展中推导出可微的满足信号，并在训练中将其用作正则化项。所得方法在不同模型下具有架构无关性。我们在包含安全性和可达性时间属性组合的规范套件的导航环境中评估所提出的框架。实验结果表明，融入背景知识不仅能提升约束满足程度，还能在与原始基线方法相比时保持具有竞争力的回报。

###### 关键词：

安全强化学习\\sep神经符号知识注入\\sep线性时序逻辑

## 1 引言

在强化学习（RL）[sutton1998reinforcement]中，安全是一个核心关注点，尤其是在机器人、自主导航和决策支持系统等现实世界或安全关键环境中，这些环境中不良行为可能导致不可逆的损害、经济损失或人身伤害[safe_rl_survey]。确保学习的策略遵守一些用户定义的约束，对于提高系统的正确性和可靠性至关重要。这一挑战在离线RL[offline_rl_survey]中尤为突出，因为策略仅从预先收集的数据中学习，无法依赖在线交互来检测和纠正不安全行为。

安全决策通常需要*时间扩展*的约束，而非纯局部或瞬时约束[prob_shielding_AAAI25]。许多需求无法通过单一状态-动作对来验证，而只能在整个轨迹上验证。例如，考虑这样的规约：*“最终到达目标，同时始终避免危险”*。该需求结合了两种时间模态：（i）*活性*条件（必须在情节结束前某个时刻到达目标），以及（ii）*安全性*条件（在任何之前的时间步都不能访问危险状态）。一个短暂踩到危险（即使之后到达目标）的策略违反了规约。一个始终保持安全但从未到达目标的策略也失败。因此，满足性取决于*整个迹*，而非仅局部奖励最大化。

在*离线强化学习（RL）*中，强制此类约束尤其具有挑战性。由于不允许在线交互，无法通过试错探索来纠正违反约束的行为。基于序列模型的策略——如轨迹Transformer（Trajectory Transformers, TTs）[trajectory_transformers]和决策Transformer（Decision Transformers, DTs）[decision_transformers]——在此设置中具有吸引力，因为它们自回归地生成轨迹，并自然地对长程依赖进行建模。然而，它们作为概率序列生成器运行，而任务和安全需求通常用形式逻辑规约来表示。这在生成建模与符号正确性保证之间造成了差距。

本文采用有限迹线性时序逻辑（LTLf\\textsc{LTL}_{f}）[LTLf]作为规约语言，研究用于离线Transformer策略的*符号约束注入*[UmiliPMAI24,mezini2025neuro]。LTLf\\textsc{LTL}_{f}提供了一种自然语言来表达情节性任务中无歧义的时间需求。我们将LTLf\\textsc{LTL}_{f}公式编译为确定性有限自动机（DFAs），并通过训练时的正则化，将生成的自动机整合到策略流水线中，利用从自动机进展导出的可微软满足信号。我们的框架支持不同的基于Transformer的RL架构（如TT和DT），通过一个共享接口抽象掉架构差异，因此在自回归序列模型类中是架构无关的。将我们的方法扩展到测试时的自动机感知约束解码也是可能的，其中生成被限制为与逻辑规约一致的动作序列，但这留待未来研究。

我们在导航环境ColourBomb[prob_shielding_AAAI25]中的时间扩展任务上评估了所提出的方法。考虑的规约涵盖不变安全性、可达性以及组合的“安全到达”目标。结果部分系统地展示了该方法的行为：逻辑正则化在TT和DT中的效果、性能与逻辑满足性之间的跨基准权衡，以及运行时开销。总结而言，我们做出如下贡献：

- • 一个统一的神经符号离线序列RL框架，用于通过自动机模块将LTLf\\textsc{LTL}_{f}约束注入基于Transformer的策略，这些模块是架构无关的。
- • 一个规范的有限迹评估栈，确保在（i）数据集序列化、（ii）令牌到符号映射以及（iii）逻辑评估之间保持一致的结束语义，从而防止模型训练与时态逻辑评估之间的语义不匹配。
- • 在导航领域中针对多样化时间规约的实证评估，突出性能与约束满足性之间的权衡。

## 2 背景

### 2.1 有限迹线性时序逻辑

线性时序逻辑（LTL）[LTL]是一种形式语言，通过模态算子扩展传统命题逻辑，允许指定必须*随时间*保持的规则。本文使用有限迹上的LTL（LTLf\\textsc{LTL}_{f}）[LTLf]，这是LTL的一个流行变体，对有限但长度无界的执行迹进行建模，因此适用于有限视界问题。给定原子命题的有限集Σ\\Sigma，LTLf\\textsc{LTL}_{f}公式φ\\varphi的归纳定义如下：

φ::=⊤∣⊥∣a∣¬φ∣φ1∧φ2∣Xφ∣φ1Uφ2,\\varphi::=\\top\\mid\\bot\\mid a\\mid\\lnot\\varphi\\mid\\varphi_{1}\\land\\varphi_{2}\\mid X\\varphi\\mid\\varphi_{1}U\\varphi_{2},其中a∈Σa\\in\\Sigma。我们用⊤\\top和⊥\\bot分别表示TrueTrue和FalseFalse。XX（强Next）和UU（Until）是时态算子。其他时态算子有NN（弱Next）和RR（Release），分别定义为Nφ≡¬X¬φN\\varphi\\equiv\\neg X\\neg\\varphi和φ1Rφ2≡¬(¬φ1U¬φ2)\\varphi_{1}R\\varphi_{2}\\equiv\\neg(\\neg\\varphi_{1}U\\neg\\varphi_{2})；GG（全局）Gφ≡⊥RφG\\varphi\\equiv\\bot R\\varphi；以及FF（最终）Fφ≡⊤UφF\\varphi\\equiv\\top U\\varphi。

迹σ=(σ1,σ2,...,σT)\\boldsymbol{\\sigma}=(\\sigma_{1},\\sigma_{2},\\dots,\\sigma_{T})是命题真值的序列赋值给Σ\\Sigma中的命题，其中σt∈2Σ\\sigma_{t}\\in 2^{\\Sigma}是在时刻tt为真的所有命题的集合。此外，|σ|=T|\\boldsymbol{\\sigma}|=T表示迹的长度。由于每条迹都是有限的，|σ|<∞|\\boldsymbol{\\sigma}|<\\infty；ε\\varepsilon表示空迹。注意，如果Σ\\Sigma中的命题符号都是*互斥*的，即域在每个步骤恰好产生一个真符号，则我们有σt∈Σ\\sigma_{t}\\in\\Sigma。令last=|σ|−1last=|\\boldsymbol{\\sigma}|-1。我们归纳定义LTLf\\textsc{LTL}_{f}公式φ\\varphi在时刻ii（其中0≤i≤last0\\leq i\\leq last）为真，记作σ,i⊧φ\\boldsymbol{\\sigma},i\\models\\varphi，如下：

- •σ,i⊧a\\boldsymbol{\\sigma},i\\models a当且仅当a∈σia\\in\\sigma_{i}，对于a∈Σa\\in\\Sigma；
- •σ,i⊧¬φ\\boldsymbol{\\sigma},i\\models\\neg\\varphi当且仅当σ,i⊧̸φ\\boldsymbol{\\sigma},i\\not\\models\\varphi；
- •σ,i⊧φ1∧φ2\\boldsymbol{\\sigma},i\\models\\varphi_{1}\\land\\varphi_{2}当且仅当σ,i⊧φ1\\boldsymbol{\\sigma},i\\models\\varphi_{1}且σ,i⊧φ2\\boldsymbol{\\sigma},i\\models\\varphi_{2}；
- •σ,i⊧Xφ\\boldsymbol{\\sigma},i\\models X\\varphi当且仅当i<lasti<last且σ,i+1⊧φ\\boldsymbol{\\sigma},i+1\\models\\varphi；
- •σ,i⊧φ1Uφ2\\boldsymbol{\\sigma},i\\models\\varphi_{1}\\mathop{\\{\\mathcal{U}\\}}\\varphi_{2}当且仅当存在某个jj使得i≤j≤lasti\\leq j\\leq last，有σ,j⊧φ2\\boldsymbol{\\sigma},j\\models\\varphi_{2}，并且对所有kk满足i≤k<ji\\leq k<j，有σ,k⊧φ1\\boldsymbol{\\sigma},k\\models\\varphi_{1}。

我们说σ\\boldsymbol{\\sigma}满足φ\\varphi，记作σ⊧φ\\boldsymbol{\\sigma}\\models\\varphi，如果σ,0⊧φ\\boldsymbol{\\sigma},0\\models\\varphi。公式φ\\varphi是可满足的，如果它关于某个迹σ\\boldsymbol{\\sigma}为真；是有效的，如果它关于每个迹σ\\boldsymbol{\\sigma}为真。

任何LTLf\\textsc{LTL}_{f}公式φ\\varphi都可以转化为一个确定性有限自动机（DFA）[LTLf]Aφ=(2Σ,Q,q0,δ,F)A_{\\varphi}=(2^{\\Sigma},Q,q_{0},\\delta,F)，其中2Σ2^{\\Sigma}是自动机字母表，QQ是有限状态集，q0∈Qq_{0}\\in Q是初始状态，δ:Q×2Σ→Q\\delta:Q\\times 2^{\\Sigma}\\rightarrow Q是转移函数，F⊆QF\\subseteq Q是最终状态集。此外，我们在迹上递归定义扩展转移函数δ∗:Q×(2Σ)∗→Q\\delta^{*}:Q\\times(2^{\\Sigma})^{*}\\rightarrow Q为：

δ∗(q,ε)=qδ∗(q,σ⋅x)=δ∗(δ(q,σ),x),\\begin{array}[]{l}\\delta^{*}(q,\\epsilon)=q\\\\ \\delta^{*}(q,\\sigma\\cdot\\boldsymbol{x})=\\delta^{*}(\\delta(q,\\sigma),\\boldsymbol{x}),\\end{array}(1)其中σ∈2Σ\\sigma\\in 2^{\\Sigma}是一个符号，x∈(2Σ)∗\\boldsymbol{x}\\in(2^{\\Sigma})^{*}是一个迹。自动机接受迹σ\\boldsymbol{\\sigma}}当且仅当δ∗(q0,σ)∈F\\delta^{*}(q_{0},\\boldsymbol{\\sigma})\\in F，此时我们说σ\\boldsymbol{\\sigma}属于自动机的语言，记作L(Aφ)L(A_{\\varphi})。我们有φ\\varphi与AφA_{\\varphi}等价，因为对于任何迹σ∈(2Σ)∗\\boldsymbol{\\sigma}\\in(2^{\\Sigma})^{*}：

σ∈L(Aφ)⇔σ⊨φ。\\boldsymbol{\\sigma}\\in L(A_{\\varphi})\\iff\\boldsymbol{\\sigma}\\vDash\\varphi。(2)

### 2.2 离线强化学习

在强化学习（RL）中，智能体与环境的交互通常建模为马尔可夫决策过程（MDP）[sutton1998reinforcement]，由元组(S,A,t,r,γ)(S,A,t,r,\\gamma)定义，其中SS是状态集，AA是动作集，t:S×A×S→[0,1]t:S\\times A\\times S\\rightarrow[0,1]是转移函数，满足∑s′∈St(s,a,s′)=1\\sum_{s^{\\prime}\\in S}t(s,a,s^{\\prime})=1，r:S×A→Rr:S\\times A\\rightarrow R是奖励函数，γ∈[0,1]\\gamma\\in[0,1]是折扣因子。策略π:S→A\\pi:S\\rightarrow A将状态映射到动作，而值函数Vπ(s)V^{\\pi}(s)表示从状态ss开始遵循π\\pi所获得的期望折扣回报。RL智能体的目标是学习最大化期望折扣回报的最优策略π∗\\pi^{*}。

传统RL方法假设训练期间可直接与环境交互。智能体通过执行动作、观察状态转移和奖励来收集经验，并相应更新其策略。这种在线交互范式使得迭代改进成为可能，但在现实应用中可能代价高昂、不安全甚至不可行。这推动了离线RL的研究[offline_rl_survey]，其中智能体获得由某个（未知）行为策略生成的固定轨迹数据集D{\\mathcal{D}}，并必须在不与环境进一步交互的情况下学习策略。为了防止超出分布数据的问题，许多离线RL算法引入了机制，将学习的策略约束在接近数据分布的支持范围内[kumar2020conservative]。

### 2.3 强化学习作为序列建模

一些工作[trajectory_transformers,decision_transformers]提出了RL的另一种视角，将其视为序列建模问题而非价值估计。在[trajectory_transformers]中，轨迹被视为一系列令牌，自回归模型用于学习序列中的下一个令牌。假设我们有NN维状态和MM维动作。一个视界为TT的轨迹τ\\boldsymbol{\\tau}可以表示为

τ=(s11,s12,...,s1N,a11,...,a1M,r1,s21,...,rT)\\boldsymbol{\\tau}=(s_{1}^{1},s_{1}^{2},...,s_{1}^{N},a_{1}^{1},...,a_{1}^{M},r_{1},s_{2}^{1},...,r_{T})(3)所有令牌的下标表示时间步，状态和动作的上标表示维度（即stis_{t}^{i}是时刻tt状态的ithi^{\\text{th}}维度）。自回归模型能够估计在已知所有过去令牌x<t\\boldsymbol{x_{<t}}的条件下，第ttht^{\\text{th}}个令牌xtx_{t}的概率：

P(xt∣x1,x2,...,xt−1)=P(xt∣x<t)。P(x_{t}\\mid x_{1},x_{2},\\dots,x_{t-1})=P(x_{t}\\mid\\boldsymbol{x_{<t}})。(4)我们可以不学习价值函数或策略，而是学习联合分布

P(x)=∏i=1|τ|P(xi∣x<i)。P(\\boldsymbol{x})=\\prod_{i=1}^{|\\tau|}P(x_{i}\\mid\\boldsymbol{x_{<i}})。(5)
在每个生成步骤，必须从下一个行为概率中*采样*一个令牌。一种常见的选择下一个令牌的方法是*贪婪地*选择，即在每一步最大化下一个令牌概率，如下所示：

xt=argmaxxP(xt∣x<t),∀t<|τ|。{x}_{t}=\\operatorname*{argmax}_{x}P(x_{t}\\mid\\boldsymbol{x}_{<t}),\\quad\\forall t<|\\tau|。(6)通常，这种贪婪搜索策略是次优的，因为它可能不会产生最大化方程5中联合概率分布的迹。其他常用的次优采样策略包括束搜索、随机采样和温度采样[ramamaneiro24]。

轨迹Transformer（TT）模型是基于Transformer的自回归架构，非常适合将RL作为序列建模处理。在离线设置中，此类模型可以通过教师强制进行最大似然训练，即最大化数据集中轨迹的对数概率。在推理时，规划可以通