Symbolic World Models in Lean 4 for Reinforcement Learning

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F25%3A10511605" target="_blank" >RIV/00216208:11320/25:10511605 - isvavai.cz</a>

Result on the web

<a href="https://openreview.net/pdf?id=CBFAMnax09" target="_blank" >https://openreview.net/pdf?id=CBFAMnax09</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Symbolic World Models in Lean 4 for Reinforcement Learning

Original language description

We propose a novel approach to model-based reinforcement learning by synthesizing symbolic world models in the Lean 4 proof assistant. Leveraging Lean’s 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 agent’s 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 lea

Czech name

—

Czech description

—

Type

O - Miscellaneous

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2025

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů