Neuro-symbolic Learning Yielding Logical Constraints
Authors: Zenan Li
Yunpeng Huang
Zhaoyu Li
Yuan Yao
Jingwei Xu
Taolue Chen
Xiaoxing Ma
Jian Lu
Venue: NeurIPS 2023 poster (2023)
Keywords: Neuro-symbolic learning
logical constraint learning
symbol grounding
difference-of-convex relaxation
TL;DR: An end-to-end neuro-symbolic learning framework that fuses neural network training, symbol grounding, and logical constraint synthesis

Abstract: Neuro-symbolic systems combine the abilities of neural perception and logical reasoning. However, end-to-end learning of neuro-symbolic systems is still an unsolved challenge. This paper proposes a natural framework that fuses neural network training, symbol grounding, and logical constraint synthesis into a coherent and efficient end-to-end learning process. The capability of this framework comes from the improved interactions between the neural and the symbolic parts of the system in both the training and inference stages. Technically, to bridge the gap between the continuous neural network and the discrete logical constraint, we introduce a difference-of-convex programming technique to relax the logical constraints while maintaining their precision. We also employ cardinality constraints as the language for logical constraint learning and incorporate a trust region method to avoid the degeneracy of logical constraint in learning. Both theoretical analyses and empirical evaluations substantiate the effectiveness of the proposed framework.

