{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreicat6lzkfb47jyampygcynu6dtms2prqvczkn4hnewg5ty2ypoozq",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mmzvaamxfel2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiflo6xt7is6b2iafwghkjahlgggocme5jwjsbeuqqwcywuvjhmszm"
    },
    "mimeType": "image/png",
    "size": 24783
  },
  "path": "/abs/2605.29537v1",
  "publishedAt": "2026-05-29T00:00:00.000Z",
  "site": "https://arxiv.org",
  "tags": [
    "Eric Alsmann",
    "Martin Lange",
    "Marco Sälzer"
  ],
  "textContent": "**Authors:** Eric Alsmann, Martin Lange, Marco Sälzer\n\nWe investigate the computational complexity of neural network verification in quantised settings. We distinguish three classes of Feedforward Neural Networks (FNNs): rational FNNs with exact rational weights, quantised FNNs whose weights come from a finite-width arithmetic, and dynamically quantised FNNs in which rational networks are evaluated with respect to a given finite-width arithmetic. We consider two types of specifications used in the literature. Linear programming (LP) specifications are conjunctions of linear constraints, while bit-vector (BV) specifications allow reasoning at the bit level and can express non-linear constraints. Our results give a complexity landscape of these verification problems. For quantised FNNs with fixed arithmetic precision, we show that verification under both LP and BV specifications remains NP-complete, matching the complexity of the rational case. For dynamically quantised FNNs with BV specifications, we establish upper bounds, complementing a previously known PSPACE-hardness result.",
  "title": "The Complexity of Verifying Feedforward Neural Networks in Quantised Settings"
}