VPP Lean RL 使用手册¶

文档目标¶

这份手册面向三类读者：

初学者：想先把项目跑起来，理解它到底在做什么。
工程师：想知道代码库结构、扩展点、调试方法和常见坑。
研究科学家：想把它当作一个可重复的实验脚手架，做算法、约束和验证方面的研究。

如果你只想用最短时间上手，先看“5 分钟快速上手”。如果你要改代码，直接看“面向工程师”。如果你要做实验或写论文原型，直接看“面向研究科学家”。

1. 项目是什么¶

VPP Lean RL 是一个把 Lean 4 和 Python 强化学习 结合起来的虚拟电厂研究脚手架。

它当前解决的是一个刻意简化但闭环完整的问题：

Python 负责训练控制策略
环境模拟一个单站点虚拟电厂
在线 safety shield 可以在动作进入环境前做过滤
Lean 负责验证轨迹是否满足约束和审计一致性

这个项目的目标不是直接做工业级调度，而是提供一个“可运行、可扩展、可验证”的最小研究底座。

2. 你可以用它做什么¶

跑一个最小的虚拟电厂强化学习实验
对比不同 tabular RL 算法
对比有无安全 shield 的策略行为
导出 Lean 生成的规则表给 Python 在线使用
生成可审计的轨迹 JSON
用 Lean 检查轨迹是否满足状态、动作、并网和 shield 审计约束

3. 当前不做什么¶

这点要说清楚，避免误用：

不是生产级 EMS / DERMS / 市场竞价系统
不是深度强化学习平台
不是多站点、多资产、多市场的真实 VPP 模型
不是对策略最优性的形式化证明系统

当前代码库更接近“研究原型 + 教学样板”。

4. 环境要求¶

4.1 必需环境¶

Lean 4 和 Lake
Python >= 3.11

项目中已经声明：

lean-toolchain: leanprover/lean4:stable
pyproject.toml: requires-python = ">=3.11"

4.2 建议环境¶

macOS / Linux
能直接运行 lake build
能直接运行 python3 -m ...

4.3 第一次进入项目建议做的事¶

lake build
python3 -m unittest discover -s tests

如果这两步都通过，说明 Lean 侧和 Python 侧的基本链路是通的。

5. 5 分钟快速上手¶

5.1 查看支持的场景和算法¶

python3 -m vpp_rl.train --list-scenarios
python3 -m vpp_rl.train --list-algorithms

当前支持：

场景：default、peak_shaving、solar_export、stress_test
算法：q_learning、sarsa、double_q

5.2 跑一个完整 demo¶

./scripts/run_demo.sh 180 double_q peak_shaving table_project

这个脚本会做 3 件事：

训练一个 RL agent
导出 trace JSON
调用 Lean verifier 验证这条 trace

输出文件默认在 artifacts/ 目录下，例如：

artifacts/peak_shaving_shield_table.json
artifacts/peak_shaving_double_q_table_project_trace.json

5.3 手工分步跑¶

如果你不想用脚本，而是想看清每一步：

python3 -m vpp_rl.rule_table \
  --scenario peak_shaving \
  --output artifacts/peak_shaving_shield_table.json

python3 -m vpp_rl.train \
  --episodes 180 \
  --algorithm double_q \
  --scenario peak_shaving \
  --shield-mode table_project \
  --shield-table artifacts/peak_shaving_shield_table.json \
  --output artifacts/peak_shaving_double_q_table_project_trace.json

lake env lean --run VppLeanRl/Cli.lean -- \
  artifacts/peak_shaving_double_q_table_project_trace.json

6. 项目目录导览¶

6.1 Lean 侧¶

