Talking with Verifiers: Automatic Specification Generation for Neural Network Verification

• URL: http://arxiv.org/abs/2603.02235v1
• Date: Fri, 13 Feb 2026 09:36:40 GMT
• Title: Talking with Verifiers: Automatic Specification Generation for Neural Network Verification
• Abstract summary: We introduce a novel component to the verification pipeline, making existing verification tools applicable to a broader range of domains and specification styles.<n>Our framework enables users to formulate specifications in natural language, which are then automatically analyzed and translated into formal verification queries compatible with state-of-the-art neural network verifiers.<n>Our results show that this translation process maintains high fidelity to user intent while incurring low computational overhead, thereby substantially extending the applicability of formal verification to real-world, high-level requirements.
• Score: 5.883923958146327
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Neural network verification tools currently support only a narrow class of specifications, typically expressed as low-level constraints over raw inputs and outputs. This limitation significantly hinders their adoption and practical applicability across diverse application domains where correctness requirements are naturally expressed at a higher semantic level. This challenge is rooted in the inherent nature of deep neural networks, which learn internal representations that lack an explicit mapping to human-understandable features. To address this, we bridge this gap by introducing a novel component to the verification pipeline, making existing verification tools applicable to a broader range of domains and specification styles. Our framework enables users to formulate specifications in natural language, which are then automatically analyzed and translated into formal verification queries compatible with state-of-the-art neural network verifiers. We evaluate our approach on both structured and unstructured datasets, demonstrating that it successfully verifies complex semantic specifications that were previously inaccessible. Our results show that this translation process maintains high fidelity to user intent while incurring low computational overhead, thereby substantially extending the applicability of formal DNN verification to real-world, high-level requirements.

Related papers

• CLAIM: Leading Open-domain Active Clarification of Large Language Models with Uncertainty Measurement [50.91045324738942]
  CLAIM is an uncertainty-driven framework for active clarification learning in open-domain settings.<n>We propose an entropy-driven synthetic data generation pipeline that integrates uncertainty estimation with semantic clustering and reasoning-based judgments.<n> Experimental results demonstrate that CLAIM can learn stable and generalizable clarification strategies without relying on manually labeled data.
  arXiv  Detail & Related papers  (2026-08-12T04:27:45Z)
• CLAIRE: Compressed Latent Autoencoder for Industrial Representation and Evaluation -- A Deep Learning Framework for Smart Manufacturing [51.56484100374058]
  CLAIRE is a hybrid end-to-end learning framework that integrates unsupervised deep representation learning with supervised classification for intelligent quality control in smart manufacturing systems.<n>It employs an optimized deep autoencoder to transform raw input into a compact latent space, effectively capturing the intrinsic data structure while suppressing irrelevant or noisy features.<n>The proposed framework highlights the potential of integrating explainable AI with feature-aware regularization for robust fault detection.
  arXiv  Detail & Related papers  (2026-03-06T15:11:58Z)
• TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
  We introduce TorchLean, a framework that treats learned models as first-class mathematical objects with a single, precise semantics shared by execution and verification.<n>We validate TorchLean end-to-end on certified robustness, physics-informed residual bounds for PINNs, and Lyapunov-style neural controller verification.
  arXiv  Detail & Related papers  (2026-02-26T05:11:44Z)
• Neural Network Reprogrammability: A Unified Theme on Model Reprogramming, Prompt Tuning, and Prompt Instruction [57.19302613163439]
  We introduce neural network reprogrammability as a unifying framework for model adaptation.<n>We present a taxonomy that categorizes such information manipulation approaches across four key dimensions.<n>We also analyze remaining technical challenges and ethical considerations.
  arXiv  Detail & Related papers  (2025-06-05T05:42:27Z)
• A Formally Verified Robustness Certifier for Neural Networks (Extended Version) [0.0]
  Neural networks are susceptible to minor perturbations in input that cause them to misclassify.<n>Globally-robust neural networks employ a function to certify that the classification of an input cannot be altered by such a perturbation.<n>We describe the program, its specifications, and the important design decisions taken for its implementation and verification.
  arXiv  Detail & Related papers  (2025-05-11T12:05:14Z)
