[ICFP'23] Formal Specification and Testing for Reinforcement Learning

Formal Specification and Testing for Reinforcement Learning (Video, ICFP 2023) Mahsa Varshosaz, Mohsen Ghaffari, Einar Broch Johnsen, and Andrzej Wąsowski (IT University of Copenhagen, Denmark; IT University of Copenhagen, Denmark; University of Oslo, Norway; IT University of Copenhagen, Denmark) Abstract: The development process for reinforcement learning applications is still exploratory rather than systematic. This exploratory nature reduces reuse of specifications between applications and increases the chances of introducing programming errors. This paper takes a step towards systematizing the development of reinforcement learning applications. We introduce a formal specification of reinforcement learning problems and algorithms, with a particular focus on temporal difference methods and their definitions in backup diagrams. We further develop a test harness for a large class of reinforcement learning applications based on temporal difference learning, including SARSA and Q-learning. The entire development is rooted in functional programming methods; starting with pure specifications and denotational semantics, ending with property-based testing and using compositional interpreters for a domain-specific term language as a test oracle for concrete implementations. We demonstrate the usefulness of this testing method on a number of examples, and evaluate with mutation testing. We show that our test suite is effective in killing mutants (90% mutants killed for 75% of subject agents). More importantly, almost half of all mutants are killed by generic write-once-use-everywhere tests that apply to any reinforcement learning problem modeled using our library, without any additional effort from the programmer. Article: https://doi.org/10.1145/3607835 Supplementary archive: https://doi.org/10.5281/zenodo.8083298 (Badges: Artifacts Available, Artifacts Evaluated — Reusable) ORCID: https://orcid.org/0000-0002-4776-883X, https://orcid.org/0000-0002-1939-9053, https://orcid.org/0000-0001-5382-3949, https://orcid.org/0000-0003-0532-2685 Video Tags: specification-based testing, reinforcement learning, Scala, icfp23main-p17-p, doi:10.1145/3607835, doi:10.5281/zenodo.8083298, orcid:0000-0002-4776-883X, orcid:0000-0002-1939-9053, orcid:0000-0001-5382-3949, orcid:0000-0003-0532-2685, Artifacts Available, Artifacts Evaluated — Reusable Presentation at the ICFP 2023 conference, September 4–9, 2023, https://icfp23.sigplan.org/ Sponsored by ACM SIGPLAN, https://www.sigplan.org/