Skip to content

VPP Lean RL Quick Start

This is the shortest path for a new user.

If your goal is simply to:

  • run the project end to end
  • understand the main inputs and outputs
  • see how Lean and RL are connected

start here instead of reading the full manuals first.

Related docs:

1. One-Sentence Summary

This project combines Lean 4, Python RL, and a simplified virtual power plant workflow:

  • Python trains the controller
  • the environment simulates battery, solar, load, and grid interaction
  • a shield can block invalid actions online
  • Lean verifies the exported rollout trace

2. Requirements

  • Lean 4
  • Lake
  • Python >= 3.11

Recommended first commands:

lake build
python3 -m unittest discover -s tests

3. Shortest Working Command

Run this from the repository root:

./scripts/run_demo.sh 180 double_q peak_shaving table_project

This will:

  1. train an agent
  2. export a trace
  3. verify that trace in Lean

4. What You Will See

You should get:

  • a training and evaluation summary
  • a shield_interventions count
  • generated JSON artifacts
  • a successful Lean verification message

Typical output files in artifacts/:

  • artifacts/peak_shaving_shield_table.json
  • artifacts/peak_shaving_double_q_table_project_trace.json

5. Three Concepts You Need First

5.1 scenario

A scenario defines:

  • battery parameters
  • 24-hour signal curves
  • initial SoC

Current scenarios:

  • default
  • peak_shaving
  • solar_export
  • stress_test

List them with:

python3 -m vpp_rl.train --list-scenarios

5.2 algorithm

Current RL algorithms:

  • q_learning
  • sarsa
  • double_q

List them with:

python3 -m vpp_rl.train --list-algorithms

5.3 shield_mode

Current online filtering modes:

  • none
  • project
  • table_project

If you want the strongest Lean-to-runtime integration path, start with table_project.

6. Run the Workflow Step by Step

Step 1: Export a Lean Rule Table

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

Step 2: Train and Export a 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

Step 3: Verify the Trace in Lean

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

7. Best Files To Read First

If you want to understand the execution path, start with these files:

  1. scripts/run_demo.sh
  2. vpp_rl/train.py
  3. vpp_rl/env.py
  4. VppLeanRl/Trace.lean

Those four files are enough to understand the main chain:

train -> rollout -> trace -> Lean verification

8. Most Important Trace Fields

The current trace schema version is:

  • traceVersion = 3

The most useful per-step fields are:

  • proposedAction
  • appliedAction
  • interventionReasons
  • interventionContext

They tell you:

  • what the agent wanted to do
  • what was actually executed
  • why the shield changed it
  • which numeric boundary was involved

9. Two Common Problems

9.1 Lean Verification Fails

Check:

  • whether the trace uses the current schema version
  • whether nextState matches appliedAction
  • whether interventionReasons and interventionContext are consistent

9.2 table_project Fails

Check:

  • whether the shield table file exists
  • whether the scenario matches the table
  • whether the action set still matches the rule table

Once you have run the demo, change only one thing at a time:

  1. switch to solar_export
  2. switch to sarsa
  3. switch shield_mode from table_project to none

For deeper engineering or research use, continue with: