Batch Normalization doesn't work well when using small batch sizes, which is often required for memory intensive tasks such as detection or segmentation, or memory intensive data such as 3D images, videos or high-res images.

Group Normalization is a simple alternative that is independent of the batch size:
![image](https://user-images.githubusercontent.com/8659132/57881829-3e255080-77f0-11e9-8ba0-56089c711e7b.png)

It works as BN, except with a different set of features for computing the mean and std:
![image](https://user-images.githubusercontent.com/8659132/57882429-ab85b100-77f1-11e9-86df-2c9865d28e8b.png)
The $\gamma$ and $\beta$ are learned per group and applied as usual:
![image](https://user-images.githubusercontent.com/8659132/57882468-c9ebac80-77f1-11e9-9d19-82b83b49ea24.png)

A group is defined as a set of channels, and the mean and std is computed for that set of channels for one sample, as illustrated:
![image](https://user-images.githubusercontent.com/8659132/57882184-200c2000-77f1-11e9-9d2c-8d3fad6d6827.png)
By default, there are 32 groups, but they show GN works well as long as there is more than one group but less than the number of channels.

In term of experiments, they try on ImageNet classification, detection and segmentation in COCO, and video classification in Kinetics. The conclusion is that **GN results in the same performance no matter the batch size, and that performance is the same as BN in large batches.** The most impressive result is a 10% increase in accuracy on ImageNet with a batch size of 2 over BN.

# Comments

- This paper got an honorable mention at ECCV 2018.
- I don't understand how it works at the entrance of the network, when there is only 1 or 3 channels. Are we just not supposed to put GN there?
- Also, the number of channels tends to increase in the network, but the number of groups stays fixed. Should it scale with the number of channels?
- They tested GN on many tasks, but mostly on ResNet. There was only one experiment on VGG-16, where they found no big difference with BN. For now I'm not convinced GN is useful outside of ResNet.

Code: https://github.com/facebookresearch/Detectron/tree/master/projects/GN

In the area of explaining model predictions over images, there are two main strains of technique: methods that look for pixels that have the highest gradient effect on the output class, and assign those as the “reason” for the class, and approaches that ask which pixel regions are most responsible for a given classification, in the sense that the classification would change the most if they were substituted with some uninformative reference value. 

The tricky thing about the second class of methods is that you need to decide what to use as your uninformative fill-in value. It’s easy enough to conceptually pose the problem of “what would our model predict if it couldn’t see this region of pixels,” but as a practical matter, these models take in full images, and you have to put *something* to give the classifier in a region, if you’re testing what the score would be if you removed the information contained in the pixels in that region. What should you fill in instead? The simplest answers are things like “zeros”, or “a constant value” or “white noise”. But all of these are very off-distribution for the model; it wouldn’t have typically seen images that resemble white noise, or all zeros, or all a single value. So if you measure the change in your model score from an off-distribution baseline to your existing pixels, you may not be getting the marginal value of the pixels, so much as the marginal disutility of having something so different from what the model has previously seen. There are other, somewhat more sensible approaches, like blurring out the areas around the pixel region of interest, but these experience less intense forms of the same issue. 

This paper proposes instead, using generative models to fill in the regions conditioned on the surrounding pixels, and use that as a reference. The notion here is that a conditioned generative model, like a GAN or VAE, can take into account the surrounding pixels, and “imagine” a fill-in that flows smoothly from the surrounding pixels, and looks generally like an image, but which doesn’t contain the information from the pixels in the region being tested, since it wasn’t conditioned on that. 

https://i.imgur.com/2fKnY0M.png

Using this approach, the authors run two types of test: one where they optimize to find the smallest region they can remove from the image, and have it switch class (Smallest Deletion Region, or SDR), and also the smallest informative region that can be added to an otherwise uninformative image, and have the model predict the class connected to that region. They find that regions calculated using their generative model fill in, and specifically with GANs, find a smaller and more compact pixel region as their explanation for the prediction, which is consistent with both human intuitions and also with a higher qualitative sensibleness of the explanations found. 

  * They suggest a new bounding box detector.
  * Their detector works without an RPN and RoI-Pooling, making it very fast (almost 60fps).
  * Their detector works at multiple scales, making it better at detecting small and large objects.
  * They achieve scores similar to Faster R-CNN.

### How
  * Architecture
    * Similar to Faster R-CNN, they use a base network (modified version of VGG16) to transform images to feature maps.
    * They do not use an RPN.
    * They predict via convolutions for each location in the feature maps:
      * (a) one confidence value per class (high confidence indicates that there is a bounding box of that class at the given location)
      * (b) x/y offsets that indicate where exactly the center of the bounding box is (e.g. a bit to the left or top of the feature map cell's center)
      * (c) height/width values that reflect the (logarithm of) the height/width of the bounding box
    * Similar to Faster R-CNN, they also use the concept of anchor boxes.
      So they generate the described values not only once per location, but several times for several anchor boxes (they use six anchor boxes).
      Each anchor box has different height/width and optionally scale.
    * Visualization of the predictions and anchor boxes:
      * ![predictions](https://github.com/aleju/papers/blob/master/neural-nets/images/SSD/predictions.jpg?raw=true "predictions")
    * They generate these predictions not only for the final feature map, but also for various feature maps in between (e.g. before pooling layers).
      This makes it easier for the network to detect small (as well as large) bounding boxes (multi-scale detection).
    * Visualization of the multi-scale architecture:
      * ![architecture](https://github.com/aleju/papers/blob/master/neural-nets/images/SSD/architecture.jpg?raw=true "architecture")
  * Training
    * Ground truth bounding boxes have to be matched with anchor boxes (at multiple scales) to determine correct outputs.
      To do this, anchor boxes and ground truth bounding boxes are matched if their jaccard overlap is 0.5 or higher.
      Any unmatched ground truth bounding box is matched to the anchor box with highest jaccard overlap.
    * Note that this means that a ground truth bounding box can be assigned to multiple anchor boxes (in Faster R-CNN it is always only one).
    * The loss function is similar to Faster R-CNN, i.e. a mixture of confidence loss (classification) and location loss (regression).
      They use softmax with crossentropy for the confidence loss and smooth L1 loss for the location.
    * Similar to Faster R-CNN, they perform hard negative mining.
      Instead of training every anchor box at every scale they only train the ones with the highest loss (per example image).
      While doing that, they also pick the anchor boxes to be trained so that 3 in 4 boxes are negative examples (and 1 in 4 positive).
    * Data Augmentation: They sample patches from images using a wide range of possible sizes and aspect ratios.
      They also horizontally flip images, perform cropping and padding and perform some photo-metric distortions.
  * Non-Maximum-Suppression (NMS)
    * Upon inference, they remove all bounding boxes that have a confidence below 0.01.
    * They then apply NMS, removing bounding boxes if there is already a similar one (measured by jaccard overlap of 0.45 or more).

### Results
  * Pascal VOC 2007
    * They achieve around 1-3 points mAP better results than Faster R-CNN.
    * ![results pascal](https://github.com/aleju/papers/blob/master/neural-nets/images/SSD/results_pascal.jpg?raw=true "results pascal")
    * Despite the multi-scale method, the model's performance is still significantly worse for small objects than for large ones.
    * Adding data augmentation significantly improved the results compared to no data augmentation (around 6 points mAP).
    * Using more than one anchor box also had noticeable effects on the results (around 2 mAP or more).
    * Using multiple feature maps to predict outputs (multi-scale architecture) significantly improves the results (around 10 mAP).
      Though adding very coarse (high-level) feature maps seems to rather hurt than help.
  * Pascal VOC 2012
    * Around 4 mAP better results than Faster R-CNN.
  * COCO
    * Between 1 and 4 mAP better results than Faster R-CNN.
  * Times
    * At a batch size of 1, SSD runs at about 46 fps at input resolution 300x300 (74.3 mAP on Pascal VOC) and 19 fps at input resolution 512x512 (76.8 mAP on Pascal VOC).
    * ![results timings](https://github.com/aleju/papers/blob/master/neural-nets/images/SSD/results_timings.jpg?raw=true "results timings")

Transformer is proposed to capture long-range information with the self-attention mechanism, but it comes with quadratic computation cost and lacks multi-resolution information. Then, Swin Transformer introduces local-window-self-attention to reduce the cost to linear w.r.t image size, shifted-window-attention to capture cross-window information and finally exploits multi-resolution information with hierarchical architecture. But shifted-window-attention struggles to capture long-range information due to the small coverage area of shifted-window-attention and lacks inductive-bias like ViT. Finally, Global Context ViT is proposed to address the limitations of the Swin Transformer.

Improvements:
(1) Unlike Swin Transformer this paper uses global context self-attention, with local self-attention, rather than shifted window self-attention, to model both long and short-range dependencies.

(2) Even though global-window-attention is a window-attention but it takes leverage of global query which contains global information and hence captures long-range information.

(3) In addition, this paper compensates for the lack of the inductive bias that exists in both ViTs and Swin Transformers by utilizing a CNN-based module.

Key components:

Stem/PatchEmbed: A stem/patchify layer processes images at the network’s beginning. For this network, it creates patches/tokens and converts them into embeddings.

Level: It is the repetitive building block that extracts features using different blocks.

Global Token Gen./FeatExtract: It generates global tokens/patches with Depthwise-CNN, SE (Squeeze-Excitation), CNN and MaxPooling. So basically it's a Feature Extractor.

Block: It is the repetitive module that applies attention to the features and projects them to a certain dimension.

Local-MSA: Local Multi head Self Attention.

Global-MSA: Global Multi head Self Attention.

MLP: Linear layer that projects a vector to another dimension.

Downsample/ReduceSize: It is very similar to Global Token Gen. module except it uses CNN instead of MaxPooling to downsample with additional Layer Normalization modules.

Head: It is the module responsible for the classification task.

Pooling: It converts  N×2D features to  N×1D features.

Classifier: It processes N×1D features to make a decision about class.

I annotated like this to make it easier to digest:
https://i.imgur.com/bTqIUH2.png

The goal is to solve SAT problems with weak supervision: In that case a model is trained only to predict ***the satisfiability*** of a formula in conjunctive normal form. As a byproduct, when the formula is satisfiable, an actual  satisfying assignment can be worked out by clustering the network's activations in most cases.

 * **Pros (+):** Weak supervision, interesting structured architecture, seems to generalize nicely to harder problems by increasing the number  message passing iterations.
 * **Cons (-):** Limited practical applicability since it is outperfomed by classical SAT solvers.
 
---
 
 # NeuroSAT
 
 ## Inputs
 We consider Boolean logic formulas in their ***conjunctive normal form*** (CNF), i.e. each input formula is represented as a conjunction ($\land$) of **clauses**, which are themselves disjunctions ($\lor$) of litterals (positive or negative instances of variables). The goal is to learn a classifier to predict whether such a formula is satisfiable.
 
 A first problem is how to encode the input formula in such a way that it preserves the CNF invariances (invariance to negating a litteral in all clauses, invariance to permutations in $\lor$ and $\land$ etc.). The authors use an  ***undirected graph representation*** where:
   * $\mathcal V$: vertices are the litterals (positive and negative form of variables, denoted as $x$ and $\bar x$) and the clauses occuring in the input formula
   * $\mathcal E$: Edges are added to connect (i) the litterals with clauses they appear in and (ii) each litteral to its negative counterpart. 
   
The graph relations are encoded as an ***adjacency matrix***, $A$, with as many rows as there are litterals and as many columns as there are clauses. In particular, this structure does not constrain the vertices ordering, and does not make any preferential treatment between positive or negative litterals. However it still has some caveats, which can be avoided by pre-processing the formula. For instance when there are disconnected components in the graph, the averaging decision rule (see next paragraph) can lead to false positives.
   
## Message-passing model
In a high-level view, the model keeps track of an embedding for each vertex (litterals, $L^t$ and clauses, $C^t$), updated via ***message-passing on the graph***, and combined via a Multi Layer perceptrion (MLP) to output the  model prediction of the formula's satisfiability. The model updates are as follow:

$$
\begin{align}
C^t, h_C^t &= \texttt{LSTM}_\texttt{C}(h_C^{t - 1}, A^T \texttt{MLP}_{\texttt{L}}(L^{t - 1}) )\ \ \ \ \ \ \ \ \ \ \ (1)\\
L^t, h_L^t &= \texttt{LSTM}_\texttt{L}(h_L^{t - 1}, \overline{L^{t - 1}}, A\ \texttt{MLP}_{\texttt{C}}(C^{t }) )\ \ \ \ \ \ (2)
\end{align}
$$

where $h$ designates a hidden context vector for the LSTMs. The operator $L \mapsto \bar{L}$  returns $\overline{L}$, the  embedding matrix $L$ where the row of each litteral is swapped with the one corresponding to the litteral's negation. 
In other words, in **(1)** each clause embedding is updated based on the litteral that composes it, while in **(2)** each litteral embedding is updated based on the clauses it appears in  and its negated counterpart.

After $T$ iterations of this message-passing scheme, the model computes a ***logit for the satisfiability classification problem***, which is trained via sigmoid cross-entropy:

$$
\begin{align}
L^t_{\mbox{vote}} &= \texttt{MLP}_{\texttt{vote}}(L^t)\\
y^t &= \mbox{mean}(L^t_{\mbox{vote}})
\end{align}
$$

---

# Training and Inference

## Training Set

The training set is built such that for any satisfiable training formula $S$, it also includes an unsatisfiable counterpart $S'$ which differs from $S$ ***only by negating one litteral in one clause***. These carefully curated samples should constrain the model to pick up substantial characteristics of the formula. In practice, the model is trained on formulas containing up to ***40 variables***, and on average ***200 clauses***. At this size, the SAT problem can still be solved by state-of-the-art solvers (yielding the supervision) but are large enough they prove challenging for Machine Learning models.


## Inferring the SAT assignment

When a formula is satisfiable, one often also wants to know a ***valuation*** (variable assignment) that satisfies it.
Recall that $L^t_{\mbox{vote}}$ encodes a "vote" for every litteral and its negative counterpart. Qualitative experiments show that thoses scores cannot be directly used for inferring the variable assignment, however they do induce a nice clustering of the variables (once the message passing has converged). Hence an assignment can be found as follows:
  * (1) Reshape $L^T_{\mbox{vote}}$  to size $(n, 2)$ where $n$ is the number of litterals. 
  * (2) Cluster the litterals into two clusters with centers $\Delta_1$ and $\Delta_2$ using the following criterion:
  \begin{align}
  \|x_i - \Delta_1\|^2 + \|\overline{x_i} - \Delta_2\|^2 \leq \|x_i - \Delta_2\|^2 + \|\overline{x_i} - \Delta_1\|^2
  \end{align}
  * (3) Try the two resulting assignments (set $\Delta_1$ to true and $\Delta_2$ to false, or vice-versa) and choose the one that yields satisfiability if any.
 
In practice, this method retrieves a satistifiability assignment for over 70% of the satisfiable test formulas.

---

# Experiments

In practice, the ***NeuroSAT*** model is trained with embeddings of dimension 128 and 26 message passing iterations using standard MLPs: 3 layers followed by ReLU activations. The final model obtains 85% accuracy in predicting a formula's satisfiability on the test set.

It also can generalize to ***larger problems***, requiring to increase the number of message passing iterations, although the classification performance decreases as the problem size grows (e.g. 25% for 200 variables).
 
Interestingly, the model also generalizes well to other classes of problems that  were first ***reduced to SAT***, although they have different structure than the random formulas generated for training, which seems to show that the model does learn some general structural characteristics of Boolean formulas.