用 Lean 证明约束，用强化学习做调度：一个面向虚拟电厂的最小可运行项目¶

虚拟电厂（Virtual Power Plant, VPP）这几年很热，但大多数技术实现都有一个长期存在的问题：

纯优化/强化学习方案，能学到策略，但不一定天然满足物理约束和安全边界
纯形式化/规则方案，约束明确，但很难直接适应复杂、动态、带不确定性的控制问题

这也是我做这个小项目的出发点：把 Lean 4 的形式化约束能力和 Python 里的强化学习训练流程接起来，做一个“能训练、能验证、还能跑通”的虚拟电厂最小闭环。

项目地址中的核心结构大致如下：

VppLeanRl/Domain.lean：定义虚拟电厂参数、状态、动作、状态转移和约束
VppLeanRl/Trace.lean：验证 Python 导出的轨迹是否满足 Lean 里的规则
VppLeanRl/Cli.lean：Lean 侧命令行入口
vpp_rl/env.py：Python 侧环境模拟
vpp_rl/agent.py：一个极简 Q-learning baseline
vpp_rl/train.py：训练并导出轨迹

这不是一个生产级 VPP 系统，而是一个研究型脚手架。它的目标很明确：证明“形式化验证 + RL 调度”这件事可以被做成一个工程上可落地的最小系统。

为什么要把 Lean 和 RL 放在一起？¶

如果你单独看这两类工具，它们的优缺点非常清楚。

强化学习的优势¶

强化学习适合做时序决策。对于虚拟电厂来说，智能体需要连续地回答这样的问题：

当前电池该不该充电？
太阳能富余时要不要向电网回送？
分时电价变化时，什么时候提前储能最划算？

这类问题不容易靠几条静态规则写死，尤其一旦接入更多 DER（Distributed Energy Resources）之后，人工规则会迅速膨胀。

强化学习的短板¶

问题也很直接：RL 学的是“收益最大化”，不是“系统永远安全”。

如果环境定义得不够严谨，或者训练阶段对非法动作处理草率，就很容易出现下面这些情况：

电池荷电状态（SoC）越界
充放电功率超过设备限制
与主网的交换功率超过并网限制
记录下来的轨迹和真实状态转移不一致

在仿真里，这些问题可能只是一个 bug；在电力系统里，它们通常意味着控制逻辑不可信。

Lean 的价值¶

Lean 在这个项目里不是拿来“训练策略”的，而是拿来做另一件更重要的事：定义什么是合法动作、什么是合法状态、什么样的轨迹可以被信任。

也就是说，RL 负责搜索好策略，Lean 负责定义不可突破的边界。

这和很多现实系统中的分层控制思路是吻合的：

上层策略可以灵活甚至带学习能力
下层安全约束必须刚性、可检验、可复现

这个最小项目建模了什么？¶

为了避免一开始就把系统做得过大，我只保留了一个单站点 VPP 中最核心的几个元素：

电池储能
光伏发电
站内负荷
与电网的买电/卖电行为
分时电价信号

状态非常简单，只有一个核心变量：

State = { soc }

动作也只保留一个控制量：

Action = { batteryDelta }

这里的 batteryDelta 表示当前时间步电池能量变化：

正值表示充电
负值表示放电
0 表示保持不动

站点与电网之间的净交换功率定义为：

netGrid = load - solar + batteryDelta

这个定义有几个好处：

负载变大，会推高购电需求
光伏变大，会减少净购电，甚至产生回送
给电池充电，本质上会增加站点当前用电
给电池放电，则会减少从电网取电的需求

这个模型不复杂，但足够支撑一个完整实验链路：环境生成状态，智能体选动作，系统推进一步，然后把轨迹拿给 Lean 验证。

Lean 里到底证明/检查了什么？¶

Lean 侧最关键的逻辑在 VppLeanRl/Domain.lean 和 VppLeanRl/Trace.lean。

项目里当前定义了几类核心约束：

1. 参数合法性¶

例如：

电池容量必须大于 0
充电上限、放电上限、并网功率上限不能为负
退化惩罚不能为负

2. 状态合法性¶

当前只检查 SoC 是否始终落在：

0 <= soc <= batteryCapacity

3. 动作合法性¶

动作是否合法由四部分共同决定：

batteryDelta 不能超过充电上限
batteryDelta 不能超过放电上限
执行动作后的 nextState.soc 仍然必须在合法区间内
netGrid 必须满足并网边界

