# DeepSaDe: Learning Neural Networks that Guarantee Domain Constraint
Satisfaction

Kshitij Goyal1, Sebastijan Dumancic2, Hendrik Blockeel1

###### Abstract

As machine learning models, specifically neural networks, are becoming
increasingly popular, there are concerns regarding their trustworthiness,
especially in safety-critical applications, e.g., actions of an autonomous
vehicle must be safe. There are approaches that can train neural networks
where such domain requirements are enforced as constraints, but they either
cannot guarantee that the constraint will be satisfied by all possible
predictions (even on unseen data) or they are limited in the type of
constraints that can be enforced. In this work, we present an approach to
train neural networks which can enforce a wide variety of constraints and
guarantee that the constraint is satisfied by all possible predictions. The
approach builds on earlier work where learning linear models is formulated as
a constraint satisfaction problem (CSP). To make this idea applicable to
neural networks, two crucial new elements are added: constraint propagation
over the network layers, and weight updates based on a mix of gradient descent
and CSP solving. Evaluation on various machine learning tasks demonstrates
that our approach is flexible enough to enforce a wide variety of domain
constraints and is able to guarantee them in neural networks.

##  1 Introduction

Widespread use of state-of-the-art machine learning (ML) techniques has given
rise to concerns regarding the trustworthiness of these models, especially in
safety-critical and socially-sensitive domains. For example, in autonomous
vehicles that employ ML approaches to predict the next action, the actions
must be safe. Such domain requirements can often be formulated as logical
constraints on combinations of inputs and outputs (e.g., whenever the input
satisfies some condition A, the output must satisfy condition B). Crucially,
these domain constraints must be satisfied for all possible inputs to the
model, not just the training data. This has motivated researchers to develop
approaches that can train models that satisfy a given constraint for all
possible predictions.

A general approach to enforcing constraints in ML models is to include a
regularization term in the cost function, which typically adds a cost for
every violation of a constraint in the training set (e.g., Xu et al. (2018);
Diligenti, Gori, and Sacca (2017)). Such an approach can reduce the number of
violations in the training set, but it does not necessarily eliminate them.
Moreover, even when it does, this does not guarantee that other instances
(outside the training set) cannot violate the constraint. Alternatively, for
some model types, such as neural networks, the architecture of the model can
be chosen in such a way that certain types of constraints are guaranteed to be
satisfied for each possible input (not just training data) (Sivaraman et al.
2020; Hoernle et al. 2022). But this is typically possible only for specific
combinations of model and constraint types.

This raises the question of whether generality and certainty can be combined.
Is it possible to come up with a generally applicable approach that guarantees
the satisfaction of constraints not only on the training set but on the entire
input space, and this for any kind of model? A step in this direction was made
by Goyal, Dumancic, and Blockeel (2023), who propose a relatively general
solution for linear models. Their approach translates the learning problem
into a MaxSMT setting. MaxSMT stands for Maximum Satisfiability Modulo
Theories. It is an extension of SAT solving that can take background theories
into account (e.g., for reasoning about the real numbers) and that
distinguishes soft and hard constraints: it returns a solution that satisfies
all hard constraints and as many soft constraints as possible. Goyal,
Dumancic, and Blockeel (2023) model the requirements as hard constraints and
maximize the fit to the data using soft constraints. Their approach works for
a wide range of constraint types but only handles linear models, and assumes a
bounded input domain.

In this paper, we substantially extend the applicability of that approach by
showing how it can be used to train feedforward neural networks. Two key
modifications to the network’s architecture and training procedure suffice for
achieving this: (1) propagating the constraints over the network layers to the
last layer, which involves adding skip connections (He et al. 2016) that copy
the input to the penultimate layer and deriving bounds on the penultimate
layer from the bounds on the input (Sunaga 1958), and (2) training the network
using a hybrid procedure that uses MaxSMT to determine the weights in the
output layer and gradient descent for all other weights. We demonstrate that
with these changes, neural networks can be trained that have good performance
and guarantee the satisfaction of given constraints. In the following, we
first describe the problem setting, then briefly describe the existing
approach that we build on, before detailing our approach. Afterward, we
compare our approach to related work and evaluate it experimentally.

##  2 Problem Statement

In this paper, we focus on semantic constraints which constrain the behavior
of the model: the predictions are required to adhere to certain requirements,
e.g. safety constraints (Katz et al. 2017), structured output constraints (Xu
et al. 2018), and hierarchical constraints (Hoernle et al. 2022).
Specifically, we focus on domain constraints: constraints that must hold for
all instances in the domain. We assume the constraints can be written with
universally quantified logic formulas. In particular, we consider the
constraints of form:

$\text{K}:\forall{\bf x}\in\bigtimes_{i=1}^{n}[l_{i},u_{i}],{\bf x}\models
P\Rightarrow f_{{\bf w}}({\bf x})\models C$ (1)

Which states that if an input ${\bf x}$ satisfies a condition $P$, the output
must satisfy a condition $C$. An example of a safety constraint that can be
represented in this way is: “if an object comes in front of a moving vehicle,
the vehicle must stop”. Solving for such a constraint exactly using specific
constraint solvers allows us to enforce the constraint for all possible
inputs. The reason for focusing on this type of constraint is mostly
practical: the constraint-solving technology we use was found to scale well
enough for these types of constraints. It is not a theoretical limitation: any
constraint that can be handled effectively by current constraint-solving
technology can be handled by the approach we develop. As demonstrated later in
section 6, our chosen constraint formulation (equation 1) already provides us
with a variety of tasks to work with.

To make the search procedure tractable, and because features in ML problems
are typically bounded (e.g., a pixel in an image takes a value in $[0,255]$),
we use bounded domains $\bigtimes_{i=1}^{n}[l_{i},u_{i}]$ instead of
$\mathbb{R}^{n}$. As a natural choice, the training data
$D\subseteq\mathcal{X}\bigtimes\mathcal{Y}$ can be used to calculate these
bounds, i.e. $l_{i}=\min_{D}({\bf x}_{i})$ & $u_{i}=\max_{D}({\bf x}_{i})$. We
rely on the SMT solver Z3 (Moura and Bjørner 2008) to solve such constraints.
Other prominent constraint-solving paradigms like MILP and CP do not support
such constraints over continuous domains (Nethercote et al. 2007).

We are now ready to formulate our problem statement:

######  Definition 2.1.

Learning problem. Given a training set
$D\subseteq\mathcal{X}\bigtimes\mathcal{Y}$, a set of domain constraints
$\mathcal{K}$, a loss function $\mathcal{L}$, and a hypothesis space
containing functions $f_{\bf w}:\mathcal{X}\rightarrow\mathcal{Y}$; find ${\bf
w}$ such that $f_{{\bf w}}$ satisfies constraints in $\mathcal{K}$ and
$\mathcal{L}(f_{\bf w},D)$ is minimal among all such $f_{{\bf w}}$.

$f_{\bf w}$ is assumed to be a feedforward neural network. The output layer is
real-valued without any activation, and a softmax layer is used to calculate
class probabilities for classification problems. The language of the
constraints in $\mathcal{K}$ is a subset of first-order logic which allows for
universal quantifiers. In practice, we focus on the constraints of the form in
equation 1, and $\mathcal{K}$ can be a set of multiple such universally
quantified constraints.

##  3 Background - Satisfiability Descent (SaDe)

Satisfiability (SAT) is the problem of finding a solution that satisfies a
given Boolean formula, e.g. $\neg a\lor b$. Satisfiability Modulo Theories
(SMT) extend SAT such that formulas can be expressed in other theories, such
as Real Arithmetic, e.g., $(a+b>3)\wedge(b<1)$ with real $a$ and $b$. Maximum
Satisfiability (MaxSMT) generalizes the SMT problem: given a set of hard
constraints $\mathcal{H}$ and soft constraints $\mathcal{S}$, it aims to find
a solution that satisfies all constraints in $\mathcal{H}$ and as many as
possible in $\mathcal{S}$.

Our work builds on SaDe (Goyal, Dumancic, and Blockeel 2023) which is a
learning algorithm that can enforce constraints in linear models and guarantee
satisfaction. SaDe modifies the parameter update process of the mini-batch
gradient descent (Goodfellow et al. 2016). Unlike gradient descent, which
updates the solution in the direction that minimizes the loss, SaDe solves a
MaxSMT problem to find the solution at each iteration, which is formulated in
such a way that its solution satisfies the domain constraint and is close to
the solution that gradient descent might lead to. At each iteration, a local
search space is defined for the MaxSMT problem around the previous solution.
This search space is a fixed-sized n-cube where each edge of the n-cube is a
hyperparameter called maximal step size that upper bounds the size of the
update in each dimension (illustrated for two parameters in figure 1(a)). SaDe
iteratively improves the performance while learning solutions that satisfy the
constraint. Formulations of the MaxSMT problem and the local search space at
each iteration are provided next.

Formulation of MaxSMT problem: A MaxSMT problem is defined for a batch of
instances in each iteration, where the soft constraints encode a certain
quality of fit of the model on the instances in the batch, and the domain
constraints are hard constraints.

A soft constraint, for a given instance $({\bf x},y)$, is defined as a logical
constraint that is fulfilled when the prediction of the model $f_{\bf w}$ for
${\bf x}$ is “sufficiently consistent” with the true label $y$. For
regression, given some error $e$, a soft constraint is defined as: $|y-e|\leq
f_{\bf w}({\bf x})\leq|y+e|$. For classification, the sign of $f_{\bf w}({\bf
x})$ is assumed to be the indicator of the class and the magnitude indicates
the certainty of prediction, the soft constraint takes the form (for a
threshold $\tau$):

$\displaystyle f_{\bf w}({\bf x})>\text{ }\tau\qquad\text{if $y=1$}$
$\displaystyle f_{\bf w}({\bf x})<-\tau\qquad\text{if $y=-1$}$

For each instance, multiple soft constraints are formulated for different
values of the error $e$ or threshold $\tau$. Satisfying a maximum of these
soft constraints, which is what the MaxSMT problem tries to achieve,
correlates with minimizing the prediction loss. Thus, the solution to this
MaxSMT problem at every iteration reduces the loss while satisfying the domain
constraints.

Local search space: At every iteration, the MaxSMT problem searches for the
next solution in a local search space defined by the n-cube around the
previous solution. It is encoded as an additional hard constraint in the
MaxSMT problem, with a “box” constraint, which states that the next solution
must be inside the axis-parallel box defined by $\hat{{\bf w}}$ and $\hat{{\bf
w}}-\alpha\cdot\mbox{sgn}({\bf g})$, where the sign function is applied
component-wise to a vector (a modified sign function is used where
sgn$(0)=1$), $\hat{{\bf w}}$ is the previous solution, ${\bf g}$ is the
gradient of the loss at $\hat{{\bf w}}$, and $\alpha$ is the maximal step
size. The box constraint serves two important purposes. Firstly, it provides a
general direction in which the loss is minimized, as the box in each dimension
is aligned with the negative gradient. Secondly, it stabilizes learning by
limiting the size of the updates. Interestingly, using a regularized loss
instead of a standard loss doesn’t make a difference, as the constraint
remains fulfilled throughout the training steps. With regularization, the
regularization factor only becomes active if an instance violates the
constraint. However, in SaDe, this never happens during the learning process,
making the regularization always $0$.

SaDe is limited to training linear models. Training neural networks with the
same procedure would require solving the MaxSMT problem with highly non-linear
soft constraints, e.g. $|y-e|\leq f_{\bf w}({\bf x})\leq|y+e|$ where $f_{\bf
w}({\bf x})$ is the network, which is not possible with state-of-the-art SMT
solvers.

