把 Lean 和强化学习接到一起，我做了一个虚拟电厂最小闭环¶

最近我一直在想一个问题。

如果我们真的想把强化学习用到虚拟电厂这种系统里，光让它“学会赚钱”其实远远不够。真正难的问题不是收益函数怎么写，而是：你怎么证明这个策略不会在某个时刻做出越界、失控或者语义错误的动作？

这也是我做这个小项目的起点。

我想做的不是一个“大而全”的虚拟电厂平台，而是一个足够小、但逻辑完整的实验：

Python 负责强化学习训练
Lean 负责定义和验证约束
两边通过一份轨迹 JSON 接起来
最终形成一个能训练、能导出、能验证的最小闭环

结果是，这个想法是能跑通的。

我在本地做了一个最小项目，把 Lean 4 + 强化学习 + 虚拟电厂 真正接到了一起。

为什么我觉得这件事值得做？¶

因为现在很多“AI + 控制”的系统，往往有一个共同问题：

它们很擅长优化目标，但不擅长给出可信边界。

换句话说，模型也许能学会：

什么时候充电更省钱
什么时候放电更赚钱
什么时候该利用光伏富余电量

但系统未必天然知道：

电池 SoC 会不会越界
充放电动作有没有超限
与主网的交换功率有没有超过并网边界
仿真里记录的轨迹和实际状态转移是不是一致

在玩具环境里，这些可能只是 bug；但在真实能源系统里，这类问题意味着系统不可托付。

所以我越来越觉得，强化学习要进入关键基础设施，必须有一层独立于策略本身的“形式化边界”。

Lean 在这个项目里扮演的就是这个角色。

它不负责找最优策略，它负责回答另一个更底层的问题：

什么样的状态是合法的？什么样的动作是允许的？什么样的轨迹是可以被信任的？

这个项目具体做了什么？¶

为了不把问题一开始做得太复杂，我只保留了一个虚拟电厂里最核心的几个元素：

一个电池储能
一条光伏出力曲线
一条站内负荷曲线
分时买卖电价格
一个简单的调度动作：电池充电、放电或不动

整个系统非常克制。

状态只有一个核心量：soc。动作也只有一个核心量：batteryDelta。

也就是说，当前这个项目讨论的是一个最基本的问题：

在一天 24 个时间步里，电池应该怎么跟着负荷、光伏和电价变化去充放电，才能把成本压下来，同时不违反系统约束？

这其实已经是一个很典型的虚拟电厂子问题了。

Lean 在里面到底做什么？¶

很多人听到 Lean，第一反应会以为我要“用定理证明器训练 AI”。

不是。

这个项目里，Lean 的职责非常明确：它是系统规则的最终裁判，不是策略生成器。

我在 Lean 里定义了几件事：

第一，什么叫合法参数¶

比如：

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

第二，什么叫合法状态¶

当前只有一个状态变量 SoC，所以规则也很简单：

0 <= soc <= batteryCapacity

第三，什么叫合法动作¶

动作不是单独判断的，而是结合当前状态和外部信号一起判断：

充电不能超过上限
放电不能超过上限
下一时刻 SoC 不能越界
与电网的净交换功率不能超过并网限制

这点很关键。

因为很多系统口头上说“动作有限制”，但实现时只是限制了动作数值本身，却没有真的检查这个动作作用到当前状态之后会发生什么。

Lean 在这里检查的是完整语义，不是表面形式。

第四，轨迹是不是自洽¶

这是我很看重的一点。

Python 训练结束之后，会导出一份 episode 轨迹，里面记录：

每一步看到的状态
当前负荷、光伏、电价信号
采取的动作
环境返回的下一状态

Lean 会重新拿这份轨迹逐步检查：

这一步状态是不是上一时刻真实推进出来的
这一步动作在当下是否真的合法
记录下来的 nextState 是否真的等于状态转移函数的结果

这样做的意义是，不只是检查“有没有越界”，而是在检查 Python 环境和 Lean 形式化模型是不是在说同一件事。

很多工程系统最后出问题，不是因为规则根本没有，而是因为代码、日志、仿真和文档慢慢漂移成了不同语义。这个轨迹验证层，本质上就是在防这个问题。

Python 侧为什么故意做得很简单？¶

