Learning Representations Through Contrastive Neural Model Checking
This work addresses the need for better representation learning in safety-critical system verification, offering a novel approach that is incremental in applying contrastive methods to a new domain.
The paper tackled the problem of underexplored representation learning in formal verification by introducing Contrastive Neural Model Checking (CNML), which uses model checking as a signal to learn aligned representations, resulting in considerable outperformance over baselines on industry-inspired retrieval tasks and effective transfer to downstream tasks.
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.