# Ada-QPacknet - adaptive pruning with bit width reduction as an efficient
continual learning method without forgetting ††thanks:  Paper accepted at ECAI
2023

Marcin Pietron
AGH-UST
Kraków
<EMAIL_ADDRESS>
&Dominik Zurek
AGH-UST
Kraków
<EMAIL_ADDRESS>
&Kamil Faber
AGH-UST
Kraków
<EMAIL_ADDRESS>
&Roberto Corizzo
American University
Washington
<EMAIL_ADDRESS>

###### Abstract

Continual Learning (CL) is a process in which there is still huge gap between
human and deep learning model efficiency. Recently, many CL algorithms were
designed. Most of them have many problems with learning in dynamic and complex
environments. In this work new architecture based approach Ada-QPacknet is
described. It incorporates the pruning for extracting the sub-network for each
task. The crucial aspect in architecture based CL methods is theirs capacity.
In presented method the size of the model is reduced by efficient linear and
nonlinear quantisation approach. The method reduces the bit-width of the
weights format. The presented results shows that low bit quantisation achieves
similar accuracy as floating-point sub-network on a well-know CL scenarios. To
our knowledge it is the first CL strategy which incorporates both compression
techniques pruning and quantisation for generating task sub-networks. The
presented algorithm was tested on well-known episode combinations and compared
with most popular algorithms. Results show that proposed approach outperforms
most of the CL strategies in task and class incremental scenarios.

_K_ eywords Continual learning $\cdot$ Quantisation $\cdot$ Pruning $\cdot$
Catastrophic Forgetting

##  1 Introduction

Continual learning (CL) is an emerging machine learning paradigm that aims at
designing new methods and strategies to provide accurate analysis in complex
and dynamic real-world environments [6]. As models are challenged with
multiple tasks over their lifetime, a desired property for CL strategies is to
maintain a high performance across all tasks. This paradigm is receiving
increasing attention from research communities, which led to a number of works
being proposed [55, 54, 2, 6, 18, 3]. There are three main types of CL
strategies: rehearsal (also known as experience replay), regularization, and
architectural. Architectural strategies are quite powerful in that they allow
to adapt and evolve the model to accommodate new tasks, and recent research
shows that such approaches are among the most efficient and effective in CL
scenarios [21, 32, 30, 18]. Forget-free methods [21, 32] accommodate new tasks
by assigning a subset of the number of available weights to each task. Their
effectiveness strongly depends on their ability to effectively leverage model
capacity to accommodate as many tasks as possible.

One important pitfall of existing pruning-based architectural forget-free
methods is that they are limited in their ability to efficiently exploit model
sparsity since each layer is pruned with the same constant sparsity level. As
a result, they do not properly tune the number of weights to be removed while
preserving classification accuracy [64, 51]. Another general limitation shared
by forget-free methods is that they are prone to a quick saturation of the
available model capacity, in that they cannot assign more than one value to
each weight and are therefore limited by the available number of weights.

In this paper, we propose Ada-QPacknet, a novel forget-free method for
continual image classification that solves these limitations by incorporating
adaptive pruning with sparsity-level identification and adaptive non-linear
weights quantization.

Specifically, to effectively exploit model sparsity, our proposed Ada-QPacknet
incorporates adaptive pruning with different sparsity levels for each layer,
where pruning ratios are chosen via fast lottery ticket search. Moreover, to
deal with the issue of quickly saturating model capacity, Ada-QPacknet
performs an adaptive quantization stage that separates each weight into
multiple components, each using a subset of the available 32 bits. This
separation allows us to reuse a single weight for more than one task, leading
to reduced use of models’ capacity and improvements in terms of model
efficiency. At the same time, by exclusively assigning single components of
weights to tasks, we overcome the bias limitation that is typically existent
in common forget-free methods, which assign multiple tasks to the same weight
value.

In summary, the contributions of our paper are the following:

  * •

An adaptive pruning approach that leverages the sensitivity and weights’
importance characterizing different layers in deep learning models. This
approach allows us to reduce the available set of model’s weights assigned to
separate tasks, allowing AdaQ-Packnet to efficiently use a subset of the
weights without significant losses in accuracy.

  * •

A quantization strategy for continual learning, which allows us to split
weights into components, each of which can be assigned to a specific task.
This capability allows AdaQ-Packnet to better exploit model efficiency and
capacity, leveraging the reduced bit-width representation of the weights.

  * •

An experimental evaluation with three benchmark CL scenarios, which highlights
that our proposed method outperforms state-of-the-art rehearsal,
regularization, and architectural CL strategies, both in terms of accuracy and
exploitation of model capacity.

The paper is structured as follows. Section 2 summarizes related works in CL
strategies and pruning methods. Section 3 describes our proposed Ada-QPacknet
method. Section 4 describes our experimental setup, and presents the results
extracted in our experiments. Section 5 wraps up the paper with a summary of
the results obtained and outlines relevant directions for future work.

##  2 Related works

Continual learning methods are commonly categorized as rehearsal,
regularization, and architectural [6]. Rehearsal methods use memory to
remember some data from past episodes. The simplest solution is to store part
of the previous training data and interleave them with new training data
(Replay [6]). Other popular rehearsal methods include GEM [19], A-GEM [25],
and GDumb [26]. Regularization methods usually use constraints on the loss
function to strengthen connections for already learned patterns. The most
popular methods are Synaptic Intelligence (SI) [22], which estimates the
importance of weights based on weighted regularization loss and gradient.
Alternative approaches are LwF [28], and EWC [20]. The most relevant works for
this study belong to the architectural category, which represents a promising
direction in recent works [21].

The architectural methods concentrate on the topology of the neural model. One
of the most known and effective methods is CWRStar [31] which performs weights
copy and re-initializes weights at the last layer to accommodate new tasks.
More efficient methods are those based on pruning which deals with the issue
of increasing model capacity and removes unimportant weights. Notable examples
include PackNet [32], which divides the model into independent sub-networks to
address different tasks. Such an approach is thought to be forget-free since
sub-networks are directly mapped to tasks and are not subject to change
weights. However, a major limitation is the risk of growing model capacity.
This issue has recently encouraged researchers to explore and devise pruning
methods, to reduce model capacity and storage requirements.

Pruning in neural networks can be structural and non-structural. Works in [39,
78, 77, 73, 74, 76, 80] concentrate on structural pruning, which involves
pruning entire channels in filters by means of different techniques. Non-
structural pruning can be carried out on pretrained models without retraining
as in [64, 68], which results in increased efficiency, or with retraining, as
in lottery tickets search [66], movement pruning [67], and variational dropout
[79]. Other efficient pruning methods include genetic-based approaches as in
[51], which adopts constant masks and defines its own crossover and mutation
operators, and reinforcement techniques as in [52]. Pruning can be conducted
in combination with retraining to avoid performance drops caused by weights’
removal [64]. Two recent continual learning methods adopting pruning
approaches are SupSup [18] and Winning Subnetworks (WSN) [21]. SupSup finds
the optimal binary mask on a fixed backbone network for each new task. On the
other hand, WSN introduced significant improvement over Packnet, as it only
considers a subset of weights from the previous task to avoid a biased forward
transfer. Another recent trend is that expandable model architectures with
compression. The Dynamically Expandable Representation (DER) method [7] adds a
new submodule to the main model each time a new task is presented, while
leveraging pruning as an additional mode. Authors in [8] present the Dytox
method, which is based on Transformer attention blocks. The continual learning
model consists of an encoder part - common for all tasks and a decoder, which
is task-specific. On the other hand, FOSTER [9] proposes a boosting approach
that expands the network by means of a new residual feature extractor and a
linear classifier layer. Both Dytox [8] and FOSTER [9] incorporate a replay
strategy to improve the model’s efficiency.

Quantization is one of the most efficient techniques for the compression of
deep learning models [68, 58]. Common strategies include the quantization of
all coefficients in a single layer with a specified number of bits to
represent the integer and fractional parts [41, 42] based on the range of
values of the coefficients set. Another strategy is to represent coefficients
and data by integer numbers with an appropriate scaling factor. Many
quantization approaches in the literature adopt linear [68, 58, 42] or non-
linear approaches including clustering [57]. Quantization can be performed
during model training [58] or can be run on a pre-trained model [68, 57].
Recently, several methods for low-bit representation have been designed [43,
44, 45, 46, 47]. Many of them can not be run without some significant
degradation in accuracy. One known advantage of quantization is the fact that
it facilitates the adoption of deep neural networks in specialized hardware
accelerators with limited arithmetic bit-width and memory space [51]. However,
to the best of our knowledge, our paper is the first attempt to apply
quantization to CL models.

##  3 Ada-QPacknet algorithm

In this section, we describe our proposed Ada-QPacknet – a forget-free method
that leverages adaptive pruning and adaptive quantization to eliminate
catastrophic forgetting, effectively exploit model sparsity, and efficiently
use model capacity.

Figure 1 presents the overview of the Ada-QPacknet algorithm, illustrating the
iterative process of adaptive pruning and quantization on a typical training
scenario with multiple tasks.

Ada-QPacknet adapts the adaptive pruning process [51, 64] to reduce the size
of task sub-networks, since the most significant drawback of state-of-the-art
forget-free methods such as PackNet [32] and WSN [21], is the constant
sparsity level applied to all layers in consecutive tasks. This significantly
restricts the adaptability of the method and poses a risk of inefficient use
of model capacity. Another crucial feature of Ada-QPacknet is adaptive
quantization, which allows us to assign more than one task to each weight, by
dividing its capacity into components. The adaptive nature of the quantization
process allows Ada-QPacknet to identify the optimal bit-width for each task,
based on the trade-off between the number of bits assigned to each task and
the model performance. In the following subsections, we describe adaptive
pruning and adaptive quantization in more detail.

Figure 1: Overview of the proposed Ada-QPacknet method. Initially, the model
has a full bit-width representation represented by white rectangles. The
method follows an iterative process that includes adaptive pruning during
training and adaptive quantization. Adaptive pruning identifies different
sparsity levels for each layer. Adaptive quantization identifies the optimal
bit-width for each task (identified by different colors, i.e. red, blue,
purple, and yellow) and quantizes weights, improving the exploitation of model
capacity. The final model has four weights that support four different tasks,
illustrating an efficient use of model sparsity and capacity.

