Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Learning Representations Through Contrastive Neural Model Checking

Vladimir Krsmanovic, Matthias Cosler, Mohamed Ghanem, Bernd Finkbeiner

TL;DR

The paper addresses the scarcity of learned representations in formal verification by proposing Contrastive Neural Model Checking (CNML), a self-supervised, dual-encoder framework that learns aligned embeddings for Linear-Time Temporal Logic (LTL) specifications and And-Inverter Graphs (AIGER) circuits. CNML uses a contrastive objective to pull together circuit-specification pairs that satisfy a given property while pushing apart non-satisfying pairs, enabling cross-modal and intra-modal retrieval and transferring to downstream tasks. A large synthetic CNML-base dataset (≈296k samples) is generated via formula construction and reactive synthesis, with augmentations to remove biases. Empirical results show CNML outperforms baselines on retrieval tasks, improves downstream model-checking performance, and generalizes from simple to complex formulas, illustrating that model checking can guide representation learning for formal languages.

Abstract

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.

Learning Representations Through Contrastive Neural Model Checking

TL;DR

The paper addresses the scarcity of learned representations in formal verification by proposing Contrastive Neural Model Checking (CNML), a self-supervised, dual-encoder framework that learns aligned embeddings for Linear-Time Temporal Logic (LTL) specifications and And-Inverter Graphs (AIGER) circuits. CNML uses a contrastive objective to pull together circuit-specification pairs that satisfy a given property while pushing apart non-satisfying pairs, enabling cross-modal and intra-modal retrieval and transferring to downstream tasks. A large synthetic CNML-base dataset (≈296k samples) is generated via formula construction and reactive synthesis, with augmentations to remove biases. Empirical results show CNML outperforms baselines on retrieval tasks, improves downstream model-checking performance, and generalizes from simple to complex formulas, illustrating that model checking can guide representation learning for formal languages.

Abstract

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.

Paper Structure

This paper contains 21 sections, 6 equations, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Related work
  3. Background
  4. Linear-Time Temporal Logic (LTL).
  5. And-Inverter Graphs.
  6. Model Checking.
  7. Contrastive Learning.
  8. Dataset
  9. Learning representations
  10. Model Architecture
  11. Training
  12. Model Evaluations
  13. Embedding Space Analysis
  14. Retrieval
  15. Downstream fine-tuning
  16. ...and 6 more sections

Figures (3)

  • Figure 1: Visualization of a simple circuit represented as an And-Inverter Graph and the corresponding AIGER text representation. The circuit models the behavior described by the formula $\varphi$.
  • Figure 2: Visualization of the forward pass and the computation of the two loss components.
  • Figure 3: Visualization of the Cosine Similarity Distribution produced by the CNML-base model