Formal Specification and Testing for Reinforcement Learning

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskning

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.
OriginalsprogEngelsk
Artikelnummer193
TidsskriftProceedings of the ACM on Programming Languages
Vol/bind7
Udgave nummerIssue ICFP
Sider (fra-til)125-158
Antal sider33
DOI
StatusUdgivet - 2023

Fingeraftryk

Dyk ned i forskningsemnerne om 'Formal Specification and Testing for Reinforcement Learning'. Sammen danner de et unikt fingeraftryk.

Citationsformater