###  3.1 Adaptive Pruning with Sparsity Level Identification

In this stage, the goal is to perform pruning while identifying separate
sparsity levels for each layer. Sparsity levels should be as high as possible
to reduce memory occupation leaving more capacity for future tasks. The
representation of the pruned model $F_{\Theta}^{p}$ is the following tuple:

$F_{\Theta}^{p}=(F_{\Theta},M),$ (1)

where $F_{\Theta}$ is defined as:

$F_{\Theta}(X)={f_{\theta_{L}}(f_{\theta_{L-1}}...(f_{\theta_{0}}(X)))}.$ (2)

$F_{\Theta}$ is the original model with a set of convolutional and fully-
connected layers $f_{\theta_{i}}$, which are defined in the specified order.
The $\Theta$ tensor is defined as:

$\Theta=\\{\theta_{0},\theta_{1},...,\theta_{L}\\},$ (3)

and contains weights of convolutional and fully-connected layers. $\theta_{i}$
is a tensor of weights between layers $i$ and $i+1$. A single entry
$w_{i,k,l}$ represents a weight between $k$-th neuron in layer $i$ and $l$-th
neuron in layer $i+1$111To simplify our notation, we assume that a single
weight value is assigned to all tasks. In our method, multiple values for a
single weight can be assigned to solve multiple tasks..

$M$ is a set of masks:

$M=\\{M^{0},M^{1},...,M^{L}\\}.$ (4)

Each mask $M^{i}$ is positioned in between layers $i$ and $i+1$ and has the
same shape as $\theta_{i}$. Masks are used to decide which weights will be
used to solve specific tasks. A single entry in $M^{i}$ contains a set of
numbers indicating in which tasks the weight is used. Therefore, each weight
can be assigned to one or more tasks. A graphical representation is shown in
Figure 2.

A single entry in the mask $M^{i}$ is represented as a binary vector:

$M^{i}_{k,l}=\\{t_{1},t_{2},\dots,t_{n}\\},$ (5)

where $k$ is the source neuron in the layer $i$, $l$ is the destination neuron
in layer $i+1$, $t_{i}$ $\in$ {0,1} indicates if a given weight is used by the
$i$-th task.

The sparsity level $\Upsilon_{i}$ is a ratio between the number of weights
that are not yet assigned to any tasks and the number of all weights in a mask
$M^{i}$:

$\Upsilon_{i}=\frac{|M^{i}|-\sum_{k,l}^{{|M^{i}|}}(|M^{i}_{k,l}|>0)}{|M^{i}|}$
(6)

The overall weighted sparsity of the model is defined as:

$\Upsilon=\sum_{i}^{L}|\theta_{i}|\cdot\Upsilon_{i}$ (7)

####  3.1.1 Generating random lottery ticket mask

Each time a new task is encountered, for each layer, a number of candidate
masks $P_{S}$ are generated according to the random lottery ticker algorithm,
taking into account a sparsity level constraint between $V_{min}$ and
$V_{max}$ values. For example, a sparsity level of $0.5$ means that half of
all weights will be leveraged to solve the task. This way, we generate a
candidate mask for task $t$ and layer $l$:

$CM^{t}_{l}=\Big{\\{}e\ |\ \ e\in M^{i}\wedge\ \ |e|<T_{L}\Big{\\}},\
|CM^{t}_{l}|<|M^{i}|,$ (8)

where $|e|$ is the number of tasks already assigned to a weight $e$, and
$T_{L}$ is a constant that determines the capacity, i.e. the maximum number of
tasks that can be assigned to a single weight, according to the desired
quantization used. For instance, $T_{L}=4$ with a weight capacity of 32-bit
and a quantization rate is 8-bit. This formulation allows us to sample a
subset of available weights from the original mask (according to the sparsity
constraint) with zero or more prior assignments to tasks.

The set of candidate masks for all layers is defined as:

$CM^{t}=\\{CM^{t}_{0},CM^{t}_{1},\dots,CM^{t}_{L}\\}$ (9)

Once all candidate masks are generated, the best candidate according to the
resulting accuracy for the current layer is selected.

0: $P_{S}$ – population size

0: $\Theta$ – weights of the model

0: $\alpha$, $\beta$ – importance of accuracy and sparsity in selection

1: $\Theta$ $\leftarrow$ initialize the available weights in $\Theta$

2: $CM^{t}\leftarrow\emptyset$ // A set of candidate masks

3: $\Theta^{t}\leftarrow\emptyset$ // A set of masked weights

4: for $i=0$ to $P_{S}$ do

5: $CM^{t,i}\leftarrow$ random lottery ticket mask (eq: 9)

6: $\Theta^{t,i}$ = $\Theta$ $\odot$ $CM^{t,i}$ {Masked weights}

7: Execute short training $\Theta^{t,i}$ on task $t$

8: $CM^{t}$ $\leftarrow CM^{t}\cup CM^{t,i}$

9: $\Theta^{t}\leftarrow\Theta^{t}\cup\Theta^{t,i}$

10: end for

11: $A^{t}\leftarrow\forall_{CM^{t,i}\in CM^{t}}$ accuracy of $\Theta\odot$
$CM^{t,i}$ on task $t$

12: $\Upsilon^{t}\leftarrow\forall_{CM^{t,i}\in CM^{t}}$ compute
$\Upsilon_{i}$ for $CM^{t,i}$ (eq: 7)

13: $id=\underset{i\in\\{0,\dots,{P_{S}}\\}}{\mathrm{argmax}}\
(\alpha\cdot\frac{A_{i}}{max(A)}+\beta\cdot\frac{\Upsilon_{i}}{max(\Upsilon)})$

14: $M^{t}$ $\leftarrow$ $CM^{t,idx}$

15: $\Theta^{\prime}\leftarrow\Theta^{t,idx}$

16: Execute full training of $\Theta^{\prime}$ on task $t$

17: return $M^{t},\Theta^{\prime}$

Algorithm 1 Adaptive Pruning for task $t$

Algorithm 1 describes the task pruning process for a task $t$. We start with
the random initialization of available model weights (line 1). Two empty sets
are created: i) $CM^{t}$ used for storing candidate masks (line 2); ii)
$\Theta^{t}$ used for storing masked weights (line 3). After that, we generate
$P_{S}$ (population size) candidate masks (lines 4-10). For each generated
candidate mask (line 5), we train masked weights (lines 6-7) with a very
limited number of epochs. Then, we add the generated candidate mask and
trained weights to the respective sets (lines 8-9). In the next step, we
compute the accuracy $A^{t}$ for all generated candidates (line 11) and
weighted sparsity $\Upsilon^{t}$ (line 12). We identify the best model
according to the equation in line 13, where the evaluation simultaneously
considers accuracy and sparsity: between two candidates with similar accuracy
but dramatically different values of sparsity, the one with the highest level
of sparsity is preferred, as we want to preserve as many weights as possible
for future tasks. After this step, we perform the full training stage of the
masked weights $\Theta^{\prime}$ on the current task $t$.

Figure 2:  The figure presents the status of the model after it is trained,
pruned, and quantized for Task 1 (left) and Task 2 (right). During the
training stage for Task 1, Adaptive Pruning releases a subset of model weights
(dashed lines), which could be used later on to accommodate new tasks. After
that, Adaptive Quantization identifies the optimal bit-width and quantizes the
representation of the weights. In this example, weight representation of
32-bits is quantized into 2 bits (red squares). Values represented on this
bits are codes from a layer-wise codebook and can be translated into full
32-bits weights. This capability allows Ada-QPacknet to divide each weight
into multiple components, each of which can be assigned to any of the tasks.
The same process is repeated when Task 2 is presented: Adaptive Pruning
quantizes the 32-bits weight representation into a single bit (blue squares).

###  3.2 Adaptive Quantization

Quantization is a key stage in the Ada-QPacknet algorithm. Its purpose is
twofold: i) it allows us to assign a single weight to multiple tasks; ii) it
helps reducing the use of capacity of the model with a specified number of
tasks. The standard 32-bit single-weight representation is divided into
multiple components with a reduced number of bits, and each component can be
assigned to a different task, as shown in Figure 2. For example, one 32-bit
single-weight representation may be divided into four 8-bit components that
are assigned to any of the tasks. However, the adaptive nature of this process
is not dependent on equal-width components, but allows us to assign a varying
number of bits for each component, evaluating the trade-off between bit-width
and model performance. For example, a 32-bit single-weight representation may
also be divided into 3 components with the following bit-widths: 8, 10, 14,
etc.

0: $\psi$ – Initial bit-width

0: $Q_{q}$ – Model accuracy

0: $\Theta$ – Pruned model

0: $\delta$ – Maximum loss in accuracy

1: $\Theta_{q},K$ = nonlinear_quantization($\psi,\Theta$) {see Algorithm 3}

2: $Q_{q}$ = acc($F$, $\Theta_{q})$

3: while $Q_{q}$ $<$ $Q$ \- $\delta$ do

4: $\psi$ = $\psi$ \+ 1

5: $\Theta_{q},K$ = nonlinear_quantization($\psi,\Theta$)

6: $Q_{q}$ = acc($F$, $\Theta_{q})$

7: end while

8: return $\psi$ – optimal bit-width for the task, $\Theta_{q}$ – quantized
model, $K$ – codebook

Algorithm 2 Adaptive Quantization for task $t$.

Algorithm 2 presents the details of the adaptive quantization process. It
starts with non-linear quantization of the task-pruned model with minimal
values of parameters $\omega$ and $\psi$ (bit-width) (line 1). We leverage the
non-linear quantization algorithm detailed in Algorithm 3. Then, we check the
model accuracy (line 2). Next, if the drop in accuracy is more than the given
threshold $\delta$ (line 3) the iterative process of increasing the bit-width
is started (lines 3-7) until the drop in performance is deemed to be
acceptable.

