Neural Network Verification using Residual Reasoning
With the increasing integration of neural networks as components in mission-critical systems, there is an increasing need to ensure that they satisfy various safety and liveness requirements. In recent years, numerous sound and complete verification methods have been proposed towards that end, but these typically suffer from severe scalability limitations. Recent work has proposed enhancing such verification techniques with abstraction-refinement capabilities, which have been shown to boost scalability: instead of verifying a large and complex network, the verifier constructs and then verifies a much smaller network, whose correctness implies the correctness of the original network. A shortcoming of such a scheme is that if verifying the smaller network fails, the verifier needs to perform a refinement step that increases the size of the network being verified, and then start verifying the new network from scratch - effectively "wasting" its earlier work on verifying the smaller network. In this paper, we present an enhancement to abstraction-based verification of neural networks, by using residual reasoning: the process of utilizing information acquired when verifying an abstract network, in order to expedite the verification of a refined network. In essence, the method allows the verifier to store information about parts of the search space in which the refined network is guaranteed to behave correctly, and allows it to focus on areas where bugs might be discovered. We implemented our approach as an extension to the Marabou verifier, and obtained promising results.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Adaptive Test-Time Compute Allocation via Learned Heuristics over Categorical Structure
Test-time computation has become a primary driver of progress in large language model (LLM) reasoning, but it is increasingly bottlenecked by expensive verification. In many reasoning systems, a large fraction of verifie…
Residualized Similarity for Faithfully Explainable Authorship Verification
Responsible use of Authorship Verification (AV) systems not only requires high accuracy but also interpretable solutions. More importantly, for systems to be used to make decisions with real-world consequences requires t…
The Future of Facts: Tracing the Factual Generation-Verification Gap
Language models are becoming the default interface to factual knowledge, yet they often verify outputs more reliably than they generate them. This generation-verification gap (GV-gap) underlies many recent advances in se…
Continual LearningAutoVerifier: Residual-Guided Non-Parametric Optimization for Reference-Based Answer Verification
Reference-based verifiers are important for evaluating reasoning models and providing accurate outcome rewards in reinforcement learning with verifiable rewards. To improve verification accuracy, prior work has explored …
Reinforcement LearningFinger-NestNet: Interpretable Fingerphoto Verification on Smartphone using Deep Nested Residual Network
Fingerphoto images captured using a smartphone are successfully used to verify the individuals that have enabled several applications. This work presents a novel algorithm for fingerphoto verification using a nested resi…