#### Introduction

* Automated Theorem Proving (ATP) - Attempting to prove mathematical theorems automatically.
* Bottlenecks in ATP:
    * **Autoformalization** - Semantic or formal parsing of informal proofs.
    * **Automated Reasoning** - Reasoning about already formalised proofs.
* Paper evaluates the effectiveness of neural sequence models for premise selection (related to automated reasoning) without using hand engineered features.
* [Link to the paper](https://arxiv.org/abs/1606.04442)

#### Premise Selection

* Given a large set of premises P, an ATP system A with given resource limits, and a new conjecture C, predict those premises from P that will most likely lead to an automatically constructed proof of C by A

#### Dataset

* Mizar Mathematical Library (MML) used as the formal corpus.
* The premise length varies from 5 to 84299 characters and over 60% if the words occur fewer than 10 times (rare word problem).

#### Approach

* The model predicts the probability that a given axiom is useful for proving a given conjecture.
* Conjecture and axiom sequences are separately embedded into fixed length real vectors, then concatenated and passed to a third network with few fully connected layers and logistic loss.
* The two embedding networks and the joint predictor path are trained jointly.

##### Stage 1: Character-level Models

* Treat premises on character level using an 80-dimensional one hot encoding vector.
* Architectures for embedding:
    * pure recurrent LSTM and GRU Network
    * CNN (with max pooling)
    * Recurrent-convolutional network that shortens the sequence using convolutional layer before feeding it to LSTM.

##### Stage 2: Word-level Models

* MML dataset contains both implicit and explicit definitions.
* To avoid manually encoding the implicit definitions, the entire statement defining an identifier is embedded and the definition embeddings are used as word level embeddings.
* This is better than recursively expanding and embedding the word definition as the definition chains can be very deep.
* Once word level embeddings are obtained, the architecture from Character-level models can be reused.

#### Experiments

##### Metrics

* For each conjecture, the model ranks the possible premises.
* Primary metric is the number of conjectures proved from top-k premises.
* Average Max Relative Rank (AMMR) is  more sophisticated measure based on the motivation that conjectures are easier to prove if all their dependencies occur earlier in ranking.
* Since it is very costly to rank all axioms for a conjecture, an approximation is made and a fixed number of random false dependencies are used for evaluating AMMR.

##### Network Training

* Asynchronous distributed stochastic gradient descent using Adam optimizer.
* Clipped vs Non-clipped Gradients.
* Max Sequence length of 2048 for character-level sequences and 500 for word-level sequences.

##### Results

* Best Selection Pipeline - Stage 1 character-level CNN which produces word-level embeddings for the next stage.
* Best models use simple CNNs followed by max pooling and two-stage definition-based def-CNN outperforms naive word-CNN (where word embeddings are learnt in a single pass).

Lauer and Needham explain the duality in expressiveness and performance between

 - message-oriented concurrency models in which there are a small number of fixed tasks that communicate explicitly, and
 - process-oriented concurrency models in which there are a larger number of dynamic processes that share memory.

Message-oriented systems can be characterized by the following hallmarks, consequences, and provided facilities.

| Hallmark                                                                                 | Consequences                                                                                            | Facilities                                                                                              |
|------------------------------------------------------------------------------------------|---------------------------------------------------------------------------------------------------------|---------------------------------------------------------------------------------------------------------|
| Long standing communication channels are typically created during program initialization | Synchronization is implicitly performed in the queues connecting processes                              | Messages and message ids                                                                                |
| There are a fewer number of long lasting processes                                       | Shared structures are passed by reference; only processes with a reference to a structure can act on it | Message channels and ports that provide the ability to Send, WaitForReply, WaitForMessage, or SendReply |
| Processes don't share memory                                                             | Peripheral devices are treated like processes and communicated with                                     | Process creation (but no deletion)                                                                      |
| Processes read a small number of messages at a time                                      |                                                                                                         |                                                                                                         |

Process-oriented systems can be similarly characterized:

| Hallmark                                                 | Consequences                                                         | Facilities                     |
|----------------------------------------------------------|----------------------------------------------------------------------|--------------------------------|
| Global data can be protected and accessed via interfaces | Synchronization is performed in locks                                | Procedures                     |
| Process creation and deletion is a lightweight task      | Data is shared directly, with small portions being locked            | fork/join procedure invocation |
| Processes typically have a single job                    | Peripheral interaction typically involves locking and sharing memory | Modules and monitors           |
| Module instantiation                                     |                                                                      |                                |
| Condition variables                                      |                                                                      |                                |

There is a duality between the two concurrency models. Any program in one has a corresponding program written in the other. Lauer and Needham demonstrate the duality not by simulating model's primitives using the other, but by drawing similarities between the two's components:

| Message-oriented                        | Process-oriented                  |
|-----------------------------------------|-----------------------------------|
| Processes, CreateProcess                | Monitors, NEW/START               |
| Message Channels                        | External Procedure identifiers    |
| Message Ports                           | ENTRY procedure identifiers       |
| SendMessage; AwaitReply                 | simple procedure call             |
| SendMessage; ... AwaitReply             | FORK; ... JOIN                    |
| SendReply                               | RETURN                            |
| WaitForMessage loop with case statement | monitor lock, ENTRY attribute     |
| arms of case statement                  | ENTRY procedure declarations      |
| selective waiting for messages          | condition variables, WAIT, SIGNAL |

This correspondence can be used to directly rewrite a canonical program between the two models. In fact, the differences between the two models becomes simply a matter of keyword choice. Moreover, if both models are implemented with identical blocking and scheduling mechanism, then the two models lead to identical performance as well. Since the choice of model does not affect the user or implementor, the decision of which model to use should be based on the architecture of the underlying hardware.

* Presents an architecture dubbed ResNeXt
* They use modules built of
    * 1x1 conv
    * 3x3 group conv, keeping the depth constant. It's like a usual conv, but it's not fully connected along the depth axis, but only connected within groups
    * 1x1 conv
    * plus a skip connection coming from the module input

* Advantages:
    * Fewer parameters, since the full connections are only within the groups
    * Allows more feature channels at the cost of more aggressive grouping
    * Better performance when keeping the number of params constant

* Questions/Disadvantages:
    * Instead of keeping the num of params constant, how about aiming at constant memory consumption? Having more feature channels requires more RAM, even if the connections are sparser and hence there are fewer params
    * Not so much improvement over ResNet

This preprint is a bit rambling, and I don't know that I fully followed what it was doing, but here's my best guess: 

https://i.imgur.com/xC2ryzp.png

- We think it's probably the case that SARS-COV2 (COVID19) uses a protease (enzyme involved in its reproduction) that isn't available and co-optable in the human body, and is also quite similar to the comparable protease protein in the original SARS virus. Therefore, it is hoped that we might be able to take inhibitors that bind to SARS, and modify them in small ways to make them bond to SARS-COV2
- The paper notes that it's specifically interested in targeted covalent inhibitors. These are drugs that inhibit the function of a protein by actually covalently binding with the relevant binding pocket, as opposed to most drugs, which by default just fit neatly inside the pocket and occupy it much of the time in equilibrium, but don't actually form permanent, stable covalent bonds with the protein. This class of drugs can be more effective, because its binding is stronger and more permanent, but it can also be more dangerous, because its potential side effects if it binds with a non-intended protein pocket can be more severe.
- In order to get a covalently-binding drug that fits with the pocket of SARS-COV2, the authors start with a known inhibitor from SARS, and then use reinforcement learning to make modifications to it. The allowed modification actions consist of adding or removing "fragments" rather than atoms, where "fragments" here refers to coherent subcomponents of other drugs from similar families that were broken up according to hand-coded chemical rules. This approach is more stable than just adding on molecules, because at every stage in generation, the generated molecule will be coherent and chemically sound.
- The part I don't fully follow is what they use for the reward function for compounds that are  in the process of being made. They specify that they do reward intermediate compounds, rather than just ones at the end of generation, but don't specify what goes into the reward. If I had to guess, I'd imagine it consists of (1) a molecular docking simulation that can't be differentiated through, and thus can't be used directly as a loss function, and/or (2) hand-coded heuristics from chemists for what makes a stable binding

_Objective:_ Robust unsupervised learning of a probability distribution using a new module called the `critic` and the `Earth-mover distance`.

 _Dataset:_ [LSUN-Bedrooms](http://lsun.cs.princeton.edu/2016/)

## Inner working:

Basically train a `critic` until convergence to retrieve the Wasserstein-1 distance, see pseudo-algorithm below:

[![screen shot 2017-05-03 at 5 05 09 pm](https://cloud.githubusercontent.com/assets/17261080/25667162/003c9330-3023-11e7-9081-c181011f4e6f.png)](https://cloud.githubusercontent.com/assets/17261080/25667162/003c9330-3023-11e7-9081-c181011f4e6f.png)

## Results:

*   Easier training: no need for batch normalization and no need to fine-tune generator/discriminator balance.
*   Less sensitivity to network architecture.
*   Very good proxy that correlates very well with sample quality.
*   Non-vanishing gradients.