The non-linear quantization approach devised in this work (see Algorithm 3) is
inspired by [57]. Specifically, we start with the identification of the number
of centroids $\omega$ and the creation of an empty codebook $K$ which will
store, for each layer, a mapping between code and weight values (lines 1-2).
We also create a copy of the model $\Theta$, where weights will contain codes
from the codebook (centroid indices) instead of real values. Subsequently, for
each layer $i$, we cluster weights values from layer $\theta_{i}$ leveraging
the K-Means clustering algorithm with a specified number of clusters $\omega$
(line 5). This step returns two outputs: a list of centroids $C$ and the list
of weight-to-centroid-index assignment $A$. We proceed by assigning the
corresponding centroid index to each weight (lines 6-8). To keep the mapping
between centroid indices and centroids, we build a codebook for each layer
(lines 9-11). The algorithm returns the copy of the model with quantized
weights obtained as codes from the codebook, as well as the codebook required
to decipher codes to the real value of the weight. We note that the number of
centroids is directly related to the desired bit-width (as shown in line 1). A
low number of centroids implies that the memory needed for storing the weights
is decreased. Each weight is stored as an index of the closest centroid. A
visual representation of the codebook is shown in Figure 2.

0: $\psi$ – desired bit-width

0: $\Theta$ – weights of a model

1: $\omega\leftarrow 2^{\psi}$ {Number of centroids}

2: $K\leftarrow[K_{0},K_{1},\dots,K_{|\Theta|}];K_{i}=\\{\\}$ {Empty codebook}

3: $\Theta^{\prime}\leftarrow$ copy of $\Theta$

4: for $\theta_{i}$ in $\Theta$ do

5: $C,A\leftarrow$ KMeans($\theta_{i}$, $\omega$) {$C$: centroids, $A$:
weight-to-centroid-index assignment}

6: for $\theta_{i,j}\in\theta_{i}$ do

7: $\theta^{\prime}_{i,j}\leftarrow A[\theta_{i,j}]$ {Use centroid index
instead of weight value}

8: end for

9: for $c_{k}\in C$ do

10: $K_{i}[k]\leftarrow c_{k}$ {Building layer-wise codebook}

11: end for

12: end for

13: return $\Theta^{\prime},K$

Algorithm 3 Non-linear quantization

##  4 Results

###  4.1 Experimental setup

The experiments were run for three CL scenarios: Permuted MNIST (p-MNIST)
[12], split CIFAR100 (s-CIFAR100) [13], and 5 datasets [10], a task-
incremental scenario consisting of MNIST, SVHN, FashionMNIST, CIFAR10, not-
MNIST, TinyImagenet [4], and Imagenet100 [5]. The p-MNIST scenario consists of
10 tasks with randomly permuted pixels of the original MNIST (10 tasks with 10
classes each). s-CIFAR100 is divided into 10 tasks with 10 classes each. The 5
datasets scenario is a sequence of 5 tasks with different datasets, each with
10 classes. The TinyImagenet scenario consists of 40 tasks with 5 randomly
sampled classes each. Finally, the Imagenet100 scenario consists of 10 tasks
with 10 randomly sampled classes each.

In our experiments, the pruning search population $PS$ is set to 16. Values
for $V_{MIN}$ and $V_{MAX}$ parameters are set to 0.45 and 0.85 for all
layers. The $\alpha$ and $\beta$ parameters are set to 0.9 and 0.1. The short
training during mask search is done with 5 epochs, while the full training for
the selected mask uses 50 epochs. For Ada-QPacknet, the learning rate is set
resorting to a dynamic scheduler starting from 0.01 and decreasing over time
with a minimum of 0.0001 for all datasets except for TinyImagenet (starting
from 0.001) and Imagenet100 (constant learning rate of 0.0001). The adopted
models are a two-layer neural network with fully connected layers (p-MNIST),
reduced AlexNet (s-CIFAR100) [27], Resnet-18 (5 datasets and Imagenet),
TinyNet (TinyImagenet) in accordance with model backbones used in the WSN
paper [21]. For weight initialization, we adopt the Xavier initializer.
Experiments are executed on a workstation equipped with an NVIDIA A100 GPU.
Our experiments involve 5 complete runs for each strategy. Therefore, the
total number of executions corresponds to the number of tasks in each scenario
multiplied by 5.

As for the metrics, we use the most standard definition of lifelong Accuracy
following the description in [34]. Moreover, we also compute the capacity
(total memory occupied by each task) inspired by the capacity computation in
[21], defined as follows:

$CAP_{t}=\sum_{i}^{L}(1-{\Upsilon_{i}})\cdot|\theta_{i}|\cdot b+|L|\cdot
2^{b}\cdot(32+b)\\\ +\sum_{i}^{L}(1-\Upsilon_{i})\cdot|M^{i}|$ (10)

The capacity can be regarded as the sum of three components. The first one
describes the number of the weights after the pruning multiplied by the bit-
width $b$. The second one describes the codebook size. The third one includes
all masks’ capacity.

###  4.2 Comparison to other methods

Table 1: Comparative results in terms of average accuracy for CL strategies in different CL scenarios: Permuted MNIST (p-MNIST), split-CIFAR100 (s-CIFAR100), and 5 datasets. | p-MNIST | s-CIFAR100 | 5 datasets | TinyImagenet
---|---|---|---|---
Naive | 60.12 | 17.32 | 33.08 | 20.27
CWRStar | 31.31 | 20.84 | 36,16 | 24.00
SI | 57.32 | 19.54 | 29.42 | 20.51
Replay | 62.22 | 19.60 | 55.24 | 23.14
CUMULATIVE | 96.45 | 36.52 | 84.44 | 27.53
Packnet | 96.31 | 72,57 | 92.59 | 55.46
WSN | 96.41 | 76.38 | 93.41 | 71.96
Ada-QPacknet | 97.1 | 74.1 | 94.1 | 71.9
Table 2: Capacity comparison for pruning-based methods Datasets | p-MNIST | s-CIFAR100 | 5 datasets | TinyImagenet
---|---|---|---|---
Packnet | 96.38% | 81.0% | 82.86% | 188.67%
WSN | 77.73% | 99.13% | 86.10% | 48.65%
Ada-QPacknet | 81.25% | 78.6% | 33.7% | 112.5%

Table 1 presents results in terms of average accuracy. In our experimental
analysis, we considered representatives from all categories of CL strategies.
Specifically, we considered Packnet and WSN (architectural) , Cumulative and
Replay (rehearsal), SI (regularization), and CWRStar (combined architectural
and regularization). The Naive strategy is a simple strategy where the model
is fine-tuned as new tasks are presented, and can be considered as a lower
bound. The Cumulative strategy, on the other hand, stores data from all tasks
observed so far to retrain the model, and is considered as an upper bound.

Results highlight that the Ada-QPacknet outperforms all the considered
strategies. In p-MNIST, Ada-QPacknet achieves $97.1\%$ ($0.50\%$ above
Cumulative), the WSN method ($96.41\%$) is just behind the Cumulative approach
($96.45\%$). Packnet achieves $96.31\%$, whereas the other methods
significantly underperform the architectural strategies (the following method
in the ranking is Replay with $62.22\%$). In s-CIFAR100, Ada-QPacknet achieves
$74.1\%$ average accuracy, achieving second-best performance. The best-
performing method is WSN, with a $2.28\%$ increase in performance, although
this method presents a higher capacity utilization when compared to Ada-
QPacknet, which yields the best results in terms of capacity ($78.6\%$). The
third strategy achieving satisfactory results is Packnet ($81.0\%$). The next
strategies in the ranking are Cumulative and CWRStar, with a significantly
lower accuracy ($36.52\%$ and $20.84\%$). In the 5 datasets scenario, Ada-
QPacknet ($94.1\%$) presents a better performance than the second-ranked WSN
($93.41\%$) and the third-ranked Packnet ($92.59\%$) with a significant
improvement for capacity ($33.7\%$) compared to Packnet ($82.86\%$) and WSN
($86.10\%$). We attribute this result to the low between-task similarity due
to the different datasets, which makes the weight reutilization strategy
adopted in Packnet and WSN less effective than Ada-QPacknet. The Cumulative
approach is quite close to these forget-free methods with a performance of
$84.44\%$. The other strategies achieve significantly worse results. In the
TinyImagenet scenario, WSN achieves the best-performing score ($71.96\%$),
slightly outperforming Ada-QPacknet ($71.9\%$), which appears to be the
second-best performing method. A possible explanation is that transfer
learning via weight reutilization performed by other strategies is more
effective in this scenario due to a higher task similarity when compared to 5
datasets. All the other strategies, such as Packnet ($55.46\%$), SI
($20.51\%$), Replay ($23.14\%$) are significantly worse and appear ineffective
in this scenario.

The results presented in Table 2 show the comparison of the model’s capacity
in three different architectural CL strategies. On p-MNIST, Packnet and WSN
use $96.38\%$ and $77.73\%$ of the original model capacity, respectively. At
the same time, Ada-QPacknet represents the middle ground, using $81.25\%$ of
the capacity while achieving the best-performing accuracy scores. In the case
of s-CIFAR100, we also observe that forget-free strategies are the best
performing. In this case, Ada-QPacknet (accuracy $74.1\%$, capacity $78.6\%$)
represents the best approach in capacity when compared to Packnet (accuracy
$72.57\%$, capacity $81.0\%$) and WSN (accuracy $76.38\%$, capacity
$99.13\%$), which suggests that the utilization of a higher capacity is a
necessary condition to achieve higher accuracy on this dataset, given its
complexity. As for the 5-datasets scenario, Ada-QPacknet achieves better
results than WSN and Packnet, while using a significantly lower model capacity
($33.7\%$ in comparison to over $80\%$ by both Packnet and WSN). Finally, as
for TinyImagenet, Ada-QPacknet presents second-best results in terms of
capacity utilization ($112.5\%$), positioning itself in the middle between WSN
($48.5\%$) and Packnet ($188.67\%$), which appears particularly ineffective.

Overall, our results highlight that Ada-QPacknet achieves competitive results
and compression ratios in all scenarios. It is noteworthy that Ada-QPacknet
vastly outperforms other methods on the most complex 5-datasets scenario built
upon heterogeneous datasets. One reason why Packnet and WSN manage to achieve
similar results for p-MNIST and s-CIFAR100 could be their ability to share
weights between tasks, while both aforementioned scenarios have homogeneous
tasks originating from a single dataset. Therefore, weight sharing provides a
huge advantage for WSN and Packnet.

