# Security Properties of Neural Networks as Decision Problems

arXiv: https://arxiv.org/abs/2609.39768 · HTML: https://mlsanity.com/paper/2609.39768/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Backdoor and data poisoning attacks, one of 12 directions in LLM safety and security.
- Builds on 23 of its 45 references that are in the map.
- First posted on arXiv 30 Sep 2026.

## Placed in

- LLM safety and security / [Backdoor and data poisoning attacks](https://mlsanity.com/safety/backdoor-and-data-poisoning-attacks/)

## Builds on (most cited first, 23 of 23)

- [Membership Inference Attacks against Machine Learning Models](https://mlsanity.com/paper/1610.05820/) (2016)
- [BadNets: Identifying Vulnerabilities in the Machine Learning Model Supply Chain](https://mlsanity.com/paper/1708.06733/) (2017)
- [Counterfactual Fairness](https://mlsanity.com/paper/1703.06856/) (2017)
- [Universal adversarial perturbations](https://mlsanity.com/paper/1610.08401/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Turning Your Weakness Into a Strength: Watermarking Deep Neural Networks by Backdooring](https://mlsanity.com/paper/1802.04633/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Bit-Flip Attack: Crushing Neural Network with Progressive Bit Search](https://mlsanity.com/paper/1903.12269/) (2019)
- [SoK: How Robust is Image Classification Deep Neural Network Watermarking? (Extended Version)](https://mlsanity.com/paper/2108.04974/) (2021)
- [Planting Undetectable Backdoors in Machine Learning Models](https://mlsanity.com/paper/2204.06974/) (2022)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [Certified Monotonic Neural Networks](https://mlsanity.com/paper/2011.10219/) (2020)
- [Verifying Individual Fairness in Machine Learning Models](https://mlsanity.com/paper/2006.11737/) (2020)
- [Provable Repair of Deep Neural Networks](https://mlsanity.com/paper/2104.04413/) (2021)
- [Counterexample-Guided Learning of Monotonic Neural Networks](https://mlsanity.com/paper/2006.08852/) (2020)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [Formalizing Generalization and Robustness of Neural Networks to Weight Perturbations](https://mlsanity.com/paper/2103.02200/) (2021)
- [Verifying Neural Networks Against Backdoor Attacks](https://mlsanity.com/paper/2205.06992/) (2022)
- [Dynamic Toolbox for ETRINV](https://mlsanity.com/paper/1912.08674/) (2019)
- [The Existential Theory of the Reals as a Complexity Class: A Compendium](https://mlsanity.com/paper/2407.18006/) (2024)
- [Checking extracted rules in Neural Networks](https://mlsanity.com/paper/2509.16547/) (2025)
- [Random Parameter Noise Does Not Make Exact ReLU Verification Easy](https://mlsanity.com/paper/2607.14375/) (2026)

## Abstract (arXiv)

Certifying a deployed neural network raises decision problems that the verification literature has not classified: whether the model carries a backdoor planted in its training data, whether a fault in its stored parameters can drive it into an unsafe state, whether its output leaks a private part of its input. We formalise eight such problems and classify what we can. The organising observation is a logical one. The function computed by a piecewise linear network, together with all its node values, is definable by a quantifier-free formula of real addition of size linear in the network, so a property of the network is a quantifier-alternation sentence, which Sontag's 1985 theorem places in the polynomial hierarchy at the level of its prefix. Membership results are thus corollaries, and the argument makes plain what they need: that the quantified objects are inputs rather than the network's own parameters. Non-interference, monotonicity and counterfactual fairness have exactly the complexity of network equivalence and of interval verification, all co-NP- complete over ReLU. Detection of backdoor triggers from a quantised alphabet is Sigma_2^P-complete, one level above robustness certification, so it does not reduce to polynomially many robustness queries unless the hierarchy collapses. Inversion resistance is co-NP-complete for every l_p metric, p a fixed positive integer. Quantifying over parameters instead of inputs - the fault model of bit-flip attacks, radiation upsets and analog accelerators - makes verification exists-R-complete already for networks of identity nodes, for which every previously studied problem is in P, and it stays so when each parameter is confined to a box of inverse-polynomial width; the corresponding safety question is forall-R-complete for ReLU.