Figure 1:  (a.) Illustration of SaDe: each grey quadrant represents the local
search space for the MaxSMT problem (maximal step size: $\alpha$), defined by
the gradients of the loss, the green points are the solutions found with
MaxSMT; (b.) DeepSaDe Architecture: Last layer is updated using the MaxSMT
framework and the layers before are updated with gradient descent. The input
features relevant to the domain constraint (in green) are mapped to the
penultimate layer via skip connections.

##  4 DeepSaDe: Deep Satisfiability Descent

We now present our approach DeepSaDe, which utilizes the MaxSMT framework
proposed in Goyal, Dumancic, and Blockeel (2023) to train neural networks with
constraints. DeepSaDe exploits the structure of neural networks, which
transform the input domain through a series of non-linear layers before a
final linear layer maps it to the output. As the network output only
explicitly depends on the last layer, enforcing the constraint on the last
layer is sufficient to enforce the constraint on the network. DeepSaDe,
therefore, uses batch learning with a hybrid procedure that uses MaxSMT to
determine the weights in the last layer and gradient descent for all other
weights. In the following, we introduce some notation before we formalize the
MaxSMT problem in the last layer, and then detail the learning algorithm.

$f_{\bf w}$ is a fully-connected neural network with $k$ layers such that
$f_{\bf w}({\bf x})=h_{k}(h_{k-1}(...h_{1}({\bf x})...))$ for input ${\bf
x}\in\mathcal{X}$, where $h_{n}$ is the $n^{th}$ layer. The input to the
$n^{th}$ layer is ${\bf x}^{(n)}=h_{n-1}(...h_{1}({\bf x})...)$, where ${\bf
x}^{(1)}={\bf x}$ and the latent input space for the $h_{n}$ is represented by
$\mathcal{X}^{(n)}$, where $\mathcal{X}^{(1)}=\mathcal{X}$. The size of a
layer, $|h_{n}|$, is the number of neurons in it. Weight and bias parameters
of $h_{n}$ are denoted by matrices $W^{(n)}$ and $B^{(n)}$ of dimensions
$|h_{n-1}|\times|h_{n}|$ and $1\times|h_{n}|$ respectively ($|h_{0}|=|{\bf
x}^{(1)}|$). Elements of $W^{(n)}$ and $B^{(n)}$ are referred with lower-case
letters.

### Formulation of the maximum satisfiability problem at the last layer of the
network

To formalize the MaxSMT problem for the last layer, it is necessary to express
both the soft constraints and the hard constraint (domain constraint) in terms
of the latent inputs ${\bf x}^{(k)}$ rather than the original inputs ${\bf
x}^{(1)}$. The soft constraint at the last linear layer can be formulated in a
similar way to what was presented in section 3. Specifically, for a regression
task, the constraint is given by $|y-e|\leq h_{k}({\bf x}^{(k)})\leq|y+e|$,
whereas for classification, it takes the form of:

$\displaystyle h_{k}({\bf x}^{(k)})>\text{ }\tau\qquad\text{if $y=1$}$
$\displaystyle h_{k}({\bf x}^{(k)})<-\tau\hskip 14.0pt\text{if $y=-1$}$

To formulate the hard domain constraints, we propose a method for translating
each original constraint K (equation 1) into a constraint K’ for the MaxSMT
problem at the last layer, given the parameters of layers
$h_{1},\ldots,h_{k-1}$, such that a solution to K’, combined with
$h_{1},\ldots,h_{k-1}$, is a solution to K.

$\text{K}^{\prime}:\forall{\bf
x}^{\prime}\in\bigtimes_{i=1}^{|h_{k-1}|}[l^{(k)}_{i},u^{(k)}_{i}],{\bf
x}^{\prime}\models P\Rightarrow h_{k}({\bf x}^{\prime})\models C$ (2)

Here ${\bf x}^{\prime}$ represent the quantified latent variable in the domain
of $\mathcal{X}^{(k)}$ bounded by
$\bigtimes_{i=1}^{|h_{k-1}|}[l^{(k)}_{i},u^{(k)}_{i}]$. We explain how this
translation is achieved in the next two paragraphs. Given a network, with this
translation, the last layer of a network can be updated to satisfy the
constraint by the network.

Domain Bound Propagation: To formulate $\text{K}^{\prime}$, we first consider
the bounds of the quantified variable for the latent space of
$\mathcal{X}^{(k)}$. The bounds of the latent space must be such that
enforcing the constraint within these bounds enforces the constraint on the
original input bounds. To construct such latent bounds, we rely on interval
arithmetic (Sunaga 1958). This involves calculating the bounds of the output
of a layer based on the bounds of the input and the layer parameters, such
that any input to the layer takes the output value within the output bounds.
Given the lower and upper bounds $l^{(n)}$ and $u^{(n)}$ for the input ${\bf
x}^{(n)}$ of the layer $h_{n}$, following the approach used in Gowal et al.
(2018), the bounds for the output ${\bf x}^{(n+1)}$ are computed as (more
details in Appendix A.1):

$\begin{split}l^{(n+1)}_{i}=\text{act}(b^{(n)}_{i}+\sum_{j:w^{(n)}_{j,i}\geq
0}w^{(n)}_{j,i}l^{(n)}_{j}+\sum_{j:w^{(n)}_{j,i}<0}w^{(n)}_{j,i}u^{(n)}_{j})\\\
u^{(n+1)}_{i}=\text{act}(b^{(n)}_{i}+\sum_{j:w^{(n)}_{j,i}\geq
0}w^{(n)}_{j,i}u^{(n)}_{j}+\sum_{j:w^{(n)}_{j,i}<0}w^{(n)}_{j,i}l^{(n)}_{j})\end{split}$

Where ‘act’ is the activation function (like ReLu, Sigmoid, and Tanh). Given
the bounds of the input space, the bounds for the latent space
$\mathcal{X}^{(k)}$ can be calculated recursively. Enforcing a constraint
within the latent bounds enforces the constraint on any input within the input
bounds.

Identity Mapping of Relevant Features: The translation also takes into account
that some domain constraints may be dependent on the input space, e.g., “if an
object comes in front of the vehicle, the vehicle must stop”. To encode such
conditions in $\text{K}^{\prime}$ (i.e., ${\bf x}^{\prime}\models P$), we make
the relevant features, i.e. the features that are needed to encode the
property $P$, available at the latent space $\mathcal{X}^{(k)}$. For this, we
use skip-connections (He et al. 2016) that map these features to the second to
last layer $h_{k-1}$ using an identity mapping, as illustrated in figure 1(b).
The network, consequently, is no longer fully-connected and these features
take the same value as the input. These mapped features become a part of
$\mathcal{X}^{(k)}$ and the input property can be expressed at the last layer.
These features are identified in advance. Finally, as the output of the
network is the same as the output of the last layer, the constraint on the
network output can be encoded with $h_{k}({\bf x}^{\prime})$. This completes
the formulation of $\text{K}^{\prime}$.

Algorithm 1 Deep Satisfiability Descent (DeepSaDe)

input: training data $D$, validation data $V$, domain constraints
$\mathbf{\mathcal{K}}$, batch size $b$, epochs $e$, loss $\mathcal{L}$,
maximal step size $\boldsymbol{\alpha}$, learning rate $\boldsymbol{\eta}$,
line search steps $\mathbf{s}$

1: $f_{\hat{W}}(.)$: Model initialized with a standard approach

2: $\mathcal{K^{\prime}}$ = TranslateDomainConstraint($\mathcal{K}$,
$f_{\hat{W}}(.)$)

3: Update $\hat{W}$ such that $\hat{W}^{(k)}\models\mathcal{K^{\prime}}$

4: restart = False; $\hat{W}_{out}$ = undefined; Partition $D$ into batches of
size $b$

5: for each epoch do

6: for each batch $B$ in $D$ do

7: ${\mathcal{G}}=\nabla\mathcal{L}(\hat{W})$

8: $\mathcal{K^{\prime}}$ = TranslateDomainConstraint($\mathcal{K}$,
$f_{\hat{W}}(.)$)

9: if restart then

10: Randomly flip the sign of each element of $\mathcal{G}^{(k)}$

11: end if // try line search, if no solution use MaxSMT

12: let $W_{i}=\hat{W}^{(k)}-\eta\mathcal{G}^{(k)}i/s$, for $i=1,2,\ldots,s$

13: if $\\{i\,|\,W_{i}\models\mathcal{K^{\prime}}\\}\not=\emptyset$ then

14: $\hat{W}^{(k)}=\hat{W}_{\max\\{i\,|\,W_{i}\models\mathcal{K^{\prime}}\\}}$

15: else

16: ${\mathcal{G}_{S}}=sgn({\mathcal{G}^{(k)}})$

17: $\mathcal{S}$ = SoftConstraints($h_{k-1}(...h_{1}(B)...)$)

18:
$\mathcal{H}=\\{W^{(k)}\in\text{Box}(\hat{W}^{(k)},\hat{W}^{(k)}-\alpha\mathcal{G}_{S})\\}\cup\mathbf{\mathcal{K^{\prime}}}$
// assuming MaxSMT returns undefined if unsat

19: $\hat{W}^{(k)}=$ MaxSMT$(\mathcal{S},\mathcal{H})$

20: end if// no solution found, restart in another direction

21: if $\hat{W}^{(k)}\text{ is undefined}$ then

22: restart = True

23: else

23: // remember best solution found

24: if $eval(f_{\hat{W}},V)>eval(f_{\hat{W}_{out}},V)$ then

25: $\hat{W}_{out}=\hat{W}$

26: end if// perform gradient descent on earlier layers

27: for $n=1,...,k-1$ do

28: $W^{(n)}=\hat{W}^{(n)}-\eta*\mathcal{G}^{(n)}$

29: end for

30: restart = False

31: end if

32: end for

33: end for

34: return $f_{\hat{W}_{out}}(.)$

### Learning Algorithm

We now present the algorithm while referring to the pseudo-code in algorithm
1. DeepSaDe modifies mini-batch gradient descent (Goodfellow et al. 2016),
where forward and backward passes at every iteration (lines 5-7) are kept the
same, but the parameter update is split into two parts. First, only the last
layer’s parameters are updated to satisfy the domain constraint using the
MaxSMT formulation presented earlier (lines 8-23) (details in next paragraph).
Second, the earlier layers are updated using gradient descent to optimize
predictive loss (lines 27-29). Importantly, after the latter update, the
network does not guarantee constraint satisfaction due to changes in the
latent space of the last layer, used to formulate the MaxSMT problem.
Therefore, the network before the latter update is used for evaluation and a
validation set is used to select the best model (lines 24-26).

For updating the last layer, first, a line search is used along the vector
that minimizes the prediction loss, and a fixed number of candidate solutions,
from furthest to closest, are checked if they satisfy $\mathcal{K^{\prime}}$
and first one that does is picked (lines 12-14). If this search does not yield
a solution, the MaxSMT problem is formulated based on the inputs to the last
layer, and a solution is searched in the local search space around the
previous solution defined based on the gradients calculated during the
backward pass (lines 16-19) (similar to the approach in SaDe). Line search is
employed first because checking if a point satisfies a constraint is faster
than searching for the solution in a domain, finding a solution by merely
checking a few candidate points speeds up learning.

Sometimes a solution for the last layer cannot be found because the MaxSMT
problem could not be solved within the local search space, possibly due to the
gradient pointing to a solution space that violates the constraint. In such
cases, a restart procedure is initiated where the signs of the gradients are
randomly flipped (lines 9-11, 21-23) to randomize the direction of the update.
This may slightly decrease predictive performance, but it effectively restarts
the learning process when it gets stuck.

