Learning Representations Through Contrastive Neural Model Checking
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915532420153344 |
|---|---|
| author | Krsmanovic, Vladimir Cosler, Matthias Ghanem, Mohamed Finkbeiner, Bernd |
| author_facet | Krsmanovic, Vladimir Cosler, Matthias Ghanem, Mohamed Finkbeiner, Bernd |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_01853 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Learning Representations Through Contrastive Neural Model Checking Krsmanovic, Vladimir Cosler, Matthias Ghanem, Mohamed Finkbeiner, Bernd Machine Learning Logic in Computer Science 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. |
| title | Learning Representations Through Contrastive Neural Model Checking |
| topic | Machine Learning Logic in Computer Science |
| url | https://arxiv.org/abs/2510.01853 |