pith. sign in

arxiv: 1907.07273 · v1 · pith:ZWJFBTQXnew · submitted 2019-07-16 · 💻 cs.LG · cs.AI· stat.ML

An Inductive Synthesis Framework for Verifiable Reinforcement Learning

He Zhu , Zikang Xiong , Stephen Magill , Suresh Jagannathan This is my paper

Pith reviewed 2026-05-24 20:42 UTC · model grok-4.3

classification 💻 cs.LG cs.AIstat.ML
keywords reinforcement learningformal verificationinductive synthesissafety verificationneural network approximationinductive invariantscyber-physical systemsruntime monitoring
0
0 comments X

The pith

Synthesized deterministic programs can enforce safety in reinforcement learning by approximating neural policies and proving invariants over infinite states.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper tries to establish that formal verification methods from conventional software can be repurposed for reinforcement learning without directly inspecting neural network weights. It frames verification as a search for a simpler deterministic program that approximates the network's behavior and comes equipped with an inductive invariant proving the desired safety property. The synthesized program then runs alongside the network to monitor proposed actions and block any that would violate the invariant. A sympathetic reader would care because this supplies concrete assurance guarantees for systems that must operate in unseen environments, while keeping the neural component intact.

Core claim

A counterexample-guided syntax-guided inductive synthesis procedure searches for both a deterministic program and an inductive invariant over an infinite state transition system that encodes the application's control logic; when found, the program is deployed with the neural policy to dynamically block unsafe actions while preserving the original network's performance.

What carries the argument

The counterexample-guided syntax-guided inductive synthesis procedure that jointly discovers a deterministic program approximating the neural policy and an inductive invariant proving safety over an infinite state space.

If this is right

  • Safety can be enforced at runtime by intercepting and rejecting unsafe actions proposed by the neural policy.
  • Verification extends to infinite state spaces through inductive invariants rather than finite enumeration.
  • Environment-specific constraints supplied by the user further restrict the space of candidate programs.
  • The approach applies across multiple cyber-physical control tasks with modest runtime overhead.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same synthesis loop could be applied to other learned controllers that must satisfy temporal logic specifications.
  • If the synthesized program is small enough, it could serve as an interpretable surrogate for post-deployment auditing.
  • A mismatch between the program and the network on new inputs would indicate the need to retrain or resynthesize.
  • The technique might be combined with reachability analysis to tighten the invariants further.

Load-bearing premise

That the synthesis procedure can consistently locate a deterministic program close enough to the neural policy that also admits an inductive invariant sufficient to prove the target safety properties.

What would settle it

An environment in which the neural policy produces an action the synthesized program permits, yet that action leads to a safety violation that the invariant was supposed to prevent.

Figures

Figures reproduced from arXiv: 1907.07273 by He Zhu, Stephen Magill, Suresh Jagannathan, Zikang Xiong.

