{"id":"fa2157d5-e75e-4ba3-92b7-7a8453d785e5","arxiv_id":"2501.05867","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Neural network verification's hardest open problems are reframed as programming language design challenges, with a unified dependently typed language proposed as the ideal solution.","lead":"The paper argues that the main obstacles to trustworthy neural network verification are programming language problems: weak specification formats, mismatches between trained and verified models, and gaps between abstract verification and real implementations. It then proposes a roadmap of new specification languages and formally verified toolchains.","discovery_kind":"review","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Table 1's claim that leading verifiers (Marabou and αβ-CROWN) satisfy none of the five PL challenges is unsupported; and the paper's roadmap depends on single-language unification that may undercut its own implementation-gap diagnosis.","rationale":"The reader's weakest assumption correctly targets the unvalidated scalability of the unified dependently typed language. My stress-test agrees that this is a weak point but identifies a more immediate, partly internal concern: the paper claims in §4 that leading tools satisfy none of the five PL challenges, while its own Table 1 gives Marabou and αβ-CROWN checkmarks for proof certificates. Without an explicit criterion for each feature, the claim is not falsifiable, and the roadmap's single-language proposal sits in tension with the implementation-gap diagnosis because it would require re-synthesizing the entire ML stack rather than verifying the existing one. That said, the diagnostic content is well-evidenced and the roadmap is clearly labeled as a proposal with acknowledged open problems, so the reader's CONDITIONAL verdict remains appropriate. My concern is a call to tighten evidence and framing, not a rejection of the central thesis.","tokens_in":23701,"tokens_out":2152,"duration_ms":21250,"concrete_test":"Reconstruct Table 1 with explicit, written criteria for each of the five features (e.g., “rigorous semantics” = published formal semantics for the specification language; “proof certificates” = verifier emits externally checkable certificates). Re-evaluate each tool against those criteria, with a citation column per checkmark. If Marabou or αβ-CROWN earns any checkmark under the stated criteria, the claim that leading tools “do not satisfy any” is false as written.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central thesis is the five-challenge diagnosis and the roadmap. The most load-bearing empirical claim is in §4 and Table 1: “some tools considered leaders ... do not satisfy any.” But the table's own rows contradict this: Marabou is marked ✓ for proof certificates (§3.5 describes its proof production), and αβ-CROWN is marked ✓ in the same column. The paper gives no inclusion criterion for “satisfy,” so the claim is unfalsifiable as stated; e.g., does VNN-COMP participation or a rigorous-but-unformalized syntax count for “rigorous semantics”? Table 1 also mixes categories (general-purpose CBMC/ESBMC versus NN-specific tools) and asserts CAISAR/Vehicle “rigorous semantics” without evidence. Separately, the §4.1 unified dependently typed language proposal, if taken literally, does not resolve the implementation gap for the actual deployed stack — it proposes re-synthesizing all components in the new language, which requires verified XLA/GPU replacements or formal verification of enormous external libraries; §4.2 admits efficiency is unsolved but no complexity argument is provided. Thus the roadmap's feasibility is unestablished, though the diagnostic sections on VNN-LIB, ONNX, floating-point mismatch, and embedding gap are well-evidenced.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper is a position piece arguing that neural network verification is, at its core, a programming language challenge. It surveys the state of the art in NN verification from the perspective of five PL challenges: rigorous specification semantics, the embedding gap (between high-level problem-space properties and real-vector network properties), the implementation gap (between verified ONNX models and actual trained implementations), proof certificate production, and property-guided training. The paper traces each of these through the existing pipeline (VNN-LIB, ONNX, verifiers such as Marabou and αβ-CROWN, and prototypes such as CAISAR and Vehicle), and then proposes a roadmap featuring a unified dependently typed language (§4.1) and, more pragmatically, formal interfaces with behavioral specifications (§4.2). The central claim is that no current tool satisfies all five challenges, and that a PL-centered approach offers a path forward.","tokens_in":23960,"tokens_out":7978,"duration_ms":74518,"significance":"If the thesis is accepted, it would redirect research effort toward specification languages with formal semantics, compiler support for embedding and unembedding, proof certificates, and tight integration of training and verification. The paper's main strengths are its synthesis of known but scattered problems (ONNX's lack of formal semantics, floating-point mismatch, nondeterminism, the VNN-LIB limitations) and its clear articulation of the embedding and implementation gaps, with concrete code snippets and a useful decomposition of the decomposition of the proof obligations (Eqs. 2–4). The paper is honest about its limitations: it disclaims bibliographic completeness and acknowledges (§4.2) that a wholly unified language faces major efficiency and adoption hurdles. It also gives credit to existing partial solutions (CAISAR, Vehicle, Marabou's proof production, Imandra-based checkers). The paper is a valuable agenda-setting contribution, provided its empirical claims are stated precisely.","major_comments":[{"comment":"The claim that \"some tools considered leaders in the neural network verification market do not satisfy any\" is not supported by Table 1 as printed. Section 3.5 explicitly describes a proof-production mechanism implemented on top of Marabou, and the footnote to Table 1 states that the Farkas witness for neural-network UNSAT problems is available in Marabou, implying a checkmark in the Proof Certificates row for Marabou. The table's row/column alignment is ambiguous in the text, and no inclusion criterion for \"satisfy\" is provided. The paper should make the alignment explicit, define precisely what a checkmark means, and weaken or qualify the \"do not satisfy any\" sentence to reflect the actual evidence.","section":"§4, Table 1 (§3.5)"},{"comment":"The statement that the implementation gap \"will be resolved\" in a unified dependently typed language is stronger than the argument supports. The paragraph itself concedes that external libraries such as XLA and OpenBLAS would need to be formally verified or synthesized type-preservingly, which is exactly the difficult work of the implementation gap, not a consequence of the language design. No complexity or scalability argument is offered. The roadmap is plausible as a research vision, but this should be phrased as a conditional research target (\"would need to be addressed by...\") rather than as a resolution.","section":"§4.1, item 3"},{"comment":"The table mixes different notions of the five challenges across tool categories. For instance, CBMC/ESBMC's \"Implementation Gap\" checkmark refers to direct verification of low-level C code, which is a different kind of gap from the ONNX-translation gap addressed (or not addressed) by neural-network verifiers. Likewise, the \"Rigorous Semantics\" checkmarks for CAISAR and Vehicle are asserted without a citation or a definition of the formal semantics they provide. The table needs a precise legend stating what each checkmark means for each category, and the caption should explain the distinction between the generic proof production of CBMC/ESBMC and the Farkas-witness certificates of Marabou.","section":"Table 1 (§3.2, §3.4)"}],"minor_comments":[{"comment":"The affiliation line contains a typo: \"Heriot-Watt Univerwsity\" should be \"Heriot-Watt University\".","section":"Author affiliations"},{"comment":"The name of the tool is written inconsistently as \"αβ-Crown\" and \"αβ-CROWN\"; please standardize.","section":"Throughout"},{"comment":"The header \"F uture\" appears to have a missing character; it should read \"Future\".","section":"Table 1"},{"comment":"References [20] and [21] both point to the same Brix et al. paper \"First three years of the international verification of neural networks competition\"; one should be removed or they should be cross-referenced.","section":"References"},{"comment":"The proposal to dynamically bind datasets in a specification language would benefit from a discussion of the formal status of such bound data (e.g., as axioms, finite constraints, or probabilistic models); the paper only mentions the mechanism without addressing how it interacts with soundness of the verification pipeline.","section":"§3.1, item 4"}],"recommendation":"major_revision","confidential_remarks":"The paper is an agenda-setting position piece, and it is naturally oriented around the authors' own tools (Vehicle, CAISAR, Marabou). The diagnosis is largely well-evidenced, but the Table 1 claims need careful checking before publication: the \"leaders satisfy none\" statement appears to conflict with the paper's own description of Marabou's proof production, and the table's layout in the text is too ambiguous to be checked. I would also recommend that the editor ask the authors to provide the exact table source and a precise legend, since this is a load-bearing point for the paper's motivating narrative."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nHere's the short version: this is a position paper worth reading, and it earns its place as a 'Fresh Perspectives' piece, but it oversells one empirical claim and proposes a roadmap that is more an aspiration than a plan. The core diagnosis is sound.\n\nWhat's genuinely useful is the organization of the field's problems around five PL challenges: rigorous semantics for specification formats, the embedding gap, the implementation gap, proof certificates, and property-guided training. The paper is at its best when documenting concrete failures — VNN-LIB's lack of formal semantics, ONNX operator descriptions that point to NumPy, Jia and Rinard's floating-point counterexamples, the long list of non-determinism sources in training and inference. The writing is clear and the references are appropriate. I also give credit for acknowledging that the unified language idea has efficiency problems (Kokke et al.) rather than hand-waving.\n\nThe soft spots are real but not fatal. Table 1 is the main problem. The text claims that 'some tools considered leaders ... do not satisfy any' of the five challenges, but the table itself gives Marabou a check in the proof-certificates column and αβ-CROWN a starred check. That is an internal inconsistency, and 'satisfy' is never defined, so the table is hard to interpret. The table also mixes general-purpose verifiers with NN-specific ones without much explanation of what counts as addressing a challenge. If the paper is revised, this needs to be fixed — either change the claim or change the table and the inclusion criteria.\n\nThe §4.1 unified dependently typed language is the weakest part of the roadmap, not because it's wrong but because it's unvalidated. The paper admits type-checking efficiency is a hard problem but gives no complexity argument, no prototype, no back-of-envelope estimate. And as the stress-test note says, the proposal would require verified replacements for XLA/GPU libraries or a way around them; that's a research program, not a solution. To be fair, the paper also offers a more realistic short-term direction in formal interfaces (§4.2), which is sensible.\n\nBottom line: the title drops the qualifier 'increasingly' from the conclusion, and that's a symptom of the paper's tendency to overstate. But the diagnosis is convincing, the field would benefit from this framing being discussed, and the flaws are addressable in revision. I'd send it to peer review. I'd also bring it to reading group — it will spark a good conversation about whether PL infrastructure should be the field's priority. I'd cite it myself as a position statement.","headline":"A well-argued position paper that correctly identifies PL infrastructure as a bottleneck in NN verification, but overstates its own table and offers a roadmap that is more aspiration than validated plan.","tokens_in":24508,"tokens_out":4410,"would_cite":true,"duration_ms":38945,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper argues that neural network verification is increasingly a programming language challenge, with rigorous specification semantics, verified translations, and proof-carrying interfaces as the decisive missing pieces.","keywords":["neural network verification","programming language design","dependently typed languages","specification languages","embedding gap","implementation gap","proof certificates","VNN-LIB"],"falsifier":"A concrete way to test the central claim is to build a prototype of the unified language and run a standard robustness certification for a small convolutional network end to end, with training, conversion, and proof all inside the language and no unverified external library calls; if the type-checker cannot finish in practical time, or if any step silently falls back to an unverified backend, the practical version of the claim fails.","tokens_in":23518,"feed_emoji":"🧠","tokens_out":7962,"duration_ms":68090,"temperature":0.7,"pith_summary":"This paper argues that the hardest remaining obstacles to trustworthy neural network verification are not solver algorithms but programming language design. It claims that verification tools currently check an idealized version of the network expressed in the ONNX exchange format, not the actual trained program, and that property languages lack formal semantics, conciseness, dataset bindings, and the ability to express multi-network or hyper-properties. It identifies two named gaps: the embedding gap between high-level problem data and low-level real vectors, and the implementation gap between real-valued verification and floating-point, non-deterministic execution. The paper concludes that neural network verification is increasingly a programming language challenge and proposes a roadmap centered on a single expressively typed language, with types that can depend on values, with formal interfaces as a fallback.","feed_headline":"Neural network verification is now a programming-language problem","feed_subtitle":"The paper maps five language gaps that keep safety certificates from reaching real systems.","key_machinery":"The load-bearing machinery is the three-lemma decomposition that turns a network-level certificate into a whole-program guarantee by threading it through explicit embedding and unembedding functions $e : P \\to \\mathbb{R}^m$ and $u : \\mathbb{R}^n \\to R$. This decomposition exposes the two gaps the paper names: the embedding gap, where problem-space values like discrete switches or image semantics are crudely approximated by real-valued intervals, and the implementation gap, where the verified object $f^*$ differs from the trained network $f$ due to ONNX conversion, floating-point arithmetic, parallel execution, and compiler optimizations. Around this decomposition, the paper also identifies five programming language features no current tool combines: rigorous semantics, embedding-gap support, implementation-gap support, proof certificates, and support for property-guided training.","core_discovery":"On the paper's own terms, the central claim is that a safety guarantee for a neural network is only meaningful when it is connected by formally specified transformations to the network's actual implementation and to the larger system around it. The paper decomposes this into three lemmas: the network satisfies a network property $\\Xi(f)$; any network satisfying $\\Xi$ yields a lifted solution $u \\circ g \\circ e$ satisfying a solution property $\\Phi$; and any such solution makes the full neuro-symbolic program $s(u \\circ f \\circ e)$ satisfy the program property $\\Psi$. Currently, verifiers check $\\Xi(f^*)$ where $f^*$ is an ONNX conversion of $f$, and neither the conversion nor the surrounding embedding is formally accounted for. The paper's proposed remedy is a single language whose types can depend on values, expressing the training pipeline, the properties, the embedding and unembedding functions, and proof certificates, with type-checking acting as proof checking; failing that, it argues for rigorously specified formal interfaces between existing components.","pith_inferences":["If the thesis is right, near-term progress is more likely through formal interface contracts for existing ONNX operators and verifier backends than through one unified language, since tool adoption is the bottleneck.","A testable extension would be a benchmark that scores verification tools not only on solver speed but on how many specification errors, conversion mismatches, and unverified library assumptions they catch.","The embedding gap suggests specification languages should treat the data manifold as a first-class citizen, possibly connecting to probabilistic or distributional specifications of the input space.","The paper's argument implies that safety certification of learned systems will eventually require the same infrastructure as compiler correctness: verified translation, proof-carrying code, and contract-based specifications for libraries."],"forward_implications":["Verification standards like VNN-LIB and ONNX need formally defined syntax and semantics before sound tools can be built around them.","New specification languages should be high-level and typed, with dataset bindings, multi-network properties, and hyper-properties, so that a single specification compiles to multiple solvers.","Property-guided training and verification should be viewed as two backends of the same specification compiler, not separate activities.","Verifiers must either verify the actual floating-point implementation or produce certificates that survive a formally justified translation, with quantized networks getting dedicated theories.","In a unified dependently typed language, proof certificates and proof checkers disappear as separate artifacts because terms are certificates and the type-checker is the checker."],"supporting_citations":[{"why":"Provides the ONNX exchange format whose lack of formal semantics underlies the implementation gap.","marker":"[1]"},{"why":"Defines the VNN-LIB query language, the de-facto standard whose weak syntax and semantics the paper criticizes.","marker":"[35]"},{"why":"Implements CAISAR, a higher-level specification language that compiles to multiple verifiers.","marker":"[51]"},{"why":"Implements Vehicle, the dependently typed specification language that bridges the embedding gap and compiles to Agda.","marker":"[32]"},{"why":"Shows floating-point counterexamples can invalidate real-valued safety certificates, grounding the implementation gap.","marker":"[71]"},{"why":"Shows that ignoring numerical precision can create undetectable backdoors, justifying the implementation gap.","marker":"[129]"},{"why":"Introduces proof production for a neural network verifier, the basis of the paper's proof-certificate discussion.","marker":"[66]"},{"why":"Uses refinement types for neural network robustness and is cited for the difficulty of efficient type-checking.","marker":"[77]"},{"why":"Introduces differentiable logic, the foundation for property-guided training as a specification-language backend.","marker":"[46]"}],"fun_headline_variants":["Neural verification needs programming language insight","Dependent types can make neural proofs checkable","The AI proof gap is a language design problem","Formal links missing between neural nets and code","Neural network safety is a typing challenge"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The paper's proposal rests on the belief that a single language with very expressive types can express the whole training-to-verification pipeline and still be efficient enough for real tools; the paper itself acknowledges that type-checking such specifications is a hard open problem and offers no implementation or scaling evidence.","fun_headline_variants_meta":{"raw":{"variants":["Neural verification needs programming language insight","Dependent types can make neural proofs checkable","The AI proof gap is a language design problem","Formal links missing between neural nets and code","Neural network safety is a typing challenge"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.0002,"raw_usage":{"total_tokens":1304,"prompt_tokens":804,"completion_tokens":500,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":420,"completion_tokens_details":{"reasoning_tokens":432}},"tokens_in":420,"tokens_out":500,"duration_ms":5693,"temperature":1.0,"reasoning_tokens":432,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T21:05:30.720373+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A concrete way to test the central claim is to build a prototype of the unified language and run a standard robustness certification for a small convolutional network end to end, with training, conversion, and proof all inside the language and no unverified external library calls; if the type-checker cannot finish in practical time, or if any step silently falls back to an unverified backend, the practical version of the claim fails.","supporting_citations":[{"cited_title":"In: 8th International Conference on Learning Representations, ICLR 2020 (2020)","cited_arxiv_id":null,"evidence_quote":"Shows that ignoring numerical precision can create undetectable backdoors, justifying the implementation gap."}],"review_version":1}