Pith. sign in

REVIEW 2 major objections 6 minor 1 cited by

TNODEV: Toolbox for Neural ODE Verification

T0 review · 2 major / 6 minor · reviewed 2026-07-12 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read TNODEV is the first end-to-end formal verifier for neural ODEs, combining falsification, fast interval reachability, and input-set refinement.

desk verdict Solid systems paper that actually ships the first falsification+refinement pipeline for neural ODEs; engineering novelty, honest experiments, clean linear-ODE soundness proof. read the letter →

arxiv 2606.16567 v2 pith:UZP6ZJ2U submitted 2026-06-15 cs.AI cs.LGcs.SYeess.SYmath.DS

Abdelrahman Sayed Sayed , Pierre-Jean Meyer , Mohamed Ghazel This is my paper · ORCID
classification cs.AIcs.LGcs.SYeess.SYmath.DS
keywords neuralordinarydifferentialequationsformalverificationreachabilityanalysiscontinuous-timemixedmonotonicityinput-setrefinementclassificationrobustnesscyber-physicalsystems
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Neural ODEs are continuous-time models used in controllers and classifiers, but existing tools only run a single reachability call and stop. That leaves many safety questions unanswered when the over-approximation is too loose. TNODEV closes that gap by wiring together a counter-example search, a cheap continuous-time mixed-monotonicity reachability engine, three splitting heuristics that refine the input set, and a parallel scheduler into one pipeline that returns SAFE, FALSIFIED, or UNKNOWN. It handles pure neural ODEs, closed-loop systems with neural controllers, and general neural ODEs with discrete layers, for both interval safe sets and classification labels. On benchmarks from 2-D spirals to 12-D cart-pole and MNIST classifiers, the loop often certifies properties that a single reachability call cannot, at the cost of wider boxes than star-set or zonotope methods.

What carries the argument

The continuous-time mixed-monotonicity (CTMM) reachability step: it embeds the neural ODE into a 2n-dimensional monotone system whose single numerical integration yields a cheap axis-aligned over-approximation of the reachable set, making repeated refinement calls practical.

What would settle it

A pure or hybrid neural ODE safety property that every existing single-call tool leaves UNKNOWN, yet TNODEV with its default MSIR heuristic also returns UNKNOWN (or times out) while a richer set representation (star sets or zonotopes) with the same refinement budget certifies SAFE.

Watch

Extended reading notes

Core claim

The paper establishes that a sound formal verifier for neural ODEs can be built by wrapping a fast interval reachability backend (continuous-time mixed monotonicity) inside a falsification-plus-refinement loop with three splitting heuristics and a parallel scheduler. This pipeline is the first of its kind for neural ODEs and returns conclusive SAFE or FALSIFIED verdicts on pure, hybrid, and general neural ODE models for both interval safe-set inclusion and classification-robustness properties.

Load-bearing premise

That splitting the input set and re-running cheap interval reachability will eventually produce boxes tight enough to decide the property before the iteration or time budget is exhausted.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The paper introduces TNODEV, presented as the first sound end-to-end formal verifier for neural ODEs that combines a falsification pass, continuous-time mixed-monotonicity (CTMM) interval reachability, an iterative input-set refinement loop with three splitting heuristics (naive, MSIR, ING), and a parallel scheduler. It targets safe-set inclusion for pure neural ODEs, hybrid closed-loop systems with NN controllers, and general neural ODEs (GNODE), with safe sets given either as intervals or as half-space intersections for classification labels. The architecture (Algorithm 1, Figure 1) returns SAFE / FALSIFIED / UNKNOWN. Experiments include a single-call reachability comparison against NNV 2.0 and CORA (speed vs geometric-mean width), verification of six safe-set benchmarks (2–12D) under the three heuristics, and a hybrid-pipeline classification-robustness comparison on MNIST GNODE classifiers against NNV 2.0. Soundness of the closed-form linear-ODE interval propagator used on MNIST is proved (Lemmas 1–2, Theorem 1); CTMM is used as a cited over-approximation backend.

Significance. The central contribution is a systems claim that fills a documented gap: existing neural-ODE tools (Table 1) expose only a single reachability call without falsification-plus-refinement. Integrating those pieces into one pipeline, with released code, modular interfaces, and honest quantification of the interval speed–tightness trade-off (including MNIST verification rates of ~58–60% vs NNV 2.0 near 100%, and ING UNKNOWN verdicts), is a useful and timely contribution for safety-critical continuous-time models. The machine-checked-style soundness argument for the linear-ODE closed-form propagator, the explicit cost analysis of the three heuristics (Appendix C), and the reproducible experimental setup strengthen the work beyond a pure engineering dump. If the pipeline claim holds—as the architecture and tables support—it provides a practical baseline that later richer set representations can plug into.