VppLeanRl/Domain.lean：参数、状态、信号、动作、转移和基础有效性定义
VppLeanRl/Parameters.lean：参数合法性相关证明
VppLeanRl/Safety.lean：动作合法性和状态保持相关证明
VppLeanRl/SignalFacts.lean：信号非负性相关证明
VppLeanRl/Shield.lean：在线 shield 合约与审计一致性检查
VppLeanRl/RuleTable.lean：Lean 规则表生成器
VppLeanRl/RuleTableCli.lean：规则表导出 CLI
VppLeanRl/Trace.lean：轨迹验证器
VppLeanRl/Cli.lean：Lean 命令行入口

6.2 Python 侧¶

vpp_rl/model.py：共享数据模型和 trace schema
vpp_rl/env.py：环境、场景、奖励和 trace 记录
vpp_rl/agent.py：tabular RL 算法实现
vpp_rl/shield.py：在线动作过滤器
vpp_rl/rule_table.py：Lean 规则表的导出和加载
vpp_rl/train.py：训练和评估入口

6.3 测试和脚本¶

tests/test_vpp.py：单元测试和 Python 到 Lean 的集成测试
scripts/run_demo.sh：一键 demo

7. 核心概念¶

7.1 场景 `scenario`¶

场景定义了：

电池参数
24 小时信号曲线
初始 SoC

当前都是确定性场景，目的是让实验更稳定、验证更容易复现。

7.2 动作 `action`¶

当前动作是电池功率离散动作，对应 batteryDelta。

环境默认使用三种动作：

放电：-control_step
空转：0
充电：+control_step

例如在默认场景里，动作集合通常是 (-3, 0, 3)。

7.3 观测 `observation`¶

当前 agent 看到的是一个离散观测键：

(time_index, soc)

这是典型的 tabular RL 建模方式。

7.4 奖励 `reward`¶

环境内部先计算成本 cost，然后返回：

reward = -cost

成本包含：

电网购电成本
售电收益
电池退化惩罚

7.5 算法 `algorithm`¶

当前提供 3 个无外部依赖的 tabular 算法：

q_learning
sarsa
double_q

如果你只是想先跑通项目，优先用 double_q。如果你在做教学或基线对比，3 个都值得保留。

7.6 在线安全过滤 `shield_mode`¶

当前支持 3 种模式：

none：不做在线过滤
project：如果动作非法，就在线投影到最近合法动作
table_project：使用 Lean 生成的规则表做投影

对于想看“形式化约束如何真正影响 RL 执行”的用户，table_project 是最完整的链路。

7.7 规则表 `rule table`¶

规则表是 Lean 导出的 JSON 文件，里面记录：

某个 (timeIndex, soc) 下哪些动作合法
对每个 proposed action，应该投影到哪个 applied action

它的作用是把 Lean 侧的约束判定提前离线算好，让 Python 运行时直接查表。

7.8 Trace¶

训练或评估后，环境可以导出一条 EpisodeTrace。

它不只是“执行轨迹”，也是 Lean verifier 的输入。

当前 trace 顶层有明确版本号：

traceVersion = 3

每个 step 里会记录：

state
signal
proposedAction
appliedAction
interventionReasons
interventionContext
nextState

7.9 `proposedAction` 和 `appliedAction`¶

这两个字段很重要：

proposedAction：agent 原本想执行的动作
appliedAction：经过 shield 后真正执行的动作

如果没有 shield 干预，这两个动作应该相同。

7.10 `interventionReasons`¶

这是 shield 为什么修改动作的类别型解释。

当前可能出现：

already_valid
charge_limit
discharge_limit
battery_bounds
grid_limit
unknown_invalid_action

7.11 `interventionContext`¶

这是 shield 审计的数值上下文，当前包括：

proposedBatteryDelta
proposedNextSoc
proposedNetGrid
chargeLimit
dischargeLimit
batteryCapacity
gridLimit
socLowerMargin
socUpperMargin
gridLowerMargin
gridUpperMargin

其中 margin 字段是相对边界的代数量：

为正：离边界还有余量
为负：已经越界

这不是 bug，而是故意保留给审计和诊断使用的。

8. 面向初学者¶

8.1 推荐学习路径¶