Since our approach is iterative, starting from an initial configuration that
satisfies the domain constraint is crucial. Otherwise, we may begin in a
solution space far from the constrained space, leading to no updates. We
ensure this by first initializing the network using a standard method (He et
al. 2015) (line 1), and then updating the weights of the last layer that
satisfy the translated constraint $\mathcal{K^{\prime}}$ (lines 2-3). It is
important to note that we are solving a satisfiability problem here, not the
maximum satisfiability problem, as we are not using any soft constraints for
this purpose.

##  5 Related Work

A standard approach for enforcing constraints in ML models is regularization,
where a penalty is added to the prediction loss whenever the model makes a
prediction that violates the constraint
($(1-\lambda)*\text{loss}+\lambda*\text{regularization}$). Xu et al. (2018)
propose a regularization defined on the weighted model count (WMC) (Chavira
and Darwiche 2008) of the constraint defined over the network output.
Diligenti, Gori, and Sacca (2017) and Serafini and Garcez (2016) propose a
fuzzy logic-based regularization for constraints in first-order logic. There
are many other regularization approaches in the literature, e.g. Fischer et
al. (2019), Hu et al. (2016), Stewart and Ermon (2017). Regularization can
enforce a variety of constraints, but does not guarantee constraint
satisfaction. Additionally, high regularization loss with a large value of
$\lambda$ may provide stronger constrain satisfaction but impacts the
predictive performance negatively.

Some approaches guarantee constraints by construction but are generally
limited to enforcing specific types of constraints. For example, monotonic
lattices (Gupta et al. 2016), deep lattice networks (You et al. 2017), and
COMET (Sivaraman et al. 2020) are approaches to enforce monotonicity in neural
networks; Leino et al. (2022) & Lin et al. (2020) propose approaches to
satisfy some safety specifications. A more general approach, MultiplexNet, was
proposed in Hoernle et al. (2022). They use a multiplexer layer to satisfy
constraints in disjunctive normal form (DNF). However, DNF representation is
limiting as certain constraints have worst-case representations in DNF which
may lead to exponentially many terms. Additionally, constraints conditioned on
the input space cannot be enforced. Another approach, DeepProbLog (Manhaeve et
al. 2018), trains neural networks within the ProbLog framework, where
constraints can be enforced with ProbLog. However, it is limited to modeling
discrete variables, and cannot model regression.

Our work relates to combinatorial optimization approaches as we use a MaxSMT-
based approach. These approaches, however, except Goyal, Dumancic, and
Blockeel (2023), are limited to discrete models like decision trees (Günlük et
al. 2021; Bertsimas and Dunn 2017; Verwer and Zhang 2019; Demirović et al.
2022) and decision sets (Yu et al. 2021; Ignatiev et al. 2021). Maximum
satisfiability, specifically, has also been used in various ML tasks (Berg et
al. 2019; Cussens 2012; Malioutov and Meel 2018). None of these, however,
focus on training neural networks.

There are approaches that rely on the idea of bound propagation, also used in
our work, to train adversarially robust neural networks (Gowal et al. 2018;
Zhang et al. 2019). However, the constraints that can be enforced are limited
to input-output bounds (if the input is in a given bound, the output should be
in a specific bound). Our approach is more general and can, in theory, handle
any constraint that can be written as an SMT formula.

Finally, there are approaches to verify if a network satisfies a constraint
(Katz et al. 2019; Wang et al. 2018; Bunel et al. 2018). DeepSaDe trains
models that do not require verification because constraints are guaranteed by
construction.

##  6 Experiments

We evaluate multiple use cases in various ML tasks with complex domain
constraints. We first outline the research questions, then describe the use
cases, our evaluation method, and finally the results.

  1. Q1: Can existing methods satisfy constraints for all predictions in practice, even if they don’t guarantee it?

  2. Q2: How does the predictive performance of DeepSaDe models compare to the baselines?

  3. Q3: Do the DeepSaDe models have a higher training time compared to the baselines?

### Use Cases

The selection of use cases is done in order to demonstrate the flexible
representation of constraints in DeepSaDe. The selected use cases tackle a
variety of learning problems and handle different types of constraints. We
consider constraints in the form presented in equation 1, where $P$ and $C$
are written as SMT formulas over
$\\{\forall,\exists,\lor,\land,\neg,\geq,\leq,=\\}$. In principle, any
constraint that can be written as an SMT formula and can be solved using
existing SMT solvers can be enforced using DeepSaDe. Use cases UC1, UC2 & UC3
are from Goyal, Dumancic, and Blockeel (2023), UC4 is novel, and UC5 is from
Xu et al. (2018).

UC1: A multi-target regression to predict 5 household expenses using 13
attributes, with 41417 data instances. We enforce two constraints: “sum of all
the expenses must be smaller than the total household income” and “going out
expense must be smaller than 5% of the household income”.

UC2: A binary classification problem of predicting if a person should be given
a loan or not based on 13 attributes, with 492 data instances. We enforce the
constraint: “a person with a salary less than 5000$ and an absent credit
history must be denied a loan”.

UC3: A multiclass classification problem to classify a song to one of 5 music
genres based on 13 attributes, with 793 data instances. We enforce the
constraint: “a song by ‘the Beatles’ must be classified as either rock or
pop”.

UC4: A multi-label classification problem of identifying the labels from a
sequence of 4 MNIST images. We enforce the constraint: “the sum of the
predicted labels must be greater than $10$”. 20000 instances are generated by
selecting 4 images at random from the MNIST dataset.

UC5: A preference learning problem to predict the preference order of
different sushi, with a constraint: “the prediction must have a coherent
preference order”. The preference order of 6 out of 10 sushi is used to
predict the preference order of the remaining 4 sushi. The dataset contains
4926 instances. The preference ordering over n items is encoded as a flattened
binary matrix $\\{X_{ij}\\}$ where $X_{ij}$ denotes that item $i$ is at
position $j$. Under this encoding, each instance has 36 features and 16
targets.

The use cases are intentionally designed with some training instances that
violate the constraints. While ‘fixing’ or ‘removing’ these violations might
be possible in certain cases (like UC2), it is not feasible with complex
constraints. For instance, in UC1, assume that there is a training instance
where the sum of expenses exceeds household income. Correcting this precisely
is problematic because it is unclear how much each expense should be reduced.
This issue gets tougher when dealing with multiple constraints. Additionally,
real-world scenarios might have violations that are hard to even identify,
such as using biased data in fairness-sensitive applications. Thus, we
evaluate DeepSaDe and the baselines in cases with such violations. More
information about the use cases is provided in Appendix A.2. Importantly, We
can only impose constraints explicitly based on model parameters: in the case
of a self-driving car (section 2), identifying pixels representing a moving
object is in itself a predictive task beyond our current scope. Thus, such
cases are not included and are left for future research.

UC | Approach | Constraint | AdI($\mathbf{\delta=0.1}$) | Accuracy/MSE | Training Time (sec)
---|---|---|---|---|---
UC1 | DeepSaDe | $\mathbf{100_{\pm 0}}$ | $\mathbf{0_{\pm 0}}$ | *$38.36_{\pm 4.59}$ | $102341_{\pm 40198}$
REG | $93.50_{\pm 2.01}$ | $0.97_{\pm 0.003}$ | *$\mathbf{30.50_{\pm 6.49}}$ | $227_{\pm 70}$
UC2 | DeepSaDe | $\mathbf{100_{\pm 0}}$ | $\mathbf{0_{\pm 0}}$ | $80.04_{\pm 4.29}$ | $447_{\pm 105}$
SL | $\mathbf{100_{\pm 0}}$ | $0.002_{\pm 0.006}$ | $\mathbf{80.17_{\pm 3.88}}$ | $45_{\pm 30}$
SBR | $\mathbf{100_{\pm 0}}$ | $0.002_{\pm 0.004}$ | $80.04_{\pm 3.95}$ | $45_{\pm 27}$
UC3 | DeepSaDe | $\mathbf{100_{\pm 0}}$ | $\mathbf{0_{\pm 0}}$ | $80.11_{\pm 4.99}$ | $6580_{\pm 1915}$
SL | $99.97_{\pm 0.03}$ | $0.42_{\pm 0.28}$ | $\mathbf{82.53_{\pm 3.58}}$ | $101_{\pm 45}$
SBR | $99.97_{\pm 0.05}$ | $0.29_{\pm 0.10}$ | $76.51_{\pm 7.50}$ | $196_{\pm 68}$
Table 1: Results: UC1, UC2 & UC3 (*MSE, lower MSE value is better) UC | Approach | Constraint | Coherent | Flattened | Jaccard | Training Time (sec)
---|---|---|---|---|---|---
UC4 | DeepSaDe | $\mathbf{100_{\pm 0}}$ | $6.62_{\pm 1.72}$ | $78.52_{\pm 1.73}$ | $62.97_{\pm 2.28}$ | $227928_{\pm 30559}$
FFN | $88.00_{\pm 3.26}$ | $\mathbf{23.94_{\pm 4.25}}$ | $\mathbf{85.81_{\pm 1.18}}$ | $\mathbf{71.55_{\pm 2.40}}$ | $3215_{\pm 2663}$
UC5 | DeepSaDe | $\mathbf{100_{\pm 0}}$ | $\mathbf{11.08_{\pm 2.61}}$ | $67.17_{\pm 1.48}$ | $\mathbf{25.94_{\pm 2.89}}$ | $17586_{\pm 5074}$
FFN | $0.04_{\pm 0.15}$ | $0.01_{\pm 0.04}$ | $\mathbf{75.69_{\pm 0.15}}$ | $13.04_{\pm 1.06}$ | $48_{\pm 10}$
SL | $\mathbf{100_{\pm 0}}$ | $4.06_{\pm 3.33}$ | $63.16_{\pm 2.62}$ | $18.08_{\pm 3.33}$ | $298_{\pm 110}$
Table 2: Results: UC4 & UC5

### Evaluation Methodology

Evaluation: Constraint satisfaction is typically evaluated by the constraint
accuracy metric used in Xu et al. (2018) and Fischer et al. (2019), which
corresponds to the percent of instances where the constraint is not violated
by the prediction. Such an evaluation, however, is limited to a finite sample
of the population. Hence, as a second measure, we also calculate the Adversity
Index (AdI) ((Goyal, Dumancic, and Blockeel 2023)), which is the fraction of
instances for which a counter-example to the constraint can be constructed in
the neighborhood, defined by an $l_{\infty}$ ball of radius $\delta$ around
the instance. AdI takes a value between 0 and 1, a higher value of AdI implies
that the model violates the constraint on more points similar to data
instances. AdI is calculated on full data (training and test) because this
provides more instances to evaluate constraint satisfaction; we want the
constraints to be satisfied on all data, not only test data. For DeepSaDe,
both constraint accuracy and AdI are zero by construction but we still
calculate it as a sanity check. We use the neural network verification
software Marabou ((Katz et al. 2019)) to find counter-examples. However, we
only compute the AdI for UC1-3 because Marabou only handles inequality
constraints and is not suitable for UC4-5.

For predictive performance, we use MSE for UC1 and accuracy for UC2-3. For
UC4-5, we use coherent accuracy which is the fraction of instances for which
the model predicts the entire configuration correctly, flattened accuracy
which is the fraction of individually correct binary labels, and the Jaccard
accuracy which is the average Jaccard index for each multi-label prediction
compared to true labels. Performance is only evaluated for instances where the
true label does not violate the constraint as there can be data instances in
practice where this happens and a comparison with such instances makes the
evaluation biased.

