Skip to content
conftrace_
2023 AAAI AAAI 2023

Formally Verified Solution Methods for Markov Decision Processes

Abstract

Abstract We formally verify executable algorithms for solving Markov decision processes (MDPs) in the interactive theorem prover Isabelle/HOL. We build on existing formalizations of probability theory to analyze the expected total reward criterion on finite and infinite-horizon problems. Our developments formalize the Bellman equation and give conditions under which optimal policies exist. Based on this analysis, we verify dynamic programming algorithms to solve tabular MDPs. We evaluate the formally verified implementations experimentally on standard problems, compare them with state-of-the-art systems, and show that they are practical.

🌉 Interdisciplinary Bridge - Artificial Intelligence and Mathematics & Optimization and Reinforcement Learning

Authors

Maximilian Schäffeler, Mohammad Abdulaziz

Topics

Machine Learning > Optimization & Theory > Theory Reinforcement Learning > Applications > Value Iteration Machine Learning > Bayesian & Probabilistic > Probabilistic Modeling Machine Learning > Learning Types > Reinforcement Learning Mathematics & Optimization > Optimization > Optimization

Keywords

formal verification markov decision process bellman equation dynamic programming probability theory expected total reward
Download PDF

More from AAAI 2023

All AAAI 2023 papers →
Certified Policy Smoothing for Cooperative Multi-Agent Reinforcement Learning
Constrained Reinforcement Learning in Hard Exploration Problems
Defending from Physically-Realizable Adversarial Attacks through Internal Over-Activation Analysis
Improving Training and Inference of Face Recognition Models via Random Temperature Scaling
Task and Model Agnostic Adversarial Attack on Graph Neural Networks
Robust Sequence Networked Submodular Maximization