Towards Scaling Robustness Verification of Semantic Features via Proof Velocity
Robustness analysis is important for understanding the reliability of neural networks. Despite the significant progress in the verification techniques for both $L_p$- and semantic features- neighborhoods, existing approaches struggle to scale to deep networks and large datasets. For example, we are unaware of any analyzer that scales to AlexNet trained for ImageNet (consisting of 224x224x3 images). In this work, we take a step towards scaling robustness analysis. We focus on robustness to perturbations of semantic features and introduce the concept of proof guided by velocity to scale the analysis. The key idea is to phrase the verification task as a dynamic system and adaptively identify how to split it into subproblems each with maximal proof velocity. We propose a policy to determine the next subproblem based on the past and by leveraging input splitting, input refinement, and bound tightening. We evaluate our approach on CIFAR-10 and ImageNet and show that it can analyze neighborhoods of various features: hue, saturation, lightness, brightness, and PCA.
Code (0)
등록된 구현이 없습니다.
Methods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual and limits scalability. Advances in large…
Mathematical ReasoningMaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling
We present MaxProof, a population-level test-time scaling framework for competition-level mathematical proof in the MiniMax-M3 series. M3 first trains three proof-oriented capabilities -- proof generation, proof verifica…
AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis
Generating formal specifications for C programs remains a challenge in formal verification due to the manual effort, expertise, and semantic precision required. While recent advancements in large language models (LLMs) o…
Zero-Knowledge Proofs in Sublinear Space
Zero-knowledge proofs allow verification of computations without revealing private information. However, existing systems require memory proportional to the computation size, which has historically limited use in large-s…
RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation
Scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts, which are challenges overlooked by existing function-centric methods. We introduce RagVerus, …
Language ModelingLanguage ModellingRAGRetrieval+1