Baselines: For UC2 and UC3, we use regularization baselines based on Xu et al.
(2018) (SL) and Diligenti, Gori, and Sacca (2017) (SBR). For UC1, we design a
custom regularization loss REG (details in appendix A.2). For UC4, we could
not find any approaches that can enforce such a constraint. Hence, we simply
compare it with a feedforward network (FFN). For UC5, we choose SL and FFN as
baselines. In Goyal, Dumancic, and Blockeel (2023), the authors use a post-
processing baseline to enforce constraints at inference time. This type of
baseline is excluded from our evaluation because, as also noted by Goyal,
Dumancic, and Blockeel (2023), this baseline is only applicable when the
constraints are simple and not a generally applicable method.

Experimental Setup: For solving the MaxSMT problem, we implement the Fu-Malik
algorithm ((Fu and Malik 2006)) over the Z3 solver for NRA (Quantified
Nonlinear Real Arithmetic) formulas. We ran experiments on an Intel(R) Xeon(R)
Silver 4214 CPU @ 2.20GHz machine with 125 GB RAM. For each use case, we run 5
experiments with 5-fold cross-validation, and the data is split 70/20/10 into
train/test/validation. Every feature is scaled in [0, 1], and the radius
$\delta=0.1$ is chosen for AdI, which is significantly smaller than the mean
$\ell_{\infty}$ distance between two points: this distance for UC1 is $0.75$,
for UC2 is $0.97$, and for UC3 is $0.89$. For regularization, the smallest
value of $\lambda$, in $[0,1]$, that leads to minimum violations on the
validation set is selected via cross-validation. Refer to appendix A.2 for
details on the architectures and hyper-parameters.

### Results (Tables 1 & 2)

Constraint Satisfaction: DeepSaDe finds a model that achieves 100% constraint
accuracy for each use case and AdI = 0 for UC1-3. For UC1, the constraint
accuracy for REG is 93.5%, and counterexamples can be constructed close to 97%
of the instances (AdI = 0.97). Similar behavior is seen for UC3 for both SL
and SBR, with SBR proving to be more effective in enforcing constraints
because of lower AdI. For UC2, SL and SBR both lead to 100% constraint
accuracy, but counterexamples can still be constructed as AdI $>0$. For UC4
and UC5, FFN fails to satisfy constraints on test set. For UC5, SL can satisfy
the constraint but the predictive performance is much worse than DeepSaDe.
Thus, in general, the baselines, in contrast to DeepSaDe, do not satisfy
domain constraint satisfaction, which answers Q1.

Predictive Performance: DeepSaDe treats the domain constraint as a hard
constraint, which limits the solution space to the regions where the
constraint is guaranteed. Thus, the predictive performance of DeepSaDe models
can be worse than existing approaches which do not guarantee constraint
satisfaction. For UC1, the predictive performance of DeepSaDe is slightly
worse than REG, while the difference is not statistically significant for UC2
& UC3. The performance of DeepSaDe is worse for UC4 on all prediction metrics
compared to FFN. For UC5, SL regularization with a high value of $\lambda$
allows for satisfying all the constraints on the test set but performs much
worse than DeepSaDe. To study this further, we plot the prediction loss
(cross-entropy) for SL models on the test set for various $\lambda$ between
$0$ and $0.9$, averaged over 5 folds, in Figure 2. For comparison, the average
loss for DeepSaDe is also plotted. DeepSaDe achieves constraint satisfaction
in addition to having better performance than SL with a high $\lambda$. High
regularization makes the prediction loss insignificant compared to the
regularization loss, leading to worse predictive performance.

Figure 2: Test loss for UC5

In DeepSaDe, at every iteration, the solver tries to satisfy as many soft
constraints as possible in addition to satisfying the domain constraints.
DeepSaDe, thus, is a more stable learner compared to regularization with high
$\lambda$. This answers Q2. Although the constraint satisfaction with DeepSaDe
comes at the cost of predictive performance in some cases, in applications
where constraints are crucial, like in safety-critical domains, this may be
acceptable.

Training Time: DeepSaDe requires between 10 to 500 times more time than
baselines across use cases. This is because DeepSaDe solves a MaxSMT problem
at each iteration, which makes the training slower than the numerical updates
in the baselines. This positively answers Q3. In applications where
constraints are imperative, training time is less relevant, e.g., a network
trained over a week and guarantees safety is still more valuable to the
autonomous vehicle compared to one trained for a few hours but cannot do so.
Our work is a starting point of such an approach that combines the exact
solving of quantifiers with gradient-based learning. With further research
into solver technology, it can be made more scalable. Additionally, possible
modifications to improve the efficiency of DeepSaDe include using an
incomplete MaxSMT approach like stochastic local search (Morgado et al. 2013)
instead of a complete one like Fu-Malik, and using compact latent bounds (Wang
et al. 2018).

##  7 Conclusion

We introduced DeepSaDe, a method for training feedforward neural networks to
satisfy a range of constraints through a combination of a satisfiability
framework and gradient-based optimization. DeepSaDe effectively addresses
various ML tasks and offers adaptable constraint representation, although
sometimes with a performance trade-off. It enforces any constraint in an SMT
formula, feasible for the solver. While Z3 is our current solver, our
framework is adaptable to any MaxSMT solver handling universally quantified
constraints. We believe that evolving solver capabilities will allow DeepSaDe
to handle more complex constraints. Extension of DeepSaDe to other
architectures (e.g. CNNs) is left for future work.

##  8 Acknowledgement

This research was jointly funded by the Flemish Government (AI Research
Program) and the Research Foundation - Flanders under EOS No. 30992574.

## References

  * Berg et al. (2019) Berg, O. J.; Hyttinen, A. J.; Järvisalo, M. J.; et al. 2019.  Applications of MaxSAT in data analysis.  _Pragmatics of SAT_.
  * Bertsimas and Dunn (2017) Bertsimas, D.; and Dunn, J. 2017.  Optimal classification trees.  _Machine Learning_ , 106(7): 1039–1082.
  * Bunel et al. (2018) Bunel, R. R.; Turkaslan, I.; Torr, P.; Kohli, P.; and Mudigonda, P. K. 2018.  A unified view of piecewise linear neural network verification.  _Advances in Neural Information Processing Systems_ , 31.
  * Chavira and Darwiche (2008) Chavira, M.; and Darwiche, A. 2008.  On probabilistic inference by weighted model counting.  _Artificial Intelligence_ , 172(6-7): 772–799.
  * Cussens (2012) Cussens, J. 2012.  Bayesian network learning by compiling to weighted MAX-SAT.  _arXiv preprint arXiv:1206.3244_.
  * Demirović et al. (2022) Demirović, E.; Lukina, A.; Hebrard, E.; Chan, J.; Bailey, J.; Leckie, C.; Ramamohanarao, K.; and Stuckey, P. J. 2022.  MurTree: Optimal Decision Trees via Dynamic Programming and Search.  _Journal of Machine Learning Research_ , 23(26): 1–47.
  * Diligenti, Gori, and Sacca (2017) Diligenti, M.; Gori, M.; and Sacca, C. 2017.  Semantic-based regularization for learning and inference.  _Artificial Intelligence_ , 244: 143–165.
  * Fischer et al. (2019) Fischer, M.; Balunovic, M.; Drachsler-Cohen, D.; Gehr, T.; Zhang, C.; and Vechev, M. 2019.  Dl2: Training and querying neural networks with logic.  In _International Conference on Machine Learning_ , 1931–1941. PMLR.
  * Fu and Malik (2006) Fu, Z.; and Malik, S. 2006.  On solving the partial MAX-SAT problem.  In _International Conference on Theory and Applications of Satisfiability Testing_ , 252–265. Springer.
  * Goodfellow et al. (2016) Goodfellow, I.; Bengio, Y.; Courville, A.; and Bengio, Y. 2016.  _Deep learning_ , volume 1.  MIT Press.
  * Gowal et al. (2018) Gowal, S.; Dvijotham, K.; Stanforth, R.; Bunel, R.; Qin, C.; Uesato, J.; Arandjelovic, R.; Mann, T.; and Kohli, P. 2018.  On the effectiveness of interval bound propagation for training verifiably robust models.  _arXiv preprint arXiv:1810.12715_.
  * Goyal, Dumancic, and Blockeel (2023) Goyal, K.; Dumancic, S.; and Blockeel, H. 2023.  Sade: Learning models that provably satisfy domain constraints.  In _Machine Learning and Knowledge Discovery in Databases: European Conference, ECML PKDD 2022, Grenoble, France, September 19–23, 2022, Proceedings, Part V_ , 410–425. Springer.
  * Günlük et al. (2021) Günlük, O.; Kalagnanam, J.; Li, M.; Menickelly, M.; and Scheinberg, K. 2021.  Optimal decision trees for categorical data via integer programming.  _Journal of global optimization_ , 81(1): 233–260.
  * Gupta et al. (2016) Gupta, M.; Cotter, A.; Pfeifer, J.; Voevodski, K.; Canini, K.; Mangylov, A.; Moczydlowski, W.; and Van Esbroeck, A. 2016.  Monotonic calibrated interpolated look-up tables.  _The Journal of Machine Learning Research_ , 17(1): 3790–3836.
  * He et al. (2015) He, K.; Zhang, X.; Ren, S.; and Sun, J. 2015.  Delving deep into rectifiers: Surpassing human-level performance on imagenet classification.  In _Proceedings of the IEEE international conference on computer vision_ , 1026–1034.
  * He et al. (2016) He, K.; Zhang, X.; Ren, S.; and Sun, J. 2016.  Deep residual learning for image recognition.  In _Proceedings of the IEEE conference on computer vision and pattern recognition_ , 770–778.
  * Hinton and Roweis (2002) Hinton, G. E.; and Roweis, S. 2002.  Stochastic neighbor embedding.  _Advances in neural information processing systems_ , 15.
  * Hoernle et al. (2022) Hoernle, N.; Karampatsis, R. M.; Belle, V.; and Gal, K. 2022.  Multiplexnet: Towards fully satisfied logical constraints in neural networks.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , 5700–5709.
  * Hu et al. (2016) Hu, Z.; Ma, X.; Liu, Z.; Hovy, E.; and Xing, E. 2016.  Harnessing deep neural networks with logic rules.  _arXiv preprint_.
  * Ignatiev et al. (2021) Ignatiev, A.; Lam, E.; Stuckey, P. J.; and Marques-Silva, J. 2021.  A scalable two stage approach to computing optimal decision sets.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , 3806–3814.
  * Katz et al. (2017) Katz, G.; Barrett, C.; Dill, D. L.; Julian, K.; and Kochenderfer, M. J. 2017.  Reluplex: An efficient SMT solver for verifying deep neural networks.  In _International conference on computer aided verification_ , 97–117. Springer.
  * Katz et al. (2019) Katz, G.; Huang, D. A.; Ibeling, D.; Julian, K.; Lazarus, C.; Lim, R.; Shah, P.; Thakoor, S.; Wu, H.; Zeljić, A.; et al. 2019.  The marabou framework for verification and analysis of deep neural networks.  In _International Conference on Computer Aided Verification_ , 443–452. Springer.
  * Leino et al. (2022) Leino, K.; Fromherz, A.; Mangal, R.; Fredrikson, M.; Parno, B.; and Păsăreanu, C. 2022.  Self-correcting Neural Networks for Safe Classification.  In _International Workshop on Numerical Software Verification, Workshop on Formal Methods for ML-Enabled Autonomous Systems_ , 96–130. Springer.
  * Lin et al. (2020) Lin, X.; Zhu, H.; Samanta, R.; and Jagannathan, S. 2020.  ART: abstraction refinement-guided training for provably correct neural networks.  In _# PLACEHOLDER_PARENT_METADATA_VALUE#_ , volume 1, 148–157. TU Wien Academic Press.
  * Malioutov and Meel (2018) Malioutov, D.; and Meel, K. S. 2018.  Mlic: A maxsat-based framework for learning interpretable classification rules.  In _CP_.
  * Manhaeve et al. (2018) Manhaeve, R.; Dumancic, S.; Kimmig, A.; Demeester, T.; and De Raedt, L. 2018.  Deepproblog: Neural probabilistic logic programming.  _Advances in Neural Information Processing Systems_ , 31.
  * Morgado et al. (2013) Morgado, A.; Heras, F.; Liffiton, M.; Planes, J.; and Marques-Silva, J. 2013.  Iterative and core-guided MaxSAT solving: A survey and assessment.  _Constraints_ , 18(4): 478–534.
  * Moura and Bjørner (2008) Moura, L. d.; and Bjørner, N. 2008.  Z3: An efficient SMT solver.  In _International conference on Tools and Algorithms for the Construction and Analysis of Systems_ , 337–340. Springer.
  * Nethercote et al. (2007) Nethercote, N.; Stuckey, P. J.; Becket, R.; Brand, S.; Duck, G. J.; and Tack, G. 2007.  MiniZinc: Towards a standard CP modelling language.  In _International Conference on Principles and Practice of Constraint Programming_ , 534. Springer.
  * Serafini and Garcez (2016) Serafini, L.; and Garcez, A. d. 2016.  Logic tensor networks: Deep learning and logical reasoning from data and knowledge.  _arXiv preprint arXiv:1606.04422_.
  * Sivaraman et al. (2020) Sivaraman, A.; Farnadi, G.; Millstein, T.; and Van den Broeck, G. 2020.  Counterexample-guided learning of monotonic neural networks.  _Advances in Neural Information Processing Systems_ , 33: 11936–11948.
  * Stewart and Ermon (2017) Stewart, R.; and Ermon, S. 2017.  Label-free supervision of neural networks with physics and domain knowledge.  In _AAAI_.
  * Sunaga (1958) Sunaga, T. 1958.  Theory of interval algebra and its applications to numerical analysis.  _RAAG Memoirs, 2-Misc. II_ , 547–564.
  * Verwer and Zhang (2019) Verwer, S.; and Zhang, Y. 2019.  Learning optimal classification trees using a binary linear program formulation.  In _Proceedings of the AAAI conference on artificial intelligence_ , 1625–1632.
  * Wang et al. (2018) Wang, S.; Pei, K.; Whitehouse, J.; Yang, J.; and Jana, S. 2018.  Formal security analysis of neural networks using symbolic intervals.  In _27th $\\{$USENIX$\\}$ Security Symposium ($\\{$USENIX$\\}$ Security 18)_, 1599–1614.
  * Xu et al. (2018) Xu, J.; Zhang, Z.; Friedman, T.; Liang, Y.; and Broeck, G. 2018.  A semantic loss function for deep learning with symbolic knowledge.  In _International conference on machine learning_ , 5502–5511. PMLR.
  * You et al. (2017) You, S.; Ding, D.; Canini, K.; Pfeifer, J.; and Gupta, M. 2017.  Deep lattice networks and partial monotonic functions.  _Advances in neural information processing systems_ , 30.
  * Yu et al. (2021) Yu, J.; Ignatiev, A.; Stuckey, P. J.; and Le Bodic, P. 2021.  Learning Optimal Decision Sets and Lists with SAT.  _Journal of Artificial Intelligence Research_ , 72: 1251–1279.
  * Zhang et al. (2019) Zhang, H.; Chen, H.; Xiao, C.; Gowal, S.; Stanforth, R.; Li, B.; Boning, D.; and Hsieh, C.-J. 2019.  Towards stable and efficient training of verifiably robust neural networks.  _arXiv preprint arXiv:1906.06316_.

