paper-with-me

Papers

Neuro-Symbolic Verification of Deep Neural Networks

2022-03-02 · Xuan Xie, Kristian Kersting, Daniel Neider

Formal verification has emerged as a powerful approach to ensure the safety and reliability of deep neural networks. However, current verification tools are limited to only a handful of properties that can be expressed as first-order constraints over the inputs and output of a network. While adversarial robustness and fairness fall under this category, many real-world properties (e.g., "an autonomous vehicle has to stop in front of a stop sign") remain outside the scope of existing verification technology. To mitigate this severe practical restriction, we introduce a novel framework for verifying neural networks, named neuro-symbolic verification. The key idea is to use neural networks as part of the otherwise logical specification, enabling the verification of a wide variety of complex, real-world properties, including the one above. Moreover, we demonstrate how neuro-symbolic verification can be implemented on top of existing verification infrastructure for neural networks, making our framework easily accessible to researchers and practitioners alike.

📄 PDF Abstract BibTeX arXiv:2203.00938

Code (1)

lebronx/neuro-symbolic-verification 공식 구현 pytorch

Tasks

Adversarial RobustnessFairness

Similar Papers 제목 키워드 기반

NeuroStrata: Harnessing Neurosymbolic Paradigms for Improved Design, Testability, and Verifiability of Autonomous CPS

2025-02-17 · Xi Zheng, Ziyang Li, Ivan Ruchkin, Ruzica Piskac 외

Autonomous cyber-physical systems (CPSs) leverage AI for perception, planning, and control but face trust and safety certification challenges due to inherent uncertainties. The neurosymbolic paradigm replaces stochastic …

A Survey on Verification and Validation, Testing and Evaluations of Neurosymbolic Artificial Intelligence

2024-01-06 · Justus Renkhoff, Ke Feng, Marc Meier-Doernberg, Alvaro Velasquez 외

Neurosymbolic artificial intelligence (AI) is an emerging branch of AI that combines the strengths of symbolic AI and sub-symbolic AI. A major drawback of sub-symbolic AI is that it acts as a "black box", meaning that pr…

A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning

2025-12-17 · Daragh King, Vasileios Koutavas, Laura Kovacs arxiv

Loop invariant generation remains a critical bottleneck in automated program verification. Recent work has begun to explore the use of Large Language Models (LLMs) in this area, yet these approaches tend to lack a reliab…

Neurosymbolic Clinical Trial Matching via LLM-Driven Abduction and Logical Verification

2026-06-18 · Baiyang Qu, Leonardo Ranaldi, Xi Wang, Marco Valentino arxiv

Large Language Models (LLMs) offer a promising path to automate Clinical Trial Matching (CTM), but still struggle with the deterministic verification required for complex eligibility criteria. Conversely, purely symbolic…

Neurosymbolic Reinforcement Learning with Formally Verified Exploration

2020-09-26 · NeurIPS 2020 12 · Greg Anderson, Abhinav Verma, Isil Dillig, Swarat Chaudhuri

We present Revel, a partially neural reinforcement learning (RL) framework for provably safe exploration in continuous state and action spaces. A key challenge for provably safe deep RL is that repeatedly verifying neura…

reinforcement-learningReinforcement LearningReinforcement Learning (RL)Safe Exploration