也就是说，动作合法性并不是单独看动作本身，而是把当前状态、当前外部信号、动作和下一状态耦合在一起检查。

4. 轨迹一致性¶

Lean 侧验证的不只是“每一步看起来合法”，还会检查：

Python 记录的 state 是否等于上一时刻的真实 nextState
Python 导出的 nextState 是否真的等于 Lean 侧转移函数 step state action

这一点非常重要。

很多仿真系统最容易被忽略的问题，不是约束写错，而是日志和真实运行语义逐渐漂移。项目里的轨迹校验就是为了卡住这个问题：只要 Python 和 Lean 对系统语义的理解不一致，验证就会失败。

Python 侧的 RL 环境怎么设计？¶

Python 环境实现位于 vpp_rl/env.py。

为了降低依赖，我没有直接上 Gymnasium 或 Stable-Baselines3，而是先做了一个纯标准库可运行的环境。这个决定有两个现实原因：

先把语义对齐，比先堆框架重要
最小项目越少外部依赖，复现实验越快

环境里预设了一组固定的 24 小时日内曲线：

光伏出力 solar
负荷 load
买电价格 buy_price
卖电价格 sell_price

动作空间是离散的三档：

充电
不动
放电

比如默认配置里，control_step = 3，那么动作集合实际就是：

[-3, 0, 3]

环境每一步都会先筛掉非法动作，只有通过约束检查的动作才会进入候选集合。这一点也很关键：

RL 训练阶段不会接触明显非法的动作
导出的轨迹天然更容易通过 Lean 校验
Python 环境和 Lean 校验器共享相同语义，减少“双重标准”

奖励函数怎么定义？¶

项目里当前采用的是一个非常直接的成本模型：

cost = buyPrice * gridImport
     - sellPrice * gridExport
     + degradationPenalty * abs(batteryDelta)

其中：

从主网购电要花钱
向主网卖电可以获得收益
电池频繁充放电会产生退化惩罚

训练时实际 reward 就是 -cost。

这意味着智能体会自然倾向于学习：

低价时充电
高价时放电
光伏富余时优先利用储能或外送
避免无意义的大幅度充放电

这套奖励设计还比较朴素，但对一个最小演示项目已经足够了。它的优势不是“高度拟真”，而是“足够简单、足够清楚、足够容易验证”。

为什么先用 Q-learning，而不是直接上 PPO？¶

我这里故意没有一上来就接深度强化学习框架，而是用了一个离散状态上的 Q-learning baseline，代码在 vpp_rl/agent.py。

理由很简单：

第一，先验证闭环是否成立¶

这个项目的首要问题不是“能不能多拿 3% 收益”，而是：

环境定义是否合理
约束是否一致
Python 到 Lean 的轨迹链路是否闭环

在这个阶段，用最简单的 RL 算法反而更合适。

第二，状态足够小¶

当前观测只用了：

时间步 time_index
电池 SoC

状态空间并不大，离散表格方法完全可以工作。

第三，便于调试¶

如果策略学坏了，用 Q 表调试远比神经网络参数直观。对于一个要和形式化系统对接的工程原型，这个优点非常现实。

Python 和 Lean 是怎么接起来的？¶

这是整个项目最核心的部分。

思路并不复杂：Python 训练，Lean 验证。两边通过结构化 JSON 交换轨迹。

Python 训练结束后，会导出一个 episode_trace.json，里面包含：

参数 params
初始状态 initialState
每一步的 state
外部信号 signal
采取的 action
得到的 nextState

为了保证字段和 Lean 完全一致，Python 侧在 vpp_rl/model.py 里专门做了 to_lean_dict()。

例如，Python 里的：

buy_price 会被序列化成 buyPrice
battery_delta 会被序列化成 batteryDelta
initial_state 会被序列化成 initialState

这样 Lean 侧就可以直接反序列化 JSON，并逐步检查整个 episode。

对应的验证命令是：

lake env lean --run VppLeanRl/Cli.lean -- artifacts/episode_trace.json

如果轨迹满足所有规则，输出类似：

trace verified; final state = { soc := 0 }

如果哪一步非法，例如 SoC 越界、网侧交换越界、nextState 对不上，Lean 会直接给出失败信息。

这个项目当前能跑出什么结果？¶

我在本地用下面这条命令跑过完整流程：

./scripts/run_demo.sh 200

一次示例输出如下：

episodes=200
training_reward=-992.0
greedy_reward=-936.0
idle_reward=-1087.0
improvement=151.0
trace_path=artifacts/episode_trace.json
trace verified; final state = { soc := 0 }

