{
  "abstract": "In this paper we investigate formal verification problems for Neural Network computations under a complexity theoretic point of view. Various reachability problems will be in the focus, such as: Given symbolic specifications of allowed inputs and outputs in form of Linear Programming instances, do valid inputs exist such that the given network computes a valid output? Does this property hold for all valid inputs? The complexity of this question has been investigated recently by Sälzer and Lange for nets using the Rectified Linear Unit and the identity function as their activation functions. We complement their achievements by showing that the problem is NP-complete for piecewise linear functions with rational coefficients that are not linear, NP-hard for almost all suitable activation functions including non-linear ones that are continuous on an interval, complete for the Existential Theory of the Reals ∃R for every non-linear polynomial and ∃R-hard for the exponential function and (almost) all sigmoidal functions. For the completeness results, linking the verification tasks with the theory of Constraint Satisfaction Problems turns out helpful. Then we relate the above problems to robustness questions, such as: Can an input be altered by just a little bit to change the output by a lot? Is the function computed by a network continuous with given parameters? And if not globally, is it continuous for a certain input? Is it Lipschitz-robust for a given L? These questions are formalized and their complexity is classified in dependence of the network's internal structure.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": null,
  "author_total": 1,
  "authors": [
    {
      "name": "Adrian Wurm"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/03yra29fdr377.bib",
  "cited_by": 0,
  "doi": null,
  "fulltext_url": null,
  "id": "03yra29fdr377",
  "issns": [],
  "landing_url": "https://hal.science/hal-04692383v3",
  "language": "en",
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "https://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": null,
  "native_subjects": [
    [
      "hal",
      "0.info"
    ],
    [
      "hal",
      "0.math"
    ]
  ],
  "openalex": null,
  "pdf_url": "https://hal.science/hal-04692383/document",
  "pmcid": null,
  "pmid": null,
  "published": "2026-10-05",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/03yra29fdr377.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:17:47Z",
      "native_id": "hal-04692383",
      "source": "hal",
      "url": "https://hal.science/hal-04692383v3"
    }
  ],
  "subjects": [
    {
      "field": "mathematics",
      "origin": "hal:0.math",
      "subfield": "general"
    }
  ],
  "title": "Complexity of Reachability and Verification Problems in Neural Networks",
  "title_text": "Complexity of Reachability and Verification Problems in Neural Networks",
  "type": "preprint",
  "updated_at": "2026-10-30T12:17:47Z",
  "url": "https://research.draconitic.com/paper/03yra29fdr377",
  "venue": "HAL",
  "versions": []
}