Formal Specification and Testing for Reinforcement LearningRemote
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 \emph{any} reinforcement learning problem modeled using our library, without any additional effort from the programmer.
Wed 6 SepDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | |||
10:30 30mTalk | Reflecting on Random GenerationDistinguished Paper ICFP Papers and Events Harrison Goldstein University of Pennsylvania, Samantha Frohlich University of Bristol, Meng Wang University of Bristol, Benjamin C. Pierce University of Pennsylvania DOI | ||
11:00 30mTalk | Etna: An Evaluation Platform for Property-Based Testing (Experience Report)Experience Report ICFP Papers and Events Jessica Shi University of Pennsylvania, Alperen Keles University of Maryland at College Park, Harrison Goldstein University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Leonidas Lampropoulos University of Maryland, College Park DOI | ||
11:30 30mTalk | Formal Specification and Testing for Reinforcement LearningRemote ICFP Papers and Events Mahsa Varshosaz IT University of Copenhagen, Denmark, Mohsen Ghaffari IT University of Copenhagen, Einar Broch Johnsen University of Oslo, Andrzej Wąsowski IT University of Copenhagen, Denmark DOI |