##  Appendix A Appendix

### A.1 DeepSaDe: Domain Bound Propagation

This appendix provides more details on the calculation of the latent bounds in
the domain-bound propagation approach in section 4. The calculation detailed
below is based on the interval arithmetic approach ((Sunaga 1958; Gowal et al.
2018)). Given the lower and upper bounds $l^{(n)}$ and $u^{(n)}$ for the input
${\bf x}^{(n)}$ of layer $h_{n}$, the output of the $i^{th}$ neuron of layer
$h_{n}$ for an arbitrary input ${\bf x}^{(n)}$ can be written as (assuming
activation):

$x^{(n+1)}_{i}=\text{activation}(b^{(n)}_{i}+\sum_{j=1}^{|h_{n-1}|}w^{(n)}_{j,i}x^{(n)}_{j})$

Assuming that the activation function is monotonically non-decreasing, which
the typically used activations (like ReLu, Sigmoid, Tanh) are, we can bound
$x^{(n+1)}_{i}$ by lower and upper bounds $l^{(n+1)}_{i}$ and $u^{(n+1)}_{i}$
where:

$\begin{split}l^{(n+1)}_{i}=\text{activation}(\min_{{\bf
x}^{(n)}}(b^{(n)}_{i}+\sum_{j=1}^{|h_{n-1}|}w^{(n)}_{j,i}x^{(n)}_{j}))\\\
u^{(n+1)}_{i}=\text{activation}(\max_{{\bf
x}^{(n)}}(b^{(n)}_{i}+\sum_{j=1}^{|h_{n-1}|}w^{(n)}_{j,i}x^{(n)}_{j}))\end{split}$

In each formula, all terms can be maximized or minimized independently because
the domain is an axis-parallel hyperrectangle. The bounds can be written as:

$\begin{split}l^{(n+1)}_{i}=\text{activation}(b^{(n)}_{i}+\sum_{j=1}^{|h_{n-1}|}\min_{{\bf
x}^{(n)}}(w^{(n)}_{j,i}x^{(n)}_{j}))\\\
u^{(n+1)}_{i}=\text{activation}(b^{(n)}_{i}+\sum_{j=1}^{|h_{n-1}|}\max_{{\bf
x}^{(n)}}(w^{(n)}_{j,i}x^{(n)}_{j}))\end{split}$

Note that for any linear function $wx$ with $x\in[l,u]$ is maximal when $x=u$
for positive $w$, and when $x=l$ for negative $w$. Thus, the bounds can be
calculated with the following expressions:

$\begin{split}l^{(n+1)}_{i}=\text{activation}(b^{(n)}_{i}+\sum_{j:w^{(n)}_{j,i}\geq
0}w^{(n)}_{j,i}l^{(n)}_{j}+\\\
\sum_{j:w^{(n)}_{j,i}<0}w^{(n)}_{j,i}u^{(n)}_{j})\\\
u^{(n+1)}_{i}=\text{activation}(b^{(n)}_{i}+\sum_{j:w^{(n)}_{j,i}\geq
0}w^{(n)}_{j,i}u^{(n)}_{j}+\\\
\sum_{j:w^{(n)}_{j,i}<0}w^{(n)}_{j,i}l^{(n)}_{j})\end{split}$

To conclude, with this approach, the bounds for the output of a layer $h_{n}$
can be calculated in terms of the bounds of the input and the parameters of
the layer. These bounds can thus be propagated from the input space to the
latent space of the last layer. An illustration of this approach is provided
in figure 3. It is important to note that the bounds calculated with this
approach as very wide, but are suitable for our purposes and are cheap to
compute. There are approaches to calculate more compact bounds ((Wang et al.
2018)) that may improve the efficiency of the model, this is left for future
work.

Figure 3: Domain Bound Propagation: the bounds for the output of each layer
are constructed in such a way that any input to the network takes a value in
the latent space within the constructed latent bounds. The input domain (in
pink), when propagated through the layers, lies completely in the constructed
latent domains (in green). Thus, enforcing a constraint on the latent bound of
the last layer guarantees that the constraint is satisfied on any input within
input bounds. In our approach, this construction is essential for achieving
constraint satisfaction guarantees for neural networks.

### A.2 Experimental Details

In this appendix, we provide details of the logical formulation of domain
constraints for each use case in SMT, along with information regarding the
network architecture and the hyper-parameters selected for each use case. We
also provide an illustration of the Adversity Index (AdI) in figure 4. In the
following, for a compact representation, we assume $\hat{y}$ represents the
real-valued output of the model. Additionally, to express the component of a
variable ${\bf x}$, we use subscript with the name of the component (e.g.,
${\bf x}_{name}$ is the value of the ‘name’ feature of the variable ${\bf
x}$). For each network, the ReLU activation is used in the hidden layers.

UC1: UC1 is the expense prediction problem with two domain constraints. The
dataset contains 35317 violations of either of the constraints in 41417
instances. The ‘household income’ feature is a part of the domain constraints,
it is mapped to the last layer with skip connections. Formulation of the
domain constraint at the last layer of the DeepSaDe approach is:

$\mathcal{K^{\prime}}:\forall{\bf
x}\in\bigtimes_{i=1}^{|h_{k-1}|}[l^{(k)}_{i},u^{(k)}_{i}],\Big{(}(\text{SUM}(\hat{y})\leq{\bf
x}_{household-income})\\\ \land(\hat{y}_{going-out}\leq 0.05*{\bf
x}_{household-income})\Big{)}$

For the baseline REG, we use two regularization parameters $\lambda$ and
$\gamma$ for each constraint with the weight on the predictive loss being
$(1-\lambda-\gamma)$:

$\mathcal{L}=(1-\lambda-\gamma)*\text{MSE}+\lambda*\frac{1}{\|D\|}*\sum_{{\bf
x}\in D}\max(0,\sum f_{{\bf w}}({\bf x})\\\ -{\bf
x}_{income})+\gamma*\frac{1}{\|D\|}*\sum_{{\bf x}\in D}\max(0,f_{{\bf w}}({\bf
x})_{going\\_out}\\\ -0.05*{\bf x}_{income})$

Both $\lambda$ and $\gamma$ are tuned in the range of $[0,0.49]$ using the
5-fold nested cross validation. For each model, a network with three hidden
layers with sizes 50, 50, & 14 is considered. The learning rate for the
baseline and DeepSaDe is selected to be $0.001$ with a batch size of $5$. For
REG, the mode is trained for 10 epochs while for DeepSaDe the model is trained
for 5 epochs. The maximal step size for DeepSaDe is selected to be 0.1 and the
error threshold of $[0.1]$ is used for defining the soft constraints.

UC2: UC2 is the loan prediction task that is modeled by a binary
classification task. The dataset contains 40 violations of the constraint in
492 instances. Features ‘income’ and ‘credit history’ are mapped to the last
layer with identity mapping. Formulation of the domain constraint at the last
layer of the DeepSaDe approach is:

$\mathcal{K^{\prime}}:\forall{\bf
x}\in\bigtimes_{i=1}^{|h_{k-1}|}[l^{(k)}_{i},u^{(k)}_{i}],\Big{(}({\bf
x}_{income}<5000)\land\\\ ({\bf
x}_{credit\\_history}=0)\Big{)}\implies\Big{(}\hat{y}_{no-
loan}>\hat{y}_{loan}\Big{)}$

For each model, a network with three hidden layers with sizes 50, 30, & 10 is
considered. For SL and SBR, the learning rate of 0.1, and batch size of 5 are
selected and the models are trained for 400 epochs. For DeepSaDe, the learning
rate of 0.1, maximal step size of 0.1, batch size of 5, and the margins
($\tau$) of $[0,1,2]$ are selected, and the models are trained for 50 epochs.

UC3: UC3 is the music genre prediction task which is modeled by a multiclass
classification task. The dataset contains 41 violations in 793 instances.
Feature ‘artist’ is mapped to the last layer. Formulation of the domain
constraint at the last layer of the DeepSaDe approach is:

