{"id":20,"identifier":"LOR-00020","url":"https://lifeofresearch.com/articles/20","title":"Formal Verification of Neural Network Safety Beyond Toy Examples: Three Distinct Gaps and a Specification-First Research Agenda","abstract":"Formal verification of neural networks has matured into a real research area. Tools such as alpha-beta-CROWN, ERAN, and\nMarabou now reliably verify L-infinity robustness properties of ReLU networks at the ResNet scale, with the annual VNNCOMP competition documenting steady year-over-year progress. The dominant framing of what remains undone — \"scale\nverification to bigger models\" — captures only one of three distinct gaps that separate current capability from useful\nguarantees on frontier AI systems. This paper makes three claims. First, the scale gap (verifiers handle networks with millions\nbut not billions of parameters), the architecture gap (standard techniques handle ReLU well but degrade sharply on\ntransformers with softmax, attention, and layer normalization), and the specification gap (we lack formal definitions of \"safe\nLLM output\" comparable to L-infinity robustness for image classifiers) are independent obstacles that need independent\nattention. Second, the specification gap is the most underweighted of the three and may be the binding constraint: even with\nverifiers that scaled to trillion-parameter models, we would not have formal specifications of harmlessness, honesty, or nondeception to verify against. Third, the most productive near-term frontier is not direct verification of LLM weights but\nverification of the systems that contain LLMs — LLM-as-policy verification, runtime monitors, agent-action guardrails. We\npropose a research agenda that reorients around the specification problem and the system-level frontier rather than\ncontinuing to pursue parameter-count scaling as the central goal.","authors":[{"name":"Pranay Mahendrakar","affiliation":"","orcid":"0009-0003-7224-029X"}],"type":"article","license":"CC-BY-4.0","keywords":[],"publication_date":"2026-04-28","version":1,"views":4,"downloads":11,"created_at":"2026-09-22 17:34:17","doi":"10.5281/zenodo.19854889","source":"Zenodo","source_url":"https://zenodo.org/records/19854889","files":[{"id":20,"name":"Formal_Verification_Neural_Networks_Mahendrakar.pdf","size":94224,"mime":"application/pdf","downloads":11,"download_url":"https://lifeofresearch.com/articles/20/files/20/Formal_Verification_Neural_Networks_Mahendrakar.pdf"}]}