paper-with-me

홈 › Papers

Uncovering the Limits of Proof Sharing for Neural Networks

2026-08-19 · Kanak Das, Shubham Ugare, Bor-Yuh Evan Chang, Sasa Misailovic, Gagandeep Singh, Manu Sridharan arxiv

Robustness verification of neural networks is increasingly important, due to their use in many critical domains. In certain scenarios, proof sharing has been shown to accelerate incomplete verification techniques by reusing intermediate-layer abstract states, or templates, across queries. However, questions remain as to the robustness of template-based acceleration across varying network architectures, properties, datasets, and training methods. In this work, we perform a systematic study of the effectiveness of template-based acceleration and its limits. Our study shows that template subsumption rates can vary widely across scenarios. We present a novel metric of jointly stable neurons to explain this variation, showing that in some cases template-based techniques are very unlikely to provide any speedup. Then, we present FastCert, a novel technique for automatically distributing templates across neural network layers to increase performance impact, eschewing templates entirely if they are unlikely to produce a speedup. Across a large set of covering-design based $L_0$-verification tasks, FastCert achieved an average speedup of 1.13x over an extant template-based reuse technique.

📄 PDF Abstract BibTeX arXiv:2608.19351

Code (0)

등록된 구현이 없습니다.

Similar Papers 제목 키워드 기반

Sharing HOL4 and HOL Light proof knowledge

2015-09-11 · Thibault Gauthier, Cezary Kaliszyk

New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing formalized proofs available in other provers…

Strategy Proof Mechanisms for Facility Location with Capacity Limits

2020-09-17 · Toby Walsh

An important feature of many real world facility location problems are capacity limits on the facilities. We show here how capacity constraints make it harder to design strategy proof mechanisms for facility location, bu…

Cross-Layer Subspace Coupling for LLM Compression: A Unifying Framework and Its Empirical Limits

2026-05-29 · Snigdha Chandan Khilar arxiv

Recent SVD based compression methods for large language models like SVD LLM and Basis Sharing can be unified under one optimization problem. While mathematical proofs and tests on Pythia models show this unified approach…

Distributed Optimization for Reactive Power Sharing and Stability of Inverter-Based Resources Under Voltage Limits

2023-02-18 · Babak Abdolmaleki, John W. Simpson-Porco, Gilbert Bergna-Diaz

Reactive power sharing and containment of voltages within limits for inverter-based resources (IBRs) are two important, yet coupled objectives in ac networks. In this article, we propose a distributed control technique t…

Distributed Optimization

A Formalizable Proof of the No-Supervenience Theorem: A Diagonal Limitation on the Viability of Physicalist Theories of Consciousness

2023-06-08 · Cathy M Reason

The no-supervenience theorem limits the capacity of physicalist theories to provide a comprehensive account of human consciousness. The proof of the theorem is difficult to formalize because it relies on both alethic and…