$\mathcal{K^{\prime}}:\forall{\bf
x}\in\bigtimes_{i=1}^{|h_{k-1}|}[l^{(k)}_{i},u^{(k)}_{i}],({\bf
x}_{artist}=\text{the beatles})\implies\\\
\Big{(}(\hat{y}_{classical}<0)\land(\hat{y}_{electronic}<0)\land\\\
(\hat{y}_{metal}<0)\land(\hat{y}_{pop}>0\lor\hat{y}_{rock}>0)\Big{)}$

For each model, a network with three hidden layers with sizes 50, 30, & 10 is
considered. For SL and SBR, the learning rate of 0.1, and batch size of 5 are
selected and the models are trained for 300 epochs. For DeepSaDe, the learning
rate of 0.1, maximal step size of 0.1, batch size of 5, and the margins
($\tau$) of $[0,1,2]$ are selected, and the models are trained for 50 epochs.

Figure 4: Illustration of AdI: 3 instances are mapped to real value
predictions using a neural network. The green region is the output region that
satisfies the constraint, the red region does not. It is possible, only for
the leftmost data point, to construct a new point in the $\ell_{\infty}$ ball
such that its prediction violates the constraint, even though the prediction
of the original instance does not. Hence, AdI = $1/3$.

UC4: UC4 is the multi-label prediction task of classifying a sequence of four
MNIST images to their respective classes. The dataset contains no violations
of the domain constraint. The domain constraint in this problem does not
depend on any of the input features. Formulation of the domain constraint at
the last layer of the DeepSaDe approach is:

$\mathcal{K^{\prime}}:\forall{\bf
x}\in\bigtimes_{i=1}^{|h_{k-1}|}[l^{(k)}_{i},u^{(k)}_{i}],\\\
\Big{(}\text{SUM([IF($\hat{y}_{i}>0$, i, 0)for i in range(10)])}>10\Big{)}$

For each model, a network with three hidden layers with sizes 50, 50, & 10 is
considered. For FFN, the learning rate of 0.1, and batch size of 10 are
selected and the models are trained for 40 epochs. For DeepSaDe, the learning
rate of 0.1, maximal step size of 0.1, batch size of 10, and the margins
($\tau$) of $[0,1,2]$ are selected, and the models are trained for 60 epochs.

Figure 5: For UC3, a visualization of the latent space of the input to the
last layer for the network trained by (a) DeepSaDe and (b) an unconstrained
model, on the test data. A 2-dimensional reduction of the latent space using
t-SNE is plotted on both plots. In the left plot, the points in orange are the
ones that satisfy the input property (i.e., artist = ‘the Beatles’). In the
right plot, the orange points are the ones for which the network predicts the
genre as either pop or rock.

Figure 6: t-SNE representation of the latent space for (a.) FFN model, and
(b.) DeepSaDe model for UC4. From left to right, the input space of the first
to the last layer is visualized in a two-dimensional space for a test dataset.
The latent vectors of the DeepSaDe model exhibit similar behavior as the FFN
model, i.e., as the model gets deeper, similar instances can be clustered
together by the t-SNE representation. This implies that similar to FFN,
DeepSaDe is also able to identify patterns in the data while enforcing hard
domain constraints which are always satisfied.

UC5: UC5 is the preference learning task with the coherence condition as the
domain constraint. The dataset contains no violations of the domain
constraint. The domain constraint in this problem does not depend on any of
the input features. The constraints are formulated in DeepSaDe using the
following encoding:

$\mathcal{K^{\prime}}:\forall{\bf
x}\in\bigtimes_{i=1}^{|h_{k-1}|}[l^{(k)}_{i},u^{(k)}_{i}],\\\
\Big{(}\text{PbEq}([\hat{y}_{0}>0,\hat{y}_{1}>0,\hat{y}_{2}>0,\hat{y}_{3}>0],1)\land\\\
\text{PbEq}([\hat{y}_{4}>0,\hat{y}_{5}>0,\hat{y}_{6}>0,\hat{y}_{7}>0],1)\land\\\
\text{PbEq}([\hat{y}_{8}>0,\hat{y}_{9}>0,\hat{y}_{10}>0,\hat{y}_{11}>0],1)\land\\\
\text{PbEq}([\hat{y}_{12}>0,\hat{y}_{13}>0,\hat{y}_{14}>0,\hat{y}_{15}>0],1)\land\\\
\text{PbEq}([\hat{y}_{0}>0,\hat{y}_{4}>0,\hat{y}_{8}>0,\hat{y}_{12}>0],1)\land\\\
\text{PbEq}([\hat{y}_{1}>0,\hat{y}_{5}>0,\hat{y}_{9}>0,\hat{y}_{13}>0],1)\land\\\
\text{PbEq}([\hat{y}_{2}>0,\hat{y}_{6}>0,\hat{y}_{10}>0,\hat{y}_{14}>0],1)\land\\\
\text{PbEq}([\hat{y}_{3}>0,\hat{y}_{7}>0,\hat{y}_{11}>0,\hat{y}_{15}>0],1)\Big{)}$

Where ‘PbEq’ encodes the exactly-k constraint, $\text{PbEq}([a,b,c],k)$
enforces that exactly $k$ of the boolean constraints $a$, $b$, and $c$ must be
true, where $k\in\\{1,2,3\\}$ in this example. For each model, a network with
three hidden layers with sizes 25, 25, & 10 is considered. For SL and FFN, the
learning rate of 0.1, and batch size of 10 are selected and the models are
trained for 40 epochs. For DeepSaDe, the learning rate of 0.1, maximal step
size of 0.1, batch size of 10, and the margins ($\tau$) of $[0,1,2]$ are
selected, and the models are trained for 40 epochs.

### A.3 Results

In addition to the experiments presented in the main text, we also perform
some supplementary experiments where we visualize the latent space for the
networks learned with DeepSaDe. These experiments demonstrate that DeepSaDe,
similar to existing gradient-based approaches, is also able to identify
patterns in the latent space, which makes it easier to satisfy the constraint
at the last layer. This experiment also adds validity to DeepSaDe as a
learning approach.

Visualizing the Latent Space: First, we consider the multiclass classification
problem of UC3 where the constraint is only enforced for a part of the input
space that satisfies the input property (i.e., when the artist = ‘the
Beatles’). In Figure 5, we plot the t-SNE (t-distributed Stochastic Neighbour
Embedding) ((Hinton and Roweis 2002)) transformation of the latent space of
the last layer. t-SNE captures the structure in the sense that neighboring
points in the latent space should be closer in the t-SNE representation. In
the left figure, data points that satisfy the input property are highlighted
(in orange), while in the right figure, data points that are predicted as
either ‘pop’ or ‘rock’ by the network are highlighted (in orange). It is shown
that the instances that satisfy the input property are clustered together
better for DeepSaDe than for the unconstrained model, which implies that
enforcing the constraint at the last layer with DeepSaDe enables us to learn
the latent space such that enforcing constraints at the last layer becomes
easier. Furthermore, the network trained through DeepSaDe satisfies the
constraint for each of these instances by predicting the genre to be either
pop’ or ‘rock,’ as shown in the right figure. However, for an unconstrained
network, the model still violates some of the constraints since the
constraints are not enforced. We selected UC3 to analyze the distribution of
the latent space in the context of the input property, which is difficult to
do for use cases UC1, UC4, and UC5, where the constraint is being enforced on
all possible predictions.

We perform another analysis for use case UC4 which classifies a collection of
MNIST images into respective labels in a multi-label classification task.
Here, the constraint is being enforced for all possible outputs of the
network, hence it is difficult to see the impact of constraint satisfaction in
the t-SNE representation. However, in this experiment, we compare how the
t-SNE representation of the DeepSaDe model compares with the t-SNE
representation for the baseline model (which in this case is a feed-forward
neural network without any constraint enforcement). The goal here is to
demonstrate the validity of DeepSaDe. Figure 6 shows that DeepSaDe exhibits
similar behavior in the low dimensional representation of the latent space for
each layer when compared with the similar representation of the FFN model.
DeepSaDe can identify similar points in the latent space (because t-SNE can
cluster data points as the model becomes deeper), which means that the network
can learn patterns from the data, similar to the FFN while enforcing hard
constraints on the predictions which are always satisfied.


# SARD: A Human-AI Collaborative Story Generation

Ahmed Y. Radwan
Department of Computer Science
ASAS AI
King Abdulaziz University
<EMAIL_ADDRESS>
Khaled M. Alasmari
Department of Computer Science
ASAS AI
King Abdulaziz University
<EMAIL_ADDRESS>
Omar A. Abdulbagi
Department of Computer Science
ASAS AI
King Abdulaziz University
<EMAIL_ADDRESS>
Emad A. Alghamdi
Center for Research Excellence in AI and Data Science
ASAS AI
King Abdulaziz University
<EMAIL_ADDRESS>

###### Abstract

Generative artificial intelligence (GenAI) has ushered in a new era for
storytellers, providing a powerful tool to ignite creativity and explore
uncharted narrative territories. As technology continues to advance, the
synergy between human creativity and AI-generated content holds the potential
to redefine the landscape of storytelling. In this work, we propose SARD, a
drag-and-drop visual interface for generating a multi-chapter story using
large language models. Our evaluation of the usability of SARD and its
creativity support shows that while node-based visualization of the narrative
may help writers build a mental model, it exerts unnecessary mental overhead
to the writer and becomes a source of distraction as the story becomes more
elaborated. We also found that AI generates stories that are less lexically
diverse, irrespective of the complexity of the story. We identified some
patterns and limitations of our tool that can guide the development of future
human-AI co-writing tools.

_Keywords_ Human-AI collaboration, Co-Creativity, Computational Creativity,
Large Language Models, Storytelling, Natural Language Generation, Evaluation,
Creativity

##  1 Introduction

Narrative expression is a fundamental element of the human experience,
manifested across various mediums such as written text, oral traditions, cave
paintings, and beyond. Generative artificial intelligence has ushered in a new
era for storytellers, providing a powerful tool to ignite creativity and
explore uncharted narrative territories (Kybartas and Bidarra, 2016; Lee et
al., 2024). Generative AI, a subset of artificial intelligence, has
revolutionized the way stories are crafted, providing a new avenue for
creativity and imagination. While extensive work on automated story generation
has been conducted in the past 40 years (Kybartas and Bidarra, 2016), the rise
of large language models (LLMs) is opening new frontiers for human-AI
collaboration. However, integrating such capabilities with human cognitive
faculties and creative processes remains challenging.

Generative AI, often associated with deep learning techniques, enables
machines to produce content that mimics human-like creativity. Unlike
traditional programming, which relies on explicit instructions, generative AI
learns patterns and styles from vast datasets to create original and diverse
content. This technology has found a unique niche in the world of
storytelling, where it is employed to generate narratives, characters, and
even entire stories and poems (Chakrabarty et al., 2022). Generative AI for
story creation involves training models on massive datasets comprised of
diverse literary works, genres, and writing styles. These models, such as
OpenAI’s GPT-3 and GPT-4, learn the nuances of language, syntax, and
semantics, enabling them to generate coherent and contextually relevant text.
Once trained, these models can be prompted with a starting point or theme, and
they autonomously produce imaginative and contextually appropriate stories.

