强化学习状态抽象的组合行为语义
Compositional Behavioral Semantics for State Abstraction in Reinforcement Learning
https://arxiv.org/abs/2606.25357
摘要
状态抽象在将强化学习扩展到复杂但结构化的系统方面发挥着关键作用。在研究此类系统时，强化学习中已经研究了广泛的行为结构，包括价值函数、不变量、互模拟关系和行为度量。然而，对于确定哪些结构在状态抽象下可被证明得以保留，目前仍缺乏一个通用原则。在本文中，我们提出了一个用于定义和分析强化学习中行为结构的统一框架。该框架提供了一种组合式方法，可基于系统动力学的局部、单步描述来指定行为语义。利用该框架，我们建立了相关结果，展示了行为结构如何在抽象系统和具体系统之间安全地转移。我们进一步展示了如何从逻辑行为语义出发构造具有可靠性保证的定量度量。综合起来，这些结果为在强化学习中推理状态抽象下的行为提供了原则性基础，并为强化学习中一大类行为结构提供了可复用的定义和证明原则。
1. 引言
强化学习（Sutton & Barto, 1998）已被应用于日益复杂的领域，如机器人技术和金融（Kober等，2013；Tang等，2025；Moody等，1998；Liu等，2024），在这些领域中，环境的大规模或高维状态空间使得直接在原始状态上进行学习和规划在计算上变得难以处理。状态抽象（Abel，2022）通过将具体状态映射到抽象状态，同时保留与决策相关的行为属性来管理这种复杂性（Mohan等，2024；Echchahed & Castro，2025）。
状态抽象已以多种形式被研究，不同形式在状态如何分组以及行为的哪些方面被保留方面存在差异。在现代强化学习中，状态抽象通常通过学习表征来实现，这些表征将高维观测压缩为用于控制和预测的潜在状态（Echchahed & Castro，2025）。一个重要的分支基于互模拟等价关系和度量（Dean & Givan，1997；Givan等，2003；Ferns等，2004；2011），其起源于并发系统和系统语义的分析（Milner，1989），后来以多种变体被引入强化学习（Taylor等，2008；Castro，2020；Zhang等，2021；Castro等，2021；Tao等，2025）。一种密切相关的方法训练编码器以保留奖励和单步动力学，如模型无关抽象（Li等，2006）、自预测抽象（Schwarzer等，2021；Ni等，2024；Voelcker等，2024），以及其他方法（François-Lavet等，2019；Gelada等，2019）。更弱的概念，如价值等价（Givan等，2003；Li等，2006；Grimm等，2020），仅识别产生相似价值的状态。然而，在实践中，状态抽象方法往往结合多个目标，使得难以分离各个抽象要求（Ni等，2024；Luo等，2025）。
尽管存在这些差异，这些状态抽象准则可以通过追问交互系统行为的哪些方面旨在被保留来加以理解。这一视角将关注点从定义抽象本身转移到理解其行为后果上。被保留的属性可以是单元的或二元的，逻辑的或定量的，精确的或近似的。为了统一地研究它们，我们需要精确的行为结构概念以及比较跨状态和跨系统行为的原理性方法。一个显著的例子是，价值函数可以被视为一种单元的、定量的行为度量，它总结了随时间推移的期望回报（Sutton & Barto，1998）。在逻辑方面，安全强化学习使用时序逻辑规范（Alshiekh等，2018）和各种其他约束形式（Hsu等，2021；Yu等，2022；Wachi等，2024）来定义单元的行为要求，而互模拟关系（Dean & Givan，1997）则是二元行为结构的典范例子。在定量方面，安全价值函数是用于衡量风险的单元行为量（Wachi等，2024），而各种行为度量则是状态抽象核心的二元结构（Luo等，2025）。尽管它们在通过动力学来刻画行为这一目标上是共同的，但这些概念仍然是零散的，并且对于它们在状态抽象下如何转移所提供的保证也有限。
这种零散性还体现在强化学习理论中一个反复出现的模式上，即即使是现有行为结构的轻微变体，也会被从头开始分析（Taylor等，2008；Castro，2020；Zhang等，2021），且常常遵循相同的证明模板（Ferns等，2004）。这一模式暗示了共享的定义和证明原则的存在，但强化学习文献缺乏一个统一的正式工具包来使这些论证可跨行为结构复用。我们的目标是通过提供一个组合式框架来定义行为结构并分析它们在状态抽象下的转移，从而使这些共享原则变得明确。
在本文中，我们提出一个组合式框架，通过余代数（Rutten，2000；Jacobs，2016）的视角来定义和分析强化学习中的行为结构。余代数提供了一种用于建模转移系统及其行为的统一语言。主要贡献有三方面：
行为结构的组合式定义。我们引入行为结构的统一定义，将不变量、价值函数以及互模拟关系或度量作为共享组合构造的实例予以包含，用共同的正式方案取代了许多特例定义。
状态抽象的一般转移保证。我们将状态抽象建模为余代数同态，并证明行为结构通过具体系统和抽象系统之间的拉回和前推运算能沿着此类抽象可靠地传递。
从逻辑语义到定量语义的一般桥梁。在明确的代数兼容性条件下，我们展示如何从逻辑行为语义系统性地构造定量度量。
具体而言，第2节介绍了行为系统的余代数框架，指明了本文所考虑的系统。第3节发展核心技术工具，包括丛、提升以及拉回和前推运算，我们将用它们来正式定义和分析行为结构。第4节将抽象框架实例化为强化学习中一些现有语义，说明其一般性和表达力。理论的严格描述被推迟到附录中。
2. 行为系统
在本节中，我们引入一个用于建模行为系统的余代数框架。我们在2.1节中将状态转移系统形式化为余代数，在2.2节中将状态抽象定义为同一类型系统之间的同态，并在2.3节中将策略依赖的转移表述为不同类型系统之间的自然变换。本文中将使用两种系统类型：用于环境的随机摩尔机，以及用于环境与策略复合后所得策略条件系统的隐马尔可夫模型。
2.1 状态转移系统
在本文中，我们使用相同的要素，但在环境和智能体之间增加了显式的输入-输出接口，这使得我们能够分别分析各组成部分的单步行为，然后组合式地将它们结合起来以理解整体系统。这种对显式接口规范和组合的关注与近期关于智能体和强化学习的研究相一致（Abel等，2023；Mohan等，2024；Abel等，2025；Rosas等，2025；Boyd等，2025）。
余代数框架中的一个核心概念是函子（Mac Lane，1978），其非正式定义如下（严格定义见A.1节）：
接下来，我们考虑一个隐马尔可夫模型（Rabiner，1989），这是一种没有输入的系统：
2.2 同类型系统之间的同态
状态抽象的一个核心且刻意强化的概念是，在抽象系统中保留原始系统的动力学。我们表明，这一要求可以形式化为同一类型两个系统之间的余代数同态（Rutten，2000；Jacobs，2016）：
注意，这种动态保持是一个强要求，并非所有抽象都满足。通常，我们可能只希望保留原始系统的某些结构或属性，例如价值函数、行为度量或最优策略（Li等，2006；Grimm等，2020；Luo等，2025）。我们将在第3节讨论此类行为结构及其如何通过同态进行传递。
一个相关但不同的概念是状态-动作抽象中的MDP同态（Ravindran & Barto，2001；2002），它涉及接口变化。我们将在第F节讨论我们的框架如何容纳这一概念。
2.3 不同类型系统之间的变换
在强化学习中，我们经常需要关联不同类型的系统，例如当智能体与环境交互形成闭环系统时，或者当环境限制可用动作或变换其输出时。因此，我们转向自然变换，将其作为比较和连接此类异构系统的原则性方法（Rutten，2000，第15章）：
该构造刻画了由环境和遵循平稳策略的智能体所诱导的闭环系统，这对于描述策略依赖的互模拟（Castro，2020）和价值等价（Li等，2006；Grimm等，2020）是有用的。
3. 行为语义
在形式化了状态转移系统如何生成行为之后，我们接下来开发一个框架，用于指定和推理此类系统状态空间上决定行为如何被解释的结构。在3.1至3.4节中，我们介绍丛、提升、拉回和前推的概念，这些构成了正式定义行为结构的技术基础。在3.5节中，我们给出关于行为结构传递的理论结果，以验证我们的框架。在本节中，我们以安全谓词、价值函数以及互模拟关系和度量作为贯穿性示例。
3.1. Bundle
首先，我们引入丛的概念，它涵盖了谓词、量、关系、距离，以及更一般地，状态空间上的 n n元结构：
3.2 丛的提升
这是后继特征（Dayan，1993；Barreto等，2017；Machado等，2023；Wiltzer等，2024）思想背后的单步向量聚合方案。
这些例子表明，选择算子等同于选择被提升丛的语义。丛的元数、余域以及这些设计选择共同决定了所研究的行为结构。例如，例3.3中的几乎必然算子定义了一种更严格的语义。⁵ 例3.4中的加法可替换为其他组合子，如最大值，从而产生不同的奖励语义。
二元丛提升当 n = 2 时，丛提升的设计空间更加丰富。一个常见的选择如下：
值得注意的是，提升操作不依赖于具体系统（即余代数），而仅依赖于系统类型（即函子）。接下来，我们引入拉回和前推操作，它们允许我们沿着映射在不同空间之间传递丛。
3.3 丛的拉回
3.4 丛的前推
3.5 行为结构的传递
现在我们已经具备了所有必要组成部分：行为系统、系统之间的映射、行为结构以及用于传递结构的操作。最后，我们给出关于行为结构传递的理论结果，以展示这些组成部分如何结合在一起。
沿同态传递行为结构
首先，我们给出主要定理，这些定理论证了沿同态使用拉回和前推来传递行为结构的合理性。这些定理给出了通用条件，在此条件下，包括安全谓词、价值函数以及互模拟关系和度量在内的常见行为结构可以沿抽象映射被拉回或前推。我们的结果基于以下引理：
该引理表明，提升和闭包算子通过构造与同态兼容。基于该引理，我们可以证明以下行为结构传递与构造定理：
该定理表明，如果编码器 φ φ是满射且保持动力学，则抽象系统上的任何行为结构 Z
都可以通过沿编码器拉回，在具体系统上被安全地验证。满射性条件，即每个抽象状态至少对应一个具体状态，确保了抽象系统不存在可能产生不可验证行为的额外状态。
该定理表明，如果提升中使用的算子通过零谓词是同态的，则定量丛的取值为零当且仅当逻辑丛求值为真。同态条件编码了算子之间的关系，例如“两个非负数的和/最大值为零当且仅当两个数均为零”（组合子），或“非负随机变量的期望为零当且仅当该变量几乎必然为零”（重心）。通过这种方式，定理3.14不仅是现有概念之间的一种关系，更是一种构造原则：一旦将逻辑行为结构指定为丛，且算子满足同态条件，相应的定量结构便自动导出。这将对互模拟关系和互模拟度量（Ferns等，2004；2011；Castro，2020）之间的联系推广到一般的行为结构。
4. 强化学习中的状态抽象
本节将我们的框架实例化到四个熟悉的强化学习主题上：下一观测预测、模型无关抽象、互模拟等价以及策略依赖转移与价值函数。
4.1 下一观测预测
4.2 模型无关抽象
接下来，我们将模型无关抽象（Li等，2006；Li，2009）纳入我们的余代数框架，并证明它等价于余代数同态条件：
命题4.2。Li等（2006）中的模型无关抽象恰好是定义2.6中的余代数同态。
4.3 从同态到互模拟
因此，命题4.2和4.3共同表明，模型无关抽象是互模拟等价的商映射。这解释了为何自预测可以在不显式计算互模拟度量的情况下恢复基于互模拟的抽象——互模拟度量的标准形式化需要优化耦合（Ferns等，2004；Castro等，2021；Calo等，2024）。
4.4 价值函数与价值等价
5. 结论
总结我们为强化学习中行为结构的定义和分析引入了一个组合式基础，将单元不变量、价值函数以及互模拟关系或度量纳入一个统一的、可传递的框架中。系统动力学被建模为余代数，一种核心且广泛使用的状态抽象概念被刻画为余代数同态，而行为结构则通过通用的提升与拉回构造从系统动力学中统一生成。我们证明了通过拉回和前推进行可靠传递，并从逻辑行为语义导出定量度量。
组合性在本文中，“组合式”意指全局行为语义通过组合更小的组件来构建。在系统层面，转移、观测和策略等组件通过函子构造组合成余代数行为系统。在语义层面，行为结构通过使用广泛选择的算子经由提升来定义。在抽象层面，这些结构通过拉回和前推与抽象映射组合，给出传递结果而非特例证明。
范围、局限性与未来工作本文聚焦于严格同态和精确的结构保持。一个自然的下一步是研究通过 lax 同态带有显式松弛的放宽交换条件。由此出发，可以发展近似的定量理论，将这种松弛转化为更弱的传递保证、实用的诊断指标或训练目标。丛的视角也支持符号化规范，包括安全约束和时序逻辑约束，不过更全面的处理超出了本文的范围。另一个方向是研究更弱的行为结构保持映射概念，这可能允许更灵活的抽象，同时保留一定的行为保证。最后，我们聚焦于行为结构的理论基础，但一个重要的下一步是开发在强化学习中学习和利用这些结构的实用算法。
原文链接：https://arxiv.org/pdf/2606.25357
热门跟贴