Stress-Testing Neural Network Verifiers with Provably Robust Instances

• URL: http://arxiv.org/abs/2605.17153v1
• Date: Sat, 16 May 2026 20:56:52 GMT
• Title: Stress-Testing Neural Network Verifiers with Provably Robust Instances
• Abstract summary: We introduce a reusable framework for generating verification instances with ground-truth labels.<n>We also introduce the verification Difficulty Profile, a collection of estimable quantities capturing distinct sources of instance hardness.<n>Using our framework and these profiles, we evaluate five state-of-the-art verifiers and show that different instances stress distinct aspects of the verification pipeline.
• Score: 10.017475431603389
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neural network verifiers aim to provide formal guarantees on model behavior, but existing verification benchmarks are fundamentally limited by their lack of ground-truth labels. As a result, verifier evaluation relies on indirect heuristics, which prevents exact scoring and systematic study of verifier failure modes. We address this gap by introducing a reusable framework for generating verification instances whose ground-truth robustness labels are known a priori through analytic construction. Our framework led to the discovery of multiple numeric tolerance concerns and an implementation bug in popular verifiers, highlighting the need for ground-truth labels. Additionally, to systematically study verifier failure modes, we introduce the verification Difficulty Profile, a collection of estimable quantities capturing distinct sources of instance hardness. Using our framework and these profiles, we evaluate five state-of-the-art verifiers and show that different instances stress distinct aspects of the verification pipeline. We show that these results can aid the future development of verifiers as they provide actionable targets for improving numerical reliability, relaxation quality, and search behavior. Our code is publicly available: https://github.com/dtroxell19/VeriStressGT.git.

Related papers

• Revisiting Lossy Verification in Speculative Decoding: Mechanisms, Trade-offs, and Failure Modes [19.68865985432786]
  We present a principled analysis of the distributions induced by lossy verification methods.<n>We show that many seemingly distinct approaches differ only superficially and can be classified into two categories: truncation-based verification and collaborative verification.
  arXiv  Detail & Related papers  (2026-07-29T08:54:27Z)
• The Hidden Signal of Verifier Strictness: Controlling and Improving Step-Wise Verification via Selective Latent Steering [67.8271652641864]
  We study whether verifier strictness can be controlled through hidden-state intervention.<n>VerifySteer exploits latent correctness signals for sample-level routing and selectively intervenes on paragraph boundaries.
  arXiv  Detail & Related papers  (2026-05-20T05:48:16Z)
• K$α$LOS finds Consensus: A Meta-Algorithm for Evaluating Inter-Annotator Agreement in Complex Vision Tasks [4.297070083645049]
  We propose K$$LOS, a unified meta-algorithm that generalizes the "Localization First" principle to dataset quality evaluation.<n>By resolving spatial correspondence before assessing agreement, our framework transforms complex-categorical problems into nominal reliability.
  arXiv  Detail & Related papers  (2026-03-28T08:54:05Z)
• Attribution-Guided Model Rectification of Unreliable Neural Network Behaviors [60.06461883533697]
  We leverage rank-one model editing to establish an attribution-guided model rectification framework.<n>We first distinguish our rectification setting from existing model editing, yielding a formulation that corrects unreliable behavior.<n>To target the primary source of misbehavior, we introduce an attribution-guided layer localization method.
  arXiv  Detail & Related papers  (2026-03-08T01:06:07Z)
• From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications [11.371752627865929]
  Keypoint detection underpins many vision tasks, including pose estimation, viewpoint recovery, and 3D reconstruction.<n>Despite its importance, formal robustness verification for keypoint detectors is largely unexplored due to high-dimensional inputs and continuous coordinate outputs.<n>We propose the first coupled robustness verification framework for heatmap-based keypoint detectors.
  arXiv  Detail & Related papers  (2026-03-05T19:01:53Z)
• Learning to Pay Attention: Unsupervised Modeling of Attentive and Inattentive Respondents in Survey Data [0.14323566945483493]
  Traditional safeguards, such as attention checks, are often costly, reactive, and inconsistent.<n>We propose a unified, label-free framework for inattentiveness detection using complementary unsupervised views.
  arXiv  Detail & Related papers  (2026-03-02T22:11:51Z)
• CREDIT: Certified Ownership Verification of Deep Neural Networks Against Model Extraction Attacks [54.04030169323115]
  We introduce CREDIT, a certified ownership verification against Model Extraction Attacks (MEAs)<n>We quantify the similarity between DNN models, propose a practical verification threshold, and provide rigorous theoretical guarantees for ownership verification based on this threshold.<n>We extensively evaluate our approach on several mainstream datasets across different domains and tasks, achieving state-of-the-art performance.
  arXiv  Detail & Related papers  (2026-02-23T23:36:25Z)
• When Does Verification Pay Off? A Closer Look at LLMs as Solution Verifiers [11.937771430269201]
  We present a systematic study across 37 large language models (LLMs)<n>We compare self-verification with verification within the same family and across different families.<n>We analyze how metrics like verifier gain and false positive rate scale with model size and post-training, and characterize differences in dataset verifiability.
  arXiv  Detail & Related papers  (2025-12-02T00:51:14Z)
• Demystifying deep search: a holistic evaluation with hint-free multi-hop questions and factorised metrics [89.1999907891494]
  We present WebDetective, a benchmark of hint-free multi-hop questions paired with a controlled Wikipedia sandbox.<n>Our evaluation of 25 state-of-the-art models reveals systematic weaknesses across all architectures.<n>We develop an agentic workflow, EvidenceLoop, that explicitly targets the challenges our benchmark identifies.
  arXiv  Detail & Related papers  (2025-10-01T07:59:03Z)
• Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models [0.0]
  This paper introduces a novel detection pipeline that integrates custom Slither-based detectors, Large Language Models (LLMs), Kontrol, and Forge.<n>Our approach is designed to reliably detect defects and generate proofs.
  arXiv  Detail & Related papers  (2025-09-16T12:46:11Z)
• TrustLoRA: Low-Rank Adaptation for Failure Detection under Out-of-distribution Data [62.22804234013273]
  We propose a simple failure detection framework to unify and facilitate classification with rejection under both covariate and semantic shifts.<n>Our key insight is that by separating and consolidating failure-specific reliability knowledge with low-rank adapters, we can enhance the failure detection ability effectively and flexibly.
  arXiv  Detail & Related papers  (2025-04-20T09:20:55Z)
• SoundnessBench: A Soundness Benchmark for Neural Network Verifiers [45.86647998712757]
  We develop a new benchmark for NN verification, named "SoundnessBench", specifically for testing the soundness of NN verifiers.<n>SoundnessBench consists of instances with deliberately inserted counterexamples that are hidden from adversarial attacks.<n>We demonstrate that our training effectively produces hidden counterexamples and our SoundnessBench successfully identifies bugs in state-of-the-art NN verifiers.
  arXiv  Detail & Related papers  (2024-12-04T09:24:33Z)
• Tracking the risk of a deployed model and detecting harmful distribution shifts [105.27463615756733]
  In practice, it may make sense to ignore benign shifts, under which the performance of a deployed model does not degrade substantially. We argue that a sensible method for firing off a warning has to both (a) detect harmful shifts while ignoring benign ones, and (b) allow continuous monitoring of model performance without increasing the false alarm rate.
  arXiv  Detail & Related papers  (2021-10-12T17:21:41Z)

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.