Injecting Logical Constraints into Neural Networks via Straight-Through
  Estimators
Injecting discrete logical constraints into neural network learning is one of
the main challenges in neuro-symbolic AI. We find that a
straight-through-estimator, a method introduced to train binary neural
networks, could effectively be applied to incorporate logical constraints into
neural network learning. More specifically, we design a systematic way to
represent discrete logical constraints as a loss function; minimizing this loss
using gradient descent via a straight-through-estimator updates the neural
network's weights in the direction that the binarized outputs satisfy the
logical constraints. The experimental results show that by leveraging GPUs and
batch training, this method scales significantly better than existing
neuro-symbolic methods that require heavy symbolic computation for computing
gradients. Also, we demonstrate that our method applies to different types of
neural networks, such as MLP, CNN, and GNN, making them learn with no or fewer
labeled data by learning directly from known constraints.
Zhun Yang, Joohyung Lee, Chiyoun Park
# Injecting Logical Constraints into Neural Networks

###### Abstract

Injecting discrete logical constraints into neural network learning is one of the main challenges in neuro-symbolic AI. We find that a straight-through-estimator, a method introduced to train binary neural networks, could effectively be applied to incorporate logical constraints into neural network learning. More specifically, we design a systematic way to represent discrete logical constraints as a loss function; minimizing this loss using gradient descent via a straight-through-estimator updates the neural network's weights in the direction that the binarized outputs satisfy the logical constraints. The experimental results show that by leveraging GPUs and batch training, this method scales significantly better than existing neuro-symbolic methods that require heavy symbolic computation for computing gradients. Also, we demonstrate that our method applies to different types of neural networks, such as MLP, CNN, and GNN, making them learn with no or fewer labeled data by learning directly from known constraints.

Machine Learning, Neural Networks, Neural Networks, Neural Networks, Neural Networks

## 1 Introduction

Neuro-symbolic AI (Besold et al., 2017; Mao et al., 2019; De Raedt et al., 2019; Garcez et al., 2019) aims to combine deep neural network learning and symbolic AI reasoning, which look intrinsically different from each other on the surface. It appears hard to incorporate discrete logical reasoning into the conventional gradient descent method that deals with continuous values. Some recent works in neuro-symbolic AI (Manhaeve et al., 2018; Yang et al., 2020; Pogancic et al., 2020; Tsamoura et al., 2021) associate continuous parameters in neural networks (NNs) with logic languages so that logical reasoning applied to NN outputs produces "semantic loss" (Xu et al., 2018). Minimizing such loss leads to updating NN parameters via backpropagation through logic layers. Like human learning that leverages known constraints, these methods have shown promising results that allow NNs to learn effectively with fewer data leveraging the semantic constraints. On the other hand, the symbolic computation performed during backpropagation is implemented by weighted model counting using circuits (Darwiche, 2011; Manhaeve et al., 2018; Tsamoura et al., 2021) or by calling symbolic solvers (Pogancic et al., 2019; Yang et al., 2020), which are often computationally expensive; it takes too long to generate arithmetic circuits or enumerate all models or proofs by calling symbolic solvers.

One main reason for the development of the different ideas is that a naive representation of discrete constraints as a loss function is not meaningfully differentiable. Even for the intervals that it is differentiable, the gradient is zero, so NNs won't update their weights. To address this, we turn to the idea of straight-through estimators (STE) (Courbariaux et al., 2015), which were originally introduced to train binary neural networks (BNNs) -- neural networks with binary weights and activation at run-time. The main idea of STE is to use a binarization function in forward propagation while its gradient, which is zero almost everywhere, is replaced by the gradient of a different, meaningfully differentiable function in backward propagation. It turns out that the method works well for NN quantization in practice.

However, adopting STE alone is not enough for learning with constraints. We need a systematic method of encoding logical constraints as a loss function and ensure that its gradient enables NNs to learn logical constraints.

This paper makes the following contributions.

* We design a systematic way to encode logical constraints in propositional logic as a loss function in neural network learning, which we call _CL-STE_. We demonstrate that minimizing this loss function via STE enforces the logical constraints in neural network learning so that neural networks learn from the explicit constraints.
* We show that by leveraging GPUs and batch training, CL-STE scales significantly better than the other neuro-symbolic learning methods that use heavy symbolic computation for computing gradients.
* We also find that the concept of Training Gate Function (TGF) (Kim et al., 2020), which was applied to channel pruning, is closely related to STE. We establish the precise relationship between them, which gives a new perspective of STE.

The paper is organized as follows. Section 2 presents related works, and Section 3 reviews STE and TFG and establish their relationships. Section 4 presents our loss function representation of logical constraints and proves its properties assuming minimization via STE, and Section 5 shows experimental results.

