Timezone: »
We study the problem of learning verifiably safe parameters for programs that use neural networks as well as symbolic, human-written code. Such neurosymbolic programs arise in many safety-critical domains. However, because they need not be differentiable, they cannot be learned using existing approaches to integrating learning and verification. Our method, Differentiable Symbolic Execution (DSE), learns such programs by sampling code paths using symbolic execution, constructing gradients of a worst-case ``safety loss'' along these paths, and then backpropagating these gradients through program operations using a generalization of the reinforce estimator. We evaluate the method on a mix of synthetic tasks and real-world control and navigation benchmarks. Our experiments show that DSE significantly outperforms the state-of-the-art DiffAI method on these tasks.
Author Information
Chenxi Yang (University of Texas, Austin)
Swarat Chaudhuri (The University of Texas at Austin)
More from the Same Authors
-
2021 Spotlight: Neural Program Generation Modulo Static Analysis »
Rohan Mukherjee · Yeming Wen · Dipak Chaudhari · Thomas Reps · Swarat Chaudhuri · Christopher Jermaine -
2022 : Neurosymbolic Programming for Science »
Jennifer J Sun · Megan Tjandrasuwita · Atharva Sehgal · Armando Solar-Lezama · Swarat Chaudhuri · Yisong Yue · Omar Costilla Reyes -
2022 : Q & A »
Swarat Chaudhuri · Jennifer J Sun · Armando Solar-Lezama -
2022 Tutorial: Neurosymbolic Programming »
Swarat Chaudhuri · Jennifer J Sun · Armando Solar-Lezama -
2022 : Neurosymbolic Programming »
Swarat Chaudhuri · Jennifer J Sun · Armando Solar-Lezama -
2022 Poster: Policy Optimization with Linear Temporal Logic Constraints »
Cameron Voloshin · Hoang Le · Swarat Chaudhuri · Yisong Yue -
2021 Poster: Neural Program Generation Modulo Static Analysis »
Rohan Mukherjee · Yeming Wen · Dipak Chaudhari · Thomas Reps · Swarat Chaudhuri · Christopher Jermaine -
2020 : Swarat Chaudhuri Talk »
Swarat Chaudhuri -
2020 Poster: Learning Differentiable Programs with Admissible Neural Heuristics »
Ameesh Shah · Eric Zhan · Jennifer J Sun · Abhinav Verma · Yisong Yue · Swarat Chaudhuri -
2020 Poster: Neurosymbolic Reinforcement Learning with Formally Verified Exploration »
Greg Anderson · Abhinav Verma · Isil Dillig · Swarat Chaudhuri