Formal Methods in AI Rigorous foundations for trustworthy intelligent systems

Software

Software repositories and documentation will appear here. Expect verification toolchains, benchmarks, and example integrations.

Library

MASA Safe-RL

Modular library for safe RL, providing baselines for a number of constraints using a variety of algorithms.

GitHub · MIT License · Docs included

Tool

ProSh

Probabilistic shielding for constrained Markov Decision Processes with unknown safety dynamics

GitHub · MIT License · Docs included

Tool

PMAS

Probabilistic shielding for decentralised multiagent RL with dynamics induced through world and opponent modelling.

GitHub · MIT License · Docs included

Tool

GR(1) Shielding

Adaptive shielding using GR(1) specifications and Inductive Logic Programming to repair specifications

GitHub · MIT License · Docs included

Tool

Approximate Model-Based Shielding

Latent shielding for safe RL, including continuous dynamics using DreamerV3

GitHub · MIT License · Docs included

Tool

Quantitative Reward Monitoring

Write formal Reinforcement Learning reward specifications in Quantitative Linear Temporal Logic on finite traces.

GitHub · MIT License · Docs included