Table 3: Comparison with SOTA architectural and replay methods on Imagenet100 (10/10). Methods | Parameters | Accuracy
---|---|---
FOSTER | - | 74.49
DyTox | 10.73M | 75.54
DER | 112.27M | 75.36
Ada-QPacknet | 11.5M | 72.26

Additional results on the Imagenet100 scenario with hybrid methods are
presented in Table 3. The results highlight that Ada-QPacknet ($72.26\%$) is
unable to outperform architectural methods extended with replay-based memory,
such as FOSTER ($74.49\%$), DyTox ($75.54\%$), and DER ($75.36\%$). This
phenomenon is expected due to the inherently higher complexity of hybrid
approaches deriving from the memory component. Nevertheless, Ada-QPacknet
performance appears still relatively close to hybrid methods, with a very low
capacity occupation ($11.5$M), which is comparable to DyTox ($10.73$M) and
significantly better than DER (112.27M) 222For FOSTER, we do not report the
number of parameters, since it was not available in the original publication..
We also note that these experiments were run without performing an extensive
optimization for Ada-QPacknet hyperparameters (e.g., we used a fixed learning
rate configuration) due to the extremely time-consuming requirements of the
Imagenet100 scenario. For this reason, we expect that a better set of
hyperparameters can be identified for our proposed method, which would
position its accuracy closer to that of hybrid methods.

###  4.3 Ablation study

We conduct experiments to verify that all stages of Ada-QPacknet contribute to
the final model capabilities. Our ablation study is twofold and aims at
assessing: i) model capacity (see Table 4), and ii) model accuracy (see Table
5) when a specific component of Ada-QPacknet is enabled.

Focusing on the most crucial factor - capacity, results in Table 4 show that,
on average, pruning allows to free a significant amount of model capacity
($45.0\%$ for p-MNIST, $50.0\%$ for s-CIFAR100, $52\%$ for 5-datasets). On the
other hand, quantization frees, on average, a higher amount of capacity
($86.58\%$) for all three scenarios (p-MNIST, s-CIFAR100, and 5-datasets).
This behavior is expected since quantization has the potential to identify a
low number of bits that retain most of the model accuracy, which is a finer-
grained work (considering that a certain number of bits can be freed from each
weight) when compared to adaptive pruning (which can only remove weight in its
entirety). When combined, the two stages yield a remarkable capacity reduction
per task ($91.88\%$ for p-MNIST, $92.30\%$ for s-CIFAR100, $90.10\%$ for
5-datasets).

Analyzing the results from the model accuracy viewpoint allows us to
understand the trade-off between the model capacity (freed by adaptive pruning
and quantization) and the corresponding model accuracy. Results in Table 5
show that quantization yields higher accuracy than pruning. It is clear that
the removal of some weights may have more impact than reducing their bit-width
in an adaptive and non-linear way. For example, for p-MNIST, the model with
adaptive pruning yields an accuracy of $97.1\%$, and the quantization yields
an accuracy of $98.5\%$. The other datasets follow a similar pattern with
quantization yielding $75.8\%$ and $95.2\%$ accuracy for s-CIFAR100 and
5-datasets respectively, where pruning yields an accuracy of $75.3\%$ and
$94.4\%$. As for the final Ada-QPacknet, the accuracy is equal or lower than
that of a single component: $97.1\%$, matching the performance of pruning,
which is lower than $98.5\%$ (quantization) for p-MNIST, whereas it drops from
$75.3\%$ (pruning) and $75.8\%$ (quantization) to $74.1\%$ for s-CIFAR100,
from $94.4\%$ (pruning) and $05.2\%$ (quantization) to $94.1\%$ for
5-datasets. However, a degree of reduction is expected since the model is
being simplified by adaptive pruning and quantization, and it is reassuring to
see that the performance drop is not significant.

Overall, we conclude that both adaptive pruning and quantization contribute to
model capacity reduction, enabling the model to accommodate future tasks
without significantly impacting model accuracy. We note that results for our
method without capacity reduction pruning and quantization are missing, as
their interpretation would be cumbersome. Conceptually, Ada-QPacknet without
pruning and quantization could be reformulated in two ways: i) behave
similarly to Naive, where the same model is fully retrained as a new task is
observed, leading to forgetting; ii) being a forget-free model, which,
however, would fully saturate its capacity after the first task, invalidating
its lifelong learning capabilities.

Table 4: Capacity of each component and both combined (Ada-QPacknet), average per each task Datasets | p-MNIST | s-CIFAR100 | 5 datasets
---|---|---|---
pruning | 45.0% | 50.0% | 52.0%
quantization | 12.5% | 15.25% | 12.5%
Ada-QPacknet | 8.12% | 7.7% | 9.9%
Table 5: Accuracy of each component and both combined (Ada-QPacknet) Datasets | p-MNIST | s-CIFAR100 | 5 datasets |
---|---|---|---|---
pruning | 97.1 | 75.3 | 94.4 |
quantization | 98.5 | 75.8 | 95.2 |
Ada-QPacknet | 97.1 | 74.1 | 94.1 |

In addition to our ablation study, we report some patterns that emerged during
our experiments. For most of the scenarios tasks, the performance drop
observed with 4-bit quantization was less than $1\%$ for all tasks (in
comparison to full 32-bit weights). For example, in p-MNIST, a performance
drop of $-0.5\%$, $-1.9\%$, and $-3.0\%$ was observed with 3, and 2 bits,
respectively. In 5 datasets, tasks have shown a different degree of complexity
ranging from low (3 bits were used for p-MNIST, notMNIST, and s-CIFAR100),
medium (4 bits for Fashion MNIST), and high (5 bits for SVHN). For
Imagenet100, the least configuration yielding a negligible drop in accuracy
was 5 bits. It should be noted that for TinyImagenet, the overall capacity was
decreased by allocating 5 separate subnetworks, each with 8 tasks. This choice
allowed us to minimize the number of bits per mask, which would otherwise be
40 bits due to the 40 tasks included in this dataset.

From a computational complexity viewpoint, we observed that the training time
in Ada-QPacknet is dominated by lottery ticket search, whereas quantization
adds a negligible cost to the execution time since it is done post-training.
Comparing our method with WSN and PackNet, we observed an overhead of about
$50\%$ in terms of overall execution time. This result shows that the positive
results obtained in terms of model accuracy and capacity for Ada-QPacknet are
achieved with a reasonable execution time that fundamentally lies in the same
complexity class as its direct competitors.

##  5 Conclusions and future works

In this paper, we proposed Ada-QPacknet, a novel forget-free architectural
method for continual learning that resorts to adaptive pruning and adaptive
quantization. The adaptive pruning approach allows the method to identify the
near optimal subset of weights that preserves the performance of the model on
single tasks while minimizing the capacity required to solve each task.
Moreover, the adaptive quantization strategy adopted in our method allows the
use of a single weight for more than one task without any significant drop in
performance. The presented results show that our proposed method achieves
competitive results in terms of accuracy and utilization of model capacity
than many continual learning strategies, including popular forget-free
methods. In future work, we will focus on devising more robust modeling
capabilities to better deal with complex scenarios (such as Imagenet100) where
Ada-QPacknet achieved a suboptimal performance. Specifically, we will focus on
estimating layer sensitivities and correlations between task distributions in
order to estimate sparsity-level boundaries for new tasks. Moreover, we will
investigate the adoption of weight sharing, to achieve higher compression
ratios per task, as well as hybrid quantization. Finally, we will devise a
mechanism to select the most suitable mask among the available ones allocated
to previously learned tasks once full model capacity is reached.

## Acknowledgments

This research was supported in part by the PLGrid Infrastructure.

