pith. sign in

arxiv: 2203.07941 · v4 · submitted 2022-03-15 · 💻 cs.CC · cs.LG

Reachability In Simple Neural Networks

Pith reviewed 2026-05-24 11:53 UTC · model grok-4.3

classification 💻 cs.CC cs.LG
keywords neural network verificationreachability problemNP-hardnesscomputational complexitylinear inequalitiesneural networksone-hidden-layer networks
0
0 comments X

The pith

Reachability in neural networks is NP-hard even for one hidden layer, one output, and weights in {-1,0,1}.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that deciding whether a neural network maps some valid input to a valid output remains NP-hard when the network is restricted to a single hidden layer and a single output dimension. Hardness also holds when every weight and bias is forced to one of the three values -1, 0 or 1. The authors first repair gaps in an earlier general-case proof of NP-completeness and then supply reductions that keep the same hardness while obeying these limits. A sympathetic reader cares because the result means that verification of neural-network behavior cannot be efficient in the worst case, no matter how simple the network is made.

Core claim

The reachability problem—existence of an input obeying a conjunction of linear inequalities such that the network output also obeys a conjunction of linear inequalities—is NP-hard for networks that have only one hidden layer and a one-dimensional output. The same problem is NP-hard when the network is further restricted so that every weight and bias belongs to the set {-1,0,1}. Both statements are obtained by polynomial reductions that preserve the stated restrictions while encoding an NP-complete source problem.

What carries the argument

A polynomial-time reduction from 3-SAT (or an equivalent NP-complete problem) to a reachability query that uses only one hidden layer, one output neuron, and weights/biases drawn exclusively from {-1,0,1}.

If this is right

  • Verification of even the simplest feed-forward networks is NP-hard, so no polynomial-time algorithm exists unless P=NP.
  • The NP upper bound proved for the general case carries over directly to the restricted classes.
  • Specifications given by conjunctions of linear inequalities are already expressive enough to encode hard reachability instances inside the restricted networks.
  • Any practical verification procedure for neural networks must handle these minimal architectures as hard cases.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same style of reduction might be adaptable to networks that have zero hidden layers, though the paper does not construct such a reduction.
  • The result supplies a family of minimal hard instances that can be used to test the completeness of future verification algorithms or SMT encodings.
  • Because the hardness proof uses only three distinct weight values, it suggests that floating-point implementations with limited precision may still encounter the same worst-case difficulty.

Load-bearing premise

The reduction from 3-SAT to the reachability instance remains correct when the target network is forced to one hidden layer, one output dimension, and weights/biases limited to -1, 0 and 1.

What would settle it

Exhibit a polynomial-time algorithm that correctly answers every reachability query on networks with one hidden layer, one output, and weights in {-1,0,1}, or produce a concrete 3-SAT formula whose satisfiability status is not preserved by the given reduction.

Figures

Figures reproduced from arXiv: 2203.07941 by Marco S\"alzer, Martin Lange.