按这个顺序最省力：

跑 ./scripts/run_demo.sh 180 double_q peak_shaving table_project
打开生成的 trace JSON 看结构
用 Lean verifier 再手动验证一遍
切换一个场景，比如 solar_export
切换一个算法，比如 sarsa

8.2 你先不用关心什么¶

第一次上手时，可以先不深入这些内容：

Lean 证明细节
shield 的规则表生成流程
tabular RL 的参数调优

先建立这条心智链路即可：

训练 -> 生成轨迹 -> Lean 验证

8.3 最常用命令¶

python3 -m vpp_rl.train --list-scenarios
python3 -m vpp_rl.train --list-algorithms
./scripts/run_demo.sh 180 double_q peak_shaving table_project
lake env lean --run VppLeanRl/Cli.lean -- artifacts/peak_shaving_double_q_table_project_trace.json

9. 面向工程师¶

9.1 代码执行主链路¶

最重要的执行路径在 vpp_rl/train.py：

根据 scenario 创建环境
根据 algorithm 创建 agent
根据 shield_mode 创建 shield
训练 agent
进行 greedy rollout
导出 trace
用 Lean verifier 检查 trace

9.2 你最需要关注的扩展点¶

新增场景¶

去 vpp_rl/env.py：

增加一个 ScenarioDefinition
放进 SCENARIOS
更新 available_scenarios()

建议先照着现有 24 点曲线写一个确定性场景，再考虑随机扰动。

新增算法¶

去 vpp_rl/agent.py：

新建一个 TabularAgent 子类
实现 policy_values()
实现 update()
在 build_agent() 中注册

如果你要接 DQN / PPO，建议不要硬塞进现有 tabular 抽象里，最好新建独立模块。

新增 shield 逻辑¶

去 vpp_rl/shield.py：

新增一个 mode
保持 ShieldDecision 结构不破
确保 proposedAction、appliedAction、interventionReasons、interventionContext 仍能完整记录

否则 Lean 侧审计会断。

9.3 改 trace schema 时要注意什么¶

trace 不是普通日志，它是 Lean verifier 的输入契约。

当前 schema 强约束如下：

顶层必须有 traceVersion
当前版本必须是 3
step 必须带齐审计字段

对应实现见：

vpp_rl/model.py
VppLeanRl/Trace.lean

如果你改了 JSON 字段名、字段结构或版本号：

先改 Python 导出
再改 Lean FromJson
再改 verifier 逻辑
最后补测试

跳过任何一步，都会造成 Python 和 Lean 漂移。

9.4 推荐调试顺序¶

当训练或验证出问题时，按这个顺序查：

python3 -m unittest discover -s tests
lake build
单独运行 python3 -m vpp_rl.train ...
单独运行 lake env lean --run VppLeanRl/Cli.lean -- <trace>
打开 trace JSON 看某一步的 proposedAction、appliedAction 和 interventionContext

9.5 常见工程问题¶

问题 1：Lean 验证失败¶

优先排查：

traceVersion 是否匹配
nextState 是否真的是用 appliedAction 推出来的
interventionReasons 是否和 proposed action 一致
interventionContext 是否和当前参数、状态、信号一致

问题 2：`table_project` 失败¶

优先排查：

shield table 是否存在
rule table 对应的 scenario 是否和当前环境一致
action deltas 是否漂移

问题 3：训练效果很弱¶

先确认这是不是算法问题，不要先怀疑 Lean：

训练轮数是否太少
场景是否更适合别的算法
shield 是否过于保守
idle_reward 是否已经接近 greedy policy

10. 面向研究科学家¶

10.1 这个代码库适合做什么研究¶

RL 与形式化约束的集成研究
在线安全过滤对策略收益和可行性的影响分析
可审计 RL 控制的轨迹设计
Lean 辅助的控制安全验证原型
不同场景和算法的基线比较

10.2 推荐实验维度¶

你至少可以系统比较这 3 个维度：