• A General Framework for Property-Driven Machine Learning [1.0485739694839669]
  We show that adversarial training can be used to improve robustness to small perturbations within $epsilon$-cubes.<n> domains other than computer vision may require more flexible input region specifications via generalised hyper-rectangles.<n>In this paper, we investigate how these two complementary approaches can be unified within a single framework for property-driven machine learning.
  arXiv  Detail & Related papers  (2025-05-01T11:33:38Z)
• Formal Verification of Deep Neural Networks for Object Detection [1.947473271879451]
  Deep neural networks (DNNs) are widely used in real-world applications, yet they remain vulnerable to errors and adversarial attacks. This work extends formal verification to the more complex domain of emphobject detection models.
  arXiv  Detail & Related papers  (2024-07-01T13:47:54Z)
• VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees [3.208888890455612]
  We propose a novel framework to generate Verification-Friendly Neural Networks (VNNs) We present a post-training optimization framework to achieve a balance between preserving prediction performance and verification-friendliness.
  arXiv  Detail & Related papers  (2023-12-15T12:39:27Z)
• On the verification of Embeddings using Hybrid Markov Logic [2.113770213797994]
  We propose a framework to verify complex properties of a learned representation. We present an approach to learn parameters for the properties within this framework. We illustrate verification in Graph Neural Networks, Deep Knowledge Tracing and Intelligent Tutoring Systems.
  arXiv  Detail & Related papers  (2023-12-13T17:04:09Z)
• Neuro-Symbolic Verification of Deep Neural Networks [20.973078277539276]
  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. We show how neuro-symbolic verification can be implemented on top of existing verification infrastructure for neural networks.
  arXiv  Detail & Related papers  (2022-03-02T08:40:01Z)
• Privacy-preserving machine learning with tensor networks [37.01494003138908]
  We show that tensor network architectures have especially prospective properties for privacy-preserving machine learning. First, we describe a new privacy vulnerability that is present in feedforward neural networks, illustrating it in synthetic and real-world datasets. We rigorously prove that such conditions are satisfied by tensor-network architectures.
  arXiv  Detail & Related papers  (2022-02-24T19:04:35Z)
• A Lightweight, Efficient and Explainable-by-Design Convolutional Neural Network for Internet Traffic Classification [9.365794791156972]
  This paper introduces a new Lightweight, Efficient and eXplainable-by-design convolutional neural network (LEXNet) for Internet traffic classification. LEXNet relies on a new residual block (for lightweight and efficiency purposes) and prototype layer (for explainability) Based on a commercial-grade dataset, our evaluation shows that LEXNet succeeds to maintain the same accuracy as the best performing state-of-the-art neural network.
  arXiv  Detail & Related papers  (2022-02-11T10:21:34Z)
• A Controllable Model of Grounded Response Generation [122.7121624884747]
  Current end-to-end neural conversation models inherently lack the flexibility to impose semantic control in the response generation process. We propose a framework that we call controllable grounded response generation (CGRG) We show that using this framework, a transformer based model with a novel inductive attention mechanism, trained on a conversation-like Reddit dataset, outperforms strong generation baselines.
  arXiv  Detail & Related papers  (2020-05-01T21:22:08Z)
• Deep Speaker Embeddings for Far-Field Speaker Recognition on Short Utterances [53.063441357826484]
  Speaker recognition systems based on deep speaker embeddings have achieved significant performance in controlled conditions. Speaker verification on short utterances in uncontrolled noisy environment conditions is one of the most challenging and highly demanded tasks. This paper presents approaches aimed to achieve two goals: a) improve the quality of far-field speaker verification systems in the presence of environmental noise, reverberation and b) reduce the system qualitydegradation for short utterances.
  arXiv  Detail & Related papers  (2020-02-14T13:34:33Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.