major comments (2)
  1. Abstract and §1 state that TNODEV “supports … general neural ODE (GNODE)”. §5.3 and Appendix A.3.2 make clear that discrete pre-/post-ODE layers are handled by NNV 2.0 ImageStar/Star-set reachability; TNODEV only supplies the linear-ODE block via the closed-form interval propagator. The standalone capability claim should be qualified in the abstract, introduction, and Table 1 so that readers do not overestimate what the released toolbox currently verifies without an external discrete-layer engine. Future-work language already acknowledges the gap; the present-tense support claim needs the same precision.
  2. §5.3 / Table 3 deliberately disables iterative refinement for both tools “to keep the comparison meaningful”. That choice is fair to NNV 2.0 but under-exercises TNODEV’s main architectural contribution precisely on the high-dimensional regime where refinement is most needed. A short discussion (or a limited refined-subset experiment) of how global input-set splitting would be expected to interact with the ~7–8× interval widening through the linear ODE would make the MNIST results more informative rather than leaving the gap entirely to future work.
minor comments (6)
  1. Table 1 column “Iterative refinement for nODE” correctly marks TNODEV “yes” and others “no”; the prose in §2 could more explicitly contrast NNV 2.0’s single-call safety check with a full falsify–reach–refine loop so the novelty claim is unambiguous for readers who only skim the table.
  2. §3.2 Step 1 obtains the reachable-tube over-approximation from CORA; the dependency is stated but the implications for a self-contained toolbox (installation, version pinning, reproducibility of Jacobian bounds) deserve a short paragraph in the architecture or experiments section.
  3. Appendix C and Table 2 show ING frequently returns UNKNOWN on higher-dimensional benchmarks; the main text (§4.3) already positions MSIR as the default, but a one-sentence caveat in the abstract or conclusion that ING is exploratory rather than production-ready would prevent over-reading of the three-heuristic comparison.
  4. Figures 3–7 captions repeat nearly identical wording; condensing the common legend once and referring to it would improve readability.
  5. Minor typographical inconsistencies appear (e.g., “NNV2.0” vs “NNV 2.0”, “over-apprimations” in Appendix B.1, “reachacility” in Appendix C). A pass for spelling and hyphenation would polish the camera-ready version.
  6. Definition 3 and the classification-robustness encoding (half-spaces Hj) are clear; adding an explicit pointer that any property admitting a sound check on Ω(X) can be plugged in would further emphasize modularity for readers implementing new specifications.

Circularity Check

1 steps flagged · score 1.0 of 10

No significant circularity: TNODEV is an engineering systems claim whose soundness rests on standard CTMM embedding and a self-contained linear-ODE box enclosure, not on fitted parameters or self-referential definitions.

  1. self citation load bearing [Section 3.2 / Table 1 / Related work]
    "TNODEV uses the CTMM method as its default reachability backend and wraps it as a full neural ODE verifier. ... The most recent addition to the literature on neural ODE reachability analysis is Sayed et al. (2025b), relying on the continuous-time mixed monotonicity (CTMM) method from TIRA (Meyer et al., 2019)"

    The default reachability engine is the authors' own prior CTMM implementation. This is ordinary self-citation of a component, not a circular definition of the verification claim: the pipeline's novelty is the falsification+refinement wrapper, and CTMM soundness is independent of the SAFE/UNKNOWN verdicts. Flagged only as a minor self-citation, not as a reduction of the central claim.

full rationale

The paper's central claim is the existence of an end-to-end neural-ODE verifier that combines falsification, CTMM interval reachability, iterative input-set refinement, and parallel scheduling (Alg. 1, Fig. 1). That claim is an engineering existence claim, not a first-principles derivation that could be circular. The CTMM backend is taken from prior literature (Meyer et al., 2021; Coogan, 2020) and from the authors' own earlier reachability paper (Sayed et al., 2025b); those citations supply a black-box component whose soundness is independent of the verification verdicts returned by TNODEV. The only fully self-contained mathematical derivation in the paper is the closed-form matrix-exponential interval propagator for linear ODE blocks (Lemmas 1–2, Theorem 1), which is a standard affine-to-homogeneous lift plus the classical tightest-box enclosure of an affine image of a box; it does not define its output in terms of the target robustness property. Experimental comparisons against NNV 2.0 and CORA are external and falsifiable. The single minor self-citation load is the reuse of the authors' CTMM implementation as the default backend; it is not used to force uniqueness of the pipeline or to redefine the SAFE/FALSIFIED/UNKNOWN verdicts. Score 1 reflects that minor self-citation without elevating it to load-bearing circularity.

Assumptions & free parameters 3 free parameters · 3 assumptions · 0 invented entities