The implementation of our method is publicly available online at [https://github.com/azreasoners/cl-ste](https://github.com/azreasoners/cl-ste).

## 2 Related Work

Our work is closely related to (Xu et al., 2018), which proposes a semantic loss function to bridge NN outputs and logical constraints. The method treats an NN output as probability and computes semantic loss as the negative logarithm of the probability to generate a state satisfying the logical constraints. Their experiments show that the encoded semantic loss function guides the learner to achieve state-of-the-art results in supervised and semi-supervised learning on multi-class classification. For the efficient computation of a loss function, they encode logical constraints in Sentential Decision Diagram (SDD) (Darwiche, 2011). However, generating SDDs is computationally expensive for most practical tasks.

Several neuro-symbolic formalisms, such as DeepProbLog (Manhaeve et al., 2018), NeurASP (Yang et al., 2020), and NeuroLog (Tsamoura et al., 2021), have been proposed to integrate neural networks with logic programming languages. Since discrete logical inference cannot be in general captured via a differentiable function, they use relaxation to weighted models or probability. While this approach provides a systematic representation of constraints, the symbolic computation is often the bottleneck in training.

Since fuzzy logic operations are naturally differentiable, several works, such as Logic Tensor Network (Serafini and Garcez, 2016), Continuous Query Decomposition (Arakelyan et al., 2020), Semantic Based Regularization (Diligenti et al., 2017; Roychowdhury et al., 2021), directly apply fuzzy operators to neural network outputs. However, as stated in (Marra et al., 2021), the fuzzification procedure alters the logical properties of the original theory (such as satisfiability).

Other works train neural networks for learning satisfiability, such as (Wang et al., 2019; Selsam et al., 2019). SATNet (Wang et al., 2019) builds on a line of research exploring SDP relaxations as a tool for solving MAXSAT, producing tighter approximation guarantees than standard linear programming relaxation.

Graph Neural Networks (GNNs) (Battaglia et al., 2018; Lamb et al., 2020) have been widely applied for logical reasoning. For example, Recurrent Relational Network (RRN) was able to learn how to solve Sudoku puzzles. GNNs use message-passing to propagate logical constraints in neural networks, but they do not have the mechanism to specify the logical constraints directly as we do.

While STE has not been exploited in neuro-symbolic learning to our best knowledge, (Pogancic et al., 2020)'s work is related in that it also uses a gradient that is different from the forward function's gradient. It uses the gradient obtained from a linear relaxation of the forward function. The work also requires a combinatorial solver to compute the gradient.

## 3 Straight-Through-Estimators and Trainable Gate Function

**Review**. STEs are used to estimate the gradients of a discrete function. Courbariaux et al. (2015) consider a binarization function \(b\) that transforms real-valued weights \(x\) into discrete values \(b(x)\) as \(b(x)=1\) if \(x\geq 0\) and \(b(x)=0\) otherwise. A loss function \(L\) is defined on binarized weights \(b(x)\), but the gradient descent won't update binarized weights in small increments. However, using STE, we could update the real-valued weights \(x\) that are input to \(b(x)\). In the end, a quantized model consists of binarized weights \(b(x)\) only. More specifically, according to the chain rule, the gradient of loss \(L\) w.r.t. \(x\) is \(\frac{\partial L}{\partial x}=\frac{\partial L}{\partial b(x)}\times\frac{ \partial b(x)}{\partial x}\), where \(\frac{\partial b(x)}{\partial x}\) is zero almost everywhere. The idea is to replace \(\frac{\partial b(x)}{\partial x}\) with an STE \(\frac{\partial s(x)}{\partial x}\) for some (sub)differentiable function \(s(x)\). The STE \(\frac{\partial s(x)}{\partial x}\) is called the _identity STE_ (iSTE) if \(s(x)=x\) and is called the _saturated STE_ (sSTE) if \(s(x)=clip(x,[-1,1])=min(max(x,-1),1)\). Since \(\frac{\partial s(x)}{\partial x}=1\), by \(\frac{\partial L}{\partial x}\stackrel{{ iSTE}}{{\approx}}\frac{ \partial L}{\partial b(x)}\), we denote the identification of \(\frac{\partial L}{\partial x}\) with \(\frac{\partial L}{\partial b(x)}\) under iSTE.

The binarization function \(b(x)\) passes only the sign of \(x\) while information about the magnitude of \(x\) is lost (Simons and Lee, 2019). In XNOR-Net (Rastegari et al., 2016), the input \(x\) is normalized to have the zero mean and a small variance before the binarization to reduce the information loss. In this paper, we normalize \(x\) by turning it into a probability using softmax or sigmoid activation functions. Indeed, several neuro-symbolic learning methods (e.g., Deep
ProbLog, NeurASP, NeuroLog) assume the neural network outputs fed into the logic layer are normalized as probabilities. To address a probabilistic input, we introduce a variant binarization function \(b_{p}(x)\) for probabilities \(x\in[0,1]\): \(b_{p}(x)=1\) if \(x\geq 0.5\) and \(b_{p}(x)=0\) otherwise. It is easy to see that iSTE and sSTE work the same with \(b_{p}(x)\) since \(x=clip(x,[-1,1])\) when \(x\in[0,1]\). A vector \(\mathbf{x}\) is allowed as input to the binarization functions \(b\) and \(b_{p}\), in which case they are applied to each element of \(\mathbf{x}\).

TGF and Its Relation to STE.The concept of STE is closely related to that of the Trainable Gate Function (TGF) from (Kim et al., 2020), which was applied to channel pruning. Instead of replacing the gradient \(\frac{\partial b(x)}{\partial x}\) with an STE, TGF tweaks the binarization function \(b(x)\) to make it meaningfully differentiable. More specifically, a differentiable binarization function \(\widetilde{b}^{K}\) is defined as

\[\widetilde{b}^{K}(x)=b(x)+s^{K}(x)g(x), \tag{1}\]

where \(K\) is a large constant; \(s^{K}(x)=\frac{Kx-\lfloor Kx\rfloor}{K}\) is called a _gradient tweaking_ function, whose value is less than \(\frac{1}{K}\) and whose gradient is always 1 wherever differentiable; \(g(x)\) is called a _gradient shaping_ function, which could be an arbitrary function, but the authors note that the selection does not affect the results critically and \(g(x)=1\) can be adopted without significant loss of accuracy. As obvious from Figure 1, as \(K\) becomes large, TGF \(\widetilde{b}^{K}(x)\) is an approximation of \(b(x)\), but its gradient is \(1\) wherever differentiable.

Proposition 3.1 tells us a precise relationship between TGF and STE: when \(K\) is big enough, the binarization function \(b(x)\) with iSTE or sSTE can be simulated by TGF. In other words, Proposition 3.1 allows us to visualize \(b(x)\) with STE as the TGF \(\widetilde{b}^{K}(x)\) with \(K=\infty\) as Figure 1 illustrates.

**Proposition 3.1**.: _When \(K\) approaches \(\infty\) and \(|g(x)|\leq c\) for some constant \(c\), the value of \(\widetilde{b}^{K}(x)\) converges to \(b(x)\):_

\[\lim_{K\to\infty}\widetilde{b}^{K}(x)=b(x).\]

_The gradient \(\frac{\partial\widetilde{b}^{K}(x)}{\partial x}\), wherever defined, is exactly the iSTE of \(\frac{\partial b(x)}{\partial x}\) if \(g(x)=1\), or the sSTE of \(\frac{\partial b(x)}{\partial x}\) if_

\[g(x)=\begin{cases}1&\text{if $-1\leq x\leq 1$},\\ 0&\text{otherwise.}\end{cases}\]

Proposition 3.1 still holds if we replace \(b(x)\) with \(b_{p}(x)\).

The proposition yields insights into STE and TGF in terms of each other. As shown in Figure 1, TGF is a sawtooth function that approximates a step function as \(K\) becomes large. At large, TGF works like a discrete function, but it is differentiable almost everywhere. In view of Proposition 3.1, this fact gives an idea why the STE method works in practice. On the other hand, the proposition tells that the implementation of TGF can be replaced with STE. That could be better because TGF in equation (1) requires that \(K\) approximate infinity and be non-differentiable when \(x\) is a multiple of \(\frac{1}{K}\) whereas STE is differentiable at every \(x\).

## 4 Enforcing Logical Constraints using STE

This section presents our method of encoding logical constraints in propositional logic as a loss function so that minimizing its value via STE makes neural network prediction follow the logical constraints.

### Encoding CNF as a Loss Function Using STE

We first review the terminology in propositional logic. A _signature_ is a set of symbols called _atoms_. Each atom represents a proposition that is true or false. A _literal_ is either an atom \(p\) (_positive literal_) or its negation \(\neg p\) (_negative literal_). A _clause_ is a disjunction over literals, e.g., \(p_{1}\vee\neg p_{2}\lor p_{3}\). A _Horn clause_ is a clause with at most one positive literal. We assume a (_propositional_) _theory_ consisting of a set of clauses (sometimes called a _CNF (Conjunctive Normal Form) theory_). A truth assignment to atoms _satisfies_ (denoted by \(|\!=\)) a theory if at least one literal in each clause is true under the assignment. A theory is _satisfiable_ if at least one truth assignment satisfies the theory. A theory _entails_ (also denoted by \(|\!=\)) a literal if every truth assignment that satisfies the theory also satisfies that literal.

We define a general loss function \(L_{cnf}\) for any CNF theory as follows. Here, bold upper and lower letters (e.g., \(\mathbf{C}\) and \(\mathbf{v}\)) denote matrices and vectors, respectively; \(\mathbf{C}[i,j]\) and \(\mathbf{v}[i]\) denote their elements.

Consider a propositional signature \(\sigma=\{p_{1},\ldots,p_{n}\}\). Given (i) a theory \(C\) consisting of \(m\) clauses (encoding domain knowledge), (ii) a set \(F\) of atoms denoting some atomic facts that we assume known to be true (representing the ground-truth label of a data instance), and (iii) a truth assignment \(v\) such that \(v\models F\), we construct their matrix/vector representations as

* the matrix \(\mathbf{C}\in\{-1,0,1\}^{m\times n}\) to represent the theory such that \(\mathbf{C}[i,j]\) is \(1\) (\(-1\), resp.) if \(p_{j}\) (\(\neg p_{j}\), resp.) belongs to the \(i\)-th clause in the theory, and is \(0\) if neither \(p_{j}\) nor \(\neg p_{j}\) belongs to the clause;
* the vector \(\mathbf{f}\in\{0,1\}^{n}\) to represent \(F\) such that \(\mathbf{f}[j]\) is \(1\) if \(p_{j}\in F\) and is \(0\) otherwise; and

Figure 1: Trainable gate function \(\widetilde{b}^{K}(x)\) when \(g(x)=1\)
* the vector \(\mathbf{v}\in\{0,1\}^{n}\) to represent \(v\) such that \(\mathbf{v}[j]\) is \(1\) if \(v(p_{j})=\texttt{true}\), and is \(0\) if \(v(p_{j})=\texttt{false}\).

Figure 2 shows an architecture that overlays the two loss functions \(L_{bound}\) and \(L_{cnf}\) over the neural network output, where \(L_{cnf}\) is the main loss function to encode logical constraints and \(L_{bound}\) is a regularizer to limit the raw neural network output not to grow too big (more details will follow). The part \(\mathbf{input}\) is a tensor (e.g., images) for a data instance; \(\mathbf{label}\) denotes the labels of input data; \(\mathbf{C}\) encodes the domain knowledge, \(\mathbf{x}\in[0,1]^{n}\) denotes the NN output (in probability), and \(\mathbf{f}\in\{0,1\}^{n}\) records the known facts in that data instance (e.g., given digits in Sudoku).1 Let \(\mathbb{1}_{\{k\}}(X)\) denote an indicator function that replaces every element in \(X\) with \(1\) if it is \(k\) and with \(0\) otherwise. Then the binary prediction \(\mathbf{v}\) is constructed as \(\mathbf{v}=\mathbf{f}+\mathbb{1}_{\{0\}}(\mathbf{f})\odot b_{p}(\mathbf{x})\), where \(\odot\) denotes element-wise multiplication. Intuitively, \(\mathbf{v}\) is the binarized NN output with part of it strictly following the given facts specified in \(\mathbf{f}\) (ensuring \(v\models F\)).

Footnote 1: In case the length of \(\mathbf{x}\) is less than \(n\), we pad \(\mathbf{x}\) with \(0\)s for all the atoms that are not related to NN output.

**Example 4.1**.: _Consider a simple example \(\mathbf{mnistAdd}\) from (Manhaeve et al., 2018), where the task is, given a pair of MNIST digit images and their sum as the label, to let a neural network learn the digit classification of the input images. The example is used to demonstrate how NNs can learn from known constraints. In Figure 2, the input consists of two-digit images \(i_{1}\) and \(i_{2}\), and the label is an integer \(l\) in \(\{0,...,18\}\) denoting the sum of \(i_{1}\) and \(i_{2}\). The neural network is the same Convolutional Neural Network (CNN) used in (Manhaeve et al., 2018)._

_The theory for this problem consists of the following clause for \(l\in\{0,\dots,18\}\), where \(sum(l)\) represents "the sum of \(i_{1}\) and \(i_{2}\) is \(l\)" and \(pred(n_{1},n_{2})\) represents "the neural network predicts \(i_{1}\) and \(i_{2}\) as \(n_{1}\) and \(n_{2}\) respectively":_

\[\neg sum(l)\vee\bigvee_{\begin{subarray}{c}n_{1},n_{2}\in\{0,\dots,9\}:\\ n_{1}+n_{2}=l\end{subarray}}pred(n_{1},n_{2}).\]

_This theory contains \(19+100=119\) atoms for \(sum/1\) and \(pred/2\) respectively. We construct the matrix \(\mathbf{C}\in\{-1,0,1\}^{19\times 119}\), where each row represents a clause. For instance, the row for the clause \(\neg sum(1)\lor pred(0,1)\lor pred(1,0)\) is a vector in \(\{-1,0,1\}^{1\times 119}\) containing a single \(-1\) for atom \(sum(1)\), two \(1s\) for atoms \(pred(0,1)\) and \(pred(1,0)\), and 116 \(0\)s._

_Vectors \(\mathbf{f}\) and \(\mathbf{v}\) are in \(\{0,1\}^{119}\) constructed from each data instance \(\langle i_{1},i_{2},l\rangle\). The fact vector \(\mathbf{f}\) contains a single \(1\) for atom \(sum(l)\) (ground truth label) and 118 \(0\)s. To obtain the prediction vector \(\mathbf{v}\), we (i) feed images \(i_{1}\),\(i_{2}\) into the CNN (with softmax at the last layer) from (Manhaeve et al., 2018) to obtain the outputs \(\mathbf{x}_{1},\mathbf{x}_{2}\in[0,1]^{10}\) (consisting of probabilities), (ii) construct the vector \(\mathbf{x}\in[0,1]^{100}\) (for 100 atoms of \(pred/2\)) such that \(\mathbf{x}[10i+j]\) is \(\mathbf{x}_{1}[i]\times\mathbf{x}_{2}[j]\) for \(i,j\in\{0,\dots,9\}\), (iii) update \(\mathbf{x}\) as the concatenation of \(\mathbf{x}\) and \(\{0\}^{19}\), and (iv) finally, let \(\mathbf{v}=\mathbf{f}+\mathbb{1}_{\{0\}}(\mathbf{f})\odot b_{p}(\mathbf{x})\)._

Using \(\mathbf{C}\), \(\mathbf{v}\), and \(\mathbf{f}\), we define the _CNF loss_\(L_{cnf}(\mathbf{C},\mathbf{v},\mathbf{f})\) as follows:

\[\mathbf{L}_{f} =\mathbf{C}\odot\mathbf{f} \tag{2}\] \[\mathbf{L}_{v} =\mathbb{1}_{\{1\}}(\mathbf{C})\odot\mathbf{v}+\mathbb{1}_{\{-1 \}}(\mathbf{C})\odot(1-\mathbf{v})\] (3) \[\mathbf{deduce} =\mathbb{1}_{\{1\}}\Big{(}sum(\mathbf{C}\odot\mathbf{C})-sum( \mathbb{1}_{\{-1\}}(\mathbf{L}_{f}))\Big{)}\] (4) \[\mathbf{unsat} =prod(1-\mathbf{L}_{v})\] (5) \[\mathbf{keep} =sum(\mathbb{1}_{\{1\}}(\mathbf{L}_{v})\odot(1-\mathbf{L}_{v})+ \mathbb{1}_{\{0\}}(\mathbf{L}_{v})\odot\mathbf{L}_{v})\] (6) \[L_{deduce} =sum(\mathbf{deduce}\odot\mathbf{unsat})\] (7) \[L_{unsat} =avg(\mathbb{1}_{\{1\}}(\mathbf{unsat})\odot\mathbf{unsat})\] (8) \[L_{sat} =avg(\mathbb{1}_{\{0\}}(\mathbf{unsat})\odot\mathbf{keep}) \tag{9}\]

\[L_{cnf}(\mathbf{C},\mathbf{v},\mathbf{f})=L_{deduce}+L_{unsat}+L_{sat} \tag{10}\]

where \(prod(X)\), \(sum(X)\), and \(avg(X)\) compute the product, sum, and average of the elements in \(X\) along its last dimension. 2 Although these equations may look complex, it helps to know that they use the form \(\mathbb{1}_{\{k\}}(X_{1})\odot X_{2}\), where the indicator function \(\mathbb{1}_{\{k\}}(X_{1})\) can be seen as a constant that is multiplied to a trainable variable \(X_{2}\). Take equation (8) as an example. To minimize \(L_{unsat}\), the NN parameters will be updated towards making \(\mathbf{unsat}[i]\) to be \(0\) whenever \(\mathbb{1}_{\{1\}}(\mathbf{unsat})\) is \(1\), i.e., towards making unsatisfied clauses satisfied.

Footnote 2: The aggregated dimension is “squeezed,” which is the default behavior in PyTorch aggregate functions (keepdim is False).

In equations (2) and (3), \(\mathbf{f}\) and \(\mathbf{v}\) are treated as matrices in \(\{0,1\}^{1\times n}\) to have element-wise multiplication (with broadcasting) with a matrix in \(\{-1,0,1\}^{m\times n}\). Take equation (2) as an example, \(\mathbf{L}_{f}[i,j]=\mathbf{C}[i,j]\times\mathbf{f}[j]\). \(\mathbf{L}_{f}\) is the matrix in \(\{-1,0,1\}^{m\times n}\) such that (i) \(\mathbf{L}_{f}[i,j]=1\) iff clause \(i\) contains literal \(p_{j}\) and \(p_{j}\in F\); (ii) \(\mathbf{L}_{f}[i,j]=-1\) iff clause \(i\) contains literal \(\neg p_{j}\) and \(p_{j}\in F\); (iii) otherwise, \(\mathbf{L}_{f}[i,j]=0\).

Figure 2: Architecture that overlays constraint loss
\(\mathbf{L}_{v}\) is the matrix in \(\{0,1\}^{m\times n}\) such that \(\mathbf{L}_{v}[i,j]=1\) iff clause \(i\) contains a literal (\(p_{j}\) or \(\neg p_{j}\)) for atom \(p_{j}\) and this literal is true under \(v\).

In equations (4), (5), and (6), \(sum(\mathbf{C}\odot\mathbf{C})\) is a vector in \(\mathbb{N}^{m}\) representing in each clause the number of literals, and \(sum(\mathbbm{1}_{\{-1\}}(\mathbf{L}_{f}))\) is a vector in \(\mathbb{N}^{m}\) representing in each clause the number of literals that are false under \(F\) (i.e., the number of literals of the form \(\neg p\) such that \(p\in F\)). Consequently, **deduce** is a vector in \(\{0,1\}^{m}\) where \(\mathbf{deduce}[i]\) is \(1\) iff clause \(i\) has all but one literal being false under \(F\). If \(C\cup F\) is satisfiable and a clause has all but one literal being false under \(F\), then we can safely deduce that the remaining literal is true. For instance, in a clause for Sudoku

\[\neg a(1,1,9)\vee\neg a(1,2,9), \tag{11}\]

if \(a(1,1,9)\) is in the ground-truth label (i.e., in \(F\)) but \(a(1,2,9)\) is not, we can safely deduce \(\neg a(1,2,9)\) is true. It follows that such a clause is always a Horn clause. Intuitively, the vector **deduce** represents the clauses that such deduction can be applied given \(F\).

The vector \(\mathbf{unsat}\in\{0,1\}^{m}\) indicates which clause is not satisfied by the truth assignment \(v\), where \(\mathbf{unsat}[i]\) is \(1\) iff \(v\) does not satisfy the \(i\)-th clause. The vector \(\mathbf{keep}\in\{0\}^{m}\) consists of \(m\) zeros while its gradient w.r.t. \(\mathbf{v}\) consists of non-zeros. Intuitively, the gradient of \(\mathbf{keep}\) tries to keep the current predictions \(\mathbf{v}\) in each clause.

In equations (7), (8), and (9), \(L_{deduce}\in\mathbb{N}\) represents the number of clauses that can deduce a literal given \(F\) and are not satisfied by \(v\). The vector \(\mathbbm{1}_{\{1\}}(\mathbf{unsat})\in\{0,1\}^{m}\) (and \(\mathbbm{1}_{\{0\}}(\mathbf{unsat})\), resp.) indicates the clauses that are not satisfied (and are satisfied, resp.) by \(v\). Intuitively, for all clauses, minimizing \(L_{unsat}\) makes the neural network change its predictions to decrease the number of unsatisfied clauses. In contrast, minimizing \(L_{sat}\) makes the neural network more confident in its predictions in the satisfied clauses. We use \(avg\) instead of \(sum\) in equations (8) and (9) to ensure that the gradients from \(L_{unsat}\) and \(L_{sat}\) do not overpower those from \(L_{deduce}\). Formal statements of these intuitive explanations follow in the next section.

For any neural network output \(\mathbf{x}\) consisting of probabilities, let \(\mathbf{x}^{r}\) denote the raw value of \(\mathbf{x}\) before the activation function (e.g., softmax or sigmoid) in the last layer. Without restriction, the value \(\mathbf{x}^{r}\) may vary in a large range when trained with STE. When such an output is fed into softmax or sigmoid, it easily falls into a saturation region of the activation function (Tang et al., 2017). To resolve this issue, we include another loss function to bound the scale of \(\mathbf{x}^{r}\):

\[L_{bound}(\mathbf{x})=avg(\mathbf{x}^{r}\odot\mathbf{x}^{r}).\]

To enforce constraints, we add the weighted sum of \(L_{cnf}(\mathbf{C},\mathbf{v},\mathbf{f})\) and \(L_{bound}(\mathbf{x})\) to the baseline loss (if any), where the weight of each loss is a hyperparameter. We call this way of semantic regularization the _CL-STE_ (Constraint Loss via STE) method.

**Example 4.1** Continued.: Given the matrix \(\mathbf{C}\) for the CNF theory, a data instance \(\langle i_{1},i_{2},l\rangle\), the NN outputs \(\mathbf{x}_{1},\mathbf{x}_{2}\) for \(i_{1},i_{2}\), and the vectors \(\mathbf{f},\mathbf{v}\) as constructed in Example 4.1, the total loss function used for \(\mathbf{mnistAdd}\) problem is

\[\mathcal{L}=L_{cnf}(\mathbf{C},\mathbf{v},\mathbf{f})+\sum_{\mathbf{x}\in\{ \mathbf{x}_{1},\mathbf{x}_{2}\}}0.1\times L_{bound}(\mathbf{x}).\]

### Properties of Constraint Loss and Its Gradients

Proposition 4.2 shows the relation between \(L_{deduce}\), \(L_{unsat}\), and \(L_{sat}\) components in the constraint loss \(L_{cnf}\) and its logical counterpart.

**Proposition 4.2**.: _Given a theory \(C\), a set \(F\) of atoms, and a truth assignment \(v\) such that \(v\models F\), let \(\mathbf{C},\mathbf{f},\mathbf{v}\) denote their matrix/vector representations, respectively. Let \(C_{deduce}\subseteq C\) denote the set of Horn clauses \(H\) in \(C\) such that all but one literal in \(H\) are of the form \(\neg p\) such that \(p\in F\). 3 Then_

Footnote 3: This implies that the remaining literal is either an atom or \(\neg p\) such that \(p\not\in F\).

* _the minimum values of_ \(L_{deduce}\)_,_ \(L_{unsat}\)_,_ \(L_{sat}\) _, and_ \(L_{cnf}(\mathbf{C},\mathbf{v},\mathbf{f})\) _are 0;_
* \(v\models C_{deduce}\) _iff_ \(L_{deduce}\) _is 0;_
* \(v\models C\) _iff_ \(L_{unsat}\) _is 0 iff_ \(L_{cnf}(\mathbf{C},\mathbf{v},\mathbf{f})\) _is 0._

Clause (11) is an example clause in \(C_{deduce}\). There could be many other ways to design \(L_{cnf}(\mathbf{C},\mathbf{v},\mathbf{f})\) to satisfy the properties in Proposition 4.2. Propositions 4.3 and 4.5 below justify our design choice.

**Proposition 4.3**.: _Given a theory \(C\) with \(m\) clauses and \(n\) atoms and a set \(F\) of atoms such that \(C\cup F\) is satisfiable, let \(\mathbf{C},\mathbf{f}\) denote their matrix/vector representations, respectively. Given a neural network output \(\mathbf{x}\in[0,1]^{n}\) denoting probabilities, we construct \(\mathbf{v}=\mathbf{f}+\mathbbm{1}_{\{0\}}(\mathbf{f})\odot b_{p}(\mathbf{x})\) and a truth assignment \(v\) such that \(v(p_{j})=\textsc{true}\) if \(\mathbf{v}[j]\) is \(1\), and \(v(p_{j})=\textsc{false}\) if \(\mathbf{v}[j]\) is \(0\). Let \(C_{deduce}\subseteq C\) denote the set of Horn clauses \(H\) in \(C\) such that all but one literal in \(H\) are of the form \(\neg p\) where \(p\in F\). Then, for any \(j\in\{1,\ldots,n\}\),_

1. _if_ \(p_{j}\in F\)_, all of_ \(\frac{\partial L_{deduce}}{\partial\mathbf{x}[j]}\)_,_ \(\frac{\partial L_{unsat}}{\partial\mathbf{x}[j]}\)_, and_ \(\frac{\partial L_{sat}}{\partial\mathbf{x}[j]}\) _are zeros;_
2. _if_ \(p_{j}\not\in F\)_,_ \[\frac{\partial L_{deduce}}{\partial\mathbf{x}[j]}\overset{iSTE}{\approx}\begin{cases}-c& \text{if $c>0$ clauses in $C_{deduce}$}\\ &\text{ contain literal $p_{j}$;}\\ c&\text{ if $c>0$ clauses in $C_{deduce}$}\\ &\text{ contain literal $\neg p_{j}$;}\\ 0&\text{ otherwise;}\end{cases}\]
\[\frac{\partial L_{unsat}}{\partial\mathbf{x}[j]}\stackrel{{ iSTE}}{{\approx}}\frac{c_{2}-c_{1}}{m}\] \[\frac{\partial L_{sat}}{\partial\mathbf{x}[j]}\stackrel{{ iSTE}}{{\approx}}\begin{cases}-\frac{c_{3}}{m}&\text{if }v\models p_{j}\\ \frac{c_{3}}{m}&\text{if }v\not\models p_{j},\end{cases}\]

_where \(\stackrel{{ iSTE}}{{\approx}}\) stands for the equivalence of gradients assuming iSTE; \(c_{1}\) (and \(c_{2}\), resp.) is the number of clauses in \(C\) that are not satisfied by \(v\) and contain \(p_{j}\) (and \(\neg p_{j}\), resp.); \(c_{3}\) is the number of clauses in \(C\) that are satisfied by \(v\) and contain \(p_{j}\) or \(\neg p_{j}\)._

Intuitively, Proposition 4.3 ensures the following properties of the gradient \(\frac{\partial L_{conf}(\mathbf{C},\mathbf{v},\mathbf{f})}{\partial\mathbf{x} [j]}\), which consists of \(\frac{\partial L_{advace}}{\partial\mathbf{x}[j]}\), \(\frac{\partial L_{unsat}}{\partial\mathbf{x}[j]}\), and \(\frac{\partial L_{ost}}{\partial\mathbf{x}[j]}\).

**P1.**: If we know for sure that \(p_{j}\) is true (\(p_{j}\in F\)), these gradients w.r.t. \(\mathbf{x}[j]\) (real values corresponding to \(p_{j}\)) are \(0\), so they do not affect the truth value of \(p_{j}\).

**P2.**: Otherwise (\(F\) does not tell whether \(p_{j}\) is true),

1. the gradient \(\frac{\partial L_{advace}}{\partial\mathbf{x}[j]}\) is negative (positive, resp.) to increase (decrease, resp.) the value of \(\mathbf{x}[j]\) by the gradient descent if \(C\cup F\) entails \(p_{j}\) (\(\neg p_{j}\), resp.);
2. the gradient \(\frac{\partial L_{unsat}}{\partial\mathbf{x}[j]}\) is negative (positive resp.) to increase (decrease, resp.) the value of \(\mathbf{x}[j]\) by the gradient descent if, among all unsatisfied clauses, more clauses contain \(p_{j}\) than \(\neg p_{j}\) (\(\neg p_{j}\) than \(p_{j}\), resp.);
3. the gradient \(\frac{\partial L_{sat}}{\partial\mathbf{x}[j]}\) is negative (positive resp.) to increase (decrease, resp.) the value of \(\mathbf{x}[j]\) by the gradient descent if \(v\models p_{j}\) (\(v\not\models p_{j}\), resp.) and there exist satisfied clauses containing literal \(p_{j}\) or \(\neg p_{j}\).

Intuitively, bullet 1 in **P2** simulates a deduction step, which is always correct, while bullets 2 and 3 simulate two heuristics: "we tend to believe a literal if more unsatisfied clauses contain this literal than its negation" and "we tend to keep our prediction on an atom if many satisfied clauses contain this atom." This justifies another property below.

**P3.**: The sign of the gradient \(\frac{\partial L_{conf}}{\partial\mathbf{x}[j]}\) is the same as the sign of \(\frac{\partial L_{advace}}{\partial\mathbf{x}[j]}\) when the latter gradient is non-zero.

**Example 4.4**.: _Consider the theory \(C\) below with \(m=2\) clauses and 3 atoms_

\[\neg a\vee\neg b\lor c\] \[\neg a\lor b\]

_and consider the set of given facts \(F=\{a\}\). They are represented by matrix \(\mathbf{C}=\begin{bmatrix}-1&-1&1\\ -1&1&0\end{bmatrix}\) and vector \(\mathbf{f}=[1,0,0]\). Suppose a neural network predicts \(\mathbf{x}=[0.3,0.1,0.9]\) as the probabilities of the 3 atoms \(\{a,b,c\}\)._

_With the above matrix and vectors, we can compute_

\[b_{p}(\mathbf{x}) =[0,0,1],\] \[\mathbf{v} =\mathbf{f}+\mathbbm{1}_{\{0\}}(\mathbf{f})\odot b_{p}(\mathbf{x} )=[1,0,1].\]

_From \(\mathbf{v}\), we construct the truth assignment \(v=\{a=\text{true},b=\text{false},c=\text{true}\}\). Clearly, \(v\) satisfies the first clause but not the second one. Given \(F=\{a\}\), we see \(C_{deduce}\) is \(\neg a\lor b\)._

_According to Proposition 4.3,_

\[\frac{\partial L_{deduce}}{\partial\mathbf{x}}\stackrel{{ iSTE}}{{\approx}}[0,-1,0],\quad\frac{\partial L_{unsat}}{ \partial\mathbf{x}}\stackrel{{ iSTE}}{{\approx}}[0,-\frac{1}{2}, 0],\] \[\frac{\partial L_{sat}}{\partial\mathbf{x}}\stackrel{{ iSTE}}{{\approx}}[0,\frac{1}{2},-\frac{1}{2}],\] \[\frac{\partial L_{conf}}{\partial\mathbf{x}}=\frac{\partial L_{ deduce}}{\partial\mathbf{x}}+\frac{\partial L_{unsat}}{\partial\mathbf{x}}+\frac{ \partial L_{sat}}{\partial\mathbf{x}}\stackrel{{ iSTE}}{{\approx}}[0,-1,-\frac{1}{2}].\]

_Intuitively, given \(C\), \(F\), and the current truth assignment \(v\), (**P1**) we know \(a\) is true (\(a\in F\)) thus no need to update it, (**P2.1** and **P3**) we know for sure that the prediction for \(b\) should be changed to true by deduction on clause \(\neg a\lor b\) and the given fact \(F=\{a\}\), (**P2.3**) we tend to strengthen our belief in \(c\) being true due to the satisfied clause \(\neg a\vee\neg b\lor c\)._

The proposition also holds with another binarization function \(b(x)\).

**Proposition 4.5**.: _Proposition 4.3 still holds for \(\mathbf{x}\in\mathbb{R}^{n}\) and \(\mathbf{v}=\mathbf{f}+\mathbbm{1}_{\{0\}}(\mathbf{f})\odot b(\mathbf{x})\)._

## 5 Evaluation

We conduct an experimental evaluation to answer the following questions.

* Is CL-STE more scalable in injecting discrete constraints into neural network learning than existing neuro-symbolic learning methods?
* Does CL-STE make neural networks learn with no or fewer labeled data by effectively utilizing the given constraints?
* Is CL-STE general enough to overlay constraint loss on different types of neural networks to enforce logical constraints and improve the accuracy of existing networks?

Our implementation takes a CNF theory in DIMACS format (the standard format for input to SAT solvers).4 Since the
CL-STE method alone doesn't have associated symbolic rules, unlike DeepProbLog, NeurASP, and NeuroLog, in this section, we compare these methods on the classification accuracy of the trained NNs (e.g., correctly predicting the label of an MNIST image) instead of query accuracy (e.g., correctly predicting the sum of two MNIST images).

### mnistAdd Revisited

We introduced the CNF encoding and the loss function for the **mnistAdd** problem in Example 4.1. The problem was used in (Manhaeve et al., 2018) and (Yang et al., 2020) as a benchmark.

Figure 3 compares the MNIST digit classification accuracy of neural networks trained by different methods on a single epoch of 30,000 addition data from (Manhaeve et al., 2018). "CL-STE(\(n\))" denotes our method with \(b_{p}(x)\) and iSTE using a batch of size \(n\). As we see, DeepProbLog, NeurASP, and CL-STE with a batch size of 1 could quickly converge to near 100% test accuracy. Training time-wise, CL-STE outperforms the other approaches since it does not need to generate arithmetic circuits for every training instance as in DeepProbLog or enumerate all models as in NeurASP. Also, while DeepProbLog and NeurASP do not support batch training, CL-STE could leverage the batch training to reduce the training time to 22s with a batch size of 16 (denoted by CL-STE(16)). We observe that increasing the batch size in CL-STE also increases the number of parameter updates for convergence, which we could decrease by using batch normalization as shown in the blue line denoted by CL-STE(16)-BN.

Furthermore, we apply CL-STE to the variants of **mnistAdd** by training with two-digit sums (**mnistAdd2**(Manhaeve et al., 2018)) and three-digit sums (**mnistAdd3**). Table 1 shows that the CL-STE method scales much better than DeepProbLog and NeurASP. The time and accuracy are reported for a single epoch of training, where the cutoff time is 24 hours after which we report "timeout."

### Benchmarks from (Tsamoura et al., 2021)

The following are benchmark problems from (Tsamoura et al., 2021). Like the **mnistAdd** problem, labels are not immediately associated with the data instances but with the results of logical operations applied to them.

**add2x2** The input is a \(2\times 2\) grid of digit images. The output is the four sums of the pairs of digits in each row/column. The task is to train a CNN for digit classification.

**apply2x2** The input is three digits and a \(2\times 2\) grid of handwritten math operator images in \(\{+,-,\times\}\). The output is the four results of applying the two math operators in each row/column in the grid on the three digits. The task is to train a CNN for math operator classification.

**member(n)** The input is a set of \(n\) images of digits and a digit in \(\{0,\dots,9\}\). The output is 0 or 1, indicating whether the digit appears in the set of digit images. The task is to train a CNN for digit classification.

Table 2 compares our method with DeepProbLog, NeurASP, and NeuroLog test accuracy-wise and training time-wise. Note that, instead of comparing the query accuracy as in (Tsamoura et al., 2021), we evaluate and compare the NN classification accuracies.

Our experiments agree with (Yin et al., 2019), which proves the instability issue of iSTE and the convergence guarantees with sSTE in a simple 2-layer CNN. Their experiments also observe a better performance of \(b(x)\)+sSTE over \(b(x)\)+iSTE on deep neural networks. Our experimental results (especially for member(5) problem) also reveal the instability issue of \(b(x)\)+iSTE and show that \(b(x)\)+sSTE achieves higher and more stable accuracy. Furthermore, we observe that \(b_{p}(x)\) works better than \(b(x)\) in terms of both accuracy and time in our experiments. This is because the input \(x\) to \(b_{p}(x)\) is normalized into probabilities before binarization, resulting in less information loss (i.e., change in magnitude

\begin{table}
\begin{tabular}{c|c c|c c|c} \hline \hline  & \multicolumn{2}{c|}{mnistAdd} & \multicolumn{2}{c|}{mnistAdd2} & \multicolumn{2}{c}{mnistAdd3} \\ \hline DeepProbLog & 98.36\% & 2565s & 97.57\% & 2269\% & timeout \\ \hline NeurASP & 97.87\% & 292s & 97.85\% & 1682s & timeout \\ \hline CL-STE & 97.48\% & 22s & 98.12\% & 92s & 97.78\% & 402s \\ \hline \hline \end{tabular}
\end{table}
Table 1: Experiments on **mnistAdd**

\begin{table}
\begin{tabular}{c|c c c} \hline \hline  & add2x2 & apply2x2 & member(3) & member(5) \\ \hline accuracy(\%) & & & \\ \hline DeepProbLog & 88.4\(\pm\)0.7 & 100\(\pm\)0 & 96.3\(\pm\)0.3 & timeout \\ \hline NeurASP & 97.6\(\pm\)0.2 & 100\(\pm\)0 & 93.5\(\pm\)0.9 & timeout \\ \hline NeurLog & 97.5\(\pm\)0.4 & 100\(\pm\)0 & 94.5\(\pm\)1.5 & 93.9\(\pm\)1.5 \\ \hline \(b(x)+iSTE\) & 95.5\(\pm\)0.7 & 100\(\pm\)0 & 73.2\(\pm\)9.1 & 51.1\(\pm\)2.9 \\ \(b(x)+sSTE\) & 95.7\(\pm\)0.5 & 100\(\pm\)0 & 83.2\(\pm\)8.4 & 88.0\(\pm\)7.1 \\ \(b_{p}(x)+iSTE\) & 98.0\(\pm\)0.2 & 100\(\pm\)0 & 95.5\(\pm\)0.7 & 95.0\(\pm\)0.5 \\ \hline time(s) & & & \\ \hline DeepProbLog & 1035\(\pm\)5.7 & 586\(\pm\)9 & 2218\(\pm\)211 & timeout \\ \hline NeurASP & 142\(\pm\)2 & 47\(\pm\)1 & 253\(\pm\)1 & timeout \\ \hline NeurLog & 2400\(\pm\)46 & 2428\(\pm\)29 & 427\(\pm\)12 & 68\(\pm\)40 \\ \hline \(b(x)\) + iSTE & 80\(\pm\)2 & 208\(\pm\)1 & 45\(\pm\)0.0 & 177\(\pm\)1 \\ \(b(x)+sSTE\) & 81\(\pm\)2 & 214\(\pm\)8 & 46\(\pm\)1 & 181\(\pm\)10 \\ \(b_{p}(x)+sSTE\) & 54\(\pm\)4 & 112\(\pm\)2 & 43\(\pm\)3 & 49\(\pm\)4 \\ \hline \hline \end{tabular}
\end{table}
Table 2: Comparison between CL-STE and other approaches: The numbers in parentheses are the times spent by NeuroLog to generate allductive proofs.

Figure 3: Comparison on mnistAdd
"\(b_{p}(x)-x\)") when the neural network accuracy increases.

### CNN + Constraint Loss for Sudoku

The following experimental setting from (Yang et al., 2020) demonstrates unsupervised learning with NeurASP on Sudoku problems. Given a textual representation of a Sudoku puzzle (in the form of a \(9\times 9\) matrix where an empty cell is represented by 0), Park (2018) trained a CNN (composed of 9 convolutional layers and a \(1\times 1\) convoutional layer, followed by softmax) using 1 million examples and achieved 70% test accuracy using an "inference trick": instead of predicting digits for all empty cells at once, which leads to poor accuracy, predict the most probable grid-cell value one by one. With the same CNN and inference trick, Yang et al. (2020) achieved 66.5% accuracy with only 7% data with no supervision (i.e., 70k data instances without labels) by enforcing semantic constraints in neural network training with NeurASP. In this section, we consider the same unsupervised learning problem for Sudoku while we represent the Sudoku problem in CNF and use \(L_{cnf}\) to enforce logical constraints during training.

We use a CNF theory for \(9\times 9\) Sudoku problems with \(9^{3}=729\) atoms and \(8991\) clauses as described in Appendix C.6. This CNF can be represented by a matrix \(\mathbf{C}\in\{-1,0,1\}^{8991\times 729}\). The dataset consists of 70k data instances, 80%/20% for training/testing. Each data instance is a pair \(\langle\mathbf{q},\mathbf{l}\rangle\) where \(\mathbf{q}\in\{0,1,\ldots,9\}^{81}\) denotes a \(9\times 9\) Sudoku board (\(0\) denotes an empty cell) and \(\mathbf{l}\in\{1,\ldots,9\}^{81}\) denotes its solution (\(\mathbf{l}\) is not used in NeurASP and our method during training). The non-zero values in \(\mathbf{q}\) are treated as atomic facts \(F\) and we construct the matrix \(\mathbf{F}\in\{0,1\}^{81\times 9}\) such that, for \(i\in\{1,\ldots,81\}\), the \(i\)-th row \(\mathbf{F}[i,\mathbf{\cdot}]\) is the vector \(\{0\}^{9}\) if \(\mathbf{q}[i]=0\) and is the one-hot vector for \(\mathbf{q}[i]\) if \(\mathbf{q}[i]\neq 0\). Then, the vector \(\mathbf{f}\in\{0,1\}^{729}\) is simply the flattening of \(\mathbf{F}\). We feed \(\mathbf{q}\) into the CNN and obtain the output \(\mathbf{x}\in[0,1]^{729}\). Finally, the prediction \(\mathbf{v}\in\{0,1\}^{729}\) is obtained as \(\mathbf{f}+\mathbf{l}_{\{0\}}(\mathbf{f})\odot b_{p}(\mathbf{x})\), and the total loss function \(\mathcal{L}\) we used is \(\mathcal{L}=L_{cnf}(\mathbf{C},\mathbf{v},\mathbf{f})+0.1\times L_{bound}( \mathbf{x})\).

Table 3 compares the training time and the (whole-board) test accuracies with and without the inference trick (\(Acc_{w}\) and \(Acc_{wo}\), resp.) using \(b_{p}(x)\)+iSTE against NeurASP and baseline CNN (Park, 2018). In each experiment, the same CNN is trained with only 70k (labeled/unlabeled) data instances from (Yang et al., 2020) with an average of 43 given digits in a puzzle (min: 26, max: 77). As we can see, our method outperforms NeurASP in both accuracy and time. Accuracy-wise, the CNN model trained using CL-STE is 27.2% more accurate than the CNN model trained using NeurASP when we use the inference trick. Training time-wise, CL-STE is 16 times faster than NeurASP because we directly encode semantic constraints in a loss function, which saves the time to call a symbolic engine externally (e.g., clingo to enumerate all stable models as in NeurASP).

Table 4 compares CNN+CL-STE with SATNet trained on Park 70k and tested on both Park 70k and Palm Sudoku dataset (Palm et al., 2018). While CNN is less tailored to logical reasoning than SATNet, our experiment shows that, when it is trained via CL-STE, it performs better than SATNet.

### GNN + Constraint Loss for Sudoku

This section investigates if a GNN training can be improved with the constraint loss functions with STE by utilizing already known constraints without always relying on the labeled data. We consider the Recurrent Relational Network (RRN) (Palm et al., 2018), a state-of-the-art GNN for multi-step relational reasoning that achieves 96.6% accuracy for hardest Sudoku problems by training on 180k labeled data instances. Our focus here is to make RRN learn more effectively using fewer data by injecting known constraints.

The training dataset in (Palm et al., 2018) contains 180k data instances evenly distributed in 18 difficulties with 17-34 given numbers. We use a small subset of this dataset with random sampling. Given a data instance \(\langle\mathbf{q},\mathbf{l}\rangle\) where \(\mathbf{q}\in\{0,1,\ldots,9\}^{81}\) denotes a \(9\times 9\) Sudoku board and \(\mathbf{l}\in\{1,\ldots,9\}^{81}\) denotes its solution, RRN takes \(\mathbf{q}\) as input and, after 32 iterations of message passing, outputs 32 matrices of probabilities \(\mathbf{X}_{s}\in\mathbf{R}^{81\times 9}\) where \(s\in\{1,\ldots,32\}\); for example, \(\mathbf{X}_{1}\) is the RRN prediction after 1 message passing step.

The baseline loss is the sum of the cross-entropy losses between prediction \(\mathbf{X}_{s}\) and label 1 for all \(s\).

We evaluate if using constraint loss could further improve the performance of RRN with the same labeled data. We use the same \(L_{cnf}\) and \(L_{bound}\) defined in CNN (with weights \(1\) and \(0.1\), resp.), which are applied to \(\mathbf{X}_{1}\) only so that the RRN could be trained to deduce new digits in a single message passing step. We also use a continuous regularizer \(L_{sum}\) below to regularize every \(\mathbf{X}_{s}\) that "the sum of the 9

\begin{table}
\begin{tabular}{c|c|c|c|c} \hline \hline \multirow{2}{*}{Method} & Train Data & Test & \multirow{2}{*}{\#Given} & Test \\  & (Supv) & Data & & Accuracy \\ \hline \multirow{2}{*}{SATNet} & Park 70k & Park 70k & 26-77 & 67.78\% \\  & (Full) & Palm & 17-34 & 6.76\% \\ \hline \multirow{2}{*}{CNN+CL-STE} & Park 70k & Park 70k & 26-77 & 95.70\% \\  & (No) & Palm & 17-34 & 27.37\% \\ \hline \hline \end{tabular}
\end{table}
Table 4: SATNet vs. CNN+CL-STE

\begin{table}
\begin{tabular}{c|c|c|c|c|c} \hline \hline Method & Supervised & \(Acc_{wo}\) & \(Acc_{w}\) & time(m) \\ \hline Park’s CNN & Full & 0.94\% & 23.3\% & 163 \\ \hline Park’s CNN+NeurASP & No & 1.69\% & 66.5\% & 13230 \\ \hline Park’s CNN+CL-STE & No & 2.38\% & 93.7\% & 813 \\ \hline \hline \end{tabular}
\end{table}
Table 3: CNN, NeurASP, and CL-STE on Park 70k Sudoku dataset (80%/20% split) w/ and w/o inference trick
probabilities in \(\mathbf{X}_{s}\) in the same row/column/box must be 1":

\[L_{sum}=\sum_{\begin{subarray}{c}s\in\{1,\dots,32\}\\ i\in\{row,col,box\}\end{subarray}}avg((sum(\mathbf{X}_{s}^{i})-1)^{2}).\]

Here, \(avg(X)\) and \(sum(X)\) compute the average and sum of all elements in \(X\) along its last dimension; \(\mathbf{X}_{s}^{row},\mathbf{X}_{s}^{col},\mathbf{X}_{s}^{box}\in\mathbb{R}^{ 81\times 9}\) are reshaped copies of \(\mathbf{X}_{s}\) such that each row in, for example, \(\mathbf{X}_{s}^{row}\) contains 9 probabilities for atoms \(a(1,C,N),\dots,a(9,C,N)\) for some \(C\) and \(N\).

Figure 4 compares the test accuracy of the RRN trained for 100 epochs under 4 settings: (a) the RRN trained with baseline loss using 30k labeled data; (b) the RRN trained with both baseline loss and constraint losses (\(L_{sum}\), \(L_{cnf}\), and \(L_{bound}\)) using the same 30k labeled data; (c) the same setting as (b) with additional 30k unlabeled data; (d) same as (a) with additional 30k labeled data. Comparing (a) and (b) indicates the effectiveness of the constraint loss using the same number of labeled data; comparison between (b) and (c) indicates even with the same number of labeled data but adding unlabeled data could increase the accuracy (due to the constraint loss); comparison between (c) and (d) shows that the effectiveness of the constraint loss is comparable to adding additional 30k labels.

Figure 5 assesses the effect of constraint loss using fixed 10k labeled data and varying numbers (10k, 30k, 70k) of unlabeled data. We see that the baseline RRN trained with 10k labeled data ([10k L] RRN) has roughly saturated while the other methods are still slowly improving the accuracy. Training with the same number of labeled data but adding more unlabeled data makes the trained RRN achieve higher test accuracy, indicating that the constraint loss is effective in training even when the labels are unavailable.

### Discussion

Regarding **Q1**, Figure 3, Tables 1 and 2 show that our method achieves comparable accuracy with existing neuro-symbolic formalisms but is much more scalable. Regarding **Q2**, Table 3 and Figures 4 and 5 illustrate our method could be used for unsupervised and semi-supervised learning by utilizing the constraints underlying the data. Regarding **Q3**, we applied constraint loss to MLP, CNN, and GNN, and observed that it improves the existing neural networks' prediction accuracy.

As we noted, the gradient computation in other neuro-symbolic approaches, such as NeurASP, DeepProbLog, and NeuroLog, requires external calls to symbolic solvers to compute stable models or proofs for every data instance, which takes a long time. These approaches may give better quality gradients to navigate to feasible solutions, but their gradient computations are associated with NP-hardness (the worst case exponential size of SDD, computing all proofs or stable models). In comparison, CL-STE treats each clause independently and locally to accumulate small pieces of gradients, allowing us to leverage GPUs and batch training as in the standard deep learning. The method resembles local search and deduction in SAT, and the gradients may not reflect the global property but could be computed significantly faster. Indeed, together with the gradient signals coming from the data, our method works well even when logical constraints are hard to satisfy, e.g., in training a neural network to solve Sudoku where a single feasible solution lies among \(9^{47}\) to \(9^{64}\) candidates when 17-34 digits are given.

## 6 Conclusion

Constraint loss helps neural networks learn with fewer data, but the state-of-the-art methods require combinatorial computation to compute gradients. By leveraging STE, we demonstrate the feasibility of more scalable constraint learning in neural networks. Also, we showed that GNNs could learn with fewer (labeled) data by utilizing known constraints. Based on the formal properties of the CNF constraint loss and the promising initial experiments here, the next step is to apply the method to larger-scale experiments.

## Acknowledgements

We are grateful to Adam Ishay and the anonymous referees for their useful comments. This work was partially supported by the National Science Foundation under Grant IIS-2006747.

Figure 4: Test accuracy on the same randomly sampled 1k data from Palm Sudoku dataset when trained with RRN(+STE) with 30k to 60k [L]abeled/[U]nlabeled data

Figure 5: Semi-supervised learning with RRN+STE on Sudoku using only 10k labeled data and varying numbers of unlabeled data from Palm dataset for training and using the same randomly sampled 1k data for testing