Figure 1
Figure 1. Figure 1: Inverted Pendulum State Transition System. The pendulum has mass m and length l. A system state is s = [η,ω] T where η is the its angle and ω is its angular velocity. A continuous control action a maintains the pendulum upright. 2.1 State Transition System We model an inverted pendulum system as an infinite state transition system with continuous actions in [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The Framework of Our Approach. We assume the existence of a neural network control pol￾icy πw : R 2 → R that executes actions over the pendu￾lum, whose weight values of w are learned from training episodes. This policy is a state-dependent function, mapping a 2-dimensional state s (η and ω) to a control action a. At each transition, the policy mitigates uncertainty through feedback over state variables in … view at source ↗
Figure 3
Figure 3. Figure 3: Invariant Inference on Inverted Pendulum [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The Framework of Neural Network Shielding. we find that the neural policy is never interrupted by the deterministic program when governing the pendulum. Note that the non-shaded areas in [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Syntax of the Policy Programming Language. Algorithm 1: Synthesize (πw, P[θ], C[·]) 1 θ ← 0; 2 do 3 Sample δ from a zero mean Gaussian vector; 4 Sample a set of trajectories C1 using C[Pθ+ν δ ]; 5 Sample a set of trajectories C2 using C[Pθ−ν δ ]; 6 θ ← θ + α[ d(πw, Pθ+ν δ ,C1)−d(πw, Pθ−ν δ ,C2) ν ]δ; 7 while θ is not converged; 8 return Pθ a collection of variables can be expressed as: P[θ](X) ::= return θ… view at source ↗
Figure 6
Figure 6. Figure 6: CEGIS for Verifiable Reinforcement Learning. If verification fails in line 11, our approach simply reduces the initial state space, hoping that a safe policy program is easier to synthesize if only a subset of initial states are con￾sidered. The algorithm in line 12 gradually shrinks the radius r ∗ of the initial state space around the sampled initial state s0. The synthesis algorithm in the next iteration… view at source ↗
read the original abstract

Despite the tremendous advances that have been made in the last decade on developing useful machine-learning applications, their wider adoption has been hindered by the lack of strong assurance guarantees that can be made about their behavior. In this paper, we consider how formal verification techniques developed for traditional software systems can be repurposed for verification of reinforcement learning-enabled ones, a particularly important class of machine learning systems. Rather than enforcing safety by examining and altering the structure of a complex neural network implementation, our technique uses blackbox methods to synthesizes deterministic programs, simpler, more interpretable, approximations of the network that can nonetheless guarantee desired safety properties are preserved, even when the network is deployed in unanticipated or previously unobserved environments. Our methodology frames the problem of neural network verification in terms of a counterexample and syntax-guided inductive synthesis procedure over these programs. The synthesis procedure searches for both a deterministic program and an inductive invariant over an infinite state transition system that represents a specification of an application's control logic. Additional specifications defining environment-based constraints can also be provided to further refine the search space. Synthesized programs deployed in conjunction with a neural network implementation dynamically enforce safety conditions by monitoring and preventing potentially unsafe actions proposed by neural policies. Experimental results over a wide range of cyber-physical applications demonstrate that software-inspired formal verification techniques can be used to realize trustworthy reinforcement learning systems with low overhead.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper presents a framework for verifiable reinforcement learning that repurposes formal verification techniques by using counterexample-guided syntax-guided inductive synthesis to generate deterministic programs as simpler, interpretable approximations of neural network policies. These programs are paired with inductive invariants over infinite-state transition systems (with optional environment constraints) to prove safety properties; the synthesized programs then act as runtime shields that monitor and block unsafe actions proposed by the neural policy. The approach is evaluated experimentally on cyber-physical benchmarks.

Significance. If the synthesis procedure reliably produces faithful program approximations that admit useful invariants, the work provides a practical route to safety guarantees for RL systems without modifying the neural network itself, combining black-box synthesis with formal methods. The experimental demonstration on multiple cyber-physical applications is a concrete strength, showing low-overhead dynamic enforcement in practice.

major comments (1)
  1. The central claim (abstract and synthesis description) requires that the CEGIS-style procedure can discover deterministic programs P that sufficiently approximate the neural policy while admitting inductive invariants proving safety over infinite state spaces. No termination, success-rate, or approximation-quality guarantees are supplied for this search; success is shown only experimentally on selected benchmarks. If the procedure fails to return a suitable P or returns one whose invariant is too coarse, the dynamic enforcement mechanism does not materialize.
minor comments (1)
  1. The abstract refers to 'a wide range of cyber-physical applications' but does not specify the exact benchmarks, success rates, or overhead measurements; these details should be summarized with quantitative results in the abstract or introduction.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive review and positive assessment of the framework's significance and experimental evaluation. We address the single major comment below.

read point-by-point responses

  1. Referee: The central claim (abstract and synthesis description) requires that the CEGIS-style procedure can discover deterministic programs P that sufficiently approximate the neural policy while admitting inductive invariants proving safety over infinite state spaces. No termination, success-rate, or approximation-quality guarantees are supplied for this search; success is shown only experimentally on selected benchmarks. If the procedure fails to return a suitable P or returns one whose invariant is too coarse, the dynamic enforcement mechanism does not materialize.

    Authors: We agree that the CEGIS-based synthesis procedure provides no termination, success-rate, or approximation-quality guarantees; such guarantees are unavailable in general because the underlying problem of synthesizing programs and inductive invariants over infinite-state systems is undecidable. The manuscript's central claim is that the framework enables verifiable safety enforcement when synthesis succeeds, rather than that synthesis always succeeds. The experimental results demonstrate that the procedure produces usable programs and invariants on the chosen cyber-physical benchmarks with low runtime overhead. When synthesis fails to return a suitable P, the neural policy is simply deployed without the shield, which is the expected behavior of an optional runtime monitor. We will revise the abstract, introduction, and conclusion to explicitly note this limitation and the undecidability of the synthesis problem. revision: partial

Circularity Check

0 steps flagged

No significant circularity; methodology applies external synthesis techniques to RL without self-referential reductions

full rationale

The paper frames neural policy verification as a counterexample-guided syntax-guided inductive synthesis search for both a deterministic program and an inductive invariant. This is presented as an application of established formal methods (CEGIS-style synthesis) to the RL setting, with success shown via experimental results on cyber-physical benchmarks rather than by any derivation that reduces to its own inputs. No equations or claims equate a 'prediction' to a fitted parameter, no load-bearing self-citations justify uniqueness, and the abstract and framing invoke no self-definitional loops. The approach is self-contained against external benchmarks and formal techniques.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the effectiveness of the inductive synthesis procedure and the existence of suitable inductive invariants; these are domain assumptions not supplied by prior literature in the abstract.

axioms (1)
  • domain assumption A counterexample-guided syntax-guided inductive synthesis procedure can find deterministic programs that approximate neural policies while preserving safety properties via inductive invariants over infinite state transition systems.
    This is the core premise invoked when the abstract frames verification as a synthesis problem.

pith-pipeline@v0.9.0 · 5777 in / 1210 out tokens · 17895 ms · 2026-05-24T20:42:53.530400+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

53 extracted references · 53 canonical work pages · 2 internal anchors

  1. [1]

    Ahmadi, C

    M. Ahmadi, C. Rowley, and U. Topcu. 2018. Control-Oriented Learning of Lagrangian and Hamiltonian Systems. In American Control Confer- ence

    work page 2018

  2. [2]

    Akametalu, Shahab Kaynama, Jaime F

    Anayo K. Akametalu, Shahab Kaynama, Jaime F. Fisac, Melanie Nicole Zeilinger, Jeremy H. Gillula, and Claire J. Tomlin. 2014. Reachability- based safe learning with Gaussian processes. In 53rd IEEE Conference on Decision and Control, CDC 2014 . 1424–1431

    work page 2014

  3. [3]

    Akametalu, Shahab Kaynama, Jaime F

    Anayo K. Akametalu, Shahab Kaynama, Jaime F. Fisac, Melanie Nicole Zeilinger, Jeremy H. Gillula, and Claire J. Tomlin. 2014. Reachability- based safe learning with Gaussian processes. In 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014. 1424–1431

    work page 2014

  4. [4]

    Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu. 2018. Safe Reinforce- ment Learning via Shielding. AAAI (2018)

    work page 2018

  5. [5]

    Madhusudan, Milo M

    Rajeev Alur, Rastislav Bodík, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa

    work page

  6. [6]

    In Dependable Software Systems Engi- neering

    Syntax-Guided Synthesis. In Dependable Software Systems Engi- neering. NATO Science for Peace and Security Series, D: Information and Communication Security, Vol. 40. IOS Press, 1–25

    work page

  7. [7]

    MOSEK ApS. 2018. The mosek optimization software . http://www. mosek.com

    work page 2018

  8. [8]

    Somil Bansal, Mo Chen, Sylvia Herbert, and Claire J Tomlin. 2017. Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances. (2017)

    work page 2017

  9. [9]

    Nori, and Antonio Criminisi

    Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vy- tiniotis, Aditya V. Nori, and Antonio Criminisi. 2016. Measuring Neural Net Robustness with Constraints. In Proceedings of the 30th Interna- tional Conference on Neural Information Processing Systems (NIPS’16) . 2621–2629

    work page 2016

  10. [10]

    Osbert Bastani, Yewen Pu, and Armando Solar-Lezama. 2018. Verifiable Reinforcement Learning via Policy Extraction. CoRR abs/1805.08328 (2018)

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  11. [11]

    Richard N Bergman, Diane T Finegood, and Marilyn Ader. 1985. As- sessment of insulin sensitivity in vivo. Endocrine reviews 6, 1 (1985), 45–86

    work page 1985

  12. [12]

    Schoellig, and Andreas Krause

    Felix Berkenkamp, Matteo Turchetta, Angela P. Schoellig, and Andreas Krause. 2017. Safe Model-based Reinforcement Learning with Stability Guarantees. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017 . 908– 919

    work page 2017

  13. [13]

    Roderick Bloem, Bettina Könighofer, Robert Könighofer, and Chao Wang. 2015. Shield Synthesis: - Runtime Enforcement for Reactive Systems. In Tools and Algorithms for the Construction and Analysis of 14 Systems - 21st International Conference, TACAS 2015 . 533–548

    work page 2015

  14. [14]

    Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th Inter- national Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08). 337–340

    work page 2008

  15. [15]

    Peter Dorato, Vito Cerone, and Chaouki Abdallah. 1994. Linear- Quadratic Control: An Introduction. Simon & Schuster, Inc., New York, NY, USA

    work page 1994

  16. [16]

    Chuchu Fan, Umang Mathur, Sayan Mitra, and Mahesh Viswanathan

    work page

  17. [17]

    In Computer Aided Verification - 30th International Conference, CA V 2018

    Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics. In Computer Aided Verification - 30th International Conference, CA V 2018. 347–366

    work page 2018

  18. [18]

    Livingston, Necmiye Ozay, and Richard M

    Ioannis Filippidis, Sumanth Dathathri, Scott C. Livingston, Necmiye Ozay, and Richard M. Murray. 2016. Control design for hybrid sys- tems with TuLiP: The Temporal Logic Planning toolbox. In 2016 IEEE Conference on Control Applications, CCA 2016 . 1030–1041

    work page 2016

  19. [19]

    Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. 2018. AI2: Safety and Robust- ness Certification of Neural Networks with Abstract Interpretation. In 2018 IEEE Symposium on Security and Privacy, SP 2018 . 3–18

    work page 2018

  20. [20]

    Gillula and Claire J

    Jeremy H. Gillula and Claire J. Tomlin. 2012. Guaranteed Safe Online Learning via Reachability: tracking a ground target using a quadrotor. In IEEE International Conference on Robotics and Automation, ICRA 2012, 14-18 May, 2012, St. Paul, Minnesota, USA . 2723–2730

    work page 2012

  21. [21]

    Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan

    work page

  22. [22]

    In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’08)

    Program Analysis As Constraint Solving. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’08). 281–292

    work page

  23. [23]

    Sumit Gulwani and Ashish Tiwari. 2008. Constraint-based approach for analysis of hybrid systems. InInternational Conference on Computer Aided Verification. 190–203

    work page 2008

  24. [24]

    Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety Verification of Deep Neural Networks. InCA V (1) (Lecture Notes in Computer Science), Vol. 10426. 3–29

    work page 2017

  25. [25]

    Dominic W Jordan and Peter Smith. 1987. Nonlinear ordinary differ- ential equations. (1987)

    work page 1987

  26. [26]

    Barrett, David L

    Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Computer Aided Verification - 29th Interna- tional Conference, CA V 2017. 97–117

    work page 2017

  27. [27]

    Hui Kong, Fei He, Xiaoyu Song, William N. N. Hung, and Ming Gu

    work page

  28. [28]

    In Proceedings of the 25th International Conference on Computer Aided Verification (CA V’13)

    Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems. In Proceedings of the 25th International Conference on Computer Aided Verification (CA V’13). 242– 257

    work page

  29. [29]

    Bettina Könighofer, Mohammed Alshiekh, Roderick Bloem, Laura Humphrey, Robert Könighofer, Ufuk Topcu, and Chao Wang. 2017. Shield Synthesis. Form. Methods Syst. Des. 51, 2 (Nov. 2017), 332–361

    work page 2017

  30. [30]

    2017 (accessed Nov 16, 2018)

    Benoît Legat, Chris Coey, Robin Deits, Joey Huchette, and Amelia Perry. 2017 (accessed Nov 16, 2018). Sum-of-squares optimization in Julia. https://www.juliaopt.org/meetings/mit2017/legat.pdf

    work page 2017

  31. [31]

    Yuxi Li. 2017. Deep Reinforcement Learning: An Overview. CoRR abs/1701.07274 (2017)

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  32. [32]

    Lillicrap, Jonathan J

    Timothy P. Lillicrap, Jonathan J. Hunt, Alexander Pritzel, Nicolas Heess, Tom Erez, Yuval Tassa, David Silver, and Daan Wierstra. 2016. Contin- uous control with deep reinforcement learning. In 4th International Conference on Learning Representations, ICLR 2016, San Juan, Puerto Rico, May 2-4, 2016, Conference Track Proceedings

    work page 2016

  33. [33]

    Horia Mania, Aurelia Guy, and Benjamin Recht. 2018. Simple random search of static linear policies is competitive for reinforcement learning. In Advances in Neural Information Processing Systems 31 . 1800–1809

    work page 2018

  34. [34]

    J Matyas. 1965. Random optimization. Automation and Remote Control 26, 2 (1965), 246–253

    work page 1965

  35. [35]

    Matthew Mirman, Timon Gehr, and Martin T. Vechev. 2018. Differen- tiable Abstract Interpretation for Provably Robust Neural Networks. In Proceedings of the 35th International Conference on Machine Learning, ICML 2018. 3575–3583

    work page 2018

  36. [36]

    Teodor Mihai Moldovan and Pieter Abbeel. 2012. Safe Exploration in Markov Decision Processes. In Proceedings of the 29th International Coference on International Conference on Machine Learning (ICML’12) . 1451–1458

    work page 2012

  37. [37]

    Yurii Nesterov and Vladimir Spokoiny. 2017. Random Gradient-Free Minimization of Convex Functions. Found. Comput. Math. 17, 2 (2017), 527–566

    work page 2017

  38. [38]

    Stephen Prajna and Ali Jadbabaie. 2004. Safety Verification of Hybrid Systems Using Barrier Certificates. In Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004 . 477–492

    work page 2004

  39. [39]

    Aravind Rajeswaran, Kendall Lowrey, Emanuel Todorov, and Sham M. Kakade. 2017. Towards Generalization and Simplicity in Continu- ous Control. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017 . 6553–6564

    work page 2017

  40. [40]

    Gordon, and Drew Bagnell

    Stéphane Ross, Geoffrey J. Gordon, and Drew Bagnell. 2011. A Re- duction of Imitation Learning and Structured Prediction to No-Regret Online Learning. In Proceedings of the Fourteenth International Confer- ence on Artificial Intelligence and Statistics, AISTATS 2011 . 627–635

    work page 2011

  41. [41]

    Wenjie Ruan, Xiaowei Huang, and Marta Kwiatkowska. 2018. Reacha- bility Analysis of Deep Neural Networks with Provable Guarantees. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018. 2651–2659

    work page 2018

  42. [42]

    Stefan Schaal. 1999. Is imitation learning the route to humanoid robots? Trends in cognitive sciences 3, 6 (1999), 233–242

    work page 1999

  43. [43]

    Bastian Schürmann and Matthias Althoff. 2017. Optimal control of sets of solutions to formally guarantee constraints of disturbed linear systems. In 2017 American Control Conference, ACC 2017 . 2522–2529

    work page 2017

  44. [44]

    David Silver, Guy Lever, Nicolas Heess, Thomas Degris, Daan Wierstra, and Martin Riedmiller. 2014. Deterministic Policy Gradient Algorithms. In Proceedings of the 31st International Conference on International Conference on Machine Learning - Volume 32 . I–387–I–395

    work page 2014

  45. [45]

    Armando Solar-Lezama. 2008. Program Synthesis by Sketching . Ph.D. Dissertation. Berkeley, CA, USA. Advisor(s) Bodik, Rastislav

    work page 2008

  46. [46]

    Armando Solar-Lezama. 2009. The Sketching Approach to Program Synthesis. In Proceedings of the 7th Asian Symposium on Programming Languages and Systems (APLAS ’09). 4–13

    work page 2009

  47. [47]

    Youcheng Sun, Min Wu, Wenjie Ruan, Xiaowei Huang, Marta Kwiatkowska, and Daniel Kroening. 2018. Concolic Testing for Deep Neural Networks. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE 2018) . 109–119

    work page 2018

  48. [48]

    Russ Tedrake. 2009. LQR-trees: Feedback motion planning on sparse randomized trees. In Robotics: Science and Systems V, University of Washington, Seattle, USA, June 28 - July 1, 2009

    work page 2009

  49. [49]

    Yuchi Tian, Kexin Pei, Suman Jana, and Baishakhi Ray. 2018. DeepTest: Automated Testing of Deep-neural-network-driven Autonomous Cars. In Proceedings of the 40th International Conference on Software Engi- neering (ICSE ’18). 303–314

    work page 2018

  50. [50]

    Matteo Turchetta, Felix Berkenkamp, and Andreas Krause. 2016. Safe Exploration in Finite Markov Decision Processes with Gaussian Pro- cesses. In Proceedings of the 30th International Conference on Neural Information Processing Systems (NIPS’16). 4312–4320

    work page 2016

  51. [51]

    Abhinav Verma, Vijayaraghavan Murali, Rishabh Singh, Pushmeet Kohli, and Swarat Chaudhuri. 2018. Programmatically Interpretable Reinforcement Learning. In Proceedings of the 35th International Con- ference on Machine Learning, ICML 2018 . 5052–5061

    work page 2018

  52. [52]

    Matthew Wicker, Xiaowei Huang, and Marta Kwiatkowska. 2018. Feature-Guided Black-Box Safety Testing of Deep Neural Networks. In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018. 408–426. 15

    work page 2018

  53. [53]

    He Zhu, Zikang Xiong, Stephen Magill, and Suresh Jagannathan. 2018. An Inductive Synthesis Framework for Verifiable Reinforcement Learn- ing. Technical Report. Galois, Inc. http://herowanzhu.github.io/ herowanzhu.github.io/VerifiableLearning.pdf 16

    work page 2018