Formal Specification and Testing for Reinforcement Learning

Research output: Journal Article or Conference Article in JournalJournal articleResearch


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.
Original languageEnglish
Article number193
JournalProceedings of the ACM on Programming Languages
Issue numberIssue ICFP
Pages (from-to)125-158
Number of pages33
Publication statusPublished - 2023


  • Theory of computation
  • Program specifications
  • Software testing and debugging


Dive into the research topics of 'Formal Specification and Testing for Reinforcement Learning'. Together they form a unique fingerprint.

Cite this