The paper is a systems/tool paper. Its load-bearing mathematical assumptions are standard (Lipschitz continuity of the neural vector field so that Jacobian bounds exist; soundness of CTMM and of the matrix-exponential interval hull). Free parameters are only the user-chosen verification budgets and the three heuristic design choices; no physical constants or data-fitted scales enter the central claim. No new physical entities are postulated.

free parameters (3)
  • refinement budget K
    User-chosen maximum number of refinement iterations (set to 5000 in experiments); directly controls whether UNKNOWN is returned.
  • wall-clock timeout Tmax
    User-chosen time limit (120 min in experiments); another termination condition for UNKNOWN.
  • ING finite-difference offset δ
    Perturbation size used to estimate partial derivatives of over-approximation width; affects split quality of the ING heuristic.
assumptions (3)
  • domain assumption The neural vector field f is Lipschitz continuous, guaranteeing existence of finite Jacobian bounds over any compact reachable tube.
    Invoked in Section 3.2 Step 1 as the only condition required for CTMM decomposition.
  • standard math CTMM embedding produces a sound interval over-approximation of the reachable set (Meyer et al. 2021).
    Used as the default reachability backend; soundness inherited from the cited literature.
  • standard math The closed-form matrix-exponential propagator plus tightest axis-aligned box enclosure is a sound over-approximation of the linear ODE flow (Theorem 1).
    Proved in Appendix A.3.2 for the MNIST GNODE linear block.

how reviews work

0 comments
Cite this review

Pith. "Pith review of TNODEV: Toolbox for Neural ODE Verification." pith.science (2026). https://pith.science/paper/UZP6ZJ2U

@misc{pith2026260616567,
  author       = {Pith},
  title        = {Pith review of: TNODEV: Toolbox for Neural ODE Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UZP6ZJ2U}},
  note         = {Machine review of arXiv:2606.16567}
}
read the original abstract

Neural ordinary differential equations (neural ODE) gained attention in safety critical settings such as continuous-time controllers for cyber-physical systems and classifiers integrated into automated decision pipelines, raising the question whether their behavior can be formally verified. Existing tools dedicated to neural ODE provide only a single reachability call without iterative input-set refinement, limiting the precision of their verdicts to whatever one reachability call can deliver. We present TNODEV, the first formal verifier for neural ODE that integrates a falsification checker, a fast interval-based reachability backend based on continuous-time mixed monotonicity, a verification and refinement loop with three input-set splitting heuristics, and a parallel scheduler in a single end-to-end pipeline. TNODEV supports safe-set inclusion verification on pure neural ODE, neural ODE in closed loop with a neural network controller and general neural ODE (GNODE), with the safe set specified either as an interval or as the half-space intersection induced by a target classification label. We evaluate TNODEV on a range of benchmarks across safe-set inclusion and classification-robustness properties, including a direct reachability comparison against NNV 2.0 and CORA and a verification comparison against NNV 2.0 on MNIST general neural ODE classifiers.

Figures

Figures reproduced from arXiv: 2606.16567 by the authors.