Python 这边我没有直接上 PPO、SAC，也没有上 Gymnasium 或 SB3，而是先写了一个最小的环境和一个 Q-learning baseline。

原因很现实：

1. 第一版最重要的是闭环，不是算法炫技¶

这个项目当前最重要的成功标准不是“收益最优”，而是：

环境语义明确
约束定义统一
Python 导出的轨迹能被 Lean 接住并验证

如果第一版就把一堆深度学习框架、并行采样、复杂网络结构堆进来，只会让问题更难定位。

2. 小状态空间没必要上重武器¶

当前观测只有时间步和电池 SoC，状态空间很有限。用表格型 Q-learning 足够跑出一个比“原地不动”更好的策略。

3. 调试成本更低¶

策略如果学坏了，Q 表是能直接看的。对于一个要和形式化系统互相对齐的项目，这一点其实非常重要。

我一直觉得，工程原型阶段最怕的不是算法不高级，而是系统不可解释。

实际跑出来的效果怎么样？¶

我在本地跑过完整流程，命令是：

./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 }

这个结果说明至少三件事：

这个极简 RL baseline 确实学到了一套比“什么都不做”更好的动作序列
Python 侧导出的轨迹可以被 Lean 成功验证
从训练到验证的整条链路是通的

这里的 improvement=151.0 当然不代表真实虚拟电厂场景里的收益结论。它只是这个最小实验在固定配置下的一个演示值。

真正重要的是另一件事：

形式化约束和学习型策略不是互斥的，它们完全可以在同一个工程原型里协同工作。

我觉得这个方向真正有价值的地方¶

如果把这个项目放大来看，它其实在试图回答一个更普遍的问题：

当 AI 开始参与基础设施调度时，我们怎么让它变得更可信？

我目前的答案是：

让学习负责适应复杂时序和不确定性
让形式化系统负责定义不可突破的边界

这两者分工明确，反而比“全部靠经验规则”或者“全部交给黑盒策略”更稳。

在虚拟电厂这个方向上，这种架构至少有三点现实意义：

第一，给 RL 加一层独立的安全边界¶

以后即使把 Q-learning 换成 PPO，甚至换成更复杂的多智能体方法，只要最后输出的是状态-动作轨迹，Lean 这一层依然可以继续用。

第二，减少系统语义漂移¶

这在工程上非常实际。

环境改了、字段名改了、日志格式改了、状态转移改了，这些东西很容易在迭代中悄悄偏掉。形式化轨迹校验能很早把问题暴露出来。

第三，为后续更强的验证打基础¶

现在验证的是单步约束和轨迹一致性。以后完全可以继续加：

多步不变式
更复杂的设备约束
多储能、多负荷、多电源建模
甚至市场竞价和策略组合

所以这个项目最重要的不是“已经做了多少”，而是它已经把后面那条路打通了。

如果继续做下去，我下一步会做什么？¶

如果要继续迭代，我会优先做三件事：

1. 把 RL baseline 换成更现实的算法¶

例如 PPO 或 SAC，让动作空间从简单三档扩展到更细粒度甚至连续控制。

2. 把物理模型做厚¶

加上更多 DER、需求响应负荷、预测误差和网络侧限制，让问题更接近真实 VPP。

3. 从离线验证走向在线安全过滤¶

现在的流程还是“先训练/执行，再验证轨迹”。

更进一步的方向应该是：

策略先给出候选动作
安全层实时拒绝非法动作
最终只允许通过验证的动作进入控制回路

一旦做到这一步，形式化系统就不只是审计工具，而会真正变成控制系统的一部分。

最后¶

我做这个项目之后，一个感受越来越强：

强化学习在能源系统里真正缺的，不只是更好的 reward 设计，而是更强的可信性设计。

Lean 并不能替代强化学习，强化学习也不可能自动解决形式化验证的问题。但把这两者接起来，至少给了我们一个很务实的方向：

用学习方法解决复杂决策
用形式化方法约束决策边界
用结构化轨迹把两者连接起来

这个项目只是一个很小的开始，但它已经足够说明一件事：

“可学习” 和 “可验证” 不一定冲突。在虚拟电厂这种系统里，它们应该一起出现。

如果你也在做储能调度、虚拟电厂、强化学习控制，或者你也对“AI 如何进入关键系统而不失控”这个问题感兴趣，我认为这条路线值得认真做下去。