Formal Specification and Testing for Reinforcement Learning
summary
Defines a declarative DSL called BDL domain-specific language that encodes TD backup diagrams, gives a denotational semantics, and generates executable specs used as test oracles. Implements tabular TD agents in Scala and exercises them with ScalaCheck tests that compare learned distributions to the BDL interpreter. Evaluates via mutation testing and reports 90% mutants killed for 75% of subject agents, with 48% of injected bugs found by generic tests alone. Code and artifacts are available alongside the paper.
AI-written summary · about
chapters (13)
- 0:00Reinforcement learning testing intro
- 2:29Testing RL challenges
- 3:52Formalizing RL setup
- 8:49TD algorithms description
- 13:40BDL semantics interpreter
- 15:03Property-based testing framework
- 18:36Implementation reusable components
- 19:22Mutation testing evaluation
- 20:27Future directions
- 21:09Coverage in continuous states
- 22:34RL formalism impact
- 25:06Tabular specs verification
- 26:53Subtle bug detection
related talks
28mA Reinforcement Learning Framework in Scala 3
39mLet LLMs Wander: Engineering RL Environments
16mA Model-Driven Generative Self Play-Based Toolchain for Developing Games and Players
33mFormal Verification of Probabilistic Deep Reinforcement Learning Policies with(…)
01h 17mTraining intelligent game agents using deep reinforcement learning
15mDLSpec: A Deep Learning Task Exchange Specification
24mTesting Techniques for Critical Deep Learning Applications
56mA Tutorial on Reinforcement Learning II