# Learning Representations Through Contrastive Neural Model Checking

arXiv: https://arxiv.org/abs/2510.01853 · HTML: https://mlsanity.com/paper/2510.01853/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 38 of its 64 references that are in the map.
- First posted on arXiv 2 Oct 2025.

## Builds on (most cited first, 30 of 38)

- [Learning Transferable Visual Models From Natural Language Supervision](https://mlsanity.com/paper/2103.00020/) (2021)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [A Simple Framework for Contrastive Learning of Visual Representations](https://mlsanity.com/paper/2002.05709/) (2020)
- [Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks](https://mlsanity.com/paper/1908.10084/) (2019)
- [Representation Learning with Contrastive Predictive Coding](https://mlsanity.com/paper/1807.03748/) (2018)
- [Scaling Laws for Neural Language Models](https://mlsanity.com/paper/2001.08361/) (2020)
- [Scaling Up Visual and Vision-Language Representation Learning With Noisy Text Supervision](https://mlsanity.com/paper/2102.05918/) (2021)
- [Supervised Contrastive Learning](https://mlsanity.com/paper/2004.11362/) (2020)
- [HuggingFace's Transformers: State-of-the-art Natural Language Processing](https://mlsanity.com/paper/1910.03771/) (2019)
- [SimCSE: Simple Contrastive Learning of Sentence Embeddings](https://mlsanity.com/paper/2104.08821/) (2021)
- [CodeBERT: A Pre-Trained Model for Programming and Natural Languages](https://mlsanity.com/paper/2002.08155/) (2020)
- [Mixed Precision Training](https://mlsanity.com/paper/1710.03740/) (2017)
- [How to Fine-Tune BERT for Text Classification?](https://mlsanity.com/paper/1905.05583/) (2019)
- [Keystroke Dynamics as Part of Lifelogging](https://mlsanity.com/paper/2010.10144/) (2020)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [CLEAR: Contrastive Learning for Sentence Representation](https://mlsanity.com/paper/2012.15466/) (2020)
- [Contrastive Learning with Adversarial Examples](https://mlsanity.com/paper/2010.12050/) (2020)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Investigating Why Contrastive Learning Benefits Robustness Against Label Noise](https://mlsanity.com/paper/2201.12498/) (2022)
- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [A Primer on Contrastive Pretraining in Language Processing: Methods, Lessons Learned and Perspectives](https://mlsanity.com/paper/2102.12982/) (2021)
- [DeepGate3: Towards Scalable Circuit Representation Learning](https://mlsanity.com/paper/2407.11095/) (2024)
- [GILE: A Generalized Input-Label Embedding for Text Classification](https://mlsanity.com/paper/1806.06219/) (2018)
- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [CircuitFusion: Multimodal Circuit Representation Learning for Agile Chip Design](https://mlsanity.com/paper/2505.02168/) (2025)
- [DeepGate4: Efficient and Effective Representation Learning for Circuit Design at Scale](https://mlsanity.com/paper/2502.01681/) (2025)

## Abstract (arXiv)

Model checking is a key technique for verifying safety-critical systems against formal specifications, where recent applications of deep learning have shown promise. However, while ubiquitous for vision and language domains, representation learning remains underexplored in formal verification. We introduce Contrastive Neural Model Checking (CNML), a novel method that leverages the model checking task as a guiding signal for learning aligned representations. CNML jointly embeds logical specifications and systems into a shared latent space through a self-supervised contrastive objective. On industry-inspired retrieval tasks, CNML considerably outperforms both algorithmic and neural baselines in cross-modal and intra-modal settings. We further show that the learned representations effectively transfer to downstream tasks and generalize to more complex formulas. These findings demonstrate that model checking can serve as an objective for learning representations for formal languages.