One of the significant advantages of generative AI in story creation is its
ability to break through creative barriers and expedite the writing process
(Lee et al., 2024). Exposing the model to a myriad of writing styles and
genres can produce content combining elements from various sources, resulting
in novel and unique narratives. This not only aids writers in overcoming
creative blocks but also fosters a collaborative relationship between human
creativity and machine-generated content. Generative AI should be viewed as a
tool to augment human creativity rather than replace it. Writers can leverage
these AI models to explore new ideas, overcome writer’s block, or even
collaborate with the AI in co-authoring projects. The human touch remains
essential in refining and contextualizing the generated content, ensuring that
it aligns with the intended emotional tone, narrative structure, and thematic
elements.

##  2 Related Work

The use of computer programs to generate a story or parts of a story has been
an interest for computer science researchers since the field’s inception
(Kybartas and Bidarra, 2016). Initial efforts in this field utilized
traditional AI algorithms, including symbolic and logical planning as well as
graph traversal, to craft narratives (Klein et al., 1973; Dehn, 1981). These
narratives often incorporated a degree of user control, allowing users to
define initial goals and conditions. In recent endeavors, researchers have
explored the potential of using LLMs to produce complete narratives
autonomously (Fan et al., 2018), whereas others have emphasized the
significance of developing AI systems that give precedence to human
participation in the process of crafting stories (Swanson et al., 2021).

###  2.1 Generative AI for Story Creation

Recent advancements in generative AI, such as GPT-4 and DALL-E2, have unlocked
new possibilities for automated story generation. Numerous prototypes of AI-
powered story-authoring systems have emerged. Yuan et al. (2022) developed
Wordcraft, a web application for story writing with an LLM. Wordcraft consists
of a traditional text editor and a set of controls that prompt an LLM to
perform various writing tasks. In Yang et al. (2022a), writers interacted with
AI in a "turn=taking" style to co=write short science-fiction stories. The
writers discovered that the language model occasionally produces texts of
subpar quality, containing words that may be challenging to comprehend. On the
contrary, there are instances where it generates high-quality inspirations
that propel the plot beyond what humans might anticipate. Calderwood et al.
(2020) explored how novelists use AI to generate stories finding that
novelists find pleasure in utilizing the language model as a constraining tool
to push the boundaries of their writing or as an opponent that aided them in
realigning and improving their purpose. Osone et al. (2021) investigated AI-
assisted storytelling for Japanese novelists and found that while novice
writers benefited from model suggestions, experts found these less useful and
underwhelming.

Concerns about LLM’s creativity have been raised. Padmakumar and He (2023)
found that LLMs aligned to human feedback, e.g., InstructGPT, generate less
diverse content and increase the similarity between the writings of different
writers. Addressing the lack of long-semantic coherence and relevance of
outputs generated by LLMs, Yang et al. (2022b) proposed the Recursive
Reprompting and Revision framework (Re3) which recursively prompt LLMs to
plan, draft, rewrite, and edit. A qualitative evaluation by human evaluators
found stories generated using this framework to have more coherent plots and
relevance to the user install premise. Mirowski et al. (2023) developed
Drematron by applying language models hierarchically via prompt chaining.
Drematron can help theatre and film professionals generate coherent scripts
and screenplays along with titles, characters, story beats, location
descriptions, and dialogues.

###  2.2 AI-Authoring Tools

There has been some recent work on integrating generative AI in writing
assistant systems and how to best support storytellers in their writing
process. These tools vary in their level of technical complexity, degrees of
automation, user interactions, and level of support they provide. A common
design paradigm for writing authoring tools takes the form of dialogue, where
a user and the language model take turns to append content to the end of the
story (Calderwood et al., 2020; Yang et al., 2022a; Yuan et al., 2022). For
example, Clark et al. (2018) performed a case study on collaborative slogans
and short story writing, observing that users preferred an interface design
where they had a higher level of control over the interactions.

###  2.3 AI Content Quality and Novelty

Assessing the quality of content generated by AI models remains a difficult
challenge, as tasks of quantifying the intricacies of narrative structure,
creativity, coherence, and emotional resonance in AI-generated stories are
complex. Numerous studies have approached this evaluation by assessing their
generated stories with various evaluation methods. One of the most efficient
methods is computer-based evaluation, where the stories generated are
automatically assessed for quality, relevance, and coherence using tools and
algorithms. Studies, such as Kong et al. (2021) and Khan et al. (2023), used
pre-trained models to evaluate the fluency and diversity in AI-generated
content.

##  3 System Overview

SARD is a multi-chapter story generation facilitated by generative AI (see 1).
It is a storyboard-based authoring tool that enables users to construct
narratives through a drag-and-drop interface. SARD editor is built with
ReactJS and shadcn/ui to help users to generate their own stories via a simple
drag-and-drop interface. SARD is connected to generative AI models through a
REST API and a WebSocket connection to the backend.

Users initiate the creation of a story by accessing the menu and selecting
their preferred story genre (thrillers, science fiction, ..etc ) and structure
(free, three-act story, and five-act story). Once initial story parameters are
set, the users can add nodes, provided in the story elements tab, that
symbolizes different narrative components such as characters, actions, and
relationships. These nodes can be interconnected with one another to form a
complex narrative structure. Another key feature of SARD is the generation of
descriptive content for characters or scenery in the story based on images
provided by the user. After finishing the storyboard, the users can order
events to enhance the narrative flow. The finalized user-generated storyboard
is converted programmaticly to prompts which are then sent to the GPT-4 model
to craft a coherent and contextually rich story.

###  3.1 Prompt Designing

The designed several prompts for the different functionalities in SARD. Table
1 shows the prompts and their functions. We experimented with different
prompts for each functionality and only included the ones generated the best
results. We designed our prompts to be as generic as possible. For example,
our prompt for ensuring coherence between all chapters is "Summarize the
following chapter in a short and concise way. Make sure you include all the
important events in your summary as the next chapters will depend on it:
[chapter to summarize]." We observed that this prompt helped the language
model to grasp what happened in the preceding and following events. We decided
to hide the prompts from the user to make them focus more on their story-
writing process and less on optimizing prompts. Our decision was motivated by
a previous study in which non-AI experts found it difficult to craft suitable
prompts to generate intended behaviors (Zamfirescu-Pereira et al., 2023).

