标题： 通过对比神经模型检测学习表示 显示英文标题

标题： Learning Representations Through Contrastive Neural Model Checking

摘要： 模型检查是验证安全关键系统与形式规范之间关系的关键技术，其中深度学习的最近应用已显示出前景。 然而，尽管在视觉和语言领域很普遍，表示学习在形式验证中仍研究不足。 我们引入了对比神经模型检查（CNML），这是一种新方法，利用模型检查任务作为学习对齐表示的指导信号。 CNML通过自监督对比目标将逻辑规范和系统联合嵌入到一个共享潜在空间中。 在行业启发的检索任务中，CNML在跨模态和同模态设置中显著优于算法和神经基线。 我们进一步证明，学习到的表示能够有效转移到下游任务，并推广到更复杂的公式。 这些发现表明，模型检查可以作为形式语言表示学习的目标。 显示英文摘要

摘要： 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.