这个结果说明几件事：

Q-learning 至少学到了一套比“什么都不做”更好的调度策略
Python 训练出来的贪心轨迹能够通过 Lean 验证
整个训练-导出-验证链路是跑通的

需要强调的是，improvement=151.0 并不代表任何工程级 KPI，它只是这个固定配置、固定价差信号下的一个演示结果。真正有价值的是：系统结构已经成立，后面可以在不推翻整体设计的情况下持续增强。

这种架构的现实价值在哪里？¶

如果把这个项目往真实系统方向推，至少有三类价值是明确的。

1. 给学习型控制加一个可验证的安全边界¶

很多团队对 RL 的担心并不是“收益不够高”，而是“我凭什么相信它不会乱来”。

Lean 在这里提供的是一层可执行、可检查、可重复验证的规则边界。即使未来上层策略从 Q-learning 换成 PPO、SAC 或者多智能体方法，只要输出动作轨迹，依然可以走同一套验证路径。

2. 让仿真语义更不容易漂移¶

工程系统里很容易发生这样的问题：

环境代码改了
日志结构改了
某个字段含义悄悄变了
结果看起来还能跑，但实际语义已经不一致

轨迹验证能尽早把这种问题暴露出来。对于多团队协作、长周期演化的系统，这点非常有用。

3. 为后续更强的形式化能力留接口¶

当前 Lean 只验证单步安全和轨迹一致性，但后续完全可以继续往前走，例如：

证明多步不变式
验证奖励函数的某些上界/下界性质
加入负荷响应、柴油机、可中断负荷等更多设备约束
把市场竞价动作也纳入形式化模型

换句话说，这个项目真正重要的不是现在已经证明了多少，而是它已经把“怎么继续证明更多东西”这条路打通了。

这个项目刻意没有做什么？¶

为了保持最小闭环，我有意识地没有做下面这些事：

没有引入深度神经网络策略
没有接 Gymnasium / SB3 / Ray RLlib
没有做随机天气、随机负荷扰动
没有接入多储能、多站点、多市场场景
没有做生产级调度器、数据库、API 或可视化界面

这是刻意为之，不是遗漏。

很多项目会在第一版里同时追求：

环境复杂
算法先进
约束完备
工程完整

结果通常是：所有方向都沾一点，但没有一个闭环真正稳定。这个项目反过来，只先做一件事：让 Lean 和 RL 在同一个 VPP 问题上说同一种语言。

如果继续往下做，我会怎么扩展？¶

如果把这个项目作为下一阶段工作的基座，我会优先做三件事。

1. 把 RL baseline 升级到更现实的算法¶

最自然的下一步是接入：

PPO
DQN / Double DQN
或者更适合连续动作的 SAC

这样可以把动作从三档离散值扩展成更细粒度甚至连续控制。

2. 把 VPP 物理模型做厚¶

例如加入：

多电池系统
需求响应负荷
柴油机或燃气轮机
多时段预测误差
网络侧约束

这样 RL 的价值会更明显，Lean 的约束系统也会更有用。

3. 把 Lean 从“离线验证”推进到“在线安全过滤”¶

当前流程是：

Python 生成轨迹
Lean 事后验证

更进一步的做法是：

策略网络先给出动作候选
安全过滤器实时拒绝非法动作
再把最终动作送入环境

这一步一旦做成，Lean 的价值就不只是“审计”，而是会真正进入控制回路。

结语¶

这个项目最想回答的，不是“Lean 能不能替代 RL”，也不是“RL 能不能自动解决虚拟电厂调度”。

真正的问题是：当我们把学习型控制引入关键基础设施时，能不能给它配上一套清晰、严格、可执行的形式化边界？

我认为答案是可以，而且应该尽早这么做。

在这个最小项目里，Lean 和 RL 的分工很明确：

RL 负责在复杂时序中寻找更好的策略
Lean 负责定义什么叫做“永远不能错”的约束

这不是一套最终方案，但它是一个方向正确、工程上可验证、后续可扩展的起点。

如果你也在做虚拟电厂、储能优化、形式化方法，或者对“AI 控制系统如何变得更可信”这个问题感兴趣，这类架构值得认真试一次。

附：项目运行方式¶

lake build
python3 -m unittest discover -s tests
python3 -m vpp_rl.train --episodes 600 --output artifacts/episode_trace.json
lake env lean --run VppLeanRl/Cli.lean -- artifacts/episode_trace.json

或者直接：

./scripts/run_demo.sh 200