Functionality |  Prompt
---|---
Describing a scenery |  This image represents a place where events happened. Describe the place in detail. If the image has characters in it, do not describe them and ignore them. Your main focus is to describe the place and its surroundings in detail.
Describing the visual appearance of a character |  Describe the character’s appearance in detail for the attached image. The character name is [name], refrain from using pronouns, please use the character name instead. Make sure you start describing the character immediately. Do not use words like ’Certainly’, or ’Okay’. If you do not receive an image, respond with nothing.
Generating a story |  Write chapter [chapter number] with dialogues using the following characters’ details:
[characters names and details]
and the relationships between them are [list of relations].
now map it to the information you have in the following events:
[list of events] [previous chapters summary]
<[description for the place where the events happened]>"""
Output Length: """<3000 words>"""
Structure of Writing: """<You are writing a chapter, follow the rules to write
an amazing chapter"""
Take your time with the writing, perfecting this chapter.
Summarizing a chapter |  Summarize the following the chapter shortly and concisely. Make sure you include all the important events in your summary as the next chapters will depend on it:
[chapter to summarize]
Table 1: The prompts used to instruct GPT-4

###  3.2 Canvas

The canvas resembles the storyboard where story characters and different
elements will be visualized as nodes. Specific nodes can be linked together
through edges to form an event in the current storyboard. In addition, the
optional initialization of metadata by providing character nodes with images.
The simplistic interface is aimed to be user-friendly with a mini-map feature
and a navigational guide to freely transport through the canvas. These
functionalities streamline the user’s creative workflow and provide a clear
picture of how the story is developed progressively.

Figure 1: SARD: Novel generation through interactive storyboard. The user
starts with (1) where the user sets the story structure and genre. (2) is
where the user can create and add elements, either character, action, or
relationship, to their storyboard. (2) can also be used to navigate through
different storyboards and set the setting with an image. When creating an
element the user drags it into the canvas (3) where it is translated into a
node. The user can click the green button to represent character nodes with
images, and then preview them with the blue button. This node can be connected
to other elements creating relationships. After the user orders events (4),
they can generate their storyboards into a story (5) which is displayed in the
story tab.

###  3.3 Setting Genre and Structure

The options tab offers two main components to writing a novel, the first one
is the genre list and the second is the story structure. The genre’s list
provides our model to be more strict, as in the novels each genre has a way of
writing and leads to a different flow of events and words. For the story
structure, there are three options, free mode which lets the user have no
rules in writing the story, as he may have at least one board to generate a
story. There is no maximum that will make the story more creative but with the
disadvantage of not following a famous structure like the others. The three-
act structure consists of three main parts, an introduction, a climax, and a
resolution, to represent each one in a storyboard, as it will control the flow
of the story, unlike the free mode. And, for the last structure is the five-
act structure, which follows Exposition, Rising, Climax, Falling Action, and
Resolution. The main difference from the three-act structure it will be longer
which will be more engaging in longer stories.

###  3.4 Adding Characters, Events and Actions

The story is built with three types of nodes: character, action, and
relationship. The user can create one or more storyboards and drop new
elements or reuse any existing story elements. The character node allows the
user to add new characters as well as images to describe the character or
scenes. For the action node, it offers multiple default actions to choose
from, as well as a custom option that allows the user to be more specific
about what he wants. Finally, the relation node is intended to bring dimension
to the characters. These components are used to build the novel’s events,
which each include at least one character on both sides and are connected by
an action node or relation. For example, the event ’Ahmad humiliated John and
Ben’ will be divided into four nodes combined from three characters, and a
single action.

###  3.5 Ordering of Events

The events sequence is of importance as it dictates the flow and coherence of
the story. Based on user feedback and testing through development, we
discovered that chaining events with edges can get messy and confusing very
quickly. To overcome this, we added a tab for ordering events in the
interface.

##  4 Methodology

###  4.1 Study 1: Evaluating The usability and collaborative aspects of SARD

The primary objective of Study 1 was to assess the usability of SARD and its
creativity support. To this end, the System Usability Scale (SUS) (Brooke,
1996) and a modified version of the Mixed-Initiative Creativity Support Index
(MICSI) (Lawton et al., 2023) were used. The SUS scale includes 10 items
(five-point Likert scale questionnaire), developed specifically to provide a
reliable metric for system usability. The final score of SUS ranges from 0 to
100 and a score of 70 or above is considered to be a good indicator of system
usability (Bangor et al., 2009). MICSI, an 18-item scale designed for
evaluating collaborative creativity between humans and machines, encompasses
five sub-scales related to Creativity Support: Enjoyment, Exploration,
Expressiveness, Immersion, and Results-Worth-Effort. Each of these sub-scales
involves a pair of seven-point Likert-scale questions, with the score
calculated based on the mean response value for each question pair.
Additionally, MICSI includes sub-scales dedicated to assessing Human-Machine
Collaboration, each measured through a distinct seven-point Likert-scale
question. These sub-scales address aspects like Communication, Alignment,
Agency, and Partnership. A score of 5 or higher on these MICSI sub-scales
indicates a positive user experience. We also allowed users to give any
feedback on their use of SARD.

####  4.1.1 Participants

We recruited five university students (4 females and 2 males) to participate
in the study. All the participants were graduate students in English and
creative writing. The participants were aged between 22 and 25 (M= 22.5, SD =
0.42).

####  4.1.2 Task and Procedure

After obtaining participants’ consent, they were given a walk-through tutorial
on how to navigate the interface and use the system. Then, they were asked to
generate a story of their choice using all the utilities of SARD. They were
given a week to complete a story.

####  4.1.3 Results

The results of scales are presented in 2. The average score for SARD’s
usability was 63.75, indicating that participants had moderately positive
attitudes toward the usability of SARD. This could be due to the novelty
effect. Two participants indicated they initially had difficulty connecting
the nodes in the canvas.

W1 "I think how to connect the nodes was a bit challenging at first. It’s hard
to link nodes with each other but after some attempts, I was able to build my
story "

We also observed that some participants did not go through the tutorial we
provided in the interface, and immediately started adding characters to the
canvas.

Figure 2: Results from Study 1: (a) SUS Scores, (b) MICSI Sub-Scale Scores,
(c) Exploratory Question Responses.

The scores of the MICSI sub-scales were slightly below five, as shown in 2 B,
but they all expressed their satisfaction with their generated stories as they
reflected in the exploratory questions as well as in their feedback in Study
2.

###  4.2 Study 2: Evaluating Story Quality

Understanding how writers assess systems output is crucial because it could
influence their interaction and engagement with the writing assistant during
the story generation process. One key characteristic of high-quality output is
its textual coherence, which underlines the need for grammatically and
contextually coherent output Gero et al. (2022). Another important facet is
textual diversity which underscores the importance of offering varied system
outputs to foster creativity in writing Singh et al. (2023); Gero et al.
(2022). In Study 2, we investigated the quality and content diversity of the
generated stories via quantitative and qualitative measures.

####  4.2.1 Measures

We assessed the lexical diversity of the generated stories using token-type
ratios (TTR). We also conducted a semi-structured interview with the
participants to solicit their opinions about the stories they generated using
SARD.

###  4.3 Results

All participants selected a three-act story structure and developed three
storyboards for each act. Our analysis of the lexical diversity of generated
stories showed that the participants’ stories had similar TTR (M = 0.47, SD =
0.09).

Regarding the participants’ judgment of their own stories, all participants
expressed their positive attitudes toward the story they generated using SARD.
Specifically, they mentioned how the tool helped them to elaborate on their
initial plot and extend their vocabulary.

W2 "I like it, it creates a very advanced level of the story. It uses advanced
vocabulary."

W5 "Honestly, I was not expecting that. I had a simple story in my mind but
this tool took it to another level."

##  5 Discussion

The results of our questionnaire and interviews with the participants have
revealed some common patterns and themes in users’ interactions with SARD,
which can provide some insights for research in the realms of Natural Language
Processing and Human-Computer Interaction.

###  5.1 Identifying Patterns in User Interactions

All writers found creating nodes to create relationships between the
characters and events to help create a mental model of the story. However, a
writer mentioned that she began to lose sight of her mental model of the story
as she elaborated more on her story and added too many characters and events
to her story canvas. While SARD summarizes and generates a plot for each
chapter, it does not show it to the users. Showing a concise summary for each
chapter might be helpful for users to stay oriented in their story generation
process as it follows. We also observed that our participants developed their
stores’ characters and modified their plots repeatedly over a week. This may
indicate that while our node-based system gives more flexibility and
elaborateness to the story development process, it nonetheless exerts more
cognitive load compared to turn-taking authoring systems.

###  5.2 Sense of agency, control, and ownership

The user’s different perceptions of AI in the co-writing process seem to
impact how they interact with the tool. While some users rely heavily on AI to
steer the story generation, others want more control of their story.
Specifically, writers felt AI does not reflect and express what they had in
their mind, despite their efforts in planning the plot of the story and how
the events should flow. Some participants felt that hiding the prompts used
for generating stories is limiting their ability to control their stories.

###  5.3 System Limitations Experienced by Participants

The participants identified some limitations in SARD. First, some participants
hoped that AI could help them in brainstorming ideas and initiating some
suggested plots to expiate the writing process. A participant mentioned that
he used ChatGPT to brainstorm some ideas before using SARD. Second, some
participants expressed disappointment or resignation when the system’s output
did not align with their expectations, and that adjusting nodes and reordering
the event sequence did not help generate more diverse content. This echoes
recent concerns on the inability of current LLMs to generate creative content
on their own (Chakrabarty et al., 2023; Franceschelli and Musolesi, 2023).

##  6 Conclusion and Future Work

AI-driven storytelling is an evolving landscape. In this study, we reported
the findings of two studies on the usability and quality of AI-powered story
generation using a custom-built interface. Our results demonstrated that the
potential of human-AI co-creative systems, such as SARD, in helping novice
writers generate novel stories. However, future systems need to take user’s
workload and their expectations of such systems into consideration. In our
future work, we aim to give users more control over their story generation by
allowing them to directly prompt and co-create with AI as a companion. We also
aim to leverage LLMs for generating graph nodes from natural text describing
story plots.

## References

  * Kybartas and Bidarra [2016] Ben Kybartas and Rafael Bidarra.  A survey on story generation techniques for authoring computational narratives.  _IEEE Transactions on Computational Intelligence and AI in Games_ , 9(3):239–253, 2016.
  * Lee et al. [2024] Mina Lee, Katy Ilonka Gero, John Joon Young Chung, Simon Buckingham Shum, Vipul Raheja, Hua Shen, Subhashini Venugopalan, Thiemo Wambsganss, David Zhou, Emad A. Alghamdi, Tal August, Avinash Bhat, Madiha Zahrah Choksi, Senjuti Dutta, Jin L.C. Guo, Md Naimul Hoque, Yewon Kim, Simon Knight, Seyed Parsa† Neshaei, Antonette Shibani, Disha Shrivastava, Lila Shroff, Agnia Sergeyuk, Jessi Stark, Sarah Sterman, Sitong Wang, Antoine Bosselut, Daniel Buschek, Joseph Chee Chang, Sherol Chen, Max Kreminski, Joonsuk Park, Roy Pea, Eugenia Ha Rim Rho, Zejiang Shen, and Pao Siangliulue.  Design space for intelligent and interactive writing assistants.  In _Proceedings of the ACM CHI Conference on Human Factors in Computing Systems_. ACM, 2024.
  * Chakrabarty et al. [2022] Tuhin Chakrabarty, Vishakh Padmakumar, and He He.  Help me write a poem: Instruction tuning as a vehicle for collaborative poetry writing.  _arXiv preprint arXiv:2210.13669_ , 2022.
  * Klein et al. [1973] Sheldon Klein, John F Aeschlimann, David F Balsiger, Steven L Converse, Mark Foster, Robin Lao, John D Oakley, Joel Smith, et al.  Automatic novel writing: A status report.  Technical report, University of Wisconsin-Madison Department of Computer Sciences, 1973.
  * Dehn [1981] Natlie Dehn.  Story generation after tale-spin.  In _IJCAI_ , volume 81, pages 16–18, 1981.
  * Fan et al. [2018] Angela Fan, Mike Lewis, and Yann Dauphin.  Hierarchical neural story generation.  _arXiv preprint arXiv:1805.04833_ , 2018.
  * Swanson et al. [2021] Ben Swanson, Kory Mathewson, Ben Pietrzak, Sherol Chen, and Monica Dinalescu.  Story centaur: Large language model few shot learning as a creative writing tool.  In _Proceedings of the 16th Conference of the European Chapter of the Association for Computational Linguistics: System Demonstrations_ , pages 244–256, 2021.
  * Yuan et al. [2022] Ann Yuan, Andy Coenen, Emily Reif, and Daphne Ippolito.  Wordcraft: story writing with large language models.  In _27th International Conference on Intelligent User Interfaces_ , pages 841–852, 2022.
  * Yang et al. [2022a] Daijin Yang, Yanpeng Zhou, Zhiyuan Zhang, Toby Jia-Jun Li, and Ray LC.  Ai as an active writer: Interaction strategies with generated text in human-ai collaborative fiction writing.  In _Joint Proceedings of the ACM IUI Workshops_ , volume 10. CEUR-WS Team, 2022a.
  * Calderwood et al. [2020] Alex Calderwood, Vivian Qiu, Katy Ilonka Gero, and Lydia B Chilton.  How novelists use generative language models: An exploratory user study.  In _HAI-GEN+ user2agent@ IUI_ , 2020.
  * Osone et al. [2021] Hiroyuki Osone, Jun-Li Lu, and Yoichi Ochiai.  Buncho: ai supported story co-creation via unsupervised multitask learning to increase writers’ creativity in japanese.  In _Extended Abstracts of the 2021 CHI Conference on Human Factors in Computing Systems_ , pages 1–10, 2021.
  * Padmakumar and He [2023] Vishakh Padmakumar and He He.  Does writing with language models reduce content diversity?  _arXiv preprint arXiv:2309.05196_ , 2023.
  * Yang et al. [2022b] Kevin Yang, Nanyun Peng, Yuandong Tian, and Dan Klein.  Re3: Generating longer stories with recursive reprompting and revision.  _arXiv preprint arXiv:2210.06774_ , 2022b.
  * Mirowski et al. [2023] Piotr Mirowski, Kory W Mathewson, Jaylen Pittman, and Richard Evans.  Co-writing screenplays and theatre scripts with language models: Evaluation by industry professionals.  In _Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems_ , pages 1–34, 2023.
  * Clark et al. [2018] Elizabeth Clark, Anne Spencer Ross, Chenhao Tan, Yangfeng Ji, and Noah A Smith.  Creative writing with a machine in the loop: Case studies on slogans and stories.  In _23rd International Conference on Intelligent User Interfaces_ , pages 329–340, 2018.
  * Kong et al. [2021] Xiangzhe Kong, Jialiang Huang, Ziquan Tung, Jian Guan, and Minlie Huang.  Stylized story generation with style-guided planning.  _arXiv preprint arXiv:2105.08625_ , 2021.
  * Khan et al. [2023] Aleem Khan, Andrew Wang, Sophia Hager, and Nicholas Andrews.  Learning to generate text in arbitrary writing styles.  _arXiv preprint arXiv:2312.17242_ , 2023.
  * Zamfirescu-Pereira et al. [2023] JD Zamfirescu-Pereira, Richmond Y Wong, Bjoern Hartmann, and Qian Yang.  Why johnny can’t prompt: how non-ai experts try (and fail) to design llm prompts.  In _Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems_ , pages 1–21, 2023.
  * Brooke [1996] John Brooke.  Sus: a “quick and dirty’usability.  _Usability evaluation in industry_ , 189(3):189–194, 1996.
  * Lawton et al. [2023] Tomas Lawton, Francisco J Ibarrola, Dan Ventura, and Kazjon Grace.  Drawing with reframer: Emergence and control in co-creative ai.  In _Proceedings of the 28th International Conference on Intelligent User Interfaces_ , pages 264–277, 2023.
  * Bangor et al. [2009] Aaron Bangor, Philip Kortum, and James Miller.  Determining what individual sus scores mean: Adding an adjective rating scale.  _Journal of usability studies_ , 4(3):114–123, 2009.
  * Gero et al. [2022] Katy Ilonka Gero, Vivian Liu, and Lydia Chilton.  Sparks: Inspiration for science writing using language models.  In _Designing interactive systems conference_ , pages 1002–1019, 2022.
  * Singh et al. [2023] Nikhil Singh, Guillermo Bernal, Daria Savchenko, and Elena L Glassman.  Where to hide a stolen elephant: Leaps in creative writing with multimodal machine intelligence.  _ACM Transactions on Computer-Human Interaction_ , 30(5):1–57, 2023.
  * Chakrabarty et al. [2023] Tuhin Chakrabarty, Philippe Laban, Divyansh Agarwal, Smaranda Muresan, and Chien-Sheng Wu.  Art or artifice? large language models and the false promise of creativity.  _arXiv preprint arXiv:2309.14556_ , 2023.
  * Franceschelli and Musolesi [2023] Giorgio Franceschelli and Mirco Musolesi.  On the creativity of large language models.  _arXiv preprint arXiv:2304.00008_ , 2023.