场景：default / peak_shaving / solar_export / stress_test
算法：q_learning / sarsa / double_q
过滤方式：none / project / table_project

这会形成一个清晰的实验矩阵。

10.3 推荐记录的指标¶

当前代码直接或间接已经能给你这些指标：

training_reward
greedy_reward
idle_reward
improvement
shield_interventions
trace 长度
每一步的 interventionReasons
每一步的 violation margins

如果你要做更严肃的实验，建议额外记录：

不同 seed 的均值和方差
不同场景下的收敛速度
shield 介入次数占比
介入类别分布
介入前后收益变化

10.4 可重复性建议¶

当前代码已经有 seed 参数。

研究使用时建议固定这些条件：

scenario
algorithm
episodes
seed
shield_mode
shield_table 文件版本
traceVersion

如果你改了场景参数或动作空间，最好重新导出规则表，不要继续复用旧表。

10.5 当前研究边界¶

这个代码库目前的研究边界很明确：

环境是确定性的，不是随机市场
agent 是 tabular，不是深度网络
资产是单站点简化模型，不是多 DER 组合系统
Lean 检查的是安全和审计一致性，不是策略最优性

如果你要写论文或做报告，这些限制应该明确写出来。

11. 命令速查表¶

11.1 构建与测试¶

lake build
python3 -m unittest discover -s tests

11.2 列出可用项¶

python3 -m vpp_rl.train --list-scenarios
python3 -m vpp_rl.train --list-algorithms

11.3 训练并输出 trace¶

python3 -m vpp_rl.train \
  --episodes 180 \
  --algorithm double_q \
  --scenario peak_shaving \
  --shield-mode project \
  --output artifacts/peak_shaving_double_q_project_trace.json

11.4 导出 Lean 规则表¶

python3 -m vpp_rl.rule_table \
  --scenario peak_shaving \
  --output artifacts/peak_shaving_shield_table.json

11.5 使用 `table_project`¶

python3 -m vpp_rl.train \
  --episodes 180 \
  --algorithm double_q \
  --scenario peak_shaving \
  --shield-mode table_project \
  --shield-table artifacts/peak_shaving_shield_table.json \
  --output artifacts/peak_shaving_double_q_table_project_trace.json

11.6 用 Lean 验证 trace¶

lake env lean --run VppLeanRl/Cli.lean -- \
  artifacts/peak_shaving_double_q_table_project_trace.json

11.7 一键 demo¶

./scripts/run_demo.sh 180 double_q peak_shaving table_project

12. 输出文件说明¶

12.1 Trace 文件¶

