- author = "Matej Kripner",
- title = "Symbolic World Models in {Lean 4} for Reinforcement Learning",
- booktitle = "Proceedings of the RLC 2025 Workshop on Programmatic Reinforcement Learning",
- year = "2025",
- pages = "8--18",
- address = "Edmonton, Canada",
- publisher = "Reinforcement Learning Journal (RLJ)",
- keywords = "genetic algorithms, genetic programming, Lean, FireHelicopter",
-
URL = "
https://ufal.mff.cuni.cz/biblio/bibtex/2025-kripner-m9202924265626005643.bib.html",
-
URL = "https://openreview.net/pdf?id=CBFAMnax09",
-
URL = "
http://ufal.mff.cuni.cz/biblio/attachments/2025-kripner-m3520584395346733158.pdf",
-
code_url = "https://github.com/Kripner/lean-worlds",
- size = "10 pages",
- abstract = "We propose a novel approach to model-based reinforcement learning by synthesizing symbolic world models in the Lean 4 proof assistant. Leveraging Lean formal language for mathematics, we encode environment dynamics as interpretable, verifiable rules. Our system integrates a planning agent, an evolutionary algorithm inspired by AlphaEvolve, and a Lean server that predicts the dynamics of an environment using a set of already synthesized rules. We evaluate our approach on a custom cellular automaton environment called FireHelicopter. This environment simulates the dynamics of a forest fire and requires the agent to maximize forest preservation. We explore two training objectives: a pragmatic one focused on maximizing agents return, and a descriptive one prioritizing accurate world prediction. To our knowledge, this is the first use of a general formal mathematics language for model-based RL. We hypothesize that this is a promising avenue for sample-efficient, safe, and interpretable reinforcement learning in real-world scenarios",
-
notes = "also known as
\cite{biblio-9202924265626005643}
Charles University, Faculty of Mathematics and Physics",
