用模型检验任务训练模型，让逻辑公式和系统代码学会‘对话’。
Learning Representations Through Contrastive Neural Model Checking
- 用对比学习让逻辑公式与系统代码在共享空间对齐。
- 在跨模态和同模态检索中超越传统方法与神经网络基线。
- 学出的表示能迁移到下游任务并适应更复杂逻辑公式。
模型检查是验证安全关键系统是否满足形式规范的重要技术。尽管深度学习在视觉和语言领域广泛应用，但在形式验证中的表示学习仍不充分。本文提出对比神经模型检查（CNML），利用模型检查任务作为信号，通过自监督对比目标，将逻辑规范与系统共同嵌入到一个共享潜在空间。在工业启发的检索任务中，CNML在跨模态和同模态设置下显著优于算法和神经基线。进一步实验表明，所学表示可有效迁移至下游任务，并泛化至更复杂的公式。这些结果证明，模型检查可作为形式语言表示学习的有效目标。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。