Neuro-symbolic Learning Yielding Logical Constraints
Zenan Li' Jingwei Xu'
Yunpeng Huang' Taolue Chen 3
Zhaoyu Li Xiaoxing Ma' Jian Lüi
Yuan Yao
State Key Lab of Novel Software Technology, Nanjing University, China
*Department Computer Science, University of Toronto, Canada School of Computing and Mathematical Sciences, Birkbeck, University of London, UK (lizn, hyp]esmail nju. edu. en, zhaoyu@cs.. ttrryuuussttttottooooooooooooo.. toronto. edu, chen@bbk. ac. uk, {y yau, jingwiiggexi xxm, 1j)@nju sec.j.ueed.cr edu.cn
Abstract
Neuro-symbolic systems combine neural perception and logical reasoning, repre- senting of the priorities of Al research. End-to-end learning of neuro-symbolic systems is highly desirable, but remains to be challenging. Resembling the dis- tinction and cooperation between System and System of human thought (à Kahneman), this paper proposes a framework that fuses neural network training, symbol grounding. and logical constraint synthesis support learning a weakly supervised setting. Technically, it is cast as game with two optimization problems which correspond to neural network learning and symbolic constraint learning re- spectively. Such a formulation naturally embeds symbol grounding and enables the interaction between the neural and the symbolic part both training and inference. The logical constraints are represented as cardinality constraints, and we use the trust region method to avoid degeneracy in learning. distinguished feature of the optimization lies in the Boolean constraints for which introduce difference-of- convex programming approach. Both theoretical analysis and empirical evaluations substantiate the effectiveness of the proposed framework.
Introduction
Perception and reasoning serve as fundamental human abilities that are intrinsically linked within the realm of human intelligence [Kahneman 2011 Booch et al. 2021]. The objective of our study is to develop a learning framework for neuro neuro-symbor symbolic systems (c.g., the one illustrated in Figure [ enabling simultaneous learning of neural perception and symbolic reasoning.
The merit of neuro-symbolic learning lies in resembling the integration of System and System 2 of human minds [Kahneman, 2011 Yoshua and Gary 22200 LeCun 2022). First, it eliminates unnatural and sometimes costly human labeling of the latent variables and conducts learning in an end-to-end fashion. Second, it generates not only a neural network for perception, but also set of explicit (symbolic) constraints enabling exact and interpretable logical reasoning. Last not least, the mutually beneficial interaction between the neural and the symbolic parts during both training and inference stages potentially achieves better performance than separated learning approaches.
However, existing approaches do not provide an adequate solution to the problem. They either (1) are not end-to-end, i.e., human intervention is employed label the latent z so that the task can be divided into a purely neural subtask of image classification and purely symbolic subtask of constraint solving, or (2) are not interpretable, i.e., can only approximate symbolic reasoning with neural network but without explicit logical constraints generated (e.g., Wang al. (2019). Yang et al. (2023), ) which inevitably sacrifices the exactness and interpretability of symbolic reasoning, resulting in an inaccurate black-box predictor but not genuine neuro-symbolic system.
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

Raw input
Neural network fe
Latent symbol
Logical reasoning 8
Final output
1
3
4
G
O-O --6
2
3
2
(x())==1
System
System
Information flow:
Inference perception neural network, reasoning SMT solver
Z3
Constraint learning revising I6 with current fo(x)
Neuro- Sonuro-ymmolicc
Symbol grounding revising to satisfy constraints Rg. (x.
Leurning Combining System 1 and System 2
SMT solver
Network training revising fo by back-propaggting grounded z
An example of neuro-symbolic learning for visual SudoKu solving. this task, the neural network is employed to transform the puzzle image (strawberry etc.) into its corresponding symbols, while symbolic reasoning is utilized to produce the puzzle's solution. Importantly, the neuro-symbolic learning task is framed in weakly supervised setting, where only the raw input (the puzzle image x) and the final output (the puzzle solution y, but without numbers in z) is observed.
Figure 1:
We argue that end-to-end and interpretable neuro-symbolic learning is extremely challenging due to the semantic and representation gaps between the neural part and the symbolic part. The semantic gap caused by the latency of the intermediate symbol (i.e., z in Figure D makes the neural network training lack effective supervision and the logic constraint synthesis lack definite inputs. The representation gap between the differentiable neural network and the discrete symbol logic makes it difficult to yield explicit symbolic constraints given the continuous neural network parameters. Despite existing proposals mitigating some of these obstacles such as visual symbol grounding (Topan et al.) 2021 Li
et al. 2023]. softened logic loss [Kimmig et al. 2012 Xu et al. 2018), semidefinite relaxation Wang al.
2019 etc., none of them realize the full merit of neuro-symbolic learning.
In this paper, we propose a new neuro-symbolic learning framework directly meeting the challenges. bridges the semantic gap with an efficient symbol grounding mechanism that models the cooperative learning of both the neural network and the logical constraint as a bilevel optimization problem. It relaxation
bridges the representation gap by employing difference-of-convve (DC) programming technique for Boolean constraints in the optimization. DC programming ensures the convergence to explicit logical constraints, which enables exact symbolic reasoning with powerful off- aff-the-shell tools such as SAT/SMT solvers [Eén and Sörensson 2006) Bailleux and Boufkhad] [2003] Bailleux et al.) (006) during the inference stage. In addition, to address degeneracy logical constraint learning. i.e., the tendency to learn only trivial logical constraints (e.g., resulting in simple rules insufficient to solve SudoKu), we introduce an additional trust region term [Boyd al., [2004] Conn al. (200). and then employ the proximal point algorithm in the learning of logical constraints.
We provide theoretical analysis of the convergence our algorithm, as well as the efficacy of the DC relaxation in preserving the exactness and the trust region in preventing degeneracy. Empirical evaluations with four tasks, viz. Visual Sudoku Solving, Self-Driving Path Planning, Chained XOR, and Nonograms, demonstrate the new learning capability and the significant performance superiority of the proposed framework.
Organization. Section 2 formulates our neuro-symbolic learning framework. Section 3 details the algorithm and theoretical analysis. Section presents empirical evaluations. Section covers related work. Section discusses the limitations. Section 7 concludes the paper.
2 Neuro-symbolic Learning Framework
In this paper, we focus on end-to-end neuro-symbolic systems comprising two components: (1) neural network fo: X > Z, which transforms the raw input x E X' into a latent state E 2; and (2) symbolic reasoning 9ø 2 - )) which deduces the final output y E ) from state z E Z. Both components are built simultaneously, taking only the input x and output y as supervision. We assume that Z and y are represented by finite sets, and thus can encode and by binary vectors using

---

one-hot encoding. For ease of discussion, we directly define 2 and y to be spaces 8 and B" of Boolean vectors, respectively, where 10.
Unlike existing work (e.g., SATNet [Wang et al. 2019)) that simulates logical reasoning in an implicit and approximate way via a network layer, our key insight is learn explicit logical constraints he: Bu+v + B on (z. y) in the training phrase, which allow to perform exact reasoning by off- the-shelf constraint solvers (e.g., SMT solvers) in the inference phrase. Fig. iillustrates our neuro- symbolic learning framework.
The latent state enables the interaction between neural perception and logical reasoning. If were observable, we could perform the learning of neural network and logical constraint by solving the following two separate optimization problems:
θ = arg ming (xx,))> (fo z)],
Φ arg min (22 y), 1)],
where (x) z) refers to the enror between network prediction fx( and the actual symbol z, and (2(ho(z))) (z, refers to the (un)satisfaction degree of the learned logical constraints h&s (z, y) = 1.
Nevertheless, with z being latent, these two problems become tightly coupled:
0 = arg ming [(x.))=((((ff(()) 2)], Φ = arg min B(x,))=(( (22 1)},
s.t. ha(z.y) = 1, Z:
s.t. z z= fo Z.
We further surrogate the constraint satisfaction by loss functions, and obtain essentially game formulation as follows:
0 arg ming ((x.))=/((((((()))
$ arg min (xxy))-l((((hh(2.))) 1)],
(I)
s.t. 7 = arg mingez (2 (z,
s.t. 7 arg minzez E (fo()),,) z).
Three players are involved in this game: neural network fe and logical constraint he pursue optimal (prediction//aatifaattio))) accuracy, while z strives for the grounding that integrates the network prediction and logical reasoning.
2.1
Efficient and Effective Logical Constraint Learning
For efficient learning of logical constraints, we adopt cardinality constraint (Syrjänen 2009 2004
Fiorini et al., 2021] to represent logical constraint Cardinality constraints can be easily arithmetized, enabling the conventional optimization method and avoiding the computationally expensive model counting sampling [Manhavve et al. 2018 Xu et al. 2018 Li et al. 2020 (202). which significantly boosts the learning efficiency. In addition, the conjunctive normal form and cardinality constraints can be easily converted from each other, ensuring not only the expressiveness of the learned constraints, but also the seamless compatibility with existing reasoning engines.
DaastraimmCCrddnaiitt
Formally, we denote the column concatenation of z and y by y), and define a cardinality constraint hep (2, y) := w (z; y) E [imins bmax], where Φ- = (w, bininy dmax), w E Bu+v is a Boolean vector, and b dmax N are two positive integers. Moreover, we can directly extend he to the matrix form representing m logical constraints, i.c.,
he (2, = W yz; = (1)
with (2; E [bmin bmax];
where Φ= -W, Amin: 6max), W : (wI:..:; E Bmnx(u+)), and bmins bmax ENm
For effective learning of logical constraints, one must tackle the frequent problem of degeneracy that causes incomplete or trivial constraint="] First, for the bounding box [bmin. bmax] any of its superset a feasible result of logical constraint Tearning, but we actually expect the tightest one. To overcome this difficulty, we propose to use the classic mean squared loss, i.e., defining (2,
[Z y) - b where b can be computed in optimization or pre-defined. Then, our logical constraint learning problem can be formulated as a Boolean least squares problem (Vandenberghe and Boyd 2004). The unbiased property of least squares indicates that b ~ (b.ii b ) 2, and
'Cardinality constraints express propositional logic formulae by constraining the number of variables being true. For example, z V y V -z encoded as + y + 1.
'For example, suppose the targeted logical constraints are Z1 + Z2 y > 2 and 2 1. Degeneracy happens if one only obtains single constraint 2 Z2 + yı 2 2 trivial constraint 2 0.

---

the minimum variance property of least squares ensures that we can achieve a tight bounding box [b max [enderson 1975 Björck 1990, Hastie al. 2009]
Second, it is highly possible that some of the m distinct logical constraints as indicated by matrix W eventually degenerate to the same one during training. because the Boolean constraints and stochastic gradient descent often introduce some implicit bias [Gunasekar et al. 2017 Smith et al. 2021 Ali
al. 2020 To mitigate this problem, we adopt the trust region method [Boyd et 2004 Conn
et al. 2000], i.e., adding constraints || - w < A 1,..., m. where w is a pre-defined centre point of the trust region. The trust region method enforces each w, search in their own local region. We give an illustrative figure Appendix D to further explain the trust region method.
To summarize, using the penalty instead of the trust region constraint, we can formulate the optimiza- tion problem of logical constraint learning in
as
min (W.6)
Exx,y>> I (z:y) - b1l + W W - 10
arg minge & (1((()),
W W Bm
b E NT
2.2 Neural Network Learning in Tandem with Constraint Learning
A key challenge underlines end-to-end neuro-symbolic learning is symbol grounding, which is to tackle the chicken-and-egg situation between network training and logical constraint learning: training the network requires the supervision of symbol z that comes from solving the learned logical constraints, but the constraint learning needs as input recognized by the trained network. Specifically, since matrix W is often underdetermined in high- sigh-dimenssonal cases, the constraint z arg mingez (2 (z. y), 1) == (z:y) bll often has multiple minimizers (i.e., multiple feasible groundings of z), all of which satisfy the logical constraints (z.y) = 1. Moreover, matrix W is also to-be-trained parameter, meaning that it is highly risky determine the symbol grounding solely on the logical constraints.
To address these issues, instead of (approximately) enumerating all the feasible solutions via model counting or sampling [Manhaeve et al. 20118, Xu et al.) 2018 [i et al. [2020] van Krieken et al. [2022] Liet al. 2023 we directly combine network prediction and logical constraint satisfaction establish symbol grounding, owing to the flexibility provided by the cardinality constraints. Specifically, for given [0, +20), the constraint in network learning can be rewritten as follows,
2 = arg millgez || [ (z; b1|2 + al|z (x))
The coefficient be interpreted as the preference of symbolic grounding for network predictions or logical constraints. For a + O, the symbol grounding process can be interpreted as distinguishing the final symbol z from all feasible solutions based on network predictions. For a - +o0, the symbol grounding process can be viewed as a "correction" step, where we revise the symbol grounding from network's prediction towards logical constraints. Furthermore, as we will show in Theorem later, both symbol grounding strategies can finally converge to the expected results.
The optimization problem of network training in ① be written
min E8 (xxx)>>Dll ||| fo (x) ][3]
(3)
s.t. z = arg mingez W y2: bl12 + al|z fe(x)]12
where we also use the mean squared loss, i.e., E (fo 2) [|5((x) - =/12, for compatibility.
3 Algorithms and Analysis
Our general framework is given by (T) instantiated by (2) and 33. Both optimizations contain Boolean
constraints of the form || |:uu <il 2 + 7 7||u 22 where are Boolean variables We propose to relax these Boolean constraints by difference of convex (DC) programming (Too and Hoal An
1997 Yuille and Rangarajan
2003 Lipp and Boyd 2016 Hoai An and Tao 2018]. Specifically,
*In 2). for each logic constraint, Q = (2:y)T, b., q2 = w and T = X: in
Q = W. W: =
q2 To(x), y). and r a.

---

Boolean constraint {0, 1 can be rewritten into two constraints of u 1 x² 2 0 and u - x² < 0. The first constraint is essentially a box constraint, i.c., E [0, 1], which is kept in the optimization. The second one is concave, and we can equivalently add it as penalty term, as indicated by the following proposition [Bertsekas] 2015. Hansen et 1993 Le Thi and Ding Tao [00T]
Let denote the all-one vector. There exists to 2 such that for every? > to. the following two problems are equivalent, i.e., they have the same optimum.
Proposition 1.
(P) min q(u) Iuuu qul1² + T +lu -2ll.
(Pt) min ('()) == |Qu - 1:112 + Tlu q2ll2 + t(e u uuu).
Remarks. We provide more details, including the setting of lg, in Appendix A
However, adding this penalty term causes non-convexity, Thus, DC programming further lincarizes the penalty u u² Rz u² + (u ū)(1 - -2ū) at the given point ú, and formulates the problem in Proposition as
min "
- qQu'- + 2
-2222 + t(e - 2u."u. u.
By applying this linearization, we achieve a successive convex approximation to the Boolean con- straint [Razaviyayn 2014), ensuring that the training is more stable and globally convergent [Lipp) and Boyd 2016). Furthermore, instead of fixing the coefficient i, we propose to gradually increase it until the Boolean constraint is fully satisfied, forming an "annealing" procedure. We illustrate the necessity of this strategy in the following proposition [Beck and Teboulle, 2000 Xia 2009
Proposition 2. A solution u E {0, is stationary point of (Pt) if and only if
[V((u))((1 2u,) + t 0,
i i= 1,....,m
Then, if u E 13" is global optimum (P) (as well (Pt),, it holds that [Vg(u))(1 -2,;) + P: 2 0,
i == I....,n.
where Pi is the i-th diagonal element of (Q_QQ TI).
Remarks. The proposition reveals a trade-off of t: larger / encourages exploration of more stationary points satisfying the Boolean constraints, but a too large t may cause the converged point to deviate from the optimality of (P). Therefore, a gradual increase of t is sensible for obtaining the desired solution. Moreover, the initial minimization under small results in a small gradient value (i.e., [[Vg(u)):)) thus Boolean stationary point can be quickly achieved with few steps of increasing t.
3.1 Algorithms
(X1,.... XN) and Y = (y1,... yN) represent the data matrix and label matrix respectively, and (X) denotes the network prediction the k-th iteration.
For a given dataset (x),y:))'' X
Logical constraint learning. Eliminating the constraint in (2) by letting Z Soco (X), the empirical version of the logical constraint learning problem at the (k+ 1-th iteration is
(x))))(()) Y):: - -b,11 + Al[w; w 2 + ti((e -2w; ww
)
min
where wi ..... Win are parameters of logical constraints the k-th iteration. In this objective function, the first term is the training loss of logical constraint learning, the second term is the trust region penalty to avoid degeneracy, and the last term is the DC penalty of the Boolean constraint.
(k)
(k)
To solve this problem, we adopt the proximal point algorithm (PPA) [Rockafellar 1976 Parikh et al.) 2014 Rockafellar 2021]. as it overcomes two challenges posed by stochastic gradient descent. First, stochastic gradient descent has an implicit inductive bias [Gunasekar et al., 2017 Ali et al. 2020 Zhang et al. 2021 Smith et al. 2021], causing different w,, I..... m, to converge to a singleton. a 0-1 matrix and often ill-conditioned, leading to diverse or slow convergence rates of stochastic gradient descent.
Second, the data matrix (Jom X);
5

---

Algorithm Neuro-symbolic Learning Procedure
Set step sizes (7, v),, and penalty coefficients (X, 41, 12). Randomly generate an initial matrix ( under [0, 1] uniform distribution.
for 0, I,....: K" do
Randomly draw batch ((x,, yt) from training data.
Compute the predicted symbol 2; - fec (x:), (x...i=I,.......
b Network prediction
Update (W, b) from (Zi, yi), 1, ... m, by PPA update (Eq. 40
Constraint learning
Correct the symbol grounding z from z; to logical constraints ha (Eq. 5
Symbol grounding
Update θ from (x,, Z,), 1....,m, m, by SGD update (Eq. 6) if W & B3xx(++)) / (3x((tt)) then Increasing t /1/12.
Network training
Enforcing DC penalty
end if
end for Estimate (bmin: bmax) based on network fo and logical constraints he from training data.
Given (W(k)) B(8)) at the k-th iteration, the update of PPA can be computed by
((++1) (M - (A 1
((oon Y) + xw + ( + t (k-W))
t
E
(k++)) = (1 - -
(X); Y)T e B(K)
(4)
where y > is the step size of PPA, E is an all-ones matrix, and M = (foce) Y (for) (X); Y). Note that the computation of matrix inverse required, but not an issue because M positive semidefinite, and so is the involved matrix, which allows the use of Cholesky decomposition to compute the inverse. Moreover, exploiting the low rank and the sparsity of M can significantly enhance the efficiency of the computation.
Neural network training. By adding the DC penalty, the constraint (i.e., symbol grounding) in
arg min W ():y) bl al|z faw (x)ll2 t2(e T))
We can also compute the closed-form solution, i.e..
= bw + (a - (X) 12 (WT Tw +al)
(5)
Similarly, the low-rank and sparsity properties of W W ensure an efficient computation of matrix inverse. Finally, the parameter 0 of network is updated by stochastic gradient descent,
g (b)) Vo (x:) Z foum (x:)).
(6)
The overall algorithm is summarized in Algorithm I which mainly involves three iterative steps: (1) update the logical constraints by combining the network prediction and observed output; (2) correct the symbol grounding by revising the prediction to satisfy logical constraints; (3) update the neural network by back- propparppggginnggg the corrected symbol grounding with observed input.
3.2 Theoretical Analysis
Theorem 1. With an increasing (or decreasing) o. the constraint learning and network training
performed by Algorithm converge the stationary point of (2) and 33. respectively. Specifically, satisfies
Ell V O( VK+I and E V
V
Remarks. The proof and additional results can be found in Appendix B In summary, Theorem T confirms the convergence of our neuro-symbolic learning framework and illustrates its theoretical

---

complexity. Furthermore, note that an iecrasse (or decrease) in a indicates preference for correcting the symbol grounding over network prediction (or logical constraint learning). In practice, we can directly set small (or large) enough instead.
Next, we analyze the setting of centre points ( in the trust region penalty as follows.
Theorem 2. Let ( E [0, 1] and w² [0, 11th be two initial points sampled from the uniform distribution. For given t 2 0, the probability that the corresponding logical constraints Φ1 and Φ2 converge to the same (binary) stationary point &f satisfies
1 ([Vg(u)).(1 - 2u.) + 1), 1), 21
Pr(mi =., 12 Φ)
II min
Remarks. The proof is in Appendix C In a nutshell, Theorem shows that the probability of w and W2 degenerating to the same logical constraint can be very small provided suitably chosen À and t. Note that and play different roles. As shown by Proposition _ the coefficient in DC penalty ensures the logical constraint learning can successfully converge to sensible result. The coefficient trust region penalty enlarges the divergence of convergence conditions between two distinet logical constraints, thereby preventing the degeneracy effectively.
4 Experiments
We carry out experiments on four tasks, viz.,, chained XOR, Nonogram, visual Sudoku solving, and self-driving path planning. We use Z3 SMT (MaxSAT) solver [Moura and Bjørner [2008] for symbolic reasoning. Other implementation details can be found in Appendix E The experimental results of chained XOR and Nonogram tasks are detailed in Appendix | code is available at httttps://githuu hom/Lizn- 1-z2-210 -ain--zn// Neey/Neyy-Be Prooy-Prorraaaee Programming
due to the space limit. The
4.1 Visual Sudoku Solving
Datasets. We consider two 9 x 9 visual SudoKu solving datasets, i.c., the SATNet dataset (Wang et al. 2019 Topan et al. 2021 and the RRN dataset Yang et al. 2023), where the latter is more challenging (17 34 versus 31 42 given digits in each puzzle). Both datasets contain 9K/1K training/test examples, and their images are all sampled from the MNIST dataset. We typically involve two additional transfer tasks, i.e., training the neuro- ceuro-yymbolic system on SATNet dataset (resp. RRN dataset), and then evaluating the system on RRN dataset (resp. SATNet dataset).
Baselines. We compare our method with four state-of-the-art methods, i.e., RRN [Palm et al. 2018 SATNet (Wang et al,, 2019]. SATNet* (Topan al. [021], and LIR32H4 (Yang et al. [0033] RRN is modified to match visual SudoKu as done by Yang et al. [002]]. SATNet* is an improved version of SATNet that addresses the symbol grounding problem by introducing an additional pre-clustering step. As part of our ablation study, we introduce two variants of our method (NTR and NDC) where NTR removes the trust region penalty (i.e., setting > = 0), and NDC removes the DC penalty (i.e., fixing f1 tu 0) and directly binarizes (W, b) as the finally learned logical constraints.
Results. We report the accuracy results (i.e., the percentage of correctly recognized boards, correctly solved boards, and both) in Table 1 5 A more detailed version of our experimental results is given in Appendix]] [F] The results show that our method significantly outperforms the existing methods in all cases, and both trust region penalty and DC penalty are critical design choices. The solving accuracy is slightly higher than the perception accuracy, as the MaxSAT solver may still solve the problem correctly even when the perception result is wrong. Notably, our method precisely Icarns logical reasoning component that (1) achieves full accuracy when the neural perception is correct; (2) ensures robust results on transfer tasks, in comparison to the highly sensitive existing methods.
all logical constraints resulting
*The SATNet dataset is originally created by Wang et al. 2019) However, Topan et al. 2021 point out that the original dataset has the label leakage problem, which was fixed by removing the labels of given digits. 'ee successfully reproduce the baseline methods, achieving consistent results with Yang et al. 2023 "We need 324 (= 9 x x 4: each row/column/block should fill 1- 9, and each cell should be in truth cardinality constraints for the Sudoku task, whose rank is 249. After removing redundant constraints, our method learns exact 324 logical constraints that one-to-one corresponding the ground-truth.
9) ground-
7

---

Table Accuracy results (%) of visual Sudoku task. Our method performs the best.
SATNet dataset
RRN dataset
SATNet + RRN
Method
Percep.
Solving
Total
Percep.
Solving
Total
Percep.
Solving
Total
RRN
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
SATNet
0.0
0.0
0.0
0.0
0,0
0.0
0.0
0.0
0.0
SATNer*
72.7
75.9
67.3
75.7
0.1
0.1
80.8
1.4
1.4
LIR32H4
94.1
91.0
90.5
87.7
65.8
65.7
84.8
21.3
21.3
NTR
87.4
0.0
0.0
91.4
3,9
3,9
90.2
0.0
0.0
NDC
79.9
0.0
0.0
88.0
0.0
0.0
86.1
0.0
0.0
Ours
95.5
95.9
95.5
93.1
94.4
93.1
93.9
95.2
93.9
20
Acturery
2-6
25C
Figure 2: Training curves accuracy (left) and rank (right). Our method significantly boosts the efficiency of symbol grounding, and accurately converges to ground-trute constraints.
Furthermore, we plot some training curves in Figure 2 The left two figures depict the training curves of neural perception accuracy on the SATNet dataset and RRN dataset, which demonstrate the extremely higher efficiency of our method in symbol grounding compared with the best competitor LIR32H4. We also compute the rank of matrix W evaluate the degeneracy of logical constraint learning. The results are presented in the right two figures, illustrating that logical constraints learned by our method are complete and precise. In contrast, the ablation methods either fail converge to the correct logical constraints or result in degenerate outcome.
4.2 Self-driving Path Planning
Motivation. Self-driving systems are fundamentally neuro-symbolic, where the primary functions delineated into components: object detection empowered by neural perception and path planning driven by symbolic reasoning. Neuro-symbolic learning has great potential in self-driving, e.g., for learning from demonstrations [Schaal] 1996] and to foster
human-friendly driving
patterns [Sun et al. 2021 Huang et al. 2021].
Datasets. We simulate the self-driving path planning task based on two datasets, i.c., Kitti [Geiger et al. 2013) and nuScenes [Caesar et al., 2020). Rather than provide the label of object detection, only planning paths supervision. To compute planning paths, we construct obstacle maps with 10 x 10 grids, and apply the A" algorithm with fixed start points and random end points. Note that Kitti and nuScenes contain 6160/500 and 7063/600 training/test examples, respectively, where nuScenes more difficult (7.4 versus 4.6 obstacles per image on average).
Baselines. We include the best competitor L1R32H4 Yang et al. 2023 in the previous experiment as comparison. Alongside this, we also build an end-to-end ResNet model (denoted by ResNet) (He et al. 2016) and end-to-end recurrent transformer model (denoted by RTNet) [Hao et al. 2019]. These models take the scene image, as well as the start point and the end point, as the input, and directly output the predicted path. Finally, as reference, train ResNet model with direct supervision (denoted by SUP) by using labels of object detection, and the logical reasoning is also done by the A' algorithm.
Results. We include the F, score of predicted path grids, the collision rate of the planning path, and the distance enror between the shortest path and the planning path (only computed for safe paths) in T The results show that our method achieves the best performance on both datasets, compared with the alternatives. Particularly, the existing offteoof-the-at art method LIR32H4 fails on this task.

---

Table Results of self-driving path planning task. Our method performs the best.
Kitti dataset
nuScenes
Method
Fj score 1
Coll. rate
Dist. Err. +
Fj score f
Coll. Rate &
Dist. Err. +
ResNet
68.5%
54.0%
2.91
51.8%
68.1 1%
3.60
RTNet
77.3%
36.8% %
2.89
55.9%
63.8%
2.94
LIR32H4
11.9%
100.0%
NA.
12.0%
91.5%
100.0
Ours
80.2% %
32.8%
2.84
58.8% %
57.8% %
2.81
SUP
84.9%
28.3%
2.75
74.6%
52.9%
2.90
resulting in high collision rate. Our method is nearly comparable to the supervised reference model SUP on the Kitti dataset. On the nuScenes dataset, our method even produces slightly less distance error of safe paths than the SUP method.
Related Work
Neuro-symbolic learning. Neuro-symbolic learning has received great attention recently. For instance, Dai et al. [2019] and Corapi et al. (2010) suggest bridging neural perception and logical reasoning via an abductive approach, where a logic program is abstracted from a given knowledge base. To reduce reliance knowledge bases, Ciravegna et al. [2020] and Dong et al. [2019) directly represent and learn constraints using neural networks. However, the learned constraints are still uninterpretable. To improve interpretability, WWng et al. (019 introduce SATNet, a method that relaxes the MaxSAT problem with semidefinite programming and incorporates it as layer into neural networks. SATNet is further followed up by several works [Topan et al. 2021 Lim al. 2022 Yang et al. 2023]. However, how to explicitly extract and use the learned constrains is still unclear for these works. In contrast the existing neuro-symbolic learning methods, method can synthesize explicit logical constraints supporting exact reasoning by off-the-shelf reasoning engines.
Constraint learning. Our work is also related to constraint learning, which can be traced back to Valiant's ' algorithm [Valiant] [984] and, more generally, inductive logic programming [Muggleton and De Raedi 1994 Bratko and Muggleton 1995 Yang et al. 2017 Evans and Grefenstette] 20188 2018). However, Cropper and Dumančid 2022] highlight that inductive logic programming is limited when learning from raw data, such as images and speech, as opposed to perfect symbolic data. To this end, our method goes a step further by properly tackling the symbol grounding problem.
Boolean quadratic programming and its relaxation. Many constraint learning and logical rea- soning tasks, e.g., learning BeeuooBooleann function [Marichal and Mathonet (010), MaxSAT learning [Wang et al., 2019] and solving [Gomes et al. [006],, and SAT solving [Lipp and Boyd 2016), can be formulated as Boolean quadratic programming (i.e., quadratic programming with binary variables) [Hammer and Rubin 1970]. However, commonly used techniques, such branch and bound [Buchheim et al. 2012] and cutting plane (Kelley 1960), cannot be applied neuro-symbole learning tasks. In literature, semidefinite relaxation (SDR) [ (d'Aseemontt and Boyd 2003 Gomes
ct al. 2006 Wang and Kolter 2019 and difference-of convex (DC) programming Tao and Hoai An
1997 7 Yuille and Rangarajan 2003 Lipp and Boyd 2016 Hoai An and Tao 2018 are typical
methods to relax Boolean constraints. Although SDR is generally more efficient, the tightness and recovering binary results from relaxation still open problem [Burer and Ye 2020 Wang and
Kiling-Karzan 2022), compromising the exactness of logical reasoning. In this work, we choose DC programming and translate DC constraints to penalty with gradually increasing weight, as to ensure that the Boolean constraints can be finally guaranteed.
6 Limitations
In this section, we discuss the limitations of our framework and outline some potential solutions. Expressiveness. The theoretical capability of cardinality constraints to represent any propositional logic formula does not necessarily imply the practical ability to learn any such formula in frame-

---

work; this remains a challenge. Fundamentally, logical constraint learning is an inductive method, and thus different learning methods would have different inductive biases. Cardinality constraint-basee learning is more suitable for tasks where the logical constraints can be straightforwardy translated into the cardinality form. typical example of such a task is Sudoku, where the target CNF formula consists of at least 8,829 clauses [Lynce and Ouaknine 2006]. while the total number of target cardinality constraints stands at mere 324.
Technically, our logical constraint learning prefers equality constraints (e.g., I + y = 2), which actually induce logical conjunction (e.g., x A = T) and may ignore potential logical disjunction which is represented by inequality constraints (e.g., x V overcome this issue, a practical trick is introduce some auxiliary variables. which commonly used in linear programming (Fang and Puthenpura [993]. Consider the disjunction æ V = T; here, the auxiliary variables 21; 22 help form two equalities, namely, x + y + 21 2 for (ar, y) = (T, T) and x + + 22 = 1 for (z, y) (T, F) or (Ir, y) (F, T).. One can refer to the Chain-XOR task (cf. Section F. p for a concrete application of auxiliary variables.
' is expressed by z + y 2 1). To
Reasoning efficiency. The reasoning efficiency, particularly that of SMT solvers, during the inference phase can be primary bottleneck our framework. For instance, in the self-driving path planning task, when we scale the map size up to 20 x 20 grid involving 800 Boolean variables (400 variables for grid obstacles and 400 for path designation), the Z3 MaxSAT solver takes more than two hours for some inputs.
To boost reasoning efficiency, there are several practical methods that could be applied. One straightforward method is to use an integer linear program (ILP) solver (e.g.. Gurobi) as an alternative to the Z3 MaxSAT solver. In addition, some learning-basse methods (e.g.. (e.g., Baluuooicc et al. 2018)
may enhance SMT solvers in our framework. Nonetheless, we do not expect that merely using more efficient solver can resolve the problem. The improve the scalability, more promising way to combine System I and System 2 also in the inference stage (e.g.. Cornelio et al. (2023). ). Generally speaking, in the inference stage, neural perception should first deliver partial solution, which is then completed by the reasoning engine. Such a paradigm ensures fast reasoning via neural perception, drastically reducing the logical variables that need be solved by the exact reasoning engine. thereby also improving its efficiency.
7
Conclusion
This paper presents a neuro-symbolic learning approach that conducts neural network training and logical constraint synthesis simultancously, fueled by symbol grounding. The gap between neural networks and symbol logic is suitably bridged by cardinality constraint-bade bassdd learning and difference- of-convex programming. Moreover, introduce the trust region method to effectively prevent the degeneracy of logical constraint learning. Both theoretical analysis and empirical evaluations have confirmed the effectiveness of the proposed approach. Future work could explore constraint learning using large language models to trim the search space of the involved logical variables, and augment reasoning efficiency by further combining logical reasoning with neural perception.
Acknowledgment
We are thankful to the anonymous reviewers for their helpful comments. This work is supported by the National Natural Science Foundation of China (Grants #62025202, #62172199). T. Chen is also partially supported by Birkbeck BEI School Project (EFFECT) and an overseas grant of the State Key Laboratory of Novel Software Technology under Grant #KFKT2022A03. Yuan Yao (y yao@nju. edu. cn) and Xiaoxing Ma (xxmânju. edu, en) are the corresponding authors.
10

---

References
Daniel Kahneman. Thinking, fast and slow. macmillan, 2011.
Grady Booch, Francesco Fabiano, Lior Horesh, Kiran Kate, Jonathan Lenchner, Nick Linck, Andreas
Loreggia, Keerthiram Murgesan, Nicholas Mattei, Francesca Rossi, et al. Thinking fast and slow in ai. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 35, pages 15042-15046, 2021.
Bengio Yoshua and Marcus Gary, Ai debate: The best way forward for ai, 2020. com/ aidebate/
URL https
Yann LeCun. A path towards autonomous machine intelligence version 0.9. 2, 2022-06-27. Open Review, 62, 2022.
Po- Wei Wang, Priya Donti, Bryan Wilder, and Zico Kolter. Satnet: Bridging deep learning and logical reasoning using differentiable satisfiability solver. In International Conference on Machine Learning, pages 6545-6554 PMLR, 2019.
Zhun Yang, Adam Ishay, and Joohyung Lee. Learning to solve constraint satisfaction problems with recurrent transformer. In The Eleventh International Conference on Learming Representations, 2023.
Sever Topan, David Rolnick, and Xujie Si. Techniques for symbol grounding with satnet. Advances in Neural Information Processing Systems, 34:20733-20744, 2021.
Zenan Li, Yuan Yao, Taolue Chen, Jingwei Xu, Chun Cao, Xiaoxing Ma, and Lü Jian. Softened symbol grounding for neuro-symbolic systems. In The Eleventh International Conference Learning Representations, 2023.
Angelika Kimmig, Stephen Bach, Matthias Broecheler, Bert Huang, and Lise Getoor. A short introduction to probabilistic soft logic. In Proceedings of the NIPS workshop on probabilistic programming: foundations and applications, pages 1-4, 2012.
Jingyi Xu, Zilu Zhang, Tal Friedman, Yitao Liang, and Guy Broeck. semantic loss function for deep learning with symbolic knowledge. In International conference machine learning, pages 5502-5511. PMLR, 2018.
Niklas Eén and Niklas Sörensson. Translating pscudo-boolean constraints into sat. Journal Satisfiability, Boolean Modeling and Computation, 2(1-4):1-26, 2006.
Olivier Bailleux and Yacine Boufkhad. Efficient enf encoding of boolean cardinality constraints. In Principles and Practice of Constraint Programming- CP 2003: 9th International Conference, CP 2003, Kinsale, Ireland, September 19-Octobbrrs 3, 2003. Proceedings 9, pages 108-122. Springer, 2003.
Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. A translation of pseudo-boolean boolean constraints to sat. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):191-22 2006.
Stephen Boyd, Stephen P Boyd, and Lieven Vandenberghe. Convex optimization. Cambridge university press, 2004.
Andrew R Conn, Nicholas IM Gould, and Philippe L. Toint. Trust region methods. SIAM, 2000.
Tommi Syrjänen. Logic programs and cardinality constraints: Theory and practice. PhD thesis, PhD
thesis, Helsinki University of Technology, 2009.
Tommi Syrjänen. Cardinality constraint programs. In Logics in Artificial Intelligence: 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27-30, 2004. Proceedings 9, pages 187-199. Springer, 2004.
Samuel Fiorini, Tony Huynh, and Stefan Weltge. Strengthening convex relaxations of 0/1-sets using boolean formulas. Mathematical programming, 190:467-482, 2021.

---

Robin Manhaeve, Sebastijan Dumancic, Angelika Kimmig, Thomas Demeester, and Luc De Raedt. Deepproblog: Neural probabilistic logic programming. advances in neural information processing systems, 31, 2018.
Qing Li, Siyuan Huang, Yining Hong, Yixin Chen, Ying Nian Wu, and Song Song-Chun Zhu. Closed loop neural-symbolic learning via integrating neural perception, grammar parsing, and symbolic reasoning. In International Conference on Machine Learning, pages 5884-5894, PMLR, 2020.
Lieven Vandenberghe and Stephen Boyd. Convex optimization (Tutorial), volume 1. Cambridge university press Cambridge, 2004.
Charles R Henderson. Best linear unbiased estimation and prediction under a selection model. Biometrics, pages 423 233-447,1 1975.
Åke Björek. Least squares methods. Handbook of numerical analysis, 1:465-652, 1990.
Trevor Hastie, Robert Tibshirani, Jerome H Friedman, and Jerome H Friedman. The elements of statistical learning: data mining, inference, and prediction, volume 2. Springer, 2009.
Suriya Gunasekar, Blake E Woodworth, Srinadh Bhojanapalli, Behnam Neyshabur, and Nati Srebro. Implicit regularization in matrix factorization. Advances in Neural Information Processing Systems, 30, 2017.
Samuel Smith, Benoit Dherin, David GT Barrett, and Soham De. On the origin of implicit regularization in stochastic gradient descent. arXiv preprint arXiv:2101.12176, 2021.
Alnur Ali, Edgar Dobriban, and Ryan Tibshirani. The implicit regularization of stochastic gradient flow for least squares. In International conference machine learning, pages 233-244. PMLR, 2020.
Emile van Krieken, Thiviyan Thanapalasingam, Jakub M Tomezak, Frank van Harmelen, and Annette ten Teije. A-nesi: A scalable approximate method for probabilistic neurosymbolic inference. arXiv preprint 12X1v:2212.12393, 2022.
Pham Dinh Tao and Le Thi Hoai An. Convex analysis approach to de programming: theory, algorithms and applications. Acta mathematica vietnamica, 22(():289-33) -359993555110 1997.
Alan Yuille and Anand Rangarajan. The concave-convex procedure. Neural computation, 15(4): 915-936, 2003.
Thomas Lipp and Stephen Boyd. Variations and extension of the convex-coneave procedure. Opti- mization and Engineering, 17:263-287, 2016.
Le Thi Hoai An and Pham Dinh Tao. De programming and dea: thirty years of developments. Mathematical Programming. 169(1):5-68, 2018.
Dimitri Bertsekas. Convex optimization algorithmss. Athena Scientific, 2015.
Pierre Hansen, Brigitte Jaumard, MichèLe Ruiz, and Junjie Xiong. Global minimization of indefinite quadratic functions subject to box constraints. Naval Research Logistics (NRL), 40(3):373-39. 1993.
Hoai An Le Thi and Pham Ding Tao. A continuous approch for globally solving linearly constrained quadratic. Optimization, 50(1-2):93-120, 2001.
Meisam Razaviyayn. Successive convex approximation: Analysis and applications. PhD thesis,
University of Minnesota, 2014.
Amir Beck and Mare Teboulle, Global optimality conditions for quadratic optimization problems with binary constraints. SIAM journal on optimization, (1 11(8):179-188, 2000.
Yong Xia. New optimality conditions for quadratic optimization problems with binary constraints. Optimization letters, 3:253-263, 2009.
12

---

R Tyrrell Rockafellar. Monotone operators and the proximal point algorithm. SIAM journal on control and optimization, 14(5):877-898, 1976.
Neal Parikh, Stephen Boyd, et al. Proximal algorithms. Foundations and trends@ in Optimization, (3):127-239, 2014.
Tyrrell Rockafellar. Advances in convergence and scope of the proximal point algorithm. J. Nonlinear and Convex Analysis, 22:2347-2375, 2021.
Chiyuan Zhang, Samy Bengio, Moritz Hardt, Benjamin Recht, and Oriol Vinyals. Understanding deep learning (still) requires rethinking generalization. Communications of the ACM, 64(3):107-115, 2021.
Leonardo de Moura and Nikolaj Björner. 73: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008.
Rasmus Palm, Ulrich Paquet, and Ole Winther, Recurrent relational networks. Advances in neural information processing systems, 31, 2018.
Stefan Schaal. Learning from demonstration. Advances in neural information processing systems, 1996.
Jiankai Sun, Hao Sun, Tian Han, and Bolei Zhou, Neuro-symbolic program search for autonomous driving decision module design. In Conference Robot Learning, pages 21-30. PMLR, 2021.
Junning Huang, Sirui Xie, Jiankai Sun, Qiurui Ma, Chunxiao Liu, Dahua Lin, and Bolei Zhou. Learning decision module by imitating driver's control behaviors. In Conference Robot Learning, pages 1-10. PMLR, 2021.
Andreas Geiger, Philip Lenz, Christoph Stiller, and Raquel Urtasun. Vision meets robotics: The kitti dataset. The International Journal of Robotics Research, 12211111311 2013.
Holger Caesar, Varun Bankiti, Alex H Lang, Sourabh Vora, Venice Erin Liong, Qiang Xu, Anush Krishnan, Yu Pan, Giancarlo Baldan, and Oscar Beijbom. nuscenes: A multimodal dataset for autonomous driving. Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, pages 11621-1163) 2020.
Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Deep residual learning for image recognition. In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 770-778, 2016.
Jie Hao, Xing Wang, Baosong Yang, Longyue Wang, Jinfeng Zhang, and Zhaopeng Tu. Modeling recurrence for transformer. arXiv preprint urXiv:1904.03092 2019.
Wang-Zhou Dai, Qiuling Xu, Yang Yu, and Zhi-Hua Zhou. Bridging machine learning and logical reasoning by abductive learning. Advances in Neural Information Processing Systems, 32, 2019.
Domenico Corapi, Alessandra Russo, and Emil Lupu. Inductive logic programming as abductive search. In Technical communications of the 26th international conference on logic programming. fuer Informatik, 2010.
Schloss Dagstubl-Lecibniz-Zeennn
Gabriele Ciravegna, Francesco Giannini, Stefano Melacci, Marco Maggini, and Marco Gori. A constraint- based approach to learning and explanation. Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pages 3658-3665, 2020.
Honghua Dong, Jiayuan Mao, Tian Lin, Chong Wang, Lihong Li, and Denny Zhou. Neural logic machines. In International Conference on Learning Representations, 2019."
Sangho Lim, Eun-Gyeol Oh, and Hongseok Yang. Learning symmetric rules with satnet. In The 36th Conference on Neural Information Processing Systems (NeurIPS 2022). Neural information processing systems foundation, 2022.
Leslie G Valiant. A theory of the learnable. Communications of the ACM, 27411: 1984.
13

---

Stephen Muggleton and Luc De Raedt. Inductive logic programming: Theory and methods. The Journal of Logic Programming. 19:629-677 679, 1994.
Ivan Bratko and Stephen Muggleton. Applications inductive logic programming. Communications of the ACM, 38(1 1))65-770 1995.
Fan Yang. Zhilin Yang, and William W Cohen. Differentiable learning of logical rules for knowledge base reasoning. Advances in neural information processing systems, 30, 2017.
Richard Evans and Edward Grefenstette. Learning explanatory rules from noisy data. Journal of
Artificial Intelligence Research, 61:1-64, 2018.
Andrew Cropper and Sebastijan Dumančić. Inductive logic programming at 30: a new introduction.
Journal of Artificial Intelligence Research, 74:765- 850, 2022.
Jean-Luc Marichal and Pierre Mathonet. Symmetric approximations of pseudo-boolean functions. arXiv preprint arXiv: 1004.2200.200 2593, 2010.
Carla P Gomes, Willem-Jan Van Hoeve, and Lucian Leahu. The power of semidefinite programming relaxations for max-sat. In Integration of Al and OR Techniques in Constraint Programming for Combinatorial Optimization Problems: Third International Conference, CPAIOR 2006, Cork, Ireland, May 31-June 2006. Proceedings pages 104-118. Springer, 2006.
Peter L Hammer and Abraham A Rubin. Some remarks on quadratic programming with 0-1 variables. Revue française d' l'informatique et de recherche opérationnelle. Série verte, 4(V3):67-7, 1970.
Christoph Buchheim, Alberto Caprara, and Andrea Lodi. An effective branch-and-bound algorithm for convex quadratic integer programming. Mathematical programming. 135:369-395, 2012.
James E Kelley, Jr. The cutting-plane method for solving convex programs. Journal of the society for Industrial and Applied Mathematics, 8(4):703-712, 1960.
Alexandre d' Aspremont and Stephen Boyd. Relaxations and randomized methods for nonconvex qeqps. EE392o Class Notes, Stanford University, 1:1-16, 2003.
Po-Wei Wang and J Zico Kolter. Low-rank semidefinite programming for the max2sat problem. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 33, pages 1641-1649, 2019.
Samuel Burer and Yinyu Ye. Exact semidefinite formulations for class (random and non-random) nonconvex quadratic programs. Mathematical Programming, 181(1):1-17, 2020.
Alex L. Wang and Fatma KilingKarzan, On the tightness of sdp relaxations of qeaps. Mathematical Programming, 193(1)333-73, 2022.
Inés Lynce and Joël Ouaknine. Sudoku as a sat problem. In AI&M, 2006.
Shu-Cherng Fang and Sarat Puthenpura. Linear optimization and extensions: theory and algorithms. Prentice-Hall, Inc., 1993.
Mislav Balunovic, Pavol Bielik, and Martin Vechev, Learning solve smt formulas. Advances in Neural Information Processing Systems, 31, 2018.
Cristina Cornelio, Jan Stuehmer, Shell Xu Hu, and Timothy Hospedales. Learning where and when to reason in neuro-symbolic inference. The Eleventh International Conference on Learning Representations, 2023.
Léon Bottou, Frank E Curtis, and Jorge Nocedal. Optimization methods for large-scale machine learning. SIAM review, 60(2):223 311, 2018.
Shai Shalev-Shwartz, Ohad Shamir, and Shaked Shammah. Failures of gradient-based deep learning. In International Conference on Machine Learning, pages 3067-3075. PMLR, 2017.
14

---

A Proofs of DC technique
Notations, We define (Q"Q+ TT), 8 (Q'qi 7q2). and denote the largest eigenvalues
and largest diagonal element of S by max and maxx respectively. Hence, the two problems can be equivalently rewritten as
min u Su 28Tu. (0.1)
(Pt)
min u IT)u (28 te) u.
A.1 Proof of Proposition
Proof. The results are primarily based on [ertsekas 2015 Proposition 1.3.4): the minima of a strictly concave function cannot be the relative interior the feasible set.
We first show that if to 2 o max- then the two problems are equivalent [Le Thi and Ding Tao 2001 Theorem 1]. Specifically, since S tI negative definite, problem (Pt) è) strictly concave. Therefore, the minima should be in the vertex set of the feasible domain, which is consistent with problem (P).
We further generalize this result to the case to 6max [Hansen al. 1993 Proposition 1]. In this case, considering the i-th component of u, its second-order derivative in problem (Pt) is 2(S - t). Similarly, the strict concavity of u, ensures a binary solution, indicating the equivalence of problems (P) and (P+).
A.2 Proof of Proposition 2
Proof. The Karush-Kuhn-Tuckee (KKT) conditions of the problem (P,) follows.
[2Su 2tu 2s + tel; - ax + Bg = 0;
u, E [0, 1]"; a 0, 3 2 0:
a, = 0, Bi(u: 1) = 0; i n.
where a and B are multiplier vector. For u E {0, 1}", the KKT condition is equivalent to
0; [2Su
2/u 28 (e] u.) 0, 3r 22Su 2tu 2s te) zu, S 0.
By using (1 22,,) E 1 1. we can further combine the above two inequalities, and obtain
2 Su. s) 2u,) + 1-220 0,
1,..., n.
On the other hand, if 2 s).(1
holds for each i 1,... ,.....,,... n. it is easy check that a 2 0 and B 2 O, which proves the first part of the proposition.
2u:) + -u.)
The proof of the second part direct result of Beck and Teboulle (2000] Theorem 2.4]. To be specific, achieves a global minimum of (P), then q(u) I q(u') for any u' E {0, Hence, we only flip the i-th value of u. i.c., considering u, and ui 1 u. and it holds that
T u Su 2s S (u') Su' -
= (u Su - 2s u) + 2[Su s),(1 2u;)) + Sei. Su
Rearranging the incquality, we obtain
2|Su s):(1 - 2u;) 2 S.. i= I,...,
which completes the proof.
B Proof of Theorem
Proof. Notations. We use || to denote the lg norm for vectors and Frobenius norm for matrices. We define
(... = /Ze, + Yu,- b122 al Y) (fo(X), Y)I Ao[w 20
For the loss functions of logic programming and network training, assume ( and (z( to be μe and ne smooth, respectively. For case of presentation, we define A for (X)w + Y b.
15

---

and let Cmax be the upper bound of || Furthermore, by using the Woodbury identity formula, we can compute
(Z"; Y²) arg
min (
iZ + Y bll2 + ail(z, Y) - -foo (X), Y)11 + A1/w0 w011 10
(Sen (X); Y) 3 3 (M="), where 8
1
a + |
Let p² = (a.3*), we have
p(Ø 0t for (X), -(0" 0h, Zt, Y = (1 ((ag3)) + -1-
= =2 |*)|\
Update of Φb We consider the single rule case (multiple rules can be directly decomposed), i.e., Φ (w, b) and .b; ; b). The update of & is conducted on the loss function
(w, b) " 0² So (X), Y) = II (X)w, + Yw,. b112 A/w w011.
The smallest and the largest eigenvalues of (Sox (X), Y) (Jo (X), Y) + AI are denoted by min and max, respectively.
The PPA method updates w by
w x+1 arrgimin min (w, b) + 7 m| w²11?
arg
which can be reduced to
w k+1
nh = - 8t
where
7 -
M (X), (fo (X), Y) AI
The (2/7)-strongly convexity of the proximal term implies the Dolyak-Lojasiewice. (PL) inequality, which derives that
p 0t, ztz x² p( 0t for (X), Y) - -
2 21 20 112 2 E (10 2 - 11
= =,0 b) 20² (1 -
-|) |
7
Plugging w k+1 w² = - * 8 into the inequality, we have
( 0h zt, Y 2 (w b) + 2 (8*) TMM))( - 2p (1- )1)1|
2 p( , + y +
-2p -
where
(z
x ,
arg min (2, Zww k+1 + Y w
- (Jex(X) (X) k+1 b112 -
= =(fo (X): Y) - g + * (W) where gh+
a + 1|
Note that (2 has the smallest eigenvalue 7² 2/(11 + moxx)) )2, and thus we have
* 0¹ k ydy 2 p(t 0h, + x 1 2) (1 + max
27
Vol2(w, \o]2( (1-0))cmmx
Cmax
Update of 0. The update of 0 is conducted on the loss function
(0) |z (x)
16

---

By using ne pe-smooth of et we obtain that
p h+ 0², " 2 Y $) p(
zh y 10-11
= ( E (0"))
2 (V ghtt= p MB 10k+1 0²11²² 2 n Vol
1
2
2
Letting Zk+1 arg minz (0 0c+1 2): we conclude
1
p 0², z y 2 c(
k+1 gct1 zkt1 Y y ) + (0
Convergent result. By combining the update of Φ and 0, we have o(0 0t zt Y p( gk+1 zk1 y
27
nll o + (1 + 70
| [ob2(0"))1 - -2p - )m)ca
Taking telescopic over k we obtain
p 00, z", Y s0 0* zk Y
2 V al (1+) +
2y (1 + max V ( 2p= pt cmaxx
Since (1 ph) S kpp(K + 1)?, we have
E|| V (0 5 (K 1)n) ((p(0", 0-, 20, YO) min sp) + 2xcmmax),
and
(1 + (0mxx) 2(K 2(K+1)
"0, ((v(0)) ,0,,'', z Y²)
min up) -em)=+n-))
+ 2x(mmax).
Stochastic version. We first introduce an additional assumption: the gradient estimate is unbiased and has bounded variance [Bottou et al., 2018 Sec. 4], i.e.
Ee Ee(Volt = (0t),
E Ve
= (o*
and
Ve V << This assumption derives the following inequalities hold for S = +1:
Ve ( < Go V
Be Vel |F < ç + (
Eell
M| < < + Cr v V (.
For the update of 0, we have
p( @h z y Ee(x(( gh+1 z++1 y , > n (0+))
n2P0 ç.
2
2
For the update of Φ, using the mm-smooth, and taking the total expectation:
p(0" 0t "².z*, x Eelp(0 k+1
Z + ; ++ (1- T
2 (V V
M ( (
H6 u E Eell eh V
2
Φ )12
(C + C V (
c + mmax
2(c* + mmin)
where we define et 1/7 for simplicity. Now, let y be sufficiently small (that is, satisfying (ch + 22 2 ua((c + m).x)) we obtain
plbb 0t, zt, y* - -E(pp( 0², t + )] + 2p (1 1
2 2( + )
(o 2( + +minn
17

---

Putting the updates of 0 and Φ together, we have
f 0h: Zt Y² Ee Ed 0u+1 Zh+1, y 21 (1)) 11
2 Volt 2 Miioss + 2(c + mmax)
1
| ( 2(c + mmin)
P
Now, setting v s Ko/oVKK and 7h S ki// VK 1 conclude
1
E vol 00
E - = 00
VK+1"
VK+
C Proof of Theorem 2
Proof. We consider the following problem.
(P&) min & { uS AI)u 2(s A "
For given t 2 0, the corresponding stationary points of (Pş) satisty
2[Su s);(1 - 2u;) + 2\(u; - E:) - -2u;) + / 2 0, = I,...,n.
Note that
U = 0: E: u
-
(u. - (1) =
For given u E {0, 1)", we denote 0: = 2(Su s);(1 -2u;). Then, the probability that (Pş) has the stationary point be computed
Pr(e: + 2>(u: - -E,)(1 (20:) + 0), Pr(u) = II E=1
where
Pr(2X(u; - EE) 2u,) 0: + min( (1 e.),).
2x
Hence, for given two different uj and u. (0) to the same result u satisfying
the probability that the corresponding rules can converge
Pr(u = u, u2 = u) S Pr(u)2 = min
21 (t - 1)).
D Trust Region Method
Figure illustrates the key concept of the trust region method. For simplicity, centre points wi w1(0) ..... .,(()) of the trust region are also set as the initial points of stochastic gradient de- scent. Stochastic gradient descent is implicitly biased to least norm solutions and finally converges to point (0, 1) by enforeing the Boolean constraints. The trust region penalty encourages the stochastic gradient descent to converge to different optimal solutions in different trust regions.
E Experiment Details
Computing configuration. We implemented our approach via the PyTorch DL framework. The experiments were conducted on GPU server with two Intel Xeon Gold 5118 CPU@2.30GIC 400GB RAM, and 9 GeForce RTX 2080 Ti GPUs. The server ran Ubuntu 16.04 with GNU/Linux kernel 4.4.0.
Hyperparameter tuning. Some hyperparameters are introduced in our framework. In Table we summarize the (hyper-)paramettrs, together with their corresponding initialization or update strategies. Most of these hyperparameters are quite stable and thus only need be fixed constant set by standard strategies. We only discuss the selection of m, and the setting of bmin d and b.
18

---

w2(0) W0(
w;(0)
(1.30
W; (0)
Wo (0)
(0.0)
(0.0)
Figure 3: Avoid degeneracy by trust region method. In logical constraint learning, the imposition of the Boolean constraints and the implicit bias of the stochastic gradient descent cause W1.... wi to converge to the same result (left figure), while the trust region constraints guarantee that they can sufficiently indicate different rules (right figure).
(I) To ensure the sufficiency of learned constraints, suggest initially setting large to estimate the actual number of logical constraints needed, and then adjusting it for more efficient training. We also observe that large does not ruins the performance of our method. For example, m = 2000 in visual SudoKu solving task, while only 324 constraints are learned. (2) For the bias term b, recommend b be tuned manually rather than set by PPA update, and one gradually increase b from to n 1 (n is the number of involved logical variables), and collect all logical constraints candidate constraints. For buin and mmax. due the prediction error, it is unreasonable to set bmin and bmax that ensure all examples to satisfy the logical constraint. An alternative method threshold (e.g. k%) on the training (or validation) set, and the constraint is only required to be satisfied by at least k% examples.
set
Table The list of
and their initialization or update strategies.
Param.
Description
Setting
0
Neural network parameters
Updated by stochastic gradient descent
W
Matrix of logical constraints
Updated by stochastic PPA
b
Bias term of logical constraints
Pre-set or Updated by stochastic PPA
uuin |max
Lower/Upper bound of logical constraints
Estimated by training set
m
Pre-set number of constraints
Adaptively tuned
a
Trade-off weight in symbol grounding
Fixed to 0.5
A
Weight of trust region penalty
Fixed to À = 0.1
t t\/t2
Weight of DC penalty
Increased per epoch
1)
Learning rate of network training
Adam schedule
7
Step size of constraint learning
Adaptively set (y = 0.001 by default)
Additional Experiment Results
F1
Chained XOR
The chained XOR, also known as the parity function, is a basic logical function, yet it has proven challenging for neural networks to learn it explicitly (Shalev-Shwartz et al. 2017 Wang et al. 2019] To be specific, given a sequence of length L, the parity function outputs 1 if there an odd number of I's in the sequence, and otherwise. The goal of the Chained XOR task is to learn this parity function with fixed L. Note that this task does not involve any perception task.
We compare our method with SATNet and L. LIR32H4. In this task, SATNet uses an implicit but strong background knowledge that the task can be decomposed into L single XOR tasks. Neither LIR32H4
19

---

130
F3 koh
100
Results (16
Results (56)
Results
Sequence Length
Sequence Length
Sequence Length
(a) SATNet
(b) LIR32H4
Ours
Figure 4: Results (%) of chained XOR task, including accuracy and Fi score (of class 0). The sequence length ranges from 20 200, showing that our method stably outperforms competitors.
nor our method uses such knowledge. For LIR32H4, adapt the embedding layer to this task and fix any other configuration. Regarding our method, we introduce
auxiliary variables
It is worth notin that these auxiliary variables essentially serve as a form of symbol grounding. Elaborately, the learned logical constraints by our method can be formulated as follows,
W | + + Wr..t. + 1r++12 + ... W2 1
where w, E B, = 1, 2L - x, E B, I....,L L and E B, I,..., L. The auxiliary variables 2,, = I..... .,. L have different truth assignments for different examples, indicting how the logical constraint satisfied by the given input. Now, combining the symbol grounding of auxiliary variables, we revise the optimization problem (T) of our framework as
min ((xy))=D W [x; z) b11 + A|| W - ( (W b)
s.t. arg mingez E(x,y>>DDll W x z, b1 W E (mx(w+))
b N
The symbol grounding solely guided by logical constraints, as neural perception not involved.
The experimental results are plotted in Figure The results show that LIR32H4 is unable to learn such a simple reasoning pattern, while SATNet often fails to converge even with sufficient iterations, leading to unstable results. Our method consistently delivers full accuracy across all settings, thereby demonstrating superior performance and enhanced scalability in comparison to existing state-of-the- art methods. To further exemplify the efficacy of our method, we formulate the learned constraints the task of 20. Eliminating redundant constraints and replacing the auxiliary variables with logical disjunctions, the final learned constraint can be expressed as
(x) + which shows that our method concludes with complete and precise logical constraints.
x + y 0) V (x1 + X + y 2) V V(x (x1+ .... + X20 + = 20),
F.2 Nonograms
Nonograms is logic puzzle with simple rules but challenging solutions. Given grid of squares, the task of nonograms to plot binary image, i.e., filling each grid in black or marking by X. The required numbers of black squares that row (resp. column) given beside (resp. above) each row (resp. column) of the grid. Figure SegureBlgiver gives a simple example.
In contrast to the supervised setting used in Yang et al. 2023), we evaluate our method on weakly supervised learning setting. Flaborately, instead of the fully solved board, only partial solutions (i.e., only one row or one column) are observed. Note that this supervision is enough to solve the nonograms, because the only logical rule to be learned is that the different black squares (in each row or column) should not be connected.
For our method, we do not introduce neural network in this task, and only aim learn the logical constraints. We carry out the experiments on x nonograms, with training data sizes ranging
"Noee that the number of auxiliary variables should not exceed the number of logical variables. If so, the logical constraints trivially converge any result.
20

---

X
X
X
Data Size
LIR32H4
Ours
X
X
1000
14.4
100.0
X
X
X
5000
62.0
100.0
9000
81.2
100.0
Empoy Nonogram
Solved Nonogram
Table 4: Accuracy (%) of the nonograms task.
Figure 5: An example of nonograms.
from 1,000 to 9,000. The results are given in Table showing the efficacy of our logical constraint learning. Compared to the L1R32H4 method, whose effectiveness highly depends the training data size, our method works well even with extremely limited data.
F,3 Visual SudoKu Solving
In the visual SudoKu task, it worth noting that the computation of z cannot be conducted by batch processing. This is because the index of y varies for each data point. For instance, in different SudoKu games, the cells to be filled are different, and thus the symbol z has to be computed in point-wise way. To solve this issue, introduce auxiliary y approximate the output symbol y:
(z. = arg min W yz: bl1² - (z) (fo(x):))11.
On the SATNet dataset, we use the recurrent transformer the perception model Yang et al. 2023 because we observe that the recurrent transformer can significantly improve the perception accuracy, and even outperforms the state-of-the-art of MNIST digit recognition model. However, find that its performance degrades on the more difficult dataset RRN, and thus we still use standard convolutional neural network model as the perception model for this dataset.
We include detailed results of board and cell accuracy in Table can observed that our method consistently superior the existing methods, and significantly outperforms the current state-of-the-an method L. L1222H4 on the RRN dataset (total board accuracy improvement exceeds 20%). Also note that the solving accuracy of our method always performs the best, illustrating the efficacy of logical constraint learning.
Next, we exchange the evaluation dataset, namely, using the RRN dataset to evaluate the model trained on the SATNet dataset, and vice versa. The results are presented Table The accurate logical constraints and exact logical reasoning engine guarantee the best performance of our method on transfer tasks. Notably, the performance of LIR32H4 drops significantly when transferring the model (trained SATNet dataset) to RNN dataset, our method remains unaffected by such shift.
F.4 Self-driving Path Planning
Inpat Scene
Neural network
Symbolic reasoning
Latent symbol
Output Path
Figure 6: A neuro-symbole system in self-driving tasks. The neural perception detects the obstacles from the image collected by the camera; the symbolic reasoning plans the driving path based on the obstacle map. The neuro-symbolic learning task is to build these two modules in an end-to-end way.
The goal of the self-driving path planning task to train the neural network for object detection and to learn the logical constraints for path planning in end-to-end way. As shown in Figure 6 we construct two maps and each contains x 10 grids (binary variables). The neural perception detects the obstacles from the image and locates it in the first map, which is essentially the symbol Next,
21

---

Table Detailed cell and board accuracy (%) of original visual Sudoku task.
SATNet dataset
RRN dataset
Method
Perception board acc.
Solving board acc.
Total board acc.
Perception board acc.
Solving board acc.
Total board acc.
RRN
0.0
0.0
0.0
0.0
0.0
0.0
SATNet
0.0
0.0
0.0
0.0
0.0
0.0
SAINet*
72.7
75.9
67.3
75.7
0.1
0.1
LIR32H4
94.1
91.0
90.5
87.7
65.8
65.7
NTR
87.4
0.0
0.0
91.4
3,9
3,9
NDC
79.9
0.0
0.0
88.0
0.0
0.01
Ours
95.5
95.9
95.5
93.1
94.4
93.1
Perception cell acc.
Solving cell acc.
Total cell acc.
Perception cell acc.
Solving cell acc.
Total
cell acc.
RRN
0.0
0.0
0.0
0.0
0.0
0.0
SATNet
0.0
0.0
0.0
0.0
0.0
0.0
SATNet*
99.1
98.6
98.8
75.7
59.7
72.0
LIR32H4
99.8
99.1
99.4
99.3
89.5
92.6
NTR
99.7
60.1
77.8
99.7
38.5
57.3
NDC
99.4
10.8
50.4
99.5
10.9
38.7
Ours
99.9
99.6
99.7
99.7
98.3
98.7
the logical reasoning computes the final path from the symbol and tags it on the second map the output y.
As detailed reference, select some results of path plamning generated by different methods and plot them in Figure 7 We find that some correct properties are learned by our method. For example, given the point Y34 in the path, we have the following connectivity:
(y34 8) + (y34 e) + Adj(y34) 2,
which means that the path point Y34 should connected by its adjacent points. In addition, some distinct constraints also learned, for example,
Y32 + 2,2 + 211
1.
In this constraint, Z11 and Zo1 are two noise points, and they always take the value of O. Therefore, it actually ensures that if Z32 an obstacle, then Y32 should not be selected as path point. However, is still unknown whether our neuro-symin sourolyymbolic framework derives all the results as expected, because some of the learned constraints are too complex to be understood.
(a) Input scene (with labels)
(b) ResNet method
(c) RT method
(d) Ours
Figure 7: Some results of neuro-symbolic learning methods in self-driving path planning task.
22

---

Table 6: Detailed cell and board accuracy (%) transfer visual Sudoku task.
SATNet RRN
RRN SATNet
Method
Perception board acc.
Solving board acc.
Total board acc.
Perception board acc.
Solving board acc.
Total board acc.
RRN
0.0
0.0
0.0
0.0
0.0
0.0
SATNet
0.0
0.0
0.0
0.0
0.0
0.0
SATNet*
80.8
1.4
1.4
0.0
0.0
0.0
L1R32H4
84.8
21.3
21.3
94.9
95.0
94.5
NTR
90.2
0.0
0.0
86.9
0.0
0.0
NDC
86.1
0.0
0.0
82.4
0.0
0.0
Ours
93.9
95.2
93.9
95.2
95.3
95.2
Perception cell acc.
Solving cell acc.
Total cell acc.
Perception cell acc.
Solving cell acc.
Total
cell acc.
RRN
0.0
0.0
0.0
0.0
0.0
0.0
SATNet
0.0
0.0
0.0
0.0
0.0
0.0
SATNet*
99.1
66.2
76.5
65.8
53.8
59.2
LIR32H4
99.3
89.5
92.6
99.7
99.6
99.7
NTR
99.6
37.1
56.3
99.6
62.4
79.0
NDC
99.4
11.0
38.7
99.5
11.3
50.7
Ours
99.8
98.4
98.8
99.8
99.7
99.7
23


Reviews:
[{"review_id": "yU3nGY8IDo", "reviewer": "Reviewer_X5tc", "summary": "The paper proposes a new neurosymbolic approach for learning symbolic representations and logical constraints on top of these simultaneously. The authors propose a new penalty term based on Difference of Convex (DC) programming in order to relax the optimzation problem. The performance of the proposed approach is demonstrated on the visual sudoku challenge and a path planning environment based on the Kitti and NuScene datasets. Overall, the method performs better than existing works and achieves results close to a fully supervised architecture in some cases.", "questions": "- What does the notation (z;y) mean exactly in w^T(z;y)? Is it some form of concatenation?\n- You mention that the solvers can find a solution even with incorrect perception. Why do you think this happens? Do you think that using more powerful solvers can actually be a problem for the perception side of things?", "limitations": "The paper does not discuss the limitations of the proposed methodology which is important in order to identify meaningful directions for future work.", "rating": 5, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "The paper takes a principled approach to the problem of learning symbolic representations and logic rules simultaneously. The proposed DC programming approach allows for the theoretical analysis as per Theorem 1 demonstrating that gradual increase of the weight of the DC penalty term results in the desired stationary point.\nAlso, the reported results demonstrate strong improvement over other neurosymbolic approaches in the two considered environments of the visual sudoku and path planning.   ", "weaknesses": "The performed experiments focus on 2 relatively simple and static environments. Moreover, one of the core motivations behind neurosymbolic approaches is the ability to learn faster and/or transfer knowledge to new environments, however none of these questions have been addressed by the conducted experiments. Overall, I think the paper would benefit from making the methodology section more concise and to the point and expanding more on the results.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "### **Response to Reviewer X5tc**\n\nThanks for the comments. \n\n**The challenge of two tasks:** The visual SudoKu solving task is a standard and commonly-evaluated task in existing neuro-symbolic learning methods. Particularly, only 17 out of 81 cells are initially filled in some of the SudoKu boards of the RRN dataset, and the difficulty of solving such a SudoKu can be well understood in the Appendix of  [1]. Furthermore, we try to explore some real applications of  neuro-symbolic learning via introducing the self-driving planning task. In this task, we extract two main modules (i.e., object localization and path planning) in self-driving systems, which is suitable for evaluating neuro-symbolic learning method (object localization is the neural part and path planning is the symbolic part).\n\nWe would also like to point out that, to the best of our knowledge, the genuine end-to-end learning of  neuro-symbolic systems has not been achieved before, even for simple (exemplar) tasks such as those used in the evaluation. This paper shows that it can be made feasible with a natural and disciplined approach, including a game theory framework connecting neural and symbolic learning, as well as more techical approaches such as trust-region penalty (to prevent degeneracy), and DC relaxation (to preserve logic exactness).\n\n**Knowledge transfer to new environments:** We agree with the reviewer on the core  motivations behind neuro-symbolic approaches. Actually, for knowledge transfer, we have conducted an experiment on transferring the learned rules from the SATNet dataset to the RRN dataset, and vice versa. Note that these two datasets vary significantly in terms the difficulty levels of Sudoku solving tasks (RRN dataset is more challenging; see Section 4.1). Our experimental results (the third-column in Table 1 and Table 6 in Appendix G.3) show that, when applying both model and learned rules from SATNet (RRN) data to RRN (SATNet) data, our method is consistently effective, while the performance of existing methods drops dramatically.\n\n**Notation $(\\mathbf{z};\\mathbf{y})$:** We represent the column concatenation of two vectors $\\mathbf{z} \\in \\mathbb{R}^m$ and $\\mathbf{y} \\in \\mathbb{R}^n$ by $(\\mathbf{z}; \\mathbf{y}) \\in \\mathbb{R}^{m+n}$. We will clarify it in the revision.\n\n**The MAXSAT solver can find a correct solution despite incorrect perception:** The MAXSAT solver returns the solution achieving the highest number of satisfied constraints. Therefore, even with perception errors causing the full set of  logical constraints unsatisfiable, MAXSAT solvers may still output the correct results by satisfying a subset of the logical constraints.\n\n**Limitation:** We discussed the limitations in Appendix A. In the revision, we will summarize the limatations into the main body of the paper.\n\n[1] Palm, R., Paquet, U., & Winther, O. (2018). Recurrent relational networks. Advances in neural information processing systems, 31.\n\n"}, {"review_id": "8JcAwpUDna", "reviewer": "Reviewer_w2hx", "summary": "The authors propose a fusion of neural network and symbolic domain via logical constraints to learn specific vision tasks in a weakly supervised way. They break it down to two optimization problems for neural and symbolic domains. The logical constraints are solved using  a deterministic solver and grounded softly to the neural component via a latent space $z$.", "questions": "* Why do you chose these specific tasks? Is it following some prior works? Please make it clear. This will help understand the scope of the work in terms of applicability to different domains.", "limitations": "* The authors don't have any limitations section. Please refer to weakness for recommendations on this.", "rating": 7, "confidence": 1, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "* The neuro-symbolic approach of solving tasks that require some planning is always an interesting direction.\n* The results on the two domains studied in the paper are quite strong, indicating that such fusion can indeed converge well ", "weaknesses": "* The paper needs more high level figures to help understand the exact logical constraints being enforced for both the domains. This will significantly improve the readability.\n* Please add some discussion about the limitations of using the specific cardinality-based logical constraints you chose in terms of where it might be applicable vs where it cannot.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "### **Response to Reviewer w2hx**\n\nThanks for the comments.  \n\n**The motivation of tasks:** The visual SudoKu solving task is a standard and commonly-evaluated task from existing neuro-symbolic learning methods. The self-driving planning task is proposed by ourselves. Specifically, we aim to introduce this more practical task for the neuro-symbolic learning community. We will further clarify this in Appendix G3 and G4.\n\n**Limitation:** We discussed the limitations in Appendix A. In the revision, we will summarize the limitations into the main body of the paper. \n"}, {"review_id": "gyeh2VGXSv", "reviewer": "Reviewer_MGh8", "summary": "This work provides a neural framework that combines network training, symbol grounding, and logical constraint synthesis. \nIt utilizes the cardinality constraints to express the logical constraint learning and a DC penalty for constraint relaxation.\nThe evaluation demonstrates that this method outperforms state-of-the-art models including both SATNET and L1R32H4 by a large margin. \n", "questions": "1. What is the limitation of using cardinality constraint? Is there a fundamental limitation other than the tricky usage where introducing auxiliary variables is required? \n2. How are the 324 cardinality constraints calculated? \n3. Suppose the number of the constraint is unknown for a new task, what should a user do? How will that impact the performance? \n4. How to interpret a boolean-based constraint to an average programmer? \n\nI am happy to raise my score if these questions are addressed. ", "limitations": "Suggestions included in the Question section. ", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "Originality: 4/5\nPros: This methodology introduces two novel important components, DC relaxation loss, and cardinality constraints, into the numerical learning framework. \nCons: One interesting component in this paper, mapping the learned numerical rules into the symbolic space is not quite clearly explained. By studying the related work section, I think the \"Softened Symbol Grounding for Neuro-symbolic Systems\"[1] seems quite related to the rule extraction part. I feel this work is probably not emphasized enough in the paper's related work section. \n\nQuality: 4/5 \nPro: The theory and properties come with all the proofs explained in the appendix, which is quite convincing. This work also reaches better than the SOTA performance for the two experiments.\nCons: The SATNET* uses Distilled LeNet as its underlying perceptual model, while you have used a recurrent transformer model. This seems an unfair comparison. \n\n\nClarity: 3/5\nPros: The math component is nicely defined and with well-explained definitions. \nCons:   It is hard to understand the process of extracting a constraint from its numerical form ($\\mathbf{w}$ and $\\mathbf{b}$). \n\nSignificance: 4/5 \nPros: This work improves from the existing work by learning constraints along with ground truth perception, which is an important task in neural symbolic learning.\nCons: The learned constraints are in boolean form and thus not high level enough to generalize across different task variants. \n\n[1] Li, Zenan, et al. \"Softened Symbol Grounding for Neuro-symbolic Systems.\" The Eleventh International Conference on Learning Representations. 2022.", "weaknesses": "See Strength. \n\nMinor comments: \n1. Line 91: There are two papers coming from different groups, whose first author's names are both Li. It seems that the two works come from the same person in the article. \n2. I would recommend putting the limitation section into the main paper. ", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "### **Response to Reviewer MGh8**\n\nThanks for the comments. Following are our responeses.\n\n**Limitation of cardinality constraint:** Essentially, cardinality constraints can represent any propositional logic formula, i.e., they have the same expressiveness with CNF (Conjunctive Normal Form) or DNF (Disjunctive Normal Form) of propositional logic. However,  when learning cardinality constraint, some biases do exist (e.g., bounding box $[b_{min}, b_{max}]$ should be tight) which may result in the incompleteness of the learned constraints.\n\n**The calculation of 324 cardinality constraints:** A logical constraint \"x_111 + x_121 + x_131 + x_141 + x_151 + x_161 + x_171 + x_181 + x_191 == 1\" means that there should be a \"1\" in the first row (where x_123 means the entry of 1st-row, 2st-column is 3). We have 9 such constraints for the first row, and we have 9 rows, resulting a total of $9\\times 9=81$ constraints for rows. We also have 81 constraitns for columns and blocks, respectively. There are also $9 \\times 9=81$ constraints requiring that each cell should be in $1-9$. Therefore, the total number of constraints is $81 \\times 4=324$. For our method, we initially set a large number, and then remove the redundant constraints, resulting exactly 324 contraints confirmed by manual checking.\n\n**How to determine the number of constraints:** One can directly set a sufficiently large $m$ (number of constraints), and we observe that a large $m$  does not ruin the effectiveness of our method. For example, we set $m = 2000$ in the visual SudoKu solving task, where only 324 constraints are required. Our method returns 324 unique constraints and the rest are redundant. A more efficient way is initially setting a large $m$ to estimate the actual number of logical constraints needed, and then adjusting it for more efficient training. We will include a brief discussion on the setting of $m$ in the revision (Appendix F).\n\n**Interpret a boolean-based constraint to an average programmer:** A reasonable method is to translate the Boolean-based constraints into a CNF formula, and we think it is more friendly for an average programmer to understand such a CNF formula. The tranlsation is studied for a long time and can be automatically conducted by off-the-shelf SMT solvers [1, 2]. \n\n**Relation to the paper “Softened symbol grounding…”:** We will highlight the relation in the revision as suggested.\n\n**Compare with SATNet using LeNet architecture:** We agree that it could be unfair to compare with SATNet* considering different architectures. As an ablation study, we use LeNet-5 model in our method, deriving the results of total board accuracy as follows. \n\n|                | SATNet dataset | RRN dataset |    SATNet $\\to$ RRN |     RRN $\\to$ SATNet |\n| ---------------- | ---------------: | ----------: | ---------------: | ---------------: |\n| SATNet*        |           67.3 |         0.1 |              1.4 |              0.0 |\n| Ours (LeNet-5) |           75.2 |        79.6 |             82.4 |             70.6 |\n\nWe also observe that our method successfully learned full logical constraints, but the accuracy of perception module degrades from 99.8% to about 99.1%, leading to the drop of overall accuracy.\n\n**Misleading citation in Line 91:** We will correct it in the revision.\n\n**Limitation section:** In the revision, we will summarize the limatations into the main body of the paper. \n\n[1] Sinz, C. (2005, October). Towards an optimal CNF encoding of boolean cardinality constraints. In International conference on principles and practice of constraint programming (pp. 827-831). Berlin, Heidelberg: Springer Berlin Heidelberg.\n\n[2] Eén, N., & Sörensson, N. (2006). Translating pseudo-boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4), 1-26.\n"}, {"review_id": "t3tMSFUS9E", "reviewer": "Reviewer_MqQr", "summary": "This paper takes inspiration from convex and bilevel optimization to derive a learning algorithm that simultaneously learns neural network perception and rules on the perceptions. The authors derive an efficient training algorithm involving multiple minimization steps.\n\nPost rebuttal: I thank the authors for addressing the concerns. I will keep my score, this is a good paper, and I am happy error bars are included in the rebuttal.", "questions": "- An SMT solver is mentioned multiple times of which in Figure 1. Is my understanding correct that it is only used during inference, not training?\n- Would the method also work by taking the cross entropy for the $\\ell_1$ loss?\n- Page 4, 131: Why is it allowed to rewrite the objective introducing alpha like that?\n- Proposition 1: Explain what $\\mathbf{e}$ is.\n- Page 5, 154: The linearization uses $(e-2u)^Tu$, but further down (line 172) it is $(e-w)^Tw$. Where did the 2 go to?\n- Same question for neural network training. Also, I think there's something wrong with the braces there. \n- To what values do you set $m$ (number of rules)?\n- Appendix, table 1: You mention that $\\alpha$ is fixed to 1, meaning the influence from the rules is ignored by symbol grounding. Why did you choose this setting? $\\alpha$ significantly complicates your mathematics. Setting it to 1 would simplify the equations significantly.", "limitations": "Inference of this method is very expensive, as highlighted in the limitations section. I'd have preferred this in the main paper, not in the appendix.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 4, "strengths": "The paper tackles the genuinely very hard problem of learning rules and perception simultaneously. The performance on, from what I can tell, quite challenging tasks is great. Ablations show multiple complex techniques help with performance. \nFurthermore, the paper has several proofs on convergence and optimality. \n\nThe method itself has many (original) interesting ideas, although there are many.", "weaknesses": "While the paper is decently written, there are a lot of technicalities to the method that makes understanding the high-level picture challenging. It relies on many optimization methods: Cardinality constraints, difference of convex programming, proximal point algorithms and trust regions, not to mention quite a few hyperparameters. Some equations fly in without a clear justification, and glancing at the appendix does not help me either. Furthermore, the paper introduces a hyperparameter alpha that significantly complicates the computation without actually using it.\n\nThe main goal of this paper is to yield logical constraints, but whether they are also interpretable is not evaluated. \n\nThe paper does not have error bars on experiments.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "### **Response to Reviewer MqQr**\n\nThanks for the comments.  \n\n**The role of SMT solvers in our framework:** Yes, SMT solvers are only used during inference.\n\n**Replace $\\ell_1$ loss by cross entropy:** Yes, we can directly change equation (6) to the gradient descent of cross entropy loss, and it should also work. This is not only implied by theory, but also observed by our preliminary experiments.  \n\n**The derivation of the equation in Line 131:** The original constraint in network training is $\\bar{\\mathbf{z}} = \\arg\\min\\nolimits_{\\mathbf{z} \\in \\mathcal{Z}}~ \\ell_2(h_{\\boldsymbol{\\boldsymbol{\\phi}}}(\\mathbf{z},\\mathbf{y}), 1) := \\\\|\\boldsymbol{W} (\\mathbf{z}; \\mathbf{y}) - \\boldsymbol{b}\\\\|^2$. \nHowever, this constraint is intractable due to the ill-conditioned $\\boldsymbol{W}$. Hence, we introduce the network prediction as a guidance, forming the final equation in Line 131. \n\n**Explain $\\boldsymbol{e}$:**  $\\boldsymbol{e}$ is an all-one vector, and we will clarify this in the revision.\n\n**The derivation in Line 154 and neural network training equation:** Thanks for pointing them out. They are typos (we also confirm that our submitted code is correct). We will carefully checked the paper again and correct them in the revision.\n\n**How to set $m$ (number of rules):** In our experiment, we directly set a large enough $m$ to  learn all possible logical constraints. For example, we set $m = 2000$ in the visual SudoKu solving task, where only 324 constraints are required. Our method returns 324 unique constraints and the rest are redundant ones. We will include it in the revision.\n\n**Hyperparameter $\\alpha$:** Sorry for the confusion due to the inconsistency of $\\alpha$ in the main text and the Appendix. In the main text, we use the following formulation for symbol grounding problem: \n\\begin{equation}\n\\bar{\\mathbf{z}} = \\arg\\min\\nolimits_{\\mathbf{z} \\in \\mathcal{Z}}~ (1-\\alpha) \\\\|\\boldsymbol{W} (\\mathbf{z}; \\mathbf{y}) - \\boldsymbol{b}\\\\|^2 + \\alpha \\\\|\\mathbf{z} - f_{\\boldsymbol{\\theta}}(\\mathbf{x})\\\\|^2. \n\\end{equation} \nIn appendix, we instead use \n\\begin{equation} \n\\bar{\\mathbf{z}} = \\arg\\min\\nolimits_{\\mathbf{z} \\in \\mathcal{Z}}~ \\\\|\\boldsymbol{W} (\\mathbf{z}; \\mathbf{y}) - \\boldsymbol{b}\\\\|^2 + \\alpha \\\\|\\mathbf{z} - f_{\\boldsymbol{\\theta}}(\\mathbf{x})\\\\|^2. \n\\end{equation} \n$\\alpha = 1$ is set for the latter, which is equivalent to $\\alpha = 0.5$ for the former (where the network prediction and constraints satisfaction are considered equally). We will correct them in the revision.\n\n**The interpretable logical constraints:** For visual SudoKu solving task, a logical constraint is in the form of \"x_111 + x_121 + x_131 + x_141 + x_151 + x_161 + x_171 + x_181 + x_191 == 1\", meaning that there should be a \"1\" in the first row (where x_123 means the entry of 1st-row, 2st-column is 3). We will add some learned logical constraints for both tasks in Appendix G4.  \n\n**Error bars on experiments:** We briefly provide some results of total board accuracy as reference, and will include the full version in the revision.\n\n|         |    SATNet dataset |       RRN dataset |  SATNet $\\to$ RRN |  RRN $\\to$ SATNet |\n| ------- | ----------------: | ----------------: | ----------------: | ----------------: |\n| SATNet* | 67.3 ($\\pm$ 2.36) |  0.1 ($\\pm$ 0.10) |  1.4 ($\\pm$ 0.14) |  0.0  ($\\pm$ 0.0) |\n| L1R32H4 | 90.5 ($\\pm$ 2.85) | 65.7 ($\\pm$ 6.97) | 21.3 ($\\pm$ 3.48) | 94.5 ($\\pm$ 1.65) |\n| Ours    | 95.6 ($\\pm$ 0.31) | 92.8 ($\\pm$ 0.73) | 93.9 ($\\pm$ 0.40) | 95.2 ($\\pm$ 0.91) |\n\n**Limitation section:** In the revision, we will summarize the limatations into the main body of the paper as suggested.\n"}]

Author rebuttal:
### **General response to reviewers**

We would like to thank all the reviewers for their kind and helpful feedback. 

We start by clarifying that we have indeed discussed the limitations of our approach which is included in Appendix A. We will summarize and include them in the main paper. 

We thank the reviewers for the suggestions on improving readability. We will give more intuitive explanations of the core ideas and the results in the revised paper, and move some technical details to the Appendix.


Meta-review: This paper tackles the important problem of learning logical constraints in neurosymbolic AI. The optimization method proposed appears to work well on standard benchmarks.
Decision: Accept (poster)