通常位于 artifacts/*.json，是：

Python 环境导出的运行结果
Lean verifier 的输入
审计 shield 干预的主数据源

12.2 Shield table 文件¶

通常位于 artifacts/*_shield_table.json，是：

Lean 离线生成的动作规则表
table_project 模式的运行前置条件

13. 常见问题与排查¶

13.1 为什么 trace 里同时要有 `proposedAction` 和 `appliedAction`¶

因为只记录最终执行动作是不够的。

如果不记录 agent 原本想做什么，你无法回答这些问题：

shield 到底有没有介入
介入频率是多少
被改掉的动作为什么非法
策略本身是不是在持续“撞约束”

13.2 为什么 verifier 要强制 `traceVersion`¶

因为 trace 是 Python 和 Lean 之间的结构化契约。

如果没有显式版本号，字段一旦升级，很容易出现“Python 正常输出、Lean 静默误读”的问题。

13.3 为什么 margin 允许为负¶

因为它的设计目的就是显示“离边界还有多远”或“已经越界多少”。

例如：

gridUpperMargin < 0 表示 proposed net grid 超过上边界
socLowerMargin < 0 表示 proposed next SoC 低于 0

13.4 为什么推荐先用确定性场景¶

因为这能让你先分离两类问题：

算法本身有没有学到东西
形式化验证和 shield 链路是否一致

如果一开始就引入随机扰动，你很难判断问题到底出在策略、环境还是约束接线。

14. 推荐使用路径¶

14.1 如果你是初学者¶

建议路线：

跑一键 demo
看 trace JSON
手动跑 Lean verifier
切换不同场景和算法

14.2 如果你是工程师¶

建议路线：

跑测试
理清 train.py -> env.py -> shield.py -> model.py -> Trace.lean
先加一个新场景或新算法
再碰 trace schema 和 Lean verifier

14.3 如果你是研究科学家¶

建议路线：

先固定一个实验矩阵
固定 seed 和 rule table
批量比较 none / project / table_project
分析 intervention reasons 和 margins
最后再扩展到更复杂环境或更强算法

VPP Lean RL 使用手册¶

文档目标¶

1. 项目是什么¶

2. 你可以用它做什么¶

3. 当前不做什么¶

4. 环境要求¶

4.1 必需环境¶

4.2 建议环境¶

4.3 第一次进入项目建议做的事¶

5. 5 分钟快速上手¶

5.1 查看支持的场景和算法¶

5.2 跑一个完整 demo¶

5.3 手工分步跑¶

6. 项目目录导览¶

6.1 Lean 侧¶

6.2 Python 侧¶

6.3 测试和脚本¶

7. 核心概念¶

7.1 场景 scenario¶

7.2 动作 action¶

7.3 观测 observation¶

7.4 奖励 reward¶

7.5 算法 algorithm¶

7.6 在线安全过滤 shield_mode¶

7.7 规则表 rule table¶

7.8 Trace¶

7.9 proposedAction 和 appliedAction¶

7.10 interventionReasons¶

7.11 interventionContext¶

8. 面向初学者¶

8.1 推荐学习路径¶

8.2 你先不用关心什么¶

8.3 最常用命令¶

9. 面向工程师¶

9.1 代码执行主链路¶

9.2 你最需要关注的扩展点¶

新增场景¶

新增算法¶

新增 shield 逻辑¶

9.3 改 trace schema 时要注意什么¶

9.4 推荐调试顺序¶

9.5 常见工程问题¶

问题 1：Lean 验证失败¶

问题 2：table_project 失败¶

问题 3：训练效果很弱¶

10. 面向研究科学家¶

10.1 这个代码库适合做什么研究¶

10.2 推荐实验维度¶

10.3 推荐记录的指标¶

10.4 可重复性建议¶

10.5 当前研究边界¶

11. 命令速查表¶

11.1 构建与测试¶

11.2 列出可用项¶

11.3 训练并输出 trace¶

11.4 导出 Lean 规则表¶

11.5 使用 table_project¶

11.6 用 Lean 验证 trace¶

11.7 一键 demo¶

12. 输出文件说明¶

12.1 Trace 文件¶

12.2 Shield table 文件¶

13. 常见问题与排查¶

13.1 为什么 trace 里同时要有 proposedAction 和 appliedAction¶

13.2 为什么 verifier 要强制 traceVersion¶

13.3 为什么 margin 允许为负¶

13.4 为什么推荐先用确定性场景¶

14. 推荐使用路径¶

14.1 如果你是初学者¶

14.2 如果你是工程师¶

14.3 如果你是研究科学家¶

15. 文档入口¶

7.1 场景 `scenario`¶

7.2 动作 `action`¶

7.3 观测 `observation`¶

7.4 奖励 `reward`¶

7.5 算法 `algorithm`¶

7.6 在线安全过滤 `shield_mode`¶

7.7 规则表 `rule table`¶

7.9 `proposedAction` 和 `appliedAction`¶

7.10 `interventionReasons`¶

7.11 `interventionContext`¶

问题 2：`table_project` 失败¶

11.5 使用 `table_project`¶

13.1 为什么 trace 里同时要有 `proposedAction` 和 `appliedAction`¶

13.2 为什么 verifier 要强制 `traceVersion`¶