## References

  * [1] Joao Rafael, Ivo Correia, Alcides Fonseca, and Bruno Cabral, _Dependency-Based Automatic Parallelization of Java Applications_ , August 2014, DOI: 10.1007/978-3-319-14313-2_16
  * [2] Kamil Faber and Roberto Corizzo and Bartlomiej Sniezynski and Nathalie Japkowicz, _VLAD: Task-agnostic VAE-based lifelong anomaly detection_ , Neural Networks, vol. 165, pp. 248-273, 2023
  * [3] Zhou, Da-Wei and Wang, Qi-Wei and Qi, Zhi-Hong and Ye, Han-Jia and Zhan, De-Chuan and Liu, Ziwei, _Deep class-incremental learning: A survey_ , arXiv preprint arXiv:2302.03648, 2023
  * [4] Le, Ya and Yang, Xuan, __Tiny imagenet visual recognition challenge
  * [5] Russakovsky, Olga and Deng, Jia and Su, Hao and Krause, Jonathan and Satheesh, Sanjeev and Ma, Sean and Huang, Zhiheng and Karpathy, Andrej and Khosla, Aditya and Bernstein, Michael, _Imagenet large scale visual recognition challenge_ , International journal of computer vision, vol. 115, pp. 211–252, 2015, Springer
  * [6] Parisi, German I and Kemker, Ronald and Part, Jose L and Kanan, Christopher and Wermter, Stefan, _Continual lifelong learning with neural networks: A review_ , Neural networks, vol. 113, pp. 54-71, 2019, Elsevier
  * [7] Yan, S. and Xie, J. and He, X., _DER: Dynamically Expandable Representation for Class Incremental Learning_ , IEEE Conference on Computer Vision and Pattern Recognition (CVPR), 2021
  * [8] Douillard, A. and Rame, A. and Couairon, G. and Cord, M., _DyTox: Transformers for Continual Learning with DYnamic TOken eXpansion_ , IEEE Conference on Computer Vision and Pattern Recognition (CVPR), 2022
  * [9] Wang, F.-Y. and Zhou, D.-W. and Ye, H.-J. and Zha, D.-C., _FOSTER: Feature Boosting and Compression for Class-Incremental Learning_ , European Conference on Computer Vision (ECCV), 2022
  * [10] Ebrahimi, Sayna and Meier, Franziska and Calandra, Roberto and Darrell, Trevor and Rohrbach, Marcus, _Adversarial continual learning_ , European Conference on Computer Vision, pp. 386-402, 2020, Springer
  * [11] Kour, George and Saabne, Raid, _Real-time segmentation of on-line handwritten arabic script_ , Frontiers in Handwriting Recognition (ICFHR), pp. 417-422, 2014, IEEE
  * [12] Yann Le Cun, _The MNIST database of handwritten digits_ , http://yann. lecun. com/exdb/mnist/
  * [13] Alex Krizhevsky, _Learning Multiple Layers of Features from Tiny Images_ , 2009
  * [14] Hadash, Guy and Kermany, Einat and Carmeli, Boaz and Lavi, Ofer and Kour, George and Jacovi, Alon, _Estimate and Replace: A Novel Approach to Integrating Deep Neural Networks with Existing Applications_ , arXiv preprint arXiv:1804.09028, 2018
  * [15] Bengio, Yoshua and LeCun, Yann, _Scaling Learning Algorithms Towards AI_ , Large Scale Kernel Machines, MIT Press, 2007
  * [16] Hinton, Geoffrey E. and Osindero, Simon and Teh, Yee Whye, _A Fast Learning Algorithm for Deep Belief Nets_ , Neural Computation, pp.1527-1554, vol. 18, 2006
  * [17] Bengio, Yoshua and Louradour, Jérôme and Collobert, Ronan and Weston, Jason, _Curriculum learning_ , Proceedings of the 26th annual international conference on machine learning, pp.41-48, 2009
  * [18] Wortsman, Mitchell and Ramanujan, Vivek and Liu, Rosanne and Kembhavi, Aniruddha and Rastegari, Mohammad and Yosinski, Jason and Farhadi, Ali, _Supermasks in Superposition_ , arXiv, https://arxiv.org/abs/2006.14769, 2020
  * [19] David Lopez-Paz, Marc’Aurelio Ranzato, journal = arXiv, _Gradient Episodic Memory for Continual Learning_ , arXiv, https://arxiv.org/abs/1706.08840, 2017
  * [20] author = Kirkpatrick, James and Pascanu, Razvan and Rabinowitz, Neil and Veness, Joel and Desjardins, Guillaume and Rusu, Andrei and Milan, Kieran and Quan, John and Ramalho, Tiago and Grabska-Barwinska, Agnieszka and Hassabis, Demis and Clopath, Claudia and Kumaran, Dharshan and Hadsell, Raia, _Overcoming catastrophic forgetting in neural networks_ , arXiv, https://arxiv.org/abs/1612.00796, 2016
  * [21] Kang, Haeyong and Mina, Rusty J. L. and Rizky, Sultan and Madjid, Hikmawan and Yoon, Jaehong and Hasegawa-Johnson, Mark and Ju-Hwang, Sung and Yoo, Chang D., _Forget-free Continual Learning with Winning Subnetworks_ , ICML, 2022
  * [22] Zenke, Friedemann and Poole, Ben and Ganguli, Surya, _Continual Learning Through Synaptic Intelligence_ , arXiv, https://arxiv.org/abs/1703.04200, 2017
  * [23] Sylvestre-Alvise, Rebuffi and Kolesnikov, Alexander and Lampert, Christoph H., _iCaRL: Incremental classifier and representation learning_ , arXiv, arXiv:1611.07725,2016
  * [24] Masse, Nicolas Y. and Grant, Gregory D. and Freedman David J., _Alleviating catastrophic forgetting using context-dependent gating and synaptic stabilization_ , Salk Institute for Biological Studies, 2018
  * [25] Chaudhry, Arslan and Ranzato, Marc’Aurelio and Rohrbach, Marcus and Elhoseiny, Mohamed, _Efficient Lifelong Learning with A-GEM_ , arXiv:1812.00420, arXiv, 2019
  * [26] Ameya Prabhu, Philip H. S. Torr and Puneet K. Dokania, _GDumb: A Simple Approach that Questions Our Progress in Continual Learning_ , Lecture Notes in Computer Science (LNIP), vol. 12347, 2020
  * [27] Saha, Gobinda and Garg, Isha and Roy, Kaushik, _Gradient Projection Memory for Continual Learning_ , International Conference on Learning Representations, 2020
  * [28] Li, Zhizhong and Hoiem, Derek, _Learning without forgetting_ , IEEE transactions on pattern analysis and machine intelligence, vol. 40, pp. 2935-2947, 2017
  * [29] M. van de Ven, Gido and Siegelmann, Hava T. and Tolias, Andreas S., _Brain-inspired replay for continual learning with artificial neural networks_ , Nature Communications, 2020
  * [30] Rusu, Andrei A. and Rabinowitz, Neil C. and Desjardins, Guillaume and Soyer, Hubert and Kirkpatrick, James and Kavukcuoglu, Koray and Pascanu, Razvan and Hadsell, Raia, _Progressive Neural Networks_ , arXiv, https://arxiv.org/abs/1606.04671, 2016
  * [31] Lomonaco, Vincenzo and Maltoni, Davide and Pellegrini, Lorenzo, _Rehearsal-Free Continual Learning over Small Non-I.I.D. Batches_ , 1st Workshop on Continual Learning in Computer Vision at CVPR2020, https://arxiv.org/abs/1907.03799, 2019
  * [32] Mallya, Arun and Lazebnik, Svetlana, _PackNet: Adding Multiple Tasks to a Single Network by Iterative Pruning_ , arXiv, https://arxiv.org/abs/1711.05769, 2017
  * [33] Kirkpatrick, James and Pascanu, Razvan and Rabinowitz, Neil and Veness, Joel and Desjardins, Guillaume and Rusu, Andrei A and Milan, Kieran and Quan, John and Ramalho, Tiago and Grabska-Barwinska, Agnieszka, _Overcoming catastrophic forgetting in neural networks_ , Proceedings of the national academy of sciences, vol. 114, pp. 3521-3526, 2017
  * [34] Díaz-Rodríguez, Natalia and Lomonaco, Vincenzo and Filliat, David and Maltoni, Davide, _Don’t forget, there is more than forgetting: new metrics for Continual Learning_ , arXiv preprint arXiv:1810.13166, 2018
  * [35] Cossu, Andrea and Graffieti, Gabriele and Pellegrini, Lorenzo and Maltoni, Davide and Bacciu, Davide and Carta, Antonio and Lomonaco, Vincenzo, _Is Class-Incremental Enough for Continual Learning?_ , Frontiers in Artificial Intelligence, vol.5, 2022, Frontiers Media SA
  * [36] Lomonaco, Vincenzo and Maltoni, Davide, _CORe50: a New Dataset and Benchmark for Continuous Object Recognition_ , Proceedings of the 1st Annual Conference on Robot Learning, pp. 17-26, vol. 78, 2017, Proceedings of Machine Learning Research
  * [37] Aljundi, Rahaf and Babiloni, Francesca and Elhoseiny, Mohamed and Rohrbach, Marcus and Tuytelaars, Tinne, _Memory Aware Synapses: Learning What (not) to Forget_ , Computer Vision – ECCV 2018, Springer International Publishing, pp. 144-161
  * [38] Matthias De Lange and Rahaf Aljundi and Marc Masana and Sarah Parisot and Xu Jia and Aleks Leonardis and Gregory G. Slabaugh and Tinne Tuytelaars, _A Continual Learning Survey: Defying Forgetting in Classification Tasks_ , IEEE Transactions on Pattern Analysis and Machine Intelligence, 2022, vol. 44, pp.3366-3385
  * [39] Aketi, S.A. and Roy, S. and Raghunathan, A. and Roy, K., _Gradual channel pruning while training using feature relevance scores for convolutional neural networks_ , pp. 171924–171932, IEEE Access 8, 2020
  * [40] Van de Ven, Gido M and Tolias, Andreas S, _Three scenarios for continual learning_ , arXiv preprint arXiv:1904.07734, 2019
  * [41] Anwar, S. and Hwang, K. and Sung, W., _Fixed point optimization of deep convolutional neural networks for object recognition_ , IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), pp. 1131-1135, 2015
  * [42] Gysel, P. and Motamedi, M. and Ghiasi, S., _Hardware-oriented approximation of convolutional neural networks_ , arXiv:1604.03168, 2016
  * [43] Park, E. and Ahn, J. and Yoo, S., _Weighted-Entropy-Based Quantization for Deep Neural Networks_ , IEEE Conference on Computer Vision and Pattern Recognition (CVPR), 2017 July
  * [44] Zhang, D. and Yang, J. and Ye, D. and Hua, G., _Learned quantization for highly accurate and compact deep neural networks_ , arXiv:1807.10029, 2018
  * [45] Jung, S. and Son, C. and Lee, S. and Son, J. and Kwak, Y. and Han, J.J. and Choi, C, _Joint training of low-precision neural network with quantization interval parameters_ , arXiv:1808.05779, 2018
  * [46] McDonnell, M. D., _Training wide residual networks for deployment using a single bit for each weight_ , ICLR, 2018
  * [47] Mishra, A. and Nurvitadhi, E., _WRPN: Wide Reduced-Precision Networks_ , ICLR, 2018
  * [48] Markus Nagel and Rana A. Amjad and Mart van Baalen and Christos Louizos and Tijmen Blankevoort. _Up or Down? Adaptive Rounding for Post-Training Quantization_ , Proceedings of ICML, 2020
  * [49] S. Mao and W.J. Dally, _Deep compression: Compressing deep neural network with pruning, trained quantization and huffman coding_ , 4th International Conference on Learning Representations, ICLR 2016, San Juan, Puerto Rico, May 2-4, 2016
  * [50] A. Ren and T. Zhang and S. Ye and J. Li and W. Xu and X. Qian and X. Lin and Y. Wang, _ADMM-NN: an algorithm-hardware co-design framework of dnns using alternating direction methods of multipliers_ , Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2019, pp. 925–938, April 13-17,
  * [51] K. Xu and D. Zhang, J. An and L. Liu and L. Liu and D. Wang, _GenExp: Multi-objective pruning for deep neural network based on genetic algorithm_ , Neurocomputing, April, 2021 DOI: 10.1016/j.neucom.2021.04.022
  * [52] S. Han and W.Dally, _Bandwidth-efficient deep learning_ , DAC, 2018
  * [53] A. Renda and J. Frankle and M. Carbin, _Comparing fine-tuning and rewinding in neural network pruning_ , ICLR, 2020
  * [54] Faber, Kamil and Corizzo, Roberto and Sniezynski, Bartlomiej and Japkowicz, Nathalie, _Active Lifelong Anomaly Detection with Experience Replay_ , IEEE 9th International Conference on Data Science and Advanced Analytics (DSAA), pp. 1-10, 2022, IEEE
  * [55] Megan M. Baker and Alexander New and Mario Aguilar-Simon and Ziad Al-Halah and Sébastien M.R. Arnold and Ese Ben-Iwhiwhu and Andrew P. Brna and Ethan Brooks and Ryan C. Brown and Zachary Daniels and Anurag Daram and Fabien Delattre and Ryan Dellana and Eric Eaton and Haotian Fu and Kristen Grauman and Jesse Hostetler and Shariq Iqbal and Cassandra Kent and Nicholas Ketz and Soheil Kolouri and George Konidaris and Dhireesha Kudithipudi and Erik Learned-Miller and Seungwon Lee and Michael L. Littman and Sandeep Madireddy and Jorge A. Mendez and Eric Q. Nguyen and Christine Piatko and Praveen K. Pilly and Aswin Raghavan and Abrar Rahman and Santhosh Kumar Ramakrishnan and Neale Ratzlaff and Andrea Soltoggio and Peter Stone and Indranil Sur and Zhipeng Tang and Saket Tiwari and Kyle Vedder and Felix Wang and Zifan Xu and Angel Yanguas-Gil and Harel Yedidsion and Shangqun Yu and Gautam K. Vallabha, _A domain-agnostic approach for characterization of lifelong learning systems_ , Neural Networks, vol. 160, pp. 274-296, 2023
  * [56] D. Lin and S. Talathi and V. Annapureddy, _Fixed point quantization of deep convolutional networks_ , vol. 48, pp. 2849-2858, ICLR, 2016
  * [57] Pietron, Marcin and Karwatowski, Michal and Wielgosz, Maciej and Duda, Jerzy, _Fast Compression and Optimization of Deep Learning Models for Natural Language Processing_ , CANDAR Workshops 2019, pp. 162-168, 2019
  * [58] Han, Song and Pool, Jeff and Tran, John and Dally, William, __Learning both weights and connections for efficient neural network, Advances in neural information processing systems, pp. 1135-1143, 2015
  * [59] Gysel, Philipp, _Ristretto: Hardware-oriented approximation of convolutional neural networks_ , arXiv preprint arXiv:1605.06402, 2016
  * [60] title=Pruning Filters while Training for Efficiently Optimizing Deep Learning Networks, author=Roy, Sourjya and Panda, Priyadarshini and Srinivasan, Gopalakrishnan and Raghunathan, Anand, journal=arXiv preprint arXiv:2003.02800, year=2020
  * [61] Zhao, Chenglong and Ni, Bingbing and Jian, Zhang and Zhao, Qiwei and Zhang, Wenjun and Tian, Qi, _Variational Convolutional Neural Network Pruning_ , 2019 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR), DOI: 10.1109/CVPR.2019.00289, 2019
  * [62] Krzysztof Wróbel and Michał Karwatowski and Maciej Wielgosz and Marcin Pietroń and Kazimierz Wiatr, _Compression of Convolutional Neural Network for Natural Language Processing_ , Computer Science, vol. 21, 2020, doi: 10.7494/csci.2020.21.1.337
  * [63] Jongsoo Park. and Sheng Li and Wei Wen and Ping Tak Peter Tang and Hai Li and Yiran Chen and Pradeep Dubey, _Faster CNNs with Direct Sparse Convolutions and Guided Pruning_ , 1608.01409, arXiv, 2016
  * [64] Marcin Pietron and Maciej Wielgosz, _Retrain or not retrain? – efficient pruning methods of deep CNN networks_ , 2002.07051, arXiv, 2020
  * [65] M.Pietron and M.Karwatowski and M.Wielgosz and J.Duda, _Fast Compression and Optimization of Deep Learning Models for Natural Language Processing_ , CANDAR Workshops, pp. 162-168, 2019
  * [66] J. Frankle and G.K. Dziugaite and D.M. Roy and M. Carbin, _The Lottery Ticket Hypothesis at Scale_ , 1903.01611, arXiv, March 2019
  * [67] V. Sanh and T. Wolf and A. M. Rush, _Movement Pruning: Adaptive Sparsity by Fine-Tuning_ , 2005.07683, arXiv, May 2020
  * [68] M. Al-Hami and M. Pietron and R. Casas and M. Wielgosz, _Methodologies of Compressing a Stable Performance Convolutional Neural Networks in Image Classification_ , pp. 1-23, Neural Processing Letters, January 2020
  * [69] CIFAR dataset, _https://paperswithcode.com/sota/image-classification-on-cifar-100_ , 2020
  * [70] Krizhevsky, Alex and Sutskever, Ilya and Hinton, Geoffrey E., _ImageNet Classification with Deep Convolutional Neural Networks_ , vol. 60, pp. 84–90, June 2017, Association for Computing Machinery
  * [71] K. He and X. Zhang and S. Ren and J. Sun, _Deep Residual Learning for Image Recognition_ , pp. 770-778, IEEE Conference on Computer Vision and Pattern Recognition (CVPR), 2016
  * [72] Simonyan, Karen and Zisserman, Andrew, _Very Deep Convolutional Networks for Large-Scale Image Recognition_ , arXiv 1409.1556, 2014
  * [73] Li, H. and Kadav, A. and Durdanovic, I. and Samet, H. and Graf, H., _Pruning filters for efficient convnets_ , arXiv preprint arXiv:1608.08710, 2016
  * [74] Liu, C. and Wu, H., _Channel pruning based on mean gradient for accelerating convolutional neural networks_ , Signal Processing, pp. 84–91, 2019
  * [75] Zhao, C. and Ni, B. and Zhang, J. and Zhao, Q. and Zhang, W. and Tian, Q., _Variational convolutional neural network pruning, in: Proc. of the IEEE Conference on Computer Vision and Pattern Recognition_ , pp. 2780–2789, 2019
  * [76] Wang, W. and Zhu, L. and Guo, B., _Reliable identification of redundant kernels for convolutional neural network compression_ , Journal of Visual Communication and Image Representation, 2019
  * [77] Hu, Y. and Sun, S. and Li, S. and Wang, X. and Gu, Q., _A novel channel pruning method for deep neural network compression_ , arXiv:1805.11394, 2018
  * [78] Chen, S. and Zhao, Q., _Shallowing deep networks: Layer-wise pruning based on feature representations_ , IEEE Transactions on Pattern Analysis and Machine Intelligence 41 (12), pp. 3048–3056, 2018
  * [79] Molchanov, D. and Ashukha, A. and Vetrov, D., _Variational dropout sparsifies deep neural networks, in: International Conference on Machine Learning_ , pp. 2498–2507, ICML, 2017
  * [80] Zhuang, Z. and Tan, M. and Zhuang, B. and Liu, J. and Guo, Y. and Wu, Q. and Huang, J. and Zhu, J., _Discrimination-aware channel pruning for deep neural networks_ , pp. 875–886, Advances in Neural Information Processing Systems (NeurIPs), 2018
  * [81] Huang, Q. and Zhou, K. and You, S. and Neumann, U., _Learning to prune filters in convolutional neural networks_ , pp. 709–718, IEEE Winter Conference on Applications of Computer Vision (WACV), 2018


