Safe Neurosymbolic Learning with Differentiable Symbolic Execution
Authors: Chenxi Yang
Swarat Chaudhuri
Venue: ICLR 2022 Poster (2022)
Keywords: Verified Learning
Neurosymbolic Programs
Safe Learning
Symbolic Execution

Abstract: 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, it is hard to learn their parameters using existing gradient-based approaches to safe learning. Our method, Differentiable Symbolic Execution (DSE), samples control flow paths in a program, symbolically constructs worst-case "safety loss" along these paths, and backpropagates the gradients of these losses through program operations using a generalization of the REINFORCE estimator. We evaluate the method on a mix of synthetic tasks and real-world benchmarks. Our experiments show that DSE significantly outperforms the state-of-the-art DiffAI method on these tasks.  

Published as a conference paper at ICLR 2022
SAFE NEUROSYMBOLIC LEARNING WITH DIFFERENTIABLE SYMBOLIC EXECUTION
Chenxi Yang, Swarat Chaudhuri The University of Texas at Austin
ABSTRACT
We study the problem of learning worst-case-safe parameters for programs that use neural networks as well as symbolic, human-written code. Such neurosym- bolic programs arise in many safety-critical domains. However, because they use nondifferentiable operations, it is hard to learn their parameters using exist- ing gradient-based approaches safe learning. Our approach to this problem, Differentiable Symbolic Execution (DSE), samples control flow paths in pro- gram, symbolically constructs worst-case "safety losses" along these paths, and backpropagates the gradients of these losses through program operations using a generalization of the REINFORCE estimator. We evaluate the method on a mix of synthetic tasks and real-world benchmarks. Our experiments show that DSE significantly outperforms the state-of-the DIFFAI method on these tasks T
INTRODUCTION
Safety on worst-case inputs has recently emerged as a key challenge in deep learning research. For- mal verification of neural networks (Albarghouthil (221T) 1 is established response to this challenge. In particular, a body of recent work (Mirman et al., 2018 Madry et al. 2017, Cohen et al.) 2019) Singhh al.] 2018) seeks to incorporate formal verification into the training of neural networks.
DIFFAI, among the most prominent of such approaches, uses a neural network verifier to construct differentiable, worst-case safety loss for the learner. This loss is used regularize standard data-driven loss, biasing the learner towards parameters that are both performant and safe.
weakness of these methods that they only consider functional properties (such as adversarial robustness) of isolated neural networks. By contrast, in real-world applications. neural networks are often embedded within human-written symbolic code, and correctness requirements apply the neurosymbolic programs (Chaudhuri et al. 2021 obtained by composing the two. For example, consider a car directed by neural controller (Qin Badgwell] (000). Safety properties for the car are functions of its trajectories, and these trajectories depend not just the controller but also the symbolic equations that define the environment. While recent work (Christakis et al. (20TT) has studied the verification of such neurosymbolic programs, there is no prior work on integrating verification and learning for such systems.
In this paper, we present the first steps towards such integration. The fundamental technical challenge here is that while a neural network is differentiable in its parameters, the code surrounding it may be non-differentiable even discontinuous. This makes problem a poor fit for methods like DIFFAI, which were designed for fully differentiable learning objectives.
We solve the problem using new method, Differentiable Symbolic Execution (DSE), that timate gradients of worst-case safety losses of nondifferentiable neurosymbolic programs. Our method approximates the program's worst-case safety loss by integral over the safety losses along individual control flow paths in the program. We compute the gradients of this integral us- ing generalization of the classic REINFORCE estimator (Williams) 1992). The gradient updates resulting from this process balance two goals: (i) choosing the parameters of individual paths so that program trajectories that follow them are safer, and (ii) learning the parameters of conditional branches so that the program is discouraged from entering unsafe paths. The procedure requires
Our implementation of DSF is available wtttp:///ghhuubccmmm/yyygg999990

---

Published as a conference paper at ICLR 2022
Example(x); E/-5, y:= (N,(x)
Loc = (12, 4, (2, (12)
Inst (-5 5)
if y < 1.0:
Safe(l)) = (2 1), Safe(12) = True, Safe(la) (
True
2 = x 10.0
Transy [(f2, True, (y = NN)
5
clse:
(6.. & 1.0), (2 = 10.0),
6
== 5.0
(fa. 1.0), (s 5.0),
assert (z <=
Figure I: (Left) An example program. NN is a neural network with parameters DIFFAI fails to learn safe parameters for this program. (Right) The program as STS. Each location & corresponds to line i the program. For brevity, the updates only depict the variable that changes value.
method for sampling paths and computing the safety loss for individual paths. We use a version of symbolic execution (Baldoni et al., (018)) to this end.
We evaluate DSE through several problems from the embedded control and navigation domains, as well as several synthetic tasks. Our baselines include an extended version of DIFFAI, the current state of the art, and an ablation that does not use an explicit safety loss. Our experiments show that DSE significantly outperforms the baselines in finding safe and ligh-performance model parameters.
To summarize, our main contributions are:
We present the first approach to worst-case safe parameter learning for neural networks em- bedded within nondifferentiable, symbolic programs.
As part of our learning algorithm, we give a new way to bring together symbolic execution and stochastic gradient estimators. that might have applications outside our immediate task.
We present experiments that show that DSE can handle programs with complex structure and also outperforms DIFFAI on our problem.
PROBLEM FORMULATION
Programs. We define programs with embedded neural networks symbolic transition systems (STS) (Manna & Pnueli 2012). Formally, program Fg is tuple (Loc, X, Init, Safe, Transo). Here, Loc is a finite set of (control) locations, X = {zI..... Imm] is a set of real-valued variables, and lo E Loc the initial location. Init, a constraint over X, is an initial condition for the pro- gram. Safe is map from locations to constraints over X; intuitively, Safe(l) is safety requirement asserted at location I. Finally, Transg is a transition relation consisting of transitions (1, G. Ug. l') such that: (i) / is the source location and I' is the destination location; (ii) the guard G is constraint over ; and (iii) the update Uo is a vector (U1.0..... Um,0), where each U2o0 is real-valued expres- sion X constructed using standard symbolic operators and neural networks with parameters 0. Intuitively, Use represents the update to the i-th variable. We assume that each Use is differentiable in 0. We also assume that each guard G is of the form 2; that this is not a significant restriction as H; can be made to store the value of a complex expression using an update. Finally, we assume that programs are deterministic. That is, if G and G' are guards for two distinct transitions from the same source state, then G A G' is unsatisfiable.
where IX E {<, >, S, ] note
Programs in higher-level languages can be translated the STS notation in standard way. For example, Figure [ (left) shows simple high-level program. The STS for this program appears in Figure [ (right). While the program simple, the state-of-the-an DIFFAI approach to verified learning fails to learn safe parameters for it.
Safety Semanties. In classical formal methods, program is considered safe all of its executions satisfy safety constraint. However, in learning settings, it helps to know not only whether program unsafe, but also the extent to which it is unsafe. Consequently, we define the safety semantics of programs in terms of (worst-casel safety loss that quantifies a program's 's safeness.
Formally, let a state of Fg be a pair 5 (1, v), where is a location and v E ET is an assignment of values to the variables (i.e., u(t) is the value of xz). Such state is said to be at location 1. For boolean constraints and assignments u to variables in B, let us write ((v) if satisfies B. state (lo, v). where Inii(v), v), is initial state. A state (1, v) is safe if (Safe(!)
Let E RD be an assignment to the variables. For a real-valued expression over X. let E(v) be the value of E when i, is substituted by vi)). For update U (U1,..., Un), we define U(v)
2

---

Published as a conference paper at ICLR 2022
as the assignment (U1 (U).,...... (o)) A length-n trajectory of F6 is sequence (so ... sn), with 8; = (1s, vi), such that: (i) so is an initial state; and (ii) for each i, there is a transition (4,, G, G,U,U44 4,11) such that ((e))) and 11+1 U(.)..
Let us fix a size bound N for trajectories. A trajectory T = (so...., 8n) ) is maximal if it has length N, if there is trajectory r' = (so..... Sa, Su+1) with length I N. Because programs deterministic, there is unique maximal trajectory from each sg. We denote this trajectory by T (8p)-
Let us assume real-valued loss Unsafe(s) that quantifies the unsafeness of each state We require Unsafe(s) = 0 if 8 is safe and Unsafe(s) >> O otherwise. We lift this measure to trajectories 7 by letting Unsafe (T) Es appears 5 Unsafe(s). The safety loss ((0) for Fa is now defined as:
max C(0) an initial state
Unsafe(T(s)).
Thus, C(O) = 0 if and only all program trajectories are safe.
Problem Statement. Our learning problem formalizes a setting in which we have training data for neural networks inside a program Fg. While training the networks with respect to this data, we must ensure that the overall program satisfies its safety requirements.
To ensure that the parameters of the different neural networks in Fsg are not incorrectly entangled, assume in this exposition that only one of these networks, NNs. has trainable parameters P We expect as input a training set of i..dd samples from an unknown distribution over the inputs and outputs of NN,, and differentiable data loss Q(+) that quantifies the network's fidelity to this training set. Our learning goal is to solve the following constrained optimization problem:
min Q(0)
S.T. C(O) S 0.
LEARNING ALGORITHM
The learning approach in DSE is based on two ideas. First, we directly apply a recentlydeveloped equivalence between constrained and regularized learning (Agarwal al. 2018 Le al., 2019) to reduce Equation 2 to series of unconstrained optimization problems. Second, we use the novel technique of differentiating through a symbolic executor to solve these unconstrained problems.
At the highest level, we convexify the class of programs Fe by allowing stochastic combinations of programs. That is, we now allow programs of the form F'g ET a,l',, where E. a; 1. To execute the program Fe from a given initial state, we sample a specific program F'g from the distribution (a.....,,az) ax) and then execute from that state.
Equation (2) can now be written into the problem max mina Q(0) + xC(0), which in turn can be solved using a classic algorithm (Freund & Schapire 1999) for computing equilibria in two-player game. See Appendix A.I for more details on this al algorithm.
A key feature of our high-level algorithm is that it repeatedly solves the optimization problem ming Q(0) + XC(8) for fixed values of X. This problem is challenging because while Q(0) is differentiable in f, C(0) depends on the entirety of Fg and may not even be continuous. DSE, our main contribution, addresses this challenge by constructing a differentiable approximation C# (0) of C(0). We present the details of this method in the next section.
4 DIFFERENTIATING THROUGH A A SYMBOLIC EXECUTOR
Background on Symbolic Execution. DSE uses a refinement of symbolic execution (Baldoni et al.) 2018), a classic technique for systematic formal analysis of programs. Symbolic execution has been recently used to analyze the safety of neural networks (Gopinath et al., 2018)). However, we are not aware of any prior attempt incorporate symbolic execution into neural network training.
NNot that some of our experimental benchmarks have & > trainable neural modules. In these tasks, each neural module comes with its own training data; thus, in effect, we have & instances of the learning problem. Our implementation learns the modules simultancously by interleaving their gradient updates. However, the gradient of Q for each module only influenced by its own data.
3

---

Published as a conference paper at ICLR 2022
A symbolic executor systematically searches the set of symbolic trajectories of programs, which we now define. Consider a program Fg = (Loc, X = {x11...., ,, l0 Init, Safe, Transy) as in Section 2 First, we fix syntactically restricted class Va of boolean constraints over X and B. Vo is required to be closed under conjunction and must include all expressions that can appear as guard in Fa- In particular, in implementation, Vo consists of formulas that specify closed open intervals, with bounds given by expressions over parameters, in which each variable lies.
A symbolic state of Fg is pair oe (1, Vo), where is location and Vo E Va. Intuitively, de rep- resents the set of states of Fg that are at location / and satisfy the property Vg. We designate a finite set of initial symbolic states (lo. v.')..... (lp. V. It required that Init = V, Vj. Intuitively, the initial symbolic states "cover" all the possible initial states of the program Fe.
We also construct an overapproximate update U Vo + Vo for each update Ug in Fo. For all V Vg. we have (o) = U# (V). where Post(v) is the formula 3o' V(e') A (U(e") v). Intuitively, U (V) is an overapproximate representation of the set of states reached by applying Up state that satisfies V.
Let us call a transition t = (1, G, enabled at a symbolic state (1 if (G is satisfiable. A symbolic trajectory of F' is sequence To" (oo...., σn) with the following properties:
og is initial symbolic state.
Let o; = (4., Vi) and Ø++1 = (l+11, V4+)). Then there is a transition t = (4,, G.,, U2, 4411) such that: (i) t is enabled at og and (ii) V4+1 U (G, A Vi). In this case, write 0:+1 t(a,).
Intuitively, Ty represents an overapproximation of the set of concrete trajectories of F' that pass through the "control path" Vo.....4..)
The above symbolic trajectory is safe if for all i, V; + Safe(l).. Intuitively, in this case, all concrete trajectories that the symbolic trajectory represents follow the program's safety requirements.
Example(Cont.) Consider the example program in Figure Let us assume single initial symbolic state where æ E [-5,5], 5]. and suppose NN+(1)) E [-2, 2] when æ [-55, 5]. The program has two symbolic trajectories from the initial symbolic state:
+ = (l2,, [-5, 5)), (l3, E [-5, A E (-2, (47, E [-5,5] AyE A= 15,)
# = (122,0 E (1), (f,, E [-5,5 Ag E [-2, (G, [-5,5] E (1,2)
2 1)),
We note that only - is safe.
Probabilistic Symbolic Execution. A key difficulty with using symbolic execution to estimate the safety loss C(0) is that our programs need not be differentiable, or even continuous. To understand the issues here, consider our running example once again. Here, the parameter is used to calculate the variable y. which is used in discontinuous conditional statement that assigns very different values to the variable in its two branches. Additionally, a slight change in can sometimes cause the guard G of the conditional to go from being True on some values of y, being False all values of y. In the second case, the updated 9 would have one, rather than two, symbolic trajectories. If the symbolic trajectory # in which G is True serves an edge case judge whether a program is worst-case-safe, learning safe parameters would be difficult, as there would be no gradient guiding the optimizer back the case in which G is True
DSE overcomes these difficulties using a probabilistic approach to symbolic execution. Specifically, symbolic state o, (4,, V.), the symbolic executor DSE samples its next action following probability distribution po (.)), where / ranges over program transitions or a special action Stop.
For a boolean expression Ve over the program variables ( $1,,4...... ..ii....,,4, .r& and parameters 0, let Vol(V)) denote the volume of the assignments to X that satisfy Vg. We assume a procedure to compute Vol(V) for any Vo. (Note that such procedure easy to implement when every Vo an interval, as is the case in our implementation.) We define:
If there is unique program transition that is enabled a, then (t(os)) 1.
4

---

Published as a conference paper at ICLR 2022
If there is no transition t that is enabled at os then po(Stoplos) 1. ly be the transitions that are enabled at oi, with ( = (li, Gi, Ui, (1,44 Then po(t;]aa) Vol(G, Vol(V,
Otherwise, let .,.... .....
We also define a weighted probability distribution p(ao) over the (finite set of) initial sym- bolic states oj. Specifically, for each oj = (la, Vo), we have
Vol(V))
p(a)) E, Vol(V;)
(3)
DSE uses the distributions po(()o:) and p(ao) sample symbolic trajectories. (oo...., .n). with 04+1 =t(()). The probability of sampling 7# is
Let Tg
pa(T = p(oo) II po(t:lo-_)).
(4)
We note that po differentiable
Approximate Safety Loss. A key decision in DSE is to approximate the overall worst-case loss C(0) by the expectation of differentiable safety loss computed per sampled symbolic trajectory. Recall the safety loss Unsafe(s) for individual states. For as a differentiable approximation of the worst-case loss max, satisfies Unsafe(s). We lift this loss to symbolic trajectories # (ao.-..,. .n) observe that Unsafe, is differentiable in 0n) by defining Unsafe = E; Unsafeg(at). We
V), define (nsafes(a)
Our approximation to the safety loss is now given by:
## (0) E, #=)) Unsafeg(**)
(5)
Intuitively, C# (0) guides the learner towards either making the unsafe trajectories safer or lowering
the probability of the program falling into unsafe trajectories. If C (0) equals zero, the program
provably safe. That said, in practice, we must estimate the expectation in Equation (5) using sam-
pling. As this sampling process may miss trajectories, a low empirical estimate of C# C#(() need not
guarantee worst-case safety. As an extreme example, suppose a program has one unsafe symbolic trajectory, but the probability of this symbolic trajectory is near-zero. This trajectory is likely to be missed by the sampling process, leading an artificially low value of C## (0).
Example (Cont.) Consider the trajectories r and 72 # in our running example. We have p(7 #
p(t2)02), as the other transitions in of have probability We compute p(tz(o2) = 0.75. Thus, p(T 0.75 and similarly, p(T = 0.25.
Voll 2.1]]
Voll (2,2))
Gradient Estimation. Our ultimate goal is to compute the gradient V VoC # (0) of the approximate safety loss. At first sight, the classic REINFORCE estimator (Williams) 1992) one of its relatives (Schulman et al.) 2015) seems suitable for this task, given that they can differentiate an integral over sampled "paths". However, subtlety in our setting is that the losses for individual paths (symbolic trajectories) is a function of 0. This calls for a generalization of traditional REINFORCE- like estimators.
More precisely, we adapt the derivation of REINFORCE to our setting as follows:
Vo(C (0)) = VoE,#~pol #) Unsafeø(7#)
= Ve I Jnanpo poo (r#)
po Unsafe dr
[ (+
p # V Unsafeg(r*)) + Unsafe Vepa (apa(7# dd>#
E Vo Unsafeo(" }] E. Unssafe
(oogo Vo
The above derivation be further refined to incorporate the variance reduction techniques for REINFORCE that are commonly employed in generative modeling and reinforcement learning. The of such techniques is orthogonal to main contribution, and ignore it in this paper.
5

---

Published as a conference paper at ICLR 2022
5 EVALUATION
Our experimental evaluation seeks to answer the following research questions:
(RQ1): Is DSE effective in learning safe and performant parameters?
(RQ2): How does data size influence DSE and baselines?
(RQ3): How well does DSE scale as the program being learned gets more complex?
5.1 EXPERIMENTAL. SETUP
System Setup. Our framework is built top of PyTorch (Paszke al. 2019). We the Adam Optimizer (Kingma & Ba 2014) for all the experiments with default parameters and a weight decay of 0.000001. We ran all the experiments using single-thres thread implementation with Intel Xeon Gold 5218 2.30GHz CPUs and GeForce RTX 2080 GPUs. (Please refer to Appendix A.7 for more training details.)
Linux system
We use two types of baselines: (i) Ablation, which ignores the safety constraint and learns only from data; (ii) DIFFAI+, an ex- tended version of the original DIFFAI method (Mirman et al. 2018). AIFFAI does not directly fit our setting neurosymbolic programs as does not handle general conditional statements. DIFFAI+ extends DIFFAI AI by adding the meet and join operations following the abstract inter- pretation framework (Cousot & Cousot 1977). Also, allow DIFFÅI+ to split the input set into several (100 if not specified) initial sym- bolic states to increase the precision of sym- bolic execution of each trajectory. (The original DIFFAI does not need to perform such splits because, being focused on adversarial robust- ness, it only propagates small regions around each input point through the model.) However, the parts of DIFFAI that propagate losses and their gradients through neural networks remain the same in DIFFAI+.
Baselines.
Provably Safe Portion
Template
Model
DIFFAI+
DSE
NNSmall
0.0
1.0
Pattern
NNMed
0.0
1.0
NNBig
0.0
1.0
NNSmall
0.0
0.70
Pattern2
NNMed
0.0
0.78
NNBig
0.0
0.73
NNSmall
1.0
Pattern3
NNMed
1.0
1.0
NNBig
1.0
1.0
NNSmall
0.0
0.76
Pattern4
NNMed
0.0
0.80
NNBig
0.58
0.97
NNSmall
0.0
1.0
Pattern5
NNMed
0.0
1.0
NNBig
0.0
1.0
We use the box (interval) domain for both DSE and DIFF A in the experiments. DSE sam- ples 50 symbolic trajectories for each starting component.
Figure 2: Results of synthetic microbenchmarks of DSE and DIFFAI+.
Benchmarks. Our evaluation uses 5 synthetic microbenchmarks and 4 case studies. The mi- crobenchmarks (Appendix AA.5) are small programs consisting basic neural network modules, arithmetic function assignment, and conditional branches. These programs designed to highlight the relationship between DIFFAI+ and DSE, The case studies, described below, model real-world control and navigation tasks (see Appendix A.4 for more details):
Thermostat, we want to leamn safe parameters for two neural networks that control the tem- perature of room.
Racetrack is a navigation benchmark (Barto al. 1995 Christakis et al. (021). Two vehicles are trained by path planners separately. The racetrack system is expected to learn two safe controllers so that vehicles do not crash into walls or into each other.
In Airerafi-olllision (AC), the goal to learn safe parameters for an airplane that performs maneuvers to avoid collision with second plane.
Cartpole aims to train a cart imitating the demonstrations and keep the cart within the safe position range.

---

Published as a conference paper at ICLR 2022
(a) Thermostat (Safety)
(b) AC (Safety)
(c) Racetrack (Safety)
(d) Cartpole (Safety)
(c) Thermostat
(1) AC
(g) Racetrack
(h) Cartpole (Test Data Loss)
(Test Data Loss)
(Test Data Loss)
(Test Data Loss)
Figure 3: The provably safe portion and the test data loss of Ablation, DIFFAI+ and DSE when
varying the size of the data to train.
For each benchmark, we first write a ground tround-trutt program that does not include neural networks and provably satisfies a safety requirement. We identify certain modules of these programs as candidates for learning. Then we replace the modules with neural networks with trainable paramcters.
For all benchmarks with the exception of Racetrack, we execute the ground-truth programs uni- formly sampled inputs to collect input-output datasets for each module that is replaced by a neural network. As for Racetrack, this benchmark involves two simulated vehicles with neural controllers; learned parameters for these controllers are safe if the vehicles do not crash into each other or a wall. To model real-world navigation, we generate the training data for the controllers from ground-truth trajectory constructed using path planner. This path planner only tries to avoid the walls in the map and does not have representation of distances from other vehicles. Thus, in this problem, even a very large data set does not contain all the information needed for learning safe parameters.
Evaluation of Safety and Data Loss. Once training is over, we evaluate the learned program's test data loss by running it on 10000 initial states that were not seen during training. We evaluate the safety loss using an abstract interpreter (Cousot & Cousot 1977) that splits the initial condition into a certain number of boxes (20* for Cartpole, 10000 for the other benchmarks). then constructs symbolic trajectories from these boxes. This analysis is sound (unlike the approximate loss em- ployed during DSE training), meaning that the program is provably worst-case safe if the safety loss evaluates to Our safety metric is the provably safe portion, which is the fraction the program's 's symbolic trajectories that are worst-case safe.
5.2 RESULTS
Overall Quality of Learned Parameters. Figure 2 exhibits the provably safe portion of DIFFAI+ and DSE on our microbenchmarks. Here, the first two patterns only use neural modules to evaluate the guards of a conditional branch, and the last three benchmarks use the neural modules in the guards well as updates (assignments) that directly affect the program's safety. We see that DIFFAI+ cannot learn safe highly non-differentiable modules (patternl, pattern2) while DSE can. For the cases where optimization across branches is not required give safe programs, DIFFAI+ can handle them (pattern3). For the patterns with neural assignments, DIFFAI+ finds it hard to learn to jump from one conditional branch to another to increase safety (pattern4, pattern5). We refer the readers to Appendix A.9 for more detailed pattern analysis.
RQI:
We show the training-time and test-time safety and data losses for our more complex benchmarks in Figure 3 From Figure 3a portion even with 200 data points and the results keep when the number of training data points is increased. Mcanwhile, both DIFFAI+ and Ablation fail to provide safe programs for AC. Racetrack and Cartpole. For Thermostat, Ablation and DIFFAI+ can achieve a provably safe portion of 0.8 only when using 5000 and 10000 data points to train.
3b
3c
3d
we exhibit that DSE can learn programs with 0.8 provably safe
7

---

Published as a conference paper at ICLR 2022
(a) Ablation(Final)
(b) DIFFAI+ (Final)
(c) DSE (Middle)
(d) DSE (Final)
(e) Ablation(Final)
DIFFAI+ (Final)
(g) DSE (Middle)
(h) DSE (Final)
i Ablation(Final) MAMANNAVETI
DIFFAI+ (Final)[pos]
(k) DSE (Middle)(pos)
DSE (Final)(pos)
(m) Ablation(Final) [dist] (n) DIFFAI+ (Final) [dist]
(0) DSE (Middle) [dist]
(p) DSE (Final) [dist]
(q) Ablation(Final)
(1) DIFFAI+ (Final)
(s) DSE (Middle)
DSE (Final)
Figure 4: Trajectories during training. Each row exhibits the concrete trajectories and symbolic trajectories of one case from different methods, From top bottom, the cases are Thermostat (Fig- 4f
ure.
4a
4b
4c
4d
AC (Figure. 4e
4g
4h
Racetrack with position property (Figure. 4i 4k
4p) and distance property (Figure. 4m 4n
4t). Each figure shows the trajectories (concrete: red, symbolic: green rhombus) of programs learnt by the method from different training stages, which is denoted by "Middle" and "Final". We separate the input state set into 100 components (81 components for Cartpole) evenly to plot the symbolic trajectories clearly. During evaluation, we separate the input set into 10000 components (20 components for Cartpole) evenly to get more accurate symbolic trajectories measurement.
4o
(4p). and Cartpole (Figure. [4q 4r 4s
Our test data loss is sometimes larger yet comparable with the Ablation and DIFFAI+ from Fig- ure 3e
Figure 3h exhibits the tension between achieving a good loss and safety, where the test data loss DSE increases as the provably safe portion becomes larger. For AC specifically, the safety constraint can help the learner overcome some local optimal yet unsafe areas to get safer result with more accurate behaviors.
3g
Overall, we find that DSE outperforms DIFFAI+ when neural modules are used in the conditional statement and the interaction between neural modules is important for the safety property. This is the case in our larger benchmarks. For example, in Thermostat and AC, the neural modules' outputs decide the actions that the neural module to take in the next steps. Racetrack, the distance between two neural modules regulates each step of the vehicles' controllers. In Cartpole, the neural modules gives the force on carts as the output.
We display representative symbolic trajectories from the programs Iearned by Ablation, DIFFAI+ and DSE in Figure 4 The larger portion of the symbolic trajectories is provably safe from DSE than the ones from baselines, which is indicated by the less overlapping between the green trajectories and the gray area. Because the symbolic trajectories are overapproximate, we also depict 100 ran- domly sampled representative conerete trajectories for each approach. We note that more concrete trajectories of Thermostat, AC, the distance property of Racetrack and Cartpole from DSE fall into the safe area compared with DIFFAI+ and Ablation.
RQ2: Impact of Data Size. Figure 3 compares the different methods' performance on the test metrics as the number of training data points changed. The Ablation and DIFFAI+ can reach 0.95 provably safe portion with 10000 data points for Thermostat. However, the variance of results is large, as the minimum provably safe portion across training can reach 0.74 and 0.0 for Ablation and DIFFAI+. In the Thermostat benchmark, DIFFAI+'s performance mainly comes from the guidance from the data loss rather than the safety loss.
For the other three cases, a larger training data set cannot help the Ablation and DIFFAI+ to give much safer programs. For AC, as in Figure the program learnt from Ablation is very close to the safe area but the Ablation is still not accurate enough give safe program in the third step. In Racetrack, increasing the data size to train the vehicles' controllers can only satisfy the requirement of "not crashing into walls". The networks cannot learn to satisfy the property of not crashing into
8

---

Published as a conference paper at ICLR 2022
other vehicles as this information is not available in the training data. In Cartpole, the baselines mainly follow the guidance of the data loss and can not give safer programs.
Scalability. As our solution for the safety loss does not rely the number of data points, the solution is scalable in terms of both data size and neural network size. In Figure 2 we use the three types of neural networks: (i) NNSmall (with about 33000 parameters); (ii) NNMed (with over 0.5 million parameters); (iii) NNBig (with over million parameters), the training time per epoch is 0.09 sec, 0. 0.10sec. 0.1 Isec for NNSmall, NNMed, NNBig separately. For the synthetic benchmarks, the program can converge within about 200 epochs which takes 18 sec, 20sec, and 22 sec.
RQ3:
Our Thermostat, AC and Racetrack benchmarks consist of neural networks with 4933, 8836 and 4547 parameters respectively, and loops with 20, 15 and 20 iterations respectively. There are 2. 1 and 2 neural modules (respectively) in each benchmark. The training times for DIFFAI+ and DSE are comparable on these benchmarks. Specifically, for Thermostat, AC, and Racetrack, the total training time of DSE is less than hour, less than 90 minutes, and around 13 hours. The corresponding numbers are over 90 minutes, more than 2 hours, and more than 17 hours for DIFFAI+ A more detailed scalability analysis is available in Appendix|A.I) A1
RELATED WORK
Verification of Neural and Neurosymbolic Models. There are many recent papers on the verifi- cation of worst-case properties of neural networks (Anderson et al. 2019 Gehr et al. 2018 Katz Elboher et al.] 2020, Wang et al. 2018). There are also several recent papers (Ivanov al. 2019 Tran et al.] 2020 Sun al. 2019 Christakis et al. 2021) on the verification of com- positions of neural networks and symbolic systems (for example, plant models). To our knowledge, the present effort is the first to integrate method of this sort propagation of worst-case intervals through neurosymbolic program - with the gradient-based training of neurosymbolic programs.
cct al.
2017:
Verified Deep Learning. There is growing literature on methods that incorporate worst-case ob- jectives (such as safety and robustness) into neural network training (Zhang et al., 2019 Mirman al. 2018 Madry et al. 2017 Cohen al. 2019; Singh et al. 2018). Most work on this topic fo- cuses on the training of single neural networks. There are a few domain-specift efforts that consider the environment of the neural networks being trained. For example, (Shi et al.) 2019) uses spectral normalization to constrain the neural network module of neurosymbolic controller and ensure that it respects certain stability properties. Unlike DSE, these methods treat neural network modules in an isolated way and do not consider the interactions between these modules and surrounding code
Stone et al. 2016 Qin & Badgwell 2000, Nassi et al. 2020 Katz et al. 202T).
Verified Parameter Synthesis for Symbolic Code. There is a large body of work on parameter synthesis for traditional symbolic code (Alur et al., 2013) Chaudhuri et al. (2014) with respect to worst-case correctness constraints. Especially relevant in this literature is Chaudhuri et al. (2014), which introduced a method to smoothly approximate abstract interpreters of programs that is closely related to DSE and DIFFAL. However, these methods do not use contemporary mudient-based learn- ing, and as a result, scaling them to programs with neural modules is impractical.
7 CONCLUSION
We presented DSE, the first approach worst-case-safe parameter learning for programs that embed neural networks inside potentially discontinuous symbolic code. The method is based on a new mechanism for differentiating through symbolic executor. We demonstrate that DSE outperforms DIFFAI, a state-of-the-att approach to worst-case-safe deep learning, in a range of tasks.
Our current implementation of DSE uses an interval representation of symbolic states. Future work should explore more precise representations such as zonotopes. Incorporating modern variance reduction techniques in our gradient estimator is another natural next step. Finally, one challenge in DSE is that learning here can get harder the symbolic state representation gets more precise. In particular, if we increase the number of initial symbolic states beyond a point, each state would only lead to unique symbolic trajectory, and there would be gradient signal to adjust the relative weights of the different symbolic trajectories. Future work should seek to identify good, possibly adaptive, tradeoffs between the precision of symbolic states and the ease of learning.

---

Published as a conference paper at ICLR 2022
Acknowledgments: We thank anonymous reviewers for their insightful comments and Radoslav Ivanov (Rensselaer Polytechnic Institute) for his help with benchmark design. Work on this paper was supported by the United States Air Force and DARPA under Contract No. FA8750-20-C-0002. by ONR under Award No. N00014-20-1--22 22-2200---111551 15, and by NSF under grant # #1901376.
REFERENCES
Alekh Agarwal, Alina Beygelzimer, Miroslav Dudík, John Langford, and Hanna Wallach. A ductions approach to fair classification. In International Conference on Machine Learning, pp- 60-69, PMLR, 2018.
Aws Albarghouthi. Introduction to neural network verification. arXiv preprint arXiv:2109.10317, 2021.
Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa Syntax- guided synthesis. IEEE, 2013.
Greg Anderson, Shankara Pailoor, Isil Dillig, and Swarat Chaudhuri. Optimization and abstrac- tion: synergistic approach for analyzing neural network robustness. Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 731- 744, 2019.
Roberto Baldoni, Emilio Coppa, Danicle Cono D'elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), 51(3)11-39, 2018.
Andrew G Barto, Steven J Bradtke, and Satinder P Singh. Learning to using real-time dynamic programming. Artificial intelligence, 72(1-2):81-188, 1995.
Osbert Bastani, Yewen Pu, and Armando Lolar-Lezama. Verifiable reinforcement learning via policy extraction. arXiv preprint arXiv:1805.000
2018.
Swarat Chaudhuri, Martin Clochard, and Armando Solar-Lezama. Bridging boolean and quantita- tive synthesis using smoothed proof search. In Proceedings of the 41 ACM JGGPLAN-SIGAG Symposium on Principles of Programming Languages, pp. 207-220, 2014.
Swarat Chaudhuri, Kevin Ellis, Oleksandr Polozov, Rishabh Singh, Armando Yue, et al. Neurosymbolic Programmingg Now Publishers, 2021.
Yisong
Maria Christakis, Hasan Ferit Eniser, Holger Hermanns, Jörg Hoffmaann, Yugesh Kothari, Jianlin Li,
Jorge A Navas, and Valentin Wüstholz. Automated safety verification of programs invoking neural networks. In International Conference on Computer Aided Verification, pp. 201-224. Springer, 2021.
Jeremy Cohen, Elan Rosenfeld, and Zico Kolter. Certified adversarial robustness via randomized smoothing. International Conference on Machine Learning, pp. 1310-1320. PMLR, 2019.
Patrick Cousot and Radhia Cousot. Abstract interpretation: unified lattice model for static anal- ysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium Principles of programming languages, pp. 238 288-552,1 1977.
Yizhak Yisrael Elboher, Justin Gottschlich, and Guy Katz. An iittraction-based framework for neural network verification. In International Conference on Computer Aided Verification, pp. 43 65. Springer, 2020.
Yoav Freund and Robert E Schapire. Game theory, on-line prediction and boosting. Proceedings of the ninth annual conference Computational learning theory, pp. 325-3332 1996.
Yoav Freund and Robert E Schapire. Adaptive game playing using multiplicative weights. Games and Economic Behavior, 29(1-2):79-103, 1999.
10

---

Published as a conference paper at ICLR 2022
Timon Gehr, Matthew Mirman, Dana Drachsler- Petar Tsankov, Swarat Chaudhuri, and Mar- tin Vechev. Ai2: Safety and robustness certification neural networks with abstract interpreta- tion. In 2018 IEEE Symposhum Security and Privacy (SP), pp. 3-18. IEEE, 2018.
Divya Gopinath, Kaiyuan Wang, Mengshi Zhang, Corina S Pasareanu, and Sarfraz Khurshid. Sym- bolic execution for deep neural networks. arXiv preprint
1007.1077...499 2018.
Radoslav Ivanov, James Weimer, Rajeev Alur, George J Pappas, and Insup Lee. Verisig: veri- fying safety properties of hybrid systems with neural network controllers. In Proceedings of the ACM International Conference on Hybrid Systems: Computation and Control, pp. 169-178, 2019.
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97-117. Springer, 2017.
Michael Katz, Kavitha Srinivas, Shirin Sohrabi, Mark Feblowitz, Octavian Udrea, and Oktie Has- sanzadeh. Scenario planning in the wild: neuro-symbolic approach. FinPlan 2021, pp. 15, 2021.
Diederik Kingma and Jimmy Ba. Adam: method for stochastic optimization, arXiv preprint 1412.698016 2014.
Hoang Le, Cameron Voloshin, and Yisong Yue. Batch policy learning under constraints. In Inter- national Conference on Machine Learning, pp. 3703-3712. PMLR, 2019.
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:/706. 06083, 2017.
Zohar Manna and Amir Pnueli. Temporal verification of reactive systems: safety. Springer Science & Business Media, 2012.
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for prov- ably robust neural networks. In International Conference on Machine Learning, pp. 3578-3586. PMLR, 2018
Ben Nassi, Yisroel Mirsky, Dudi Nassi, Raz Ben Ben-Netanel, Oleg Drokin, and Yuval Elovici. Phantom of the adas: Securing advanced driver-assistance systems from split-second phantom attacks. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, pp. 293-308, 2020.
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang. Zachary Vetito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d' d'Alché-Buc. E. Fox, and R. Garnett (eds.), Advances in Neural Information Processing Systems 32, pp. 8024-8035. Curran Associates, Inc., 2019.
Joe Qin and Thomas A Badgwell. An overview of nonlinear model predictive control applications. Nonlinear model predictive control, pp. 369-392 2000.
John Schulman. Nicolas Heess, Theophane Weber, and Pieter Abbeel. Gradient estimation using stochastic computation graphs. Advances in Neural Information Processing Systems, 28, 2015.
Guanya Shi, Xichen Shi. Michael O'Connell, Rose Yu, Kamyar Azizzadenesheli, Animashree Anandkumar, Yisong Yue, and Soon-Jo Chung. Neural lander: Stable drone landing control using learned dynamics. In 20/9 International Conference on Robotics and Automation (ICRA), pp. 17784-9794 IEBE, 2019.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. NewrPPS, 1(4):6, 2018.
11

---

Published as a conference paper at ICLR 2022
Peter Stone, Rodney Brooks, Erik Brynjolfsson, Ryan Calo, Oren Etzioni, Greg Hager, Julia Hirschberg, Shivaram Kalyanakrishnan, Ece Kamar, Sarit Kraus, et al. Artificial intelligence and life in 2030: the one hundred year study on artificial intelligence. 2016.
Xiaowu Sun, Haitham Khedr, and Yasser Shoukry. Formal verification of neural network controlled autonomous systems. In Proceedings of the 22nd ACM International Conference on Hybrid Sys- tems: Computation and Control, pp. 147-156, 2019.
Daaang-Dnngga Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T Johnson. Nnv: The neural network verification tool for deep neural networks and learning-enann
cyber-physical systems. International Conference Computer Aided Verification, pp. 3-17. Springer, 2020.
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang. and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In 27th {USENIX] Security Symposium ( ((USENIX) Security 18), pp. 1599-1614, 2018.
Ronald J Williams. Simple statistical
algorithms for connectionist reinforcement
learning. Machine learning, 8(3):229-22 25666.,, 1992.
Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane Boning, and Cho-Jui Hsich. Towards stable and efficient training of verifiably robust neural networks. arXiv preprint arXiv: /906.06366, 2019.
12

---

Published as a conference paper at ICLR 2022
Algorithm 1: Learning Safe, Optimal Parameter Mixtures (Agarwal et al. 2018 Le et al. 2019)
for 1 N do
8, f (A.)
Uniform(@1...... 01), de 1 Σ d
Luuax -- L(0,, Best (0))
Lmin L(Best (^t),
if Limxx Lmin < y then return (0,, Ac);
A--1 - A-Update((1......
A APPENDIX
A.1 LEARNING FRAMEWORK
We use an equivalence between constrained and regularized learning that (Agarwal al., 2018
Le et al. 2019). among others, have recently developed in other learning settings, we reduce our problem to a series of unconstrained optimization tasks.
We convexify the program set {Fo E IR*) by considering stochastic mixtures (Le al. 2019) and represent the convexified set as probabilistic function Fg. Following DSE, we rewrite Equation in terms of these mixtures:
arg min Q(0)
s.t. C*(0) S
(6)
We convert Equation to a Lagrangian function
L(O, A) Q(0) *C
(7)
where E R+ is a Lagrange multiplier. Following the equilibrium computation technique by Freund & Schapire (1996), Equation 6 can be rewritten
max min L(O, A). XER 6
Solutions to this problem can be interpreted as equilibria of a game between a X-player and a d- player in which the d-player minimizes L(O, A) given the current X, and the A-player maximizes ((,,)) A) given the current ô. Our overall algorithm is shown in Algorithm In this pseudocode, is a predefined positive real. Uniform(@1...... is the mixture that selects a 0g out of (f..... 0.} uniformly at random.
Besta (A) refers to the player's best response for given value of À (it can be shown that this best response a single parameter value, rather than a mixture of parameters). Computing this best response amounts solving the unconstrained optimization problem ming T.(O, A), i.e.,
Best (A) min Q AC# (0).
(10)
Best, (0) is the X-player's best response to particular parameter mixture Å. We define this function as
Best x (0) = 0 if C# (0) 50 otherwise
(11)
where S is the upper bound on X. Intuitively, when C## (#) is non-positive the current parameter mixture is safe. As is linear function of X, the minimum value of L achieved in this case when À is zero. For other cases, the minimum L is reached by setting À to the maximum value S.
Finally, A-Update(0.) computes, in constant time, a new value of À based on the most recent best response by player. We do not describe this function in detail; please see (Agarwal et al. 2018 for more details.
Following prior work, we can show that Algorithm converges to a value (0, Å) that is within additive distance from saddle point for Equation 9 To solve our original problem (Equation 2.
13

---

Published as a conference paper at ICLR 2022
take the returned @ and then return the real-valued parameter 02 to which this mixture assigns the
highest probability. It is easy to see that this value is an approximate solution to Equation 2
14

---

Published as a conference paper at ICLR 2022
A.2 ABSTRACT UPDATE FOR NEURAL NETWORK MODULES
We consider the box domain in the implementation. For a program with m variables, each com- ponent the domain represents m--iimensional box. Each component of the domain pair b = (bey be), where be E R is the center of the box and be E 12 represents the non-negative deviations. The interval concretization of the i-th dimension variable of b given by
[(b,); (b (6o); + (6+),)-
Now we give the abstract update for the box domain following Mirman et al. (0118)
Add. For conerete function that replaces the i-th element in the input vector R" by the sum of the j-th and k-th element:
f(x) (21 :.1:...;2-111
2he 2441, Imm)
The abstraction function of f' is given by:
(b) (M b.r M Mbb):
where M E mmxm replace the i-th element of by the of the j-th and k-th element by M be.
Multiplication. For a concrete function f that multiplies the i-th element in the input vector I.m by a constant wt
(xx) = (#1,-.., -,- w Tigy I4+1:- Fm )T
The abstraction function of is given by:
f* (b) (Mw be: Mw/ be),
where M be multiplies the i-th element of be by w and M be multiplies the i-th element b with /tcl.
Matrix Multiplication. For concrete function f that multiplies the input I by fixed matrix M E Rm xm.
f(x) = M x.
The abstraction function of f is given by:
f (b) (M be, |M| -b),
where M is an element-win wise absolute value operation. Convolutions follow the same approach, as they also linear operations.
ReLU. For concrete element-wise ReLU operation over x E I:
ReLU(()) = (max( O).... max (Im. 0))
the abstraction function of ReLU is given by: ReI.U* (b) = ReLUUb, b.) ReLU -b)) be) ReLU + be) ReLU - -be),
2 where b, + be and b, be denotes the element-wise sum and element-wise subtraction between b, and b..
2
Sigmoid. As Sigmoid and ReLU are both monotonic functions, the abstraction functions follow the same approach. For concrete element-wise Sigmoid operation over Rm.
Sigmoid x)) = exp(-x))
1 expepp(-- xmm)
the abstraction function of Sigmoid is given by: Sigmoid# (b) = Sigmoid(b, + ba) Sigmoid(b. be) Sigmoid(b. ba) Sigmoid be),
where b. + b. and b. b. denotes the element-wise and element-wiss subtraction between b. and be. All the above abstract updates can be easily differentiable and parallelized on the GPU,
15

---

Published as a conference paper at ICLR 2022
A.3 INSTANTIATION OF THE Unsafe FUNCTION
In general, the (n) function over individual states can be any differentiable distance function between point and which satisfies the property that Unsafe(s) 0 if in the safe set, A. and Unsafe(s) > 0 & is not in A. We give the following instantiation as the unsafeness score over individual states:
Unsafe(s) {{
min DIST(s, x)
if $ A if
0
where DIST denotes the euclidean distance between two points.
Similarly, the Unsafe(a) function over symbolic states can be any differentiable distance function between two sets which satisfies the property that Unsafe(or) 0 if V is in A, and Unsafe(a) > is not in A. We give the following instantiation as differentiable approximation of the worst- case loss max, saissies V Unsafe(s) in our implementation:
mill, satisfies (nsafe(s) +
V 0
Unsafe(o)= =
Vol(VAA)
V A 0
Vol(V)
16

---

Published as a conference paper at ICLR 2022
A.4 BENCHMARKS FOR CASE STUDIES
The detailed programs describing Aircraft Collision, Thermostat and Racetrack are in Figure 5 and 7 The Ty of Aireraft Collision and Tq m5o01, T0 aheat in Thermostat with 64 nodes in each layer and a ReLU after each layer except the last one. A sigmoid layer serves as the last layer. Both the x6 regenti and mg in Racetrack are a layer feed forward net with 64 nodes in each and ReLU after each layer. The Cartpole benchmark is linear approximation following Bastani et al. (0188) with a layer feed forward net with 64 nodes in each layer as the controller.
3 layer feed forward
aircraftcol
(x)
2
x1, yl : x, -15.0
3
x2, y2 := 0.0, 0.0
4
N 1= 15
==0
while < N:
7
p0, pl, p?, p3, step :- To (x1, yl, x2, y2, step, stage)
8
stage :- argmax (p0, pl, p2, p3)
9
if stage CRJISE:
x1, yl := MOVE CRUISE (x1, yl)
else if stage == LEFT:
12
x1, y1 : MOVE_LEFTE (x1, yl)
13
else if stage
STRAIGHT:
x1, y1 ;= MOVE_ NOVE_STRAIGHT (x1, yl)
else if stage RIGHT: xl, yl : NOVE_RIGHT (x1, yl)
16
17
18
x2, y2 MOVE (x2, y2)
== i
20
assert [IT__CRASHCCC yl, x2, y21)
21
return
Figure 5: Aircraft Collision
thermostat (x)
2
N = 20
3
isOn = 0.0
4
=
while N:
6
if is0n $ 0.5:
7
is0n := Tg0el (x)
8
x := COOLING (x)
9
else:
isOn, heat == heat (x)
x := WARMING (x, heat))
12
== i
13
assert (!EXTREME TEMPERATURE (x)
return
Figure 6: Thermostat
17

---

Published as a conference paper at ICLR 2022
1 racetrack (x):
2
x1, yl, x2, y2 := x, 0.0, x, 0.0
3
N 20
while N:
5
p10, pll, p12 " arent: (xl, yl)
6
p20, p21, p22 : x m (x2, y2)
7
actionl argmax (p10, pll, p12)
action2 :- argmax (p20, p21, p22)
9
x1, yl : MOVE (x1, yl, actionl)
10
x2, y2 ;= MOVE (x2, y2, action2)
i
assert (CRASH_WALD (xl, yl) !CRASH_WALL (x2, y2)
6& !CRASH(X) yl, x2, y2))
14
15
return
Figure 7: Racetrack
18

---

Published as a conference paper at ICLR 2022
A.5 SYNTHETIC MICROBENCHMARKS
Figure&Bexhibit the 5 synthetic microbenchmarks in our evaluation. Specifically, the neural network modules used conditions in pattern and pattern 2. The neural network modules serve both conditions and the assignment variable in pattern 3, pattern 4 and pattern 5. To highlight the impact from the safety loss, we only train with safety loss for synthetic microbenchmarks.
1 patternl (x)
pattern2 (x)
pattern3 (x)
E [-5, 5]
x [-5, 5]
x [-5,
y :- To (X)
y :- Ta (x)
y :- mg (x)
4 if y < 1.0:
if y S 1.0:
if S 1.0:
5
10
5
+ 10
5
10 y
6 else:
else:
else:
2:
21 x
2:
8 assert (z 1 1)
assert (z & 0)
assert (z S 1)
9
return 2
9
return 2
return
(a) Patternl
(b) Pattem22
(c) Pattern3
pattern4 (x)
pattern5 (x)
2
# x E 1-5, 51
# x E 1-1, 11
3
Na (x)
if 1= ne (x)
4
if y S -1.0:
1.0:
5
2
2 :
else:
else:
7
2: 2 +
2: = -10
8
assert (z v 1)
assert (z 0 aa z 2 -5)
9
return
return
(d) Pattern4
(c) Pattern5
Figure 8: Programs for Patterns
19

---

Published as a conference paper at ICLR 2022
A.6 DATA GENERATION
In this section, we provide more details about our data generation process. We give our ground-truth programs and the description of each benchmark:
Thermostat: Figure 6 exhibits the program with initial temperature E [60.0, 64.0] in training, where a 20-1ength loop is involved. The COOLING and WARMING are two differentiable functions updating the temperature, 2. The T rggol and T Thest are two lin- car feed-forward neural networks. We set the safe temperature to the area [55.0, 83.0]. TETREMEETEEEERRTTEEE
EXTREME_ TEMPERATURE measures that whether is not within the safe temperature
scope. The ground-truth program replaces ggooi and Theat with two different functional mechanisms (including branches and assignment), which decides the value of isOn and heat. To mimic the real-world signal sensing process of thermostat, we carefully add noise to the output of these functional mechanisms and restricts the noise does not influ- ence the safety of the ground-truth program.
AC: Figure 5 illustrates the program in training with initial input x-axis of aircraft x E [12.0, 16.0). where 15-Iength loop is involved. The MOVEL functions update the position of aircraft in a differentiable way. The Te is one linear feed- ferd-forward neural networks. IS ___CASSH measures the distances between two aircraft and the safe distance area is set to be larger than 40.0. In the ground-truth program, the To is replaced by one functional mechanism mimicing the real-world aireraft planner. If the stage is CRUISE, the ground- truth planner detects the distance between aircraft and decides the next step's stage by assignment values 1 or 0 to p0, pl, p2, p3. The step is set to O. When the stage is in LEFT or RIGHT, stage keeps and the step increases if the number of steps in this stage is within a threshold, and the stage changes to STRAIGHT or CRUISE SE and the step is set to 0 otherwise. Specifically, we convert the argmax to nested If- Then-Elss([TEE block to select the index of the p with the maximum value.
Figure 7 illustrates the program in training with the input x-axis of each agent x E [5.0, 6.0] (The two agents start from the same location.) This program has 20-length loop with a dynamic length of 223 lines (The unfold ITE of argmax consists of lines code.) In training, the Tg 2gentt and mq zagent2 are two linear feed-forward neural network. The MOVE is differentiable functions that update agents' positions. CRASH W ALL measures whether the agents' position collides with the wall. CRASH measures whether the two agents crash into each other. In ground-truth program, aggenti and g agent2 are replaced by functional path planners guiding the agent's 'ss direction. The path planner only tries to avoid wall-collision in the map. That is to say, in the trajectories data generated, arbitrary pair of trajectories of agent and agent2 2 is not guaranteed to be no- collision with each other. To model real-world navigation, we also add noise in the next step selection for one position to generate independent trajectories of each agent. In the ground-truth program, the noise is added by uniformly selecting from the safe next step area.
Racetrack:
Cartpole: In the Cartpole experiment, use the trajectories data generated from the expert model from Imitation Package. Starting from S, = 0.005, 0.05) we train a cart of which the position is within range [-0.1, 0.1). The state space is 4 and the action space is 2. We use a layer fully connected neural network (each layer followed by ReLU and the last layer followed by Sigmoid) to train. We follow the two points in Bastani et al. (2018) below to setup the experiment:
We approximate the system using a finite time horizon Tmaz = 10;
- we use a linear approximation f(s, a) ~ As + Ba.
When generating the trajectory dataset, we uniformly sample the input from the input space and run the ground-truth program to get the trajectory. Specifically, the trajectories in the dataset is represented by a sequence of neural network input-output pairs and the in- dex of the neural networks. Take Thermostat as an example, we get a sequence of [isCna) "cool"), ")..., ([xx], [isOng, heat,), "heat").... for one starting point. The k represents the data collected in the k-th step of the program.
20

---

Published as a conference paper at ICLR 2022
A.7 TRAINING PROCEDURE
Our framework is built on top of PyTorch (Paszke et al. 2019). We use the Adam Optimizer (Kingma & Ba 2014) for all the experiments with learning of 0.001 and weight decay of 0.000001. We ran all the experiments using a single-thread implementation on Linux system with Intel Xeon Gold 5218 2.30GHz CPUs and GeForce RTX 2080 Ti GPUs.
We represent the data loss (Q) following imitation learning techniques. The trajectory dataset is converted to several input-output example pair sets. Each input-output pair represents the input- output pairs for each neural network. Q is calculated by the average of the Mean Squared Error of the each neural network over the corresponding input-output pair set.
The C## of DSE follows the algorithm given in the Section 4 with one symbolic state covering the input space. In DIFF we use sound join operation, which is used in classic abstract interpretation Cousot & Cousot (1977), whenever encountering branches. Sound join means that the symbolic state after the branch block is the join of the symbolic states computed from each branch. The concretization of the symbolic state after sound join covers the union of the concretization of the symbolic states from each branch. Intuitively, starting from one input symbolic state, DIFFAI+ gets one symbolic trajectory which covers all the potential trajectories starting from the concrete input satisfying the input symbolic state. For the safety loss of DIFFAI+, we first split the input space into 100 subregions evenly to give more accuracy for DIFFAI+. After that, trajectories. We compute the average of the safety loss of all the 100 symbolic trajectories as the training safety loss C# of DuFFAI+.
get 100 symbolic
We set the convergence criterion as a combination of epoch number and loss. In each training iteration, the final loss is represented Q(0)+ C# (0). We set the maximum epoch for Thermostat, AC and Racetrack as 1500, 1200 and 6000. We set the early stop if the final loss has less than I % decrease over 200 epochs.
21

---

Published as a conference paper at ICLR 2022
A.8 TRAINING PERFORMANCE
Figure SasureDand and Figure 10 illustrates the training performance of safety loss and data loss when we vary data points (2%. 10%. 20%, 50%, 100% of the training dataset) used by DIFFAI and DSE. We can see that the safety loss of DSE can converge while the variance of the safety loss of DIFFAT is quite large for these three cases and can not converge to a small safety loss.
While we found that starting from random initialization can give us safe programs in Thermostat, achieved much quicker convergence when initializing Thermostat programs trained purely with data and then continue to train with safety loss. We show the results and training performance for Thermostat with data-loss initialized program. The other two benchmarks do not benefit lot from the data loss initialized program. We keep the training of them with random initialization.
A.8.1 SAFETY Loss
(a) (20)
(b) Thermostat(1k) kk)
(c) Thermostat(2k)
(d) (hermostat(5k)
(c) Thermostat (10k)
(f) AC(150)
g AC(750)
AC(1.5k)
AC(3.75k)
i AC(7.5k)
(k) Racetrack(200)
(1) Racetrack(Ik)
(m) Racetrack(2k)
(n) Racetrack(5k)
(0) Racetrack(1Ok)
(p) Cartpole(200)
(q) Cartpole(1k)
(r) Cartpole(2k)
(s) Cartpolc(5k)
(1) Cartpole(1Ok)
Figure 9: Training performance of data loss on different benchmarks varying data points. The y-axis represents the safety loss (C# (0)) and the x-axis gives the number of training epochs. Overall, DSE converges within 1500, 1000. 6000, and 2000 epochs for Thermostat, AC, Racetrack, Cartpole, while DIFFAI+ casily gets stuck or fluctuates these benchmarks.
22

---

Published as a conference paper at ICLR 2022
A.8.2
DATA Loss
(a) T2ermostat(200)
(b) (1kr
(c) Thermostat(2k)
(d) (Ser
Thermostat
(1 AC(150)
gg) AC(750)
(h) AC(1.K))
ii) AC(3.75k)
AC(7.5k)
(k) Racctrack(200)
(I) Racetrack(1k)
(m) Racetrack(2k)
(m) Racetrack(5k)
(0) Racetrack(10k)
(p) Cartpole(200)
(q) Cartpolc(1k)
Cartpole(2k)
(s) Cartpole(Sk)
(1) Cartpole(1Ok)
Training performance of data loss different benchmarks varying data points. The y-axis represents the data loss (Q))) and the x-axis gives the number of training epochs. Since Thermostat is initialized with data trained programs to give quicker convergence, the data loss does not change lot during training. For other benchmarks, data loss DSE and DIFFAI+ are both converging, Overall speaking, DSE sacrifices some data loss to give safer programs.
Figure 10:
A.8.3 DETAILS OF TRAINING AND TEST DATA
We also attach the detailed training data loss (Q), training safety loss (C#), test data loss and prov- ably safe portion for Thermostat( IT), AC(Figure and [acetrack(Figure/]] 133). Specifically, training safety loss measures the expectation of the quantitative safety of the symbolic trajectories and provably safe portion measures the portion of the symbolic trajectories that is provably safe. In- tuitively, in training, the number of unsafe symbolic trajectories is larger and the unsafe symbolic trajectories further away from safe areas, C is larger. In test, if the number of provably safe symbolic trajectories is larger, the provably safe portion is larger.
23

---

Published as a conference paper at ICLR 2022
Data Size
Approach
Q
C#
Test Data Loss
Provably Safe Portion
DSE DIFFAI+
0.13
0.02
0.24
0.99
200
0.07
25.37
0.21
0.28
DSE DIFFAI+
0.09
0.0
0.22
0.99
1000
0.05
1.96
0.14
0.55
DSR
0.08
0.0
0.21
0.99
2000
DIFFAI+
0.05
2.70
0.15
0.46
DSE
0.07
0.0
0.19
0.99
5000
DIFFAI+
0.04
4.58
0.18
0,40
DSE
0.04
0.0
0.19
0.99
10000
DIFFAI+
0.02
1,23
0.19
0.80
Figure 11: Training and Test Results of Thermostat
Data Size
Approach
Q
C#
Test Data Loss
Provably Safe Portion
DSE DIFFAI+
0.60
0.0
0.85
0.99
150
0.53
21.46
0.87
0.22
DSE DIFFAI+
0.64
0.0
0.86
1.0
750
0.57
20.66
0.87
0.26
DSE DIFFAI+
0.58
0.84
1.0
1500
0.53
28.28
0.87
0.17
DSE DIFFAI+
0.62
0.0
0.85
1.0
3750
0.53
26.31
0.87
0.21
DSE DIFFAI+
0.61
0.0
0.86
1.0
7500
0.52
27.23
0.88
0.27
Figure 12: Training and Test Results of AC
Data Size
Approach
Q
C#
Test Data Loss
Provably Safe Portion
DSR
0.22
1.12
0.28
0.66
200
DIFFAI+
0.11
2.04
0.31
0.0
DSE
0.22
0.0
0.25
0.99
1000
DIFFAI+
0.17
2.03
0.26
0.0
DSE
0.21
0.0
0.25
0.99
2000
DIFFAI+
0.17
2.03
0.25
0.0
DSE
0.22
0.0
0.27
1.0
5000
DIFFAI+
0.17
2.03
0.24
0.0
DSR DIFFAI+
0.22
0.0
0.24
0.99
10000
0.13
2.26
0.24
0.0
Figure 13: Training and Test Results of Racetrack
24

---

Published as a conference paper at ICLR 2022
A.9 ADDITIONAL PATTERN ANALYSIS
Figure Figure exxhibit safety performance of learnt patterns. The details of the patterns are in Figure g We highlight the patterns that cover the scope differences between AIFFAI+ and DSE, including
parameterized branch conditions(Pattern 1-4) and bad joins(Pattern 5). In addition, we describe the characteristics in each pattern that influence DSE's performance, including deep local minimum in branches and limitations on sampling. In implementation, we randomly initialize the neural network's parameter (DIFFAI+ and DSE start from the initialization). We observe that all the neural networks are initialized to come with an output I when z E [-5, 5], which gives 0.0 provably unsafe portion for Pattern 1, 2 and 5 in initialization.
We give detailed description of each patterns" characteristic (with results analysis), where all the patterns' safety loss is over the only variable in assertion:
Pattern: The output, y, of the neural network module is only used the parameters to calculate the branch condition satisfaction. In each branch, is only updated with con- stants. When the gradient pack-propagation executes in DIFFAI+, the gradients over is constantly zero since the branch splitting computation is not involved in safety loss. While for DSE, we consider the y by using the volume-based probability in safety loss calculation. Therefore, DSE is able to guide the program to fall into the second branch thoroughly by reducing the probability of y falling into the first branch.
Pattern2: Similar to Pattern 1, the output of the neural network is used in branch condition. Different from Pattern 1, the input of the neural network, z, participates the assignment for 2. DIFF AI+ has the same "0 gradient" issue as Pattern DSE sometimes reaches an area during training where only a super small portion of falls into the first branch and the sampling operation does not pick the portion because the probability is super small. this way, DSE still steadily converges with a C## = 0.0. However, the program is safer but not worst-case safe because C## 0.0 represents all the trajectories sampled by DSE during training is safe.
Pattern 3 uses y in the branch condition as well. For the two branches, z in the first branch is directly assigned by a function over y and the second branch naturally safe. Therefore, the goal for learning safe programs is to optimize 2 10 y to the safe area. Both AIFFAI+ and DSE success on this pattern only optimizing over one branch is enough to learn safe program.
Pattern3:
Pattern4: Pattern 4 is typical example of local minimum. As the branch condition is y S -1.0, the neural network may be initialized to fall into both branches. The first branch is naturally safe and the second branch comes with a local minimum = 2. DIFFAI+ is not able to Iearn the safe programs guided by the safe loss and DSE can learn. DSE not achieving 1.0 provably safe portion as there is part of training gets stuck in the local minimum with the second branch. There is an exception for AI+: it gets 0.58 for NNBig. The 0.58 can not be viewed as it specifically benefits from the random initialization. Since this is not a complicated task, DiffAl+ benefits from weights initialization when using NNBig. Specifically, some random initializations of NNBig may pick neural network parameters that make all the fall into the first branch(safe). This leads to a not bad result of DiffAl+ for Pattern4 with NNBig. If there are other random initializations that can benefit the approach, DiffAl+ and DSE should benefit the same way. DSE does not specifically benefit from the random initialization for Pattern 4 since DiffAl+ fails on NNSmall and NNMed while DSE does not and DSE gives a safer program on NNBig.
result benefiting from the safety loss calculation
Pattern5: The first branch in this pattern is a function over the output of the neural network and the second branch is unsafe. There are bad joins for DIFFAI+. For here, one symbolic representation of y falling into both branches always joins with the unsafe results (z := - -10). There is no gradient from 2 = - 10.0 can direct the neural network to the safe area. DSE can work on this pattern as there a volume-based probability used in learning to guide the y to fall into the first branch.
25

---

Published as a conference paper at ICLR 2022
A.10 ADDITIONAL DETAILS OF THE CORE ALGORITHM
The key point of "sampling based on volume" is the volume-based probability, which is measured by the volume portion satisfying one condition. Therefore, the volume portion must be differentiable (w.r. 0). In addition, the volume is not required to be non-zero. We give a detailed description as below: We represent the Vg by the box domain (The detailed definition of Vy is in Appendix A.2). When the branch condition splits the box domain into two polyhedra (direct volume calculation for polyhedra is -P hard [1]), we add one new dimension (with a new variable) to allow that the splitting is over this new dimension. Formally, starting from one state s = (Z, V), condition if.f xR) <= M ..... DSE transforms the program first by converting the condition to Then, the volume portion is measured by the intersection portion of the concrete interval representation of Zk+11- Specifically, the additional variable's is concrete interval length is O, it indicates that the variable represents one point. It falls into one branch (Say branch 1) completely. Then the probability to select branch is 1.0, and the
2 f( Tk); fr <= M
probability select other branches is 0.0.
A.11 ADDITIONAL SCALABILITY EVALUATION
For most of the additional experiments for scalability, we take Thermostat. We take AC as the base benchmark for 'different neural network architectures' we add convolutional layers. There is one variable as the input for the NN in Thermostat, and using Conv d with kernel size=1 is the same as fully connected layers.
In the original Thermostat, there is a 20-Iength loop with dynamic program length of x = 120. In each iteration, there are 2 branches. Branches stacking on each other would increase the number of branches exponentially. Thus, in the original Thermostat, there is 2 paths to go in total. We evaluate the scalability over Thermostat by increase the number branch in each iteration, doubling the loop length, and use super refined input size.
A.11.1
DIFFERENT NUMBER OF BRANCHES
Data Size
Approach
C##
Test Data Loss
Provably Safe Portion
Ablation
0.03
0.2
0.66
200
DIFFAI+
0.07
1.08
0.19
0.66
DSE
0.07
0.25
0.99
Ablation
0.01
0.2
0.68
10000
AIFFAI+
0.05
1.53
0.18
0.67
DSB
0.06
0
0.22
0.99
Figure 14: Results from Thermostat with Three Branches in Each Iteration.
With Thermostat, increase the number of branches in the iteration from 2 to 3, by allowing the isOn has three branches to go. We convert the branches from (cool, heat to (cool, lowHeat, highHeat). J. That said, the entire number of branches in the program increases from 220 to 3 We show that DSE still performs well. And DiffAl+ can not give very good results even if ablation gives reasonable number.
A.11.2 DIFFERENT DYNAMIC LENGTH
With the same structure the original thermostat, we set the loop length of 40, which doubles the dynamic length and the number of branches increases from 220 to 240 accordingly.
We show that with 200 data, DSE gives a result better than baselines but definitely less-than-perfect In the training where DSE did not give safe programs in the cases where the symbolic state (split by too many branches) is too refined. The symbolic state gets stuck in area where it's not safe but it falls into one trajectory fully. In this way, the volume-base later transitions and the gradient over 0 is 0.0. The highly unsafe stuck state gives very high state safety loss, which exhibited by the large training safety loss for DSE. When DSE is not stuck, can learn safe programs. That's why the average provable safe portion is still larger than baselines.
probability is always 1.0 for the
26

---

Published as a conference paper at ICLR 2022
Data Size
Approach
Q
C#
Test Data Loss
Provably Safe Portion
Ablation
0.03
0.19
0
200
DIFFAI+
0.05
2.05
0.21
0
DSE
0.17
396
0.26
0.36
Ablation
0.01
0.19
0.67
10000
DIFFAI+
0.05
25.42
0.21
0
DSB
0.08
0.24
0.99
Figure 15: Results from Thermostat with 40-Length Loop.
We also show that, with more data, DSE can give a very good safe program for this challenging task while baselines not. Specifically, DIFFAI+ (splitting 100) easily gets stuck when guided by the highly non-differentiable representation of the safety loss even if ablation gives a reasonable result.
A.11.3
SUPER REFINED INPUT SIZE
Data Size
Approach
Q
C#
Test Data Loss
Provably Safe Portion
Ablation
0.02
0.19
0.33
200
DIFFAI+
0.04
4.5
0.18
0.33
DSE
0.07
129.5
0,25
0.33
Ablation
0.01
0.19
1
10000
DIFFAI+
0.01
0.19
1
DSB
0.01
0.19
1
Figure 16: Results from Thermostat with Super Refined Input Size.
With the Thermostat, this task starts from a super refined input size: [60.0. 60.1]. The input in the original Thermostat is [60.0, 64.0]. We can see here DSE does not give good results with 200 data and gives the same result with the Ablation when using the full dataset.
This benchmark exhibits the trade-off between refinement and the ease of learning of DSE. When the input size is small enough that it only fully falls into one trajectory with an updated I during learning. In this way, the volume-base probability is also 1.0 for this trajectory and there is not gradient guiding the state to jump from this trajectory to another. Thus, when this case occurs in the training, DSE gets stuck.
A.11.4
DIFFERENT NEURAL NETWORK ARCHITECTURE
Data Size
Approach
Q
C#
Test Data Loss
Provably Safe Portion
Ablation
0.02
0.19
0.33
200
DIFFAI+
0.04
4.5
0.18
0.33
DSE
0.07
129.5
0.25
0.33
Ablation
0.01
0.19
1
10000
DIFFAI+
0.01
0.19
1
DSE
0.01
0.19
1
Figure 17: Results from AC with Convolutional Layers
With AC, we use NN with Convld(1, 1, 2)-Rel.UO-Convlddf. 1, 2)-ReLJU0-Linear44 32)- Rel.UO)-Linea(32,, 6) Diggmmood,,, where ConvId(X Y, 7.) means an input channel of X, an output channel of Y and kernel size of Z and Linear(X. Y) means input channel of X and output channel of Y.
The above table exhibits that DSE can work for neural networks with convolutional layers. For AC specifically, all the training data comes from safe trajectories. There a lack of generality for Ablation to get good test data loss. When adding additional safety constraint(e.g. In DSE). it helps to overcome some local minimum areas and gives a better test data loss even if the training data loss worse than Ablation.
27

---

Published as a conference paper at ICLR 2022
A.11.5 CART-POLE EXPERIMENTS
In the Cartpole experiment, we use the trajectories data generated from the expert model from Imi- lation Package. Starting from S |-0.05, 0.05]*, we follow Bastani et al. (2018) to train cart of which the pole keeps upright E [-12 * * moth.pi/360 2 math.pi. pt/330/ the definition of upright is the standard one from OpenAl Gym). The state space is 4 and the action space is 2. We use layer fully connected neural network (each layer followed by a ReLU and the last layer followed by Sigmoid) to train. We follow the two points in Bastani et al. (2018) below to setup the experiment:
We approximate the system using a finite time horizon Tmaz 10;
We use linear approximation f(s. a) ~ As + Ba.
We did the verification by splitting the input space into 20 boxes. And we extract the percentage of safe concrete trajectories from 100 uniformly sampled starting points. The results for restricting pole angle are shown in Figure 18
Approach
Q
C#
Test Data Loss
Provably Safe Portion
Percentage of Safe Concrete Trajectories
Ablation
0.13
0.14
0.67
100%
DIFFAI+
0.13
0.66
0.14
0.62
100%
DSE
0.16
0
0.18
0.78
100%
Figure 18: Results of Cart-Pole(angee)
As indicated by the above figure, pure imitation learning (Ablation) can already learn pole keeping upright. To show DSE 's ability to train a safe program without too much help from the data loss, we add another experiment following the same setting above except the constraint, which is shown in the main paper.
A.11.6 TRAIN DSE FROM HIGHLY UNSAFE DATA
Benchmark
Data Size
Approach
Q
C#
Test Data Loss
Provably Safe Portion
Ablation
0.04
0.19
0.20
200
DIFFAI+
0.06
4.40
0.21
0.20
DSE
0.16
0.00
0.27
0.99
The5mosta((45% Unsafety)
Ablation
0.04
0.18
0.59
10000
DIFFAI+
0.05
3.72
0.17
0.46
DSE
0.06
0.00
0.18
0.99
Ablation
0.89
1.04
0.32
150
DIFFA
0.90
25.20
1.04
0.24
DSF
0.96
0.00
1.03
1.00
AC(49% Unsafety)
Ablation
0.79
1.03
0.00
7500
DIFFAI+ 0.81
15.00
1.03
0.00
DSE
0.88
0.00
1.03
1.00
Figure 19: Results from Highly Unsafe Data
In summary, DSE can scale to programs with reasonable length, branches and different neural net- work architectures. One challenge DSE is that learning becomes harder when symbolic state rep- resentation becomes more refined(including super refined input space, safety constraint, and branch splitting). We leave this open for future works to seek identify better tradeoffs between precision of symbolic states and ease of learning.
28


Reviews:
[{"review_id": "gTEp-HgACBO", "reviewer": "Reviewer_X2YM", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "**Strengths**\n\nThe paper is well written and proposes a mathematically rigorous algorithm to compute gradients in the presence of discontinuous conditionals. The formulation looks sound to me. The need to take gradients through symbolic components arises in many other scenarios, so I am excited to see this idea explored beyond the context of this work.\n\n\n**Weaknesses**\n\nI have several concerns regarding the current evaluation setup. \n\t\n— In my opinion, all of the tasks (even the thermostat, ac, racetrack) are synthetic. In particular, I am calling them synthetic because the data to train these models are artificially generated. Thus, the lack of a real-world application of this technique is one of my main concerns. \n\n— I am not convinced about generating the training data from a manually written “safe” program. In these safety-critical domains, one main challenge is the tension between achieving good loss and achieving safety. That seems to be missing in this paper (except probably for the racetrack benchmark).\n\n— These benchmarks actually seem like reinforcement learning problems rather than supervised learning problems. It is not clear to me how the current approach would work in a reinforcement learning setting. Moreover, there are several safe RL works [1, 2, 3] that might form as good baselines to compare this approach to. And these safe RL approaches don’t need to take gradients through the environment code. \n \n— Another potential issue with optimizing through symbolic code is the presence of numerous minima. This issue is a much bigger issue than just being able to take the gradient. I guess that the authors didn’t encounter this local minima issue because of the supervised data (which is collected from a safe program). More realistic benchmarks might reveal this problem. \n\n**Other comments**\n\nWhy is safety not measured on concrete trajectories during the evaluation? From figure 4, most of the concrete trajectories from the baselines look safe, but the symbolic trajectories are not safe. \n", "summary_of_the_paper": "This paper presents an approach to learn worst-case safe parameters for neurosymbolic programs (programs with neural networks + symbolic portions). The key contribution is an algorithm to compute gradients for the worst-case safety loss by symbolically sampling control paths in the programs and using a modification of the Reinforce estimate to approximate the gradients. The approach is compared with DiffAI on several synthetic tasks. ", "summary_of_the_review": "The evaluation is not satisfactory as it is very synthetic and seems to be tailored to benefit the presented approach. Therefore, I lean towards rejecting this paper. \n\nUpdate after the author's response: I am happy with the additional experiments and increasing my score to a 6. ", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "YYKMJfkd3ij", "reviewer": "Reviewer_yj7y", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "This paper is well-motivated and targets an important, forward-looking problem: how to learn neurosymbolic programs that are worst-case-safe. The proposed technique of combining symbolic execution with sampling  and REINFORCE-styled learning is interesting. And the experiments show that the proposed method is effective on the benchmarks considered in the paper. I have a few questions regarding the method, which I put below.\n\nStrength\n- This paper is well-motivated, targeting an important, forward-looking problem\n- The proposed technique is interesting\n- Experiments show that the method works well on the benchmarks considered, and also significantly outperforms a prior approach \n\nWeakness/questions\n- How are the symbolic states $\\sigma$ generated, in particular, the logical formula V’s? Are they human-specified? Seems that they are the key to reduce the trajectory space to a finite set of symbolic trajectories, but I did not find how they are generated in the paper.\n- It seems that the proposed REINFORCE-based algorithm essentially works by pushing the parameters of the neural models so that they will only trigger the safe symbolic trajectories. If that is the case, the following simpler method seems to work as well: starting with the set of symbolic trajectories, first determine the subset that are safe, convert the subset into constraints on input/output of the neural model, then train the model directly to satisfy this constraint (by penalization). I would like to see the authors compare to this baseline, or discuss why this would not work.\n- In page 3, it was mentioned that the proposed method assumes that the program contains only one learnable neural network. Why does the method require this constraint? This seems to limit the applicability of the proposed method. \n", "summary_of_the_paper": "This paper targets the problem of learning parameters of programs that involve both neural and symbolic components, with the objective that the program is guaranteed to be safe. This objective is challenging because it is not differentiable. The proposed method uses symbolic execution to finitize the execution trajectories and uses sampling with REINFORCE-styled algorithm to optimize for an approximated objective. Results show that although the proposed method is not guaranteed to be sound, it in practice produces programs that are safe on the example benchmarks.\n", "summary_of_the_review": "This paper is well-motivated and targets an important problem. The proposed method is novel and interesting. However, I have some questions regarding the justification of the proposed method and the limitations on its applicability. Overall, I am slightly leaning towards acceptance, but would like the authors to address my questions before I can solidify my recommendation.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "4: The contributions are significant, and do not exist in prior works.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "DcF-Rno5b_", "reviewer": "Reviewer_ohyh", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "## Novelty and Significance\n\nThe proposed approach is both novel and significant. There is an emerging field of approaches for developing and verifying such neurosymbolic programs with safety constraints. DSE represents an advance in that literature which, depending on how well the technique scales to other programs, could emerge as an influential approach in this literature.\n\n## Correctness and Clarity\n\nTo the best of my knowledge, the approach presented in the paper is technically sound. My main qualm with the correctness of the approach is in the lack of discussion of the implications of sampling based on volume. Specifically:\n- Sampling based on volume:\n  - The definition of $V_\\theta$ near the top of page 4 is relatively loose. Specifically, it seems $V_\\theta$ must consist of shapes with differentiable (w.r.t. $\\theta$) and non-zero volume. The choice of intersection of intervals seems to be a sufficient choice (it doesn't seem to allow for the full generality, but that's fine), though it does leave open the possibility of zero volume (e.g., if the shape is lower dimensional than the full space [such as a plane](https://math.stackexchange.com/questions/1697067/lebesgue-n-dimensional-measure-of-a-hyperplane)).\n  - In addition to clarifying these points (or correcting me if my understanding of this is wrong), the paper should discuss the case of identically zero volume symbolic states, since this would cause the probability to become undefined.\n  - It would also be helpful to see some explicit analysis of the volume and sampling based approach, especially as volumes can behave unintuitively in high dimensions. The paragraph in the middle of page 5 (\"Note that a low value ... employed during learning\") addresses some of these questions, but the evaluation does not show the probabilities along trajectories induced by this volume-based approach.\n\nI am less convinced of the correctness of the empirical evaluation (corresponding to the final contribution in Section 1). This is due to a combination of the both the benchmarks chosen as well as the evaluation of the results.\n- The approach is only validated on programs with control flow, on which DiffAI was not evaluated. DiffAI+ is not a published system, so it's hard to reason about what to expect its performance to be. The paper would be significantly stronger if either the authors compared against a system with well-understood behavior on the given task (i.e., some other neurosymbolic network training system with safety constraints) or the authors additionally evaluate DSE in a setting that DiffAI is validated to perform well in (i.e., on programs without branches).\n- The approach is only validated on small-scale programs, using a manual heuristic of splitting the input space into 100 subregions. How was this heuristic decided upon? Does the approach still work when not splitting, or splitting at a finer granularity? Does the approach work on longer programs (with more than 20 lines of code) or when using different neural network architectures? Though of course I don't expect the technique to scale perfectly, it would help to understand where the technique breaks down rather than showing only benchmarks on which it gets perfect or near-perfect results.\n- There is also little discussion of the actual results. For instance, there is no analysis of what characteristics of the benchmarks allow DSE to achieve perfect of less-than-perfect results. As a minor point here, the paragraph at the bottom of page 7 also claims that DSE is able to successfully learn pattern2 while DiffAI finds pattern4 hard; however, actual gap in results between the two benchmarks is relatively small (0.58 v.s. 0.78) which makes the claims of success and failure feel arbitrary.\n- The paper doesn't show C^# for many problems, meaning there is something of a disconnect between the main body of the paper and the results. Figure 9 shows this over the course of training, though for a tiny dataset size. I would be interested in seeing this for all data points (potentially just the final value). I'm also somewhat confused by DSE's behavior on the racetrack and the thermostat. Is DSE's loss conservative? My understanding was that it is not (that C^# > 0 means that the program is not safe) but both the Thermostat and Racetrack show some variance still, implying to me that the program is unsafe.\n- The paper also doesn't show Q^# over the course of training. This especially hampers the understanding of the baseline results -- for instance, why is it that Ablation has consistently high test data loss when it's trained with no constraints? Is this just an issue with generalization?\n\n\nMoreover, the paper (both approach and evaluation) is not sufficiently clear, such that it would likely not be possible to reproduce the results (or even implement the algorithm) based on the description in the paper.\n- Clarity of approach:\n  - I'm not super familiar with the prior work, but why convexify the program space? Algorithm 1 shows that this is essentially an iterative algorithm that often will repeat prior steps (with a different value for lambda). Please correct me if I'm misunderstanding something about this.\n  - Top of page 5: it would be helpful to define volume here, since it's not immediately clear that the formulae describe shapes (on first pass, I thought that this meant something like the count of satisfying assignments).\n  - This is a minor point, but it would be great if the entire set of terms, types, and definitions in the formalism were collected in one place (e.g., as a table in the appendix). I found myself continually having to scroll back and forth and search to find definitions.\n\n- Clarity of evaluation:\n  - Many details of the evaluation are left out. Specifically these include the details of the \"ground-truth program\", the specific loss functions (i.e., the definition of Q^# and C^# for each approach), the meaning of the error bars in Figure 3, the training procedure for the neural networks (i.e., learning rate, convergence criteria, etc.), the approach for interleaving the training of the networks, and the actual architecture of the neural networks.\n  - It is also very hard to understand the plots in Figure 4 -- my understanding of the symbolic trajectories is that they should encode intervals of state, but the trajectories seem to be individual lines. It also seems like the symoblic trajectories for the Thermostat allow for the possibility of failure, while Figure 3a seems to show that DSE is verifiably correct.\n\n\n# Response to author response\n\nThanks to the authors for the very detailed replies. Based on these clarifications and new results, I plan to raise my score to an accept (under the assumption that these clarifications are integrated into the paper).\n\n## Volume calculation\n\nThanks to the authors for the clarification here. To confirm my understanding, the description in the paper:\n\n> let Vol($V_\\theta$) denote the volume of the assignments to X that satisfy $V_\\theta$\n\nis incorrect: for instance in Example_volume, the volume of the assignments to X that satisfy $V_\\theta$ is zero, because res=0. However, the example shows that the volume calculation is not actually performed over the entire program state X, and instead is only calculated as the fraction of the range of the singular variable in an if condition.\n\nIf this is the case, the authors should correct this description for the final version of the paper. Regardless, the clarification has convinced me that the authors have thought this through and that the approach is sound.\n\n\n> Could you please clarify further what you mean by “volumes can behave unintuitively in high dimensions”? We are not confident that we fully understand the question.\n\nSorry for including such a vague statement without an example/citation, I should have been much more clear in the original review. I meant the examples along the lines of the majority of the volume being near the surface of high-dimensional shapes (so e.g. if a vector `x` of length 100 had all elements $\\in [0, 1]$, then a branch that checked that all elements were less than 0.9 would likely never be sampled) and that the volume of the unit n-ball tends towards zero. I was curious to see the actual volumes computed by the technique, to understand whether the technique was falling prey to any of these degenerate behaviors.\n\n## Scalability\n\nThanks for these results -- I would still be interested in seeing results where DSE falls apart even with more data (10,000 does not seem like a particularly large dataset by ML standards, especially considering that this data is synthetically generated, so the fact that DSE still works in this domain gives the impression that these are still small-scale problems), but I'm overall satisfied by this presentation which shows the dimensions on which scalability can be a concern and the knobs to turn to address them.\n\n## Additional experimental details and results\n\nThanks to the authors for the additional details on the programs, Q, C^#, and the additional analysis. This additional data and analysis seems to be sufficient for readers to much more completely understand the experiments performed, their results, and the comparisons between DSE and the baselines.\n", "summary_of_the_paper": "The paper proposes DSE, an approach to optimizing parameters of neurosymbolic programs (programs with mixed neural and symbolic components) while satisfying a safety constraint. To accomplish this, DSE defines a *safety loss*, a nonnegative term in the loss function which is nonzero when the function does not satisfy the safety constraint. This safety loss is constructed by symbolically executing the program, executing discrete transitions probabilistically according to a uniform distribution over concrete states. The paper evaluates DSE on a set of small-scale case studies, showing that in programs with discrete control flow, DSE can often train neural networks that soundly lead to safe behavior, with similar quality of learned results as those of a neurosymbolic training approach which does not take into account safety.", "summary_of_the_review": "Weak reject. Though the approach is novel and significant and seems correct, the clarity of the description of the approach and clarity and correctness of its evaluation are lacking. I would be willing to raise my score if the authors provided a much more clear description of the algorithm and its evaluation such that it would be possible to reproduce the majority of the results based on the paper alone. I would be willing to raise my score further if the authors provided a more thorough evaluation of the scalability of the approach beyond just neural networks of different parameters (i.e., programs of different static and dynamic lengths, more or less branches, different input sizes and splits, and different neural network architectures).", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "4: The contributions are significant, and do not exist in prior works.", "empirical_novelty_and_significance": "Not applicable"}, "extra_text": {}}]

Author rebuttal:

Meta-review: The proposed method, Differentiable Symbolic Execution (DSE), addresses the safety of learned navigation and control programs. The approach samples code paths using a softened probabilistic version of symbolic execution,  constructing gradients of a "safety loss" along these paths, and then backpropagating these gradients through program operations using RL. 

Pros
 - The paper is well-written and sound
 - The issue of safety is underexplored
 - The method improves over a strong baseline on benchmarks

Cons
 - The benchmarks are relatively small-scale and artificial
Decision: Accept (Poster)