**NeuroTactic** is a model for theorem proving which leverages [graph neural networks](https://paperswithcode.com/methods/category/graph-models) to represent the theorem and premises, and applies graph contrastive learning for pre-training. Specifically, premise selection is designed as a pretext task for the graph contrastive learning approach. The learned representations are then used for the downstream task, tactic prediction

The goal of **Triplet loss**, in the context of Siamese Networks, is to maximize the joint probability among all score-pairs i.e. the product of all probabilities. By using its negative logarithm, we can get the loss formulation as follows:

$$
L\_{t}\left(\mathcal{V}\_{p}, \mathcal{V}\_{n}\right)=-\frac{1}{M N} \sum\_{i}^{M} \sum\_{j}^{N} \log \operatorname{prob}\left(v p\_{i}, v n\_{j}\right)
$$

where the balance weight $1/MN$ is used to keep the loss with the same scale for different number of instance sets.

Triplet Loss

Triplet Loss in Siamese Network for Object Tracking

NeuroTactic

Graph Contrastive Pre-training for Effective Theorem Reasoning

JDeskew is a novel skew estimation method that extracts the dominant skew angle of the given document image by applying an Adaptive Radial Projection on the 2D Discrete Fourier Magnitude spectrum.

Source	Graph Contrastive Pre-training for Effective Theorem Reasoning
Year	2000
Data Source	CC BY-SA - https://paperswithcode.com