5/ This work is a first step towards improving the reliability of learning agents by unifying RL and reactive synthesis.

I'm very grateful to my co-authors for this great collaboration!
Check my blogpost for more insights!

I'll present the paper in a few weeks at @aamasconf.bsky.social

4/ This approach allows for
- a separation of concerns
- formal guarantees through (PAC) bounds on both the world model quality and policy performance
- reusability and scaling to domains where synthesis was not applicable

3/ Given the map, the learned low-level models/policies, and a formal specification describing what the agent should do or not, we apply reactive synthesis to obtain a high-level planner.

2/ We consider scenarios where a "map" describing the environment's high-level structure can be provided as a graph. Each vertex is a "room," where we apply RL to get low-level policies. In addition, we learn a world model of each room that can be formally verified.

1/ RL enables agents to learn efficient policies in complex domains, but lacks formal guarantees — a challenge in high-stakes scenarios. In contrast, when the environment model is accessible, reactive synthesis offers formal guarantees, but struggles to scale.

📌

Thanks!

Hi, I'd be pleased if you could add me too if there's still room :-)

Thanks!

Hey, I’d love to be added!

hey! working on RL and formal verification, do you mind adding me? :-)