Figure 1
Figure 1. Figure 1: Schema of a neural network with five layers, input di [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Gadgets used in the reduction from 3SAT to REACH. A non-weighted outgoing edge of a gadget is connected to a weighted incoming edge of another gadget in the actual construction or is considered an output of the overall neural network. The obvious candidates for these gadgets are visualized in [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: NN resulting from the reduction of the 3 [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Gadgets used to show that REACH is NP-hard if restricted to NN from NN ({−c, 0, d}). A non￾weighted outgoing edge of a gadget is connected to a weighted incoming one of another gadget in the actual construction or are considered as outputs of the overall neural networks. Lemma 4.5. Let c, d ∈ Q>0 . The following statements hold: 1. disc(r) = 0 if and only if r = − d c 2 or r = 1 c [PITH_FULL_IMAGE:figure… view at source ↗
read the original abstract

We investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem is NP-complete for general neural networks and specifications over the input/output dimension given by conjunctions of linear inequalities. We recapitulate the proof and repair some flaws in the original upper and lower bound proofs. Motivated by the general result, we show that NP-hardness already holds for restricted classes of simple specifications and neural networks. Allowing for a single hidden layer and an output dimension of one as well as neural networks with just one negative, zero and one positive weight or bias is sufficient to ensure NP-hardness. Additionally, we give a thorough discussion and outlook of possible extensions for this direction of research on neural network verification.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The manuscript claims that the reachability problem for neural networks (does a network compute a valid output for some valid input, under specifications given by conjunctions of linear inequalities) is NP-complete in the general case, after repairing flaws in prior upper- and lower-bound proofs; it further asserts that NP-hardness already holds for severely restricted networks consisting of a single hidden layer, output dimension one, and weights/biases drawn only from {-1,0,1}.

Significance. If the repaired reductions are valid, the result shows that verification hardness persists even for networks with minimal architectural and weight restrictions, providing a strong lower bound that motivates specialized verification methods and extensions discussed in the outlook section.

major comments (1)
  1. [restricted-case reduction (abstract and main hardness section)] The central NP-hardness claim for the restricted case rests on a reduction (asserted to succeed after general-case repairs) from an NP-complete problem such as 3-SAT to a reachability instance limited to one hidden layer, output dimension 1, and weights/biases in {-1,0,1}. The explicit construction steps and verification that the reduction preserves these restrictions are not visible, so it is impossible to confirm that the lower bound holds under exactly the stated constraints.
minor comments (1)
  1. [Abstract] The abstract states that upper- and lower-bound proofs were repaired but does not enumerate the specific flaws or the nature of the repairs; adding a brief enumeration would improve traceability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful review and for highlighting the need for greater clarity in the restricted-case reduction. We address the comment below and will revise the manuscript accordingly.

read point-by-point responses
  1. Referee: [restricted-case reduction (abstract and main hardness section)] The central NP-hardness claim for the restricted case rests on a reduction (asserted to succeed after general-case repairs) from an NP-complete problem such as 3-SAT to a reachability instance limited to one hidden layer, output dimension 1, and weights/biases in {-1,0,1}. The explicit construction steps and verification that the reduction preserves these restrictions are not visible, so it is impossible to confirm that the lower bound holds under exactly the stated constraints.

    Authors: We agree that the submitted manuscript did not make the explicit construction steps and verification for the restricted-case reduction sufficiently visible. In the revised version we will include the full reduction from 3-SAT, detailing the single-hidden-layer architecture with output dimension 1, the assignment of all weights and biases from the set {-1,0,1}, and a step-by-step argument confirming that the reduction is polynomial-time and preserves satisfiability under these exact restrictions. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper proves NP-hardness of reachability by explicit polynomial-time reductions from independently known NP-complete problems (e.g., 3-SAT) to the restricted neural-network instances. These reductions are constructed directly in the paper and do not rely on any self-referential definitions, fitted parameters renamed as predictions, or load-bearing self-citations whose validity depends on the present work. The repairs to an earlier general-case proof are likewise external to the restricted hardness claims. The derivation chain is therefore self-contained against external benchmarks and contains no circular steps.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard complexity-theoretic background (P vs NP, polynomial-time reductions) and the correctness of the repaired reduction; no free parameters, invented entities, or ad-hoc axioms are introduced.

axioms (1)
  • standard math Standard assumptions of computational complexity theory (polynomial-time reductions preserve hardness)
    Invoked when reducing a known NP-complete problem to the restricted reachability instance.

pith-pipeline@v0.9.0 · 5652 in / 1233 out tokens · 22796 ms · 2026-05-24T11:53:00.293970+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages · 2 internal anchors

  1. [1]

    ImageNet classific ation with deep convolutional neural networks

    Krizhevsky A, Sutskever I, Hinton GE. ImageNet classific ation with deep convolutional neural networks. Commun. ACM, 2017. 60(6):84–90. doi:10.1145/3065386

  2. [2]

    A developer’s guide to audit logging,

    Hinton G, Deng L, Y u D, Dahl GE, Mohamed Ar, Jaitly N, Senio r A, V anhoucke V , Nguyen P , Sainath TN, et al. Deep Neural Networks for Acoustic Modeling in Spee ch Recognition: The Shared Views of Four Research Groups. IEEE Signal Process. Mag., 2012. 29(6):82–97. doi:10.1109/MSP .2012.2205597

  3. [3]

    A survey of deep learning techniques for autonomous driving

    Grigorescu SM, Trasnea B, Cocias TT, Macesanu G. A survey of deep learning techniques for autonomous driving. J. Field Robotics, 2020. 37(3):362–386. doi:10.1002/rob.21918

  4. [4]

    A survey on deep learning in medical image analysis

    Litjens G, Kooi T, Bejnordi BE, Setio AAA, Ciompi F, Ghafo orian M, van der Laak JAWM, van Ginneken B, S´ anchez CI. A survey on deep learning in medical image analysis. Medical Image Anal., 2017. 42:60–

  5. [5]

    doi:10.1016/j.media.2017.07.005

  6. [6]

    Classification-based financi al markets prediction using deep neural net- works

    Dixon M, Klabjan D, Bang JH. Classification-based financi al markets prediction using deep neural net- works. Algorithmic Finance, 2017. 6(3-4):67–77. doi:10.3233/AF-170176

  7. [7]

    A survey of safety and trustwor- thiness of deep neural networks: V erification, testing, adv ersarial attack and defence, and interpretability

    Huang X, Kroening D, Ruan W , Sharp J, Sun Y , Thamo E, Wu M, Yi X. A survey of safety and trustwor- thiness of deep neural networks: V erification, testing, adv ersarial attack and defence, and interpretability. Comput. Sci. Rev., 2020. 37:100270. doi:10.1016/j.cosrev.2020.100270

  8. [8]

    Re luplex: An Efficient SMT Solver for V er- ifying Deep Neural Networks

    Katz G, Barrett CW , Dill DL, Julian K, Kochenderfer MJ. Re luplex: An Efficient SMT Solver for V er- ifying Deep Neural Networks. In: Majumdar R, Kuncak V (eds.) , Computer Aided V erification - 29th International Conference, CA V 2017, Heidelberg, Germany,July 24-28, 2017, Proceedings, Part I, volume 10426 of Lecture Notes in Computer Science . Springer, ...

  9. [9]

    Formal V erification of Piece-Wise Linear Feed- Forward Neural Networks

    Ehlers R. Formal V erification of Piece-Wise Linear Feed- Forward Neural Networks. In: D’Souza D, Kumar KN (eds.), Automated Technology for V erification and A nalysis - 15th International Symposium, A TV A 2017, Pune, India, October 3-6, 2017, Proceedings, vol ume 10482 of Lecture Notes in Computer Science. Springer, 2017 pp. 269–286. doi:10.1007/978-3-319...

  10. [10]

    V erifying Properties of Binarized Deep Neural Networks

    Narodytska N, Kasiviswanathan SP , Ryzhyk L, Sagiv M, Wal sh T. V erifying Properties of Binarized Deep Neural Networks. In: McIlraith SA, Weinberger KQ (eds. ), Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educa ti...

  11. [11]

    A U nified View of Piecewise Linear Neural Network V erification

    Bunel R, Turkaslan I, Torr PHS, Kohli P , Mudigonda PK. A U nified View of Piecewise Linear Neural Network V erification. In: Bengio S, Wallach HM, Larochelle H , Grauman K, Cesa-Bianchi N, Garnett R (eds.), Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018...

  12. [12]

    Reachability Analysis o f Deep Neural Networks with Provable Guarantees

    Ruan W , Huang X, Kwiatkowska M. Reachability Analysis o f Deep Neural Networks with Provable Guarantees. In: Lang J (ed.), Proceedings of the Twenty-Sev enth International Joint Conference on Ar- tificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockh olm, Sweden. ijcai.org, 2018 pp. 2651–2659. doi:10.24963/ijcai.2018/368. M. S¨ alzer and M. Lange/ Re...

  13. [13]

    Reachability Analysis of Deep Neural Networks with Provable Guarantees

    Ruan W , Huang X, Kwiatkowska M. Reachability Analysis o f Deep Neural Networks with Provable Guarantees. CoRR, 2018. abs/1805.02242. 1805.02242, URL http://arxiv.org/abs/1805.02242

  14. [14]

    R eluplex: a calculus for reasoning about deep neural networks

    Katz G, Barrett CW , Dill DL, Julian K, Kochenderfer MJ. R eluplex: a calculus for reasoning about deep neural networks. F orm Methods Syst Des, 2021. doi:10.1007/s10703-021-00363-7

  15. [15]

    In: Structural, Syntactic, and Statistical Pattern Recognition

    S¨ alzer M, Lange M. Reachability is NP-Complete Even fo r the Simplest Neural Networks. In: Reachabil- ity Problems - 15th International Conference, RP 2021, Liverpool, UK, October 25-27, 2021, Proceedings, volume 13035 of Lecture Notes in Computer Science . Springer, 2021 pp. 149–164. doi:10.1007/978-3- 030-89716-1 10

  16. [16]

    A new polynomial-time algorithm for linea r programming

    Karmarkar N. A new polynomial-time algorithm for linea r programming. Comb., 1984. 4(4):373–396. doi:10.1007/BF02579150

  17. [17]

    Reachab ility Analysis for Neural Agent-Environment Systems

    Akintunde M, Lomuscio A, Maganti L, Pirovano E. Reachab ility Analysis for Neural Agent-Environment Systems. In: Thielscher M, Toni F, Wolter F (eds.), Principl es of Knowledge Representation and Rea- soning: Proceedings of the Sixteenth International Confer ence, KR 2018, Tempe, Arizona, 30 Octo- ber - 2 November 2018. AAAI Press, 2018 pp. 184–193. URL h...

  18. [18]

    Reducibility Among Combinatorial Problems

    Karp RM. Reducibility Among Combinatorial Problems. I n: Miller RE, Thatcher JW (eds.), Proceedings of a symposium on the Complexity of Computer Computations, h eld March 20-22, 1972, at the IBM Thomas J. Watson Research Center, Y orktown Heights, New Y or k, USA, The IBM Research Symposia Series. Plenum Press, New Y ork, 1972 pp. 85–103. doi:10.100 7/978...

  19. [19]

    Combinatorial Optimization

    Korte B, Vygen J. Combinatorial Optimization. Springe r Berlin, Heidelberg, 2006. ISBN 978-3-540- 29297-5. doi:10.1007/3-540-29297-7

  20. [20]

    A survey of the re cent architectures of deep convolutional neural networks

    Khan A, Sohail A, Zahoora U, Qureshi AS. A survey of the re cent architectures of deep convolutional neural networks. Artif. Intell. Rev., 2020. 53(8):5455–5516. doi:10.1007/s10462-020-09825-6

  21. [21]

    Yu , title =

    Wu Z, Pan S, Chen F, Long G, Zhang C, Y u PS. A Comprehensive Survey on Graph Neural Networks. IEEE Trans. Neural Networks Learn. Syst. , 2021. 32(1):4–24. doi:10.1109/TNNLS.2020.2978386

  22. [22]

    Fundamental Limits in Formal V erific ation of Message-Passing Neural Networks

    S¨ alzer M, Lange M. Fundamental Limits in Formal V erific ation of Message-Passing Neural Networks. In: The Eleventh International Conference on Lea rning Representations. 2023 URL https://openreview.net/forum?id=WlbG820mRH-

  23. [23]

    Reachability In Simple Neural Networks

    Stockmeyer LJ. The polynomial-time hierarchy. Theor . Comp. Sci., 1976. 3(1):1–22. This figure "image001.png" is available in "png" format from: http://arxiv.org/ps/2203.07941v4