# Practical Model Reductions for Verification of Multi-Agent Systems

Wojciech Jamroga1,2 Yan Kim1 1Interdisciplinary Centre for Security,
Reliability, and Trust, SnT, University of Luxembourg
2Institute of Computer Science, Polish Academy of Science, Warsaw, Poland
{wojciech.jamroga<EMAIL_ADDRESS>
###### Abstract

Formal verification of intelligent agents is often computationally infeasible
due to state-space explosion. We present a tool for reducing the impact of the
explosion by means of state abstraction that is (a) easy to use and understand
by non-experts, and (b) agent-based in the sense that it operates on a modular
representation of the system, rather than on its huge explicit state model.

##  1 Introduction

_Multi-agent systems (MAS)_ Wooldridge (2002); Shoham and Leyton-Brown (2009)
describe interactions of autonomous agents, often assumed to be intelligent
and/or rational. With the development of Internet and social networks, the
impact of MAS on everyday life is becoming more and more significant. At the
same time, their complexity is rapidly increasing. In consequence, formal
methods for analysis and verification of MAS are badly needed.

Verification and model reduction. Algorithms and tools for verification have
been in constant development for 40 years, with temporal model checking being
most popular Baier and Katoen (2008); Clarke et al. (2018). The main obstacle
for _practical_ use of those techniques is state-space explosion. Model
checking of MAS with respect to their _modular representations_ ranges from
$\mathbf{{PSPACE}}$-complete to undecidable Schnoebelen (2003); Jamroga
(2015). A possible way to mitigate the complexity is by model reductions, such
as abstraction refinement Clarke et al. (2000) and partial-order reduction
Peled (1993). Unfortunately, lossless reductions (i.e., ones that produce
fully equivalent models) are usually too weak, in the sense that the resulting
model is still too large for feasible verification.

Towards practical abstraction. In this work, we revisit the idea of lossy
state abstraction Cousot and Cousot (1977); Clarke et al. (1994), and in
particular _may/must abstraction_ Godefroid et al. (2001) that potentially
removes relevant information about the system, but produces arbitrarily small
reduced models. Such verification works best with users who are knowledgeable
about the application domain, as its conclusiveness crucially depends on what
aspects of the model are being removed. Ideally, the user should be a domain
expert, which often implies no in-depth knowledge of verification algorithms.
This calls for a technique that is easy to use and understand, preferably
supported by a Graphical User Interface (GUI). Moreover, the abstraction
should be _agent-based_ in the sense that it operates on modular
representations of the MAS, and does not require to generate the full
explicit-state model before the reduction. The theoretical backbone of our
abstraction scheme is presented in Jamroga and Kim (2022). Here, we report on
the implementation, and show its usefulness through case studies.

Contribution. We propose a tool for reduction of MAS models by removing an
arbitrary subset of variables from the model specification. After the user
selects the variables to be removed, the tool can produce two new model
specifications: one guaranteed to overapproximate, and one to underapproximate
the original model. Then, the user can verify properties of the original model
by model checking the new specifications with a suitable model checker. Our
model specifications are in the form of _MAS Graphs_ Jamroga and Kim (2022), a
variant of automata networks with asynchronous execution semantics and
synchronization on joint action labels Priese (1983); Jamroga et al. (2020).
As the model checker of choice, we use Uppaal Behrmann et al. (2004), one of
the few temporal model checkers with GUI.

Our tool provides a simple command-line interface, where the user selects the
input file with a model specification prepared in Uppaal, the variables to be
abstracted away, and the abstraction parameters. It outputs a file with the
over- (resp. under-)approximating model specification, that can be opened in
Uppaal for scrutiny and verification. The source code and examples are
available at https://tinyurl.com/ijcai-demo. Importantly, the abstraction uses
modular representations for input and output; in fact, it does _not_ involve
the generation of the global state space at all. To our best knowledge, this
is the first tool for practical user-defined model reductions in model
checking of MAS.

Related work. The existing implementations of state abstraction for temporal
model checking concern mostly automated abstraction. In particular, CEGAR
Clarke et al. (2000, 2003) has been implemented for NuSMV Cimatti et al.
(2002), and 3-valued abstraction Godefroid et al. (2001); Godefroid (2014) was
implemented in Yasm Gurfinkel et al. (2006) and YOGI Godefroid et al. (2010).
In each case, abstraction involves the generation of the global state space,
which is the main bottleneck when verifying MAS. Other, user-defined
abstraction schemes have been defined only theoretically Shoham and Grumberg
(2004); Ball and Kupferman (2006); Dams and Grumberg (2018), and also require
to generate all global states and/or transitions. The approaches in Cohen et
al. (2009); Belardinelli et al. (2019) come closest to our work, as they use
modular representations of the state space. However, they both need a global
representation of the transition space, and no implementation is reported.

##  2 Formal Background

MAS graphs and templates. To specify the system to be verified, we use _MAS
graphs_ , based on standard models of concurrency, and compatible with Uppaal
model specifications. A _MAS graph_ is a multiset of _agent graphs_ , possibly
sharing a set of _global variables_. Each agent graph includes finitely many
_locations_ and _private variables_ that, together, define its local state
space. Moreover, _edges_ between locations determine the local transition
relation. Each edge can be labelled with a randomized _selection_ command,
boolean _precondition_ , _synchronisation_ command, and/or a _postcondition_
updating the values of some variables. A synchronizing edge can only be taken
with a complementary one in another agent. An example agent graph is shown in
Figure 1.

A _MAS template_ treats each agent graph as a template, and specifies the
number of its instances that occur in the verified system (each differing only
by the value of variable id).

Models. Every MAS graph $G$ can be transformed to its _combined MAS graph_ :
technically, a single agent graph $comb(G)$ given by the asynchronous product
of the agent graphs in $G$. Each location in $comb(G)$ is a tuple of agents’
locations in $G$. Moreover, the set of variables in $comb(G)$ is the union of
all variables occurring in $G$. A _global model_ is obtained from $comb(G)$ by
unfolding it to the labelled transition system where states are defined by
combined locations and valuations of all the variables. Such models are
usually huge, and create an important bottleneck in model checking MAS.

Formal verification and model reduction. Our tool addresses model checking of
temporal properties expressed in the well known branching-time logic
$\mathbf{CTL^{\star}}$ Emerson (1990). To mitigate the impact of state-space
explosion, we use _state abstraction_ , i.e., a method that reduces the state
space by clustering similar _concrete states_ into a single _abstract state_.
In order for the scheme to be practical, it must be easy to use, and avoid the
generation of the concrete global model. We summarize the details of our
abstraction scheme in the next section.

Figure 1: _Voter_ template. The agent first declares if she prefers to receive
the election package by post (dec=2) or in person (dec=1). Then, she waits
until it can be collected, and casts the ballot together with her voting card.
The _select_ label for edge idle$\xrightarrow{}$waits (resp.
has$\xrightarrow{}$end) specifies a nondeterministic choice of the value of
variable $\texttt{dec}\in\\{{1,2}\\}$ (resp.
$\texttt{vt}\in\\{{1,\ldots,NC}\\}$ and $\texttt{sg}\in\\{{0,1}\\}$)

##  3 Abstraction by Removal of Variables

Our tool employs the abstraction scheme of Jamroga and Kim (2022), and
produces specifications of two abstract models: a _may-abstraction_ (that
overapproximates the concrete states and transitions) and a _must-abstraction_
(that underapproximates them). Consequently, if a universal
$\mathbf{CTL^{\star}}$ formula is true in the _may_ -abstraction, then it must
be true in the concrete model, and if it is false in the _must_ -abstraction,
then it must be false in the concrete model.

Variable removal. In the simplest variant, the abstraction concerns a complete
removal of some variables $V\subseteq\textit{Var}$ from the model
specification. For example, one might remove variables mem_vt, mem_sg from the
agent graph in Figure 1, i.e., the voter’s memory of the cast vote and the
voting declaration status. Selection of the right variables to remove requires
a good understanding of the application domain; we assume that it is provided
by the user. Roughly speaking, the abstraction procedure takes the combined
MAS graph $comb(G)$, computes an approximation of the reachable values for
every $v\in V$, and processes the edges of $comb(G)$ by substituting the
occurrences of $v$ at location $\ell$ with the values $u\in appr(v,\ell)$. If
$appr(v,\ell)$ overapproximates (resp. underapproximates) the actual reachable
values of $v$ at $\ell$, then the resulting model is a _may_ (resp.
_must_)-abstraction of $G$.

Variable merge and scoping. More generally, a subset of variables can be
merged into a fresh variable by means of a user-defined mapping function. For
example, mem_sg and mem_vt can be merged into a boolean variable valid given
by (mem_sg*mem_vt>0), indicating the validity of the vote.

Additionally the user can specify the scope of abstraction, i.e., a subset of
locations where the abstraction is applied.

Abstraction on MAS templates. In some cases, approximation of variable domains
on the combined MAS graph is computationally infeasible. An alternative is to
compute it directly on the MAS template by the right approximation of the
synchronization edges. On the down side, this sometimes results in largely
suboptimal abstract models, i.e., ones more likely to produce inconclusive
verification results.

#V | Concrete | Abstract (A1) | Abstract (A2) | Abstract (A3)
---|---|---|---|---
#St | t | #St | t | #St | t | #St | t
1 | 31 | 0 | 23 | 0 | 22 | 0 | 18 | 0
2 | 529 | 0.1 | 217 | 0.1 | 214 | 0.1 | 120 | 0.1
3 | 10891 | 0.1 | 2203 | 0.1 | 2440 | 0.1 | 838 | 0.1
4 | 2.3e+5 | 0.9 | 22625 | 1 | 29938 | 0.1 | 5937 | 0.1
5 | 5.1e+6 | 25 | 2.3e+5 | 1 | 3.7e+5 | 1 | 42100 | 0.6
6 | memout | 2.3e+6 | 20 | 4.9e+6 | 23 | 2.9e+5 | 5
7 | memout | 2.2e+7 | 304 | memout | 2.0e+6 | 33
8 | memout | memout | memout | 1.4e+7 | 357

Table 1: Verification of $\varphi_{\mathit{bstuff}}$ on models with 3
candidates. $\\#V$ is the number of Voter instances. We report the model
checking performance for the concrete model, followed by _may_ -models
obtained by abstractions A1, A2, and A3

##  4 Architecture

The main components of the tool are: (1) local domain approximation and (2)
generation of abstract model specifications. Additionally, the tool allows to
perform simple pre-processing and code analysis, and to store parameters in a
configuration file. Each component can be called from command line, possibly
followed by a list of arguments:

  * •

configure: sets the parameters in the configuration file;

  * •

unfold: produces the combined MAS graph;

  * •

approx: computes an approximation of the local domain;

  * •

abstract: generates an abstract model specification based on the provided
approximation of local domain;

  * •

info: lists the variables, locations, and edges in the model.

Local domain approximation. Takes a subset of variables $V$, a target template
(‘ext’ for the combined MAS graph) and an abstraction type
$\text{t}\in\\{{\text{upper},\text{lower}}\\}$, and computes a t-approximation
of the local domain over $V$. The result is saved to a JSON file, where
location identifiers are mapped to an array of evaluation vectors.

Abstract model generation. Takes the mapping function with an upper-
approximation (resp. lower-approximation) of the local domain, and computes
the corresponding may-abstraction (resp. must-abstraction). The mapping
function specifies the target agent name or template name, the scope of
abstraction, variables to be removed, and possibly a merge variable. We assume
that the input provided by the user is correct; some debugging might be added
in the future.

##  5 Experimental Results

We have evaluated the tool by means of experiments on two benchmarks: a simple
postal voting scenario and gossip learning for social AI. The model
specifications are available for download with the tool. The experiments have
been performed in combination with Uppaal v4.1.24 (32-bit) on a machine with
Intel i7-8665U 2.11 GHz CPU, running Ubuntu 22.04. We report the results for
_may-abstractions_ , typically more useful for universal branching-time
properties.

Postal voting. We use a scalable family of MAS graphs proposed in Kim et al.
(2022) to model a simplified postal voting system. The system consists of
$\mathit{NV}$ Voters, voting for $\mathit{NC}$ candidates, and a single
Election Authority, and proceeds in four subsequent phases: collection of
voting declarations, preparation and distribution of election packages, ballot
casting, and tallying. The verification concerns a variant of resistance to
ballot stuffing, expressed by formula $\varphi_{\mathit{bstuff}}$:

A[](b_recv<=ep_sent && ep_sent<=NV)

where b_recv and ep_sent are variables storing the number of received ballots
and sent election packages, respectively. For the experiments, we try the
following abstractions:

A1:

removes variables mem_vt and mem_sg from the Voter template, i.e., the voter’s
memory of the cast vote and the voting declaration status;

A2:

removes variables mem_dec at Voter’s locations {has, voted} and variable
dec_recv at Authority’s location {coll_vts}, i.e., the information about how
the election package has been delivered;

A3:

the combination of A1 and A2.

The results in Table 1 present the numbers of states in the global model
generated during the verification, as well as the verification running times
(in seconds), including the generation of abstract model specifications where
applicable. Formula $\varphi_{\mathit{bstuff}}$ is satisfied in all the
reported instances; all three abstractions have been conclusive on it.

#Ag | Concrete | Abstract
---|---|---
#St | t | #St | Reduct | t
2 | 165 | 0 | 38 | 76.97 | 0
3 | 8917 | 0.1 | 555 | 93.78 | 0
4 | 4.6e+5 | 1.5 | 10247 | 97.77 | 0.1
5 | 2.1e+7 | 123 | 1.5e+5 | 99.29 | 1.2
6 | memout | 2.8e+6 | – | 42
7 | memout | 4.1e+7 | – | 682
8 | memout | memout

Table 2: Verification of $\varphi_{\mathit{compr}}$ on models of social AI.
$\\#Ag$ is the number of agents. “Reduct” shows the level of reduction of the
state space (in %)

Social AI. The second series of experiments uses the specifications of gossip
learning for social AI Heaven (2013); Hegedüs et al. (2021), proposed in
Kurpiewski et al. (2023). The system consists of a ring network of AI agents,
acting in three phases: data gathering, learning, and sharing of knowledge.
The goal of the agents is to collectively reach knowledge of quality
$mqual\geq 2$. The system includes also an attacker who can impersonate any
agent and fake its quality level. The model specification given as
asynchronous MAS Jamroga et al. (2020) and coded in the input language of the
STV model checker Kurpiewski et al. (2021) was manually translated into the
input language of Uppaal. Afterwards, we hardcoded the attacker’s strategy to
always share the lowest quality model, and verified formula
$\varphi_{\mathit{compr}}$:

A[](exists(i:int[1,NA])(impersonated!=i &&

(!AI(i).wait || AI(i).mqual<2))).

$\varphi_{\mathit{compr}}$ says that, on all execution paths, at least one AI
agent is compromised. The model checking performance is shown in Table 2. We
have been able to conduct verification for concrete models with up to 5 agents
(4 honest AI and 1 attacker), and up to 7 agents after applying a _may_
-abstraction that discards all variables except for $mqual$ in the AI
template.

##  6 Conclusions

We propose a tool for practical model reductions in multi-agent systems. The
tool addresses state-space explosion by removal of selected variables from the
model while preserving the truth of $\mathbf{ACTL}$ formulas. The experiments
show significant gains in terms of verification time as well as memory, with
minimal time used by the abstraction procedure.

In the future, we plan to extend our tool to abstractions preserving temporal-
epistemic and strategic properties in combination with the MCMAS and STV model
checkers Lomuscio et al. (2017); Kurpiewski et al. (2021).

## Acknowledgments

The work was supported by NCBR Poland and FNR Luxembourg under the PolLux/FNR-
CORE projects STV (POLLUX-VII/1/2019) and SpaceVote (POLLUX-
XI/14/SpaceVote/2023), as well as the CHIST-ERA grant CHIST-ERA-19-XAI-010 by
NCN Poland (2020/02/Y/ST6/00064).

## References

  * Baier and Katoen [2008] C. Baier and J.-P. Katoen.  Principles of Model Checking.  MIT Press, 2008.
  * Ball and Kupferman [2006] T. Ball and O. Kupferman.  An abstraction-refinement framework for multi-agent systems.  In Proceedings of Logic in Computer Science (LICS), pages 379–388. IEEE, 2006.
  * Behrmann et al. [2004] G. Behrmann, A. David, and K.G. Larsen.  A tutorial on uppaal.  In Formal Methods for the Design of Real-Time Systems: SFM-RT, number 3185 in LNCS, pages 200–236. Springer, 2004.
  * Belardinelli et al. [2019] Francesco Belardinelli, Alessio Lomuscio, and Vadim Malvone.  An abstraction-based method for verifying strategic properties in multi-agent systems with imperfect information.  In Proceedings of AAAI, pages 6030–6037, 2019.
  * Cimatti et al. [2002] A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, M. Sebastiani, and A Tacchella.  NuSMV2: An open-source tool for symbolic model checking.  In Proceedings of Computer Aided Verification (CAV), volume 2404 of Lecture Notes in Computer Science, pages 359–364, 2002.
  * Clarke et al. [1994] E.M. Clarke, O. Grumberg, and D.E. Long.  Model checking and abstraction.  ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, 1994.
  * Clarke et al. [2000] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.  Counterexample-guided abstraction refinement.  In Proceedings of CAV, volume 1855 of Lecture Notes in Computer Science, pages 154–169. Springer, 2000.
  * Clarke et al. [2003] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.  Counterexample-guided abstraction refinement for symbolic model checking.  J. ACM, 50(5):752–794, 2003.
  * Clarke et al. [2018] E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem, editors.  Handbook of Model Checking.  Springer, 2018.
  * Cohen et al. [2009] Mika Cohen, Mads Dam, Alessio Lomuscio, and Francesco Russo.  Abstraction in model checking multi-agent systems.  In AAMAS (2), pages 945–952. Citeseer, 2009.
  * Cousot and Cousot [1977] P. Cousot and R. Cousot.  Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints.  In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.
  * Dams and Grumberg [2018] Dennis Dams and Orna Grumberg.  Abstraction and abstraction refinement.  In Handbook of Model Checking, pages 385–419. Springer, 2018.
  * Emerson [1990] E.A. Emerson.  Temporal and modal logic.  In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995–1072. Elsevier, 1990.
  * Godefroid et al. [2001] P. Godefroid, M. Huth, and R. Jagadeesan.  Abstraction-based model checking using modal transition systems.  In Proceedings of CONCUR, volume 2154 of Lecture Notes in Computer Science, pages 426–440, 2001.
  * Godefroid et al. [2010] Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and SaiDeep Tetali.  Compositional may-must program analysis: unleashing the power of alternation.  In Proceedings of POPL, pages 43–56. ACM, 2010.
  * Godefroid [2014] Patrice Godefroid.  May/must abstraction-based software model checking for sound verification and falsification.  In Orna Grumberg, Helmut Seidl, and Maximilian Irlbeck, editors, Software Systems Safety, volume 36 of NATO Science for Peace and Security Series, D: Information and Communication Security, pages 1–16. IOS Press, 2014.
  * Gurfinkel et al. [2006] Arie Gurfinkel, Ou Wei, and Marsha Chechik.  Yasm: A software model-checker for verification and refutation.  In Proceedings of CAV, volume 4144 of Lecture Notes in Computer Science, pages 170–174. Springer, 2006.
  * Heaven [2013] Douglas Heaven.  Social AI likes to gossip.  New Scientist, 218(2923):20, 2013.
  * Hegedüs et al. [2021] István Hegedüs, Gábor Danner, and Márk Jelasity.  Decentralized learning works: An empirical comparison of gossip learning and federated learning.  J. Parallel Distributed Comput., 148:109–124, 2021.
  * Jamroga and Kim [2022] Wojciech Jamroga and Yan Kim.  Practical abstraction for model checking of multi-agent systems.  arXiv preprint arXiv:2202.12016, 2022.
  * Jamroga et al. [2020] W. Jamroga, W. Penczek, T. Sidoruk, P. Dembiński, and A. Mazurkiewicz.  Towards partial order reductions for strategic ability.  Journal of Artificial Intelligence Research, 68:817–850, 2020.
  * Jamroga [2015] W. Jamroga.  Logical Methods for Specification and Verification of Multi-Agent Systems.  ICS PAS Publishing House, 2015.
  * Kim et al. [2022] Yan Kim, Wojciech Jamroga, and Peter Y.A. Ryan.  Verification of the socio-technical aspects of voting: The case of the Polish postal vote 2020.  In Proceedings of STAST, 2022.  To appear, available at https://arxiv.org/abs/2210.10694.
  * Kurpiewski et al. [2021] Damian Kurpiewski, Witold Pazderski, Wojciech Jamroga, and Yan Kim.  STV+Reductions: Towards practical verification of strategic ability using model reductions.  In Proceedings of AAMAS, pages 1770–1772. ACM, 2021.
  * Kurpiewski et al. [2023] Damian Kurpiewski, Wojciech Jamroga, and Teofil Sidoruk.  Towards modelling and verification of social explainable AI.  In Proceedings of ICAART, 2023.  To appear, available at https://arxiv.org/abs/2302.01063.
  * Lomuscio et al. [2017] A. Lomuscio, H. Qu, and F. Raimondi.  MCMAS: An open-source model checker for the verification of multi-agent systems.  International Journal on Software Tools for Technology Transfer, 19(1):9–30, 2017.
  * Peled [1993] Doron A. Peled.  All from one, one for all: on model checking using representatives.  In Costas Courcoubetis, editor, Proceedings of CAV, volume 697 of Lecture Notes in Computer Science, pages 409–423. Springer, 1993\.
  * Priese [1983] L. Priese.  Automata and concurrency.  Theoretical Computer Science, 25:221–265, 1983.
  * Schnoebelen [2003] Ph. Schnoebelen.  The complexity of temporal model checking.  In Advances in Modal Logics, Proceedings of AiML 2002. World Scientific, 2003.
  * Shoham and Grumberg [2004] Sharon Shoham and Orna Grumberg.  Monotonic abstraction-refinement for CTL.  In Proceedings of TACAS, volume 2988 of Lecture Notes in Computer Science, pages 546–560. Springer, 2004.
  * Shoham and Leyton-Brown [2009] Y. Shoham and K. Leyton-Brown.  Multiagent Systems - Algorithmic, Game-Theoretic, and Logical Foundations.  Cambridge University Press, 2009.
  * Wooldridge [2002] M. Wooldridge.  An Introduction to Multi Agent Systems.  John Wiley & Sons, 2002.