VPP Lean RL 快速上手¶

这是一份给新用户的最短路径文档。

如果你的目标只是：

把项目跑起来
看懂它的基本输入输出
知道 Lean 和 RL 是怎么接起来的

那么先看这份，不必一开始就读完整手册。

完整说明见：

1. 项目一句话说明¶

这是一个把 Lean 4、Python 强化学习 和 虚拟电厂 场景结合起来的最小研究原型：

Python 训练策略
环境模拟电池、负荷、光伏和电网交互
shield 可以在线拦截非法动作
Lean 验证输出轨迹是否满足约束

2. 环境要求¶

Lean 4
Lake
Python >= 3.11

建议先在项目根目录跑：

lake build
python3 -m unittest discover -s tests

3. 最短可运行命令¶

直接运行：

./scripts/run_demo.sh 180 double_q peak_shaving table_project

这条命令会完成：

训练 agent
导出 trace
调用 Lean verifier 验证 trace

4. 你会看到什么¶

通常会得到几类输出：

训练和评估摘要
shield_interventions
trace 文件
Lean 验证成功信息

常见输出文件在 artifacts/ 目录，例如：

artifacts/peak_shaving_shield_table.json
artifacts/peak_shaving_double_q_table_project_trace.json

5. 三个最重要的概念¶

5.1 `scenario`¶

表示一个运行场景，定义了：

电池参数
24 小时负荷/光伏/价格曲线
初始 SoC

当前支持：

default
peak_shaving
solar_export
stress_test

查看命令：

python3 -m vpp_rl.train --list-scenarios

5.2 `algorithm`¶

表示 RL 算法，当前支持：

q_learning
sarsa
double_q

查看命令：

python3 -m vpp_rl.train --list-algorithms

5.3 `shield_mode`¶

表示在线动作过滤方式：

none
project
table_project

如果你想看最完整的“Lean 约束进入 RL 执行链路”的版本，优先用 table_project。

6. 手工分步跑一次¶

如果你不想用脚本，而是想看清完整过程，就按这三步执行。

第一步：导出 Lean 规则表¶

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

第二步：训练并导出 trace¶

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

第三步：用 Lean 验证 trace¶

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

7. 先看哪个文件最有帮助¶

如果你是第一次接触这个项目，建议按这个顺序看：

scripts/run_demo.sh
vpp_rl/train.py
vpp_rl/env.py
VppLeanRl/Trace.lean

这 4 个文件已经足够让你理解主链路：

训练 -> rollout -> trace -> Lean 验证

8. Trace 里最值得看的字段¶

当前 trace schema 版本是：

traceVersion = 3

每个 step 里最值得看的字段是：

proposedAction
appliedAction
interventionReasons
interventionContext

它们分别回答：

agent 想做什么
实际执行了什么
shield 为什么改
具体是哪条数值边界被碰到了

9. 最常见的两个问题¶

9.1 Lean 验证失败¶

优先检查：

trace 文件是不是当前版本
nextState 是否和 appliedAction 一致
interventionReasons 和 interventionContext 是否一致

9.2 `table_project` 跑不通¶