Figure 1
Figure 1. TNODEV verifier architecture. The verifier starts with a falsification check on the full initial set [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. TNODEV verification results on the Spiral 2D benchmark. In all sub figures, the dashed black [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. TNODEV verification results on the linear spiral 2D benchmark using naive and MSIR refinement. [PITH_FULL_IMAGE:figures/full_fig_p023_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: TNODEV verification results on the nonlinear spiral 2D benchmark using naive, MSIR and ING [PITH_FULL_IMAGE:figures/full_fig_p024_4.png]
Figure 5
Figure 5. Figure 5: TNODEV verification results on the FPA 5D benchmark using naive refinement. In all sub figures, [PITH_FULL_IMAGE:figures/full_fig_p025_5.png]
Figure 6
Figure 6. Figure 6: TNODEV verification results on the FPA 5D benchmark using MSIR refinement. In all sub figures, [PITH_FULL_IMAGE:figures/full_fig_p026_6.png]
Figure 7
Figure 7. Figure 7: TNODEV verification results on the FPA 5D benchmark using ING refinement. In all sub figures, [PITH_FULL_IMAGE:figures/full_fig_p027_7.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Robustness Verification of an Autonomous Underwater Vehicle-based Plankton Classifier

    cs.RO 2026-07 conditional novelty 5.0 of 10

    A hybrid reachability verifier certifies L∞ robustness of compact neural-ODE SilCam plankton classifiers and filters non-robust detections for AUV pipelines.

Reference graph

Works this paper leans on

10 extracted references · 2 canonical work pages · cited by 1 Pith paper

  1. [1]

    Ffjord: Free-form continuous dynamics for scalable reversible generative models.arXiv preprint arXiv:1810.01367,

    Will Grathwohl, Ricky TQ Chen, Jesse Bettencourt, Ilya Sutskever, and David Duvenaud. Ffjord: Free-form continuous dynamics for scalable reversible generative models.arXiv preprint arXiv:1810.01367,

    arXiv

  2. [2]

    Zhen Liang, Dejin Ren, Bai Xue, Ji Wang, Wenjing Yang, and Wanwei Liu

    doi: 10.1109/5.726791. Zhen Liang, Dejin Ren, Bai Xue, Ji Wang, Wenjing Yang, and Wanwei Liu. Verifying safety of neural networks from topological perspectives.Science of Computer Programming, 238:103160,

    doi:10.1109/5.726791

  3. [3]

    Zhaozhi Qian, William Zame, Lucas Fleuren, Paul Elbers, and Mihaela van der Schaar

    URL https://doi.org/10.29007/6czp. Zhaozhi Qian, William Zame, Lucas Fleuren, Paul Elbers, and Mihaela van der Schaar. Integrating expert odes into neural odes: pharmacology and disease progression.Advances in Neural Information Processing Systems, 34:11364–11383,

    work page doi:10.29007/6czp

  4. [4]

    Bridging neural ODE and ResNet: A formal error bound for safety verification

    Abdelrahman Sayed Sayed, Pierre-Jean Meyer, and Mohamed Ghazel. Bridging neural ODE and ResNet: A formal error bound for safety verification. InInternational Symposium on AI Verification, pp. 97–114. Springer, 2025a. Abdelrahman Sayed Sayed, Pierre-Jean Meyer, and Mohamed Ghazel. Mixed monotonicity reachability analysis of neural ode: A trade-off between ...

    arXiv

  5. [5]

    A System description This appendix describes the neural ODE benchmarks used in the experiments, organized by the three model classes introduced in Section

    14 Under review as submission to TMLR Appendix Experiments Settings:All the experiments 1 herein are run on MATLAB R2026a with the Continuous Reachability Analyzer (CORA) version 2025.1.1, the Toolbox for Interval Reachability Analysis (TIRA) version 2, and the Neural Network Verification Software Tool (NNV 2.0) on an AMD Ryzen™9 5950X CPU (16 cores, 32 t...

    2025

  6. [6]

    We consider two variants from the literature, anonlinearvariant from Chen et al

    whose trajectories form a spiral in the state space. We consider two variants from the literature, anonlinearvariant from Chen et al. (2018) and a linearvariant from Manzanas Lopez et al. (2022). The two variants share the same architecture of a 2-layer feed-forward network with a hidden layer of10neurons, in which the input is inR2, the hidden layer is i...

    2018

  7. [7]

    Since the hidden layer applies no activation, the dynamics reduce to a 2-dimensional linear ODE˙x=Ax+bwithA=W 2W1∈R2×2 andb=W 2b1 +b 2∈R2

    +b 2, withW 1,b 1,W 2,b 2 of the same shapes as in the nonlinear variant above. Since the hidden layer applies no activation, the dynamics reduce to a 2-dimensional linear ODE˙x=Ax+bwithA=W 2W1∈R2×2 andb=W 2b1 +b 2∈R2. The exact values of the weight matrices and bias vectors are defined within the MATLAB functionSystem_description.m. A.1.2 FPA TheFixed-Po...

    work page doi:10.5281/zenodo.20546365 1995

  8. [8]

    The exact values of the weight matrices and bias vectors are loaded from the MATLAB data fileplant_3rd_order_tanh.mat

    +b 2, whereW 1,b 1,W 2,b 2 are as in the linear variant andtanh(·)is applied element-wise to the hidden vector W1u+b 1∈Rh. The exact values of the weight matrices and bias vectors are loaded from the MATLAB data fileplant_3rd_order_tanh.mat. A.3 General neural ODE (GNODE) classification benchmarks A.3.1 MNIST Classification neural ODE The MNIST classifica...

    1998

Show all 10 references
  1. [9]

    that produces the tightest axis-aligned box enclosing the affine image of a box. We attempted to apply CTMM to the linear ODE block of this benchmark on a full imageL∞attack (i.e., all784pixels are perturbed), but CTMM produced no verified images on either network within our c...

    2022

  2. [10]

    TNODEV verifies58–60%of test images. Atϵ= 1/255, twice this magnitude, the verification rate falls to 1/50on both networks under both bound-extraction modes, while NNV 2.0 retains49/50on CNODES and 50/50on CNODE M (Manzanas Lopez et al., 2022). For verification under larger ad...

    2022

Pith tools

Reviewed July 12, 2026 · model on record in the stance chip above.