Robustness Verification of an Autonomous Underwater Vehicle-based Plankton Classifier

Abdelrahman Sayed Sayed; Asgeir J. S{\o}rensen; Mohamed Ghazel; Pierre-Jean Meyer

REVIEW 2 major objections 4 minor 17 references

Robustness Verification of an Autonomous Underwater Vehicle-based Plankton Classifier

T0 review · 2 major / 4 minor · reviewed 2026-07-11 · grok-4.5

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

Pith's one-line read A reachability verifier certifies that a neural-ODE plankton classifier stays correct under bounded pixel noise, filtering ambiguous AUV images automatically.

desk verdict Solid applied demo of hybrid neural-ODE reachability on SilCam plankton data that produces real certificates, but the deliberate 8 imes8 downscaling keeps the operational filter claim provisional. read the letter →

arxiv 2607.04453 v1 pith:HPT7CE5Q submitted 2026-07-05 cs.RO cs.AIcs.SYeess.SYmath.DS

Abdelrahman Sayed Sayed , Pierre-Jean Meyer , Asgeir J. S{o}rensen , Mohamed Ghazel This is my paper · ORCID

classification cs.ROcs.AIcs.SYeess.SYmath.DS

keywords neuralODEreachabilityanalysisrobustnessverificationplanktonclassificationautonomousunderwatervehiclesformalmethodsSilCam

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

Autonomous underwater vehicles now capture high-resolution images of plankton, but noise, turbidity and bubble artifacts cause standard classifiers to mislabel particles and force marine biologists into slow manual checks. This paper replaces the usual discrete CNN stack with a compact continuous-time neural ordinary differential equation model and wraps it in a reachability-based verifier. The verifier first samples for quick counter-examples; if none appear it over-approximates every possible output of the network under a chosen noise bound and proves whether the original class label remains dominant. When the proof succeeds the image is accepted with a formal guarantee; when it fails or times out the image is flagged for human review. The result is an automated filter that can cut post-processing workload while giving operators mathematical assurance that accepted classifications will not flip under the modelled environmental perturbations.

What carries the argument

The hybrid reachability loop: falsification sampling, continuous-time mixed-monotonicity reachability of the neural-ODE dynamics, star-set over-approximation of the pre- and post-ODE layers, and heuristic partitioning of uncertain input boxes until every subset is proven robust or the time budget expires.

What would settle it

Take a set of full-resolution SilCam images that the operational high-resolution classifier labels correctly, down-scale them exactly as the paper does, certify them under the same noise bounds, then re-inject the certified images into the original high-resolution pipeline and check whether any of those images flip class under the same pixel perturbations.

Watch

Extended reading notes

Core claim

A hybrid reachability pipeline (mixed-monotonicity for the continuous ODE block, star-set propagation for the surrounding layers, plus iterative refinement) can formally certify that a compact neural-ODE SilCam classifier remains correctly labelled under bounded L-infinity pixel perturbations, thereby acting as an automated filter that supplies stability guarantees and reduces manual validation of AUV plankton imagery.

Load-bearing premise

The deliberately reduced 8-by-8-by-3 input resolution and 32-dimensional ODE state still preserve the classification decisions that matter on real high-resolution SilCam images; if down-scaling itself destroys the true decision boundary, the certificates do not transfer to the operational pipeline.

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.

Desk Editor's Note

read the letter

The one thing worth knowing is that this is a working end-to-end demonstration: they take their prior mixed-monotonicity ODE reachability, glue it to NNV star-sets for the surrounding layers, add a cheap falsification pre-check, and actually certify a compact neural-ODE classifier on real SilCam imagery under explicit L∞ pixel sets. Tables I–II give concrete ROBUST / NOT ROBUST / UNKNOWN verdicts with runtimes for both ReLU and Tanh; models and code are public. That is new for the marine-imaging setting and useful.

What they do well is keep the architecture honest and verifiable. The GNODE is a deliberate compaction of an earlier CNN (two conv blocks → 32-dim ODE state → small FC head), the falsification sample check kills obviously non-robust cases in zero time, and they correctly flag that Tanh yields tighter bounds than ReLU on the harder full-image cases. The hybrid pipeline itself looks sound; no circularity, no invented math.

The soft spot is exactly the one the reader flagged and the paper itself lists as future work: everything is certified on 8×8×3 inputs chosen purely for tractability. If the down-scaling changes the decision boundary or the noise model that matters on full-resolution SilCam frames, the certificates do not transfer to the AUV pipeline. They only show a handful of (ε, k) pairs, many full-image cases time out at 7200 s, and there is no side-by-side with a standard CNN baseline. Those are real but proportionate limitations; they do not break the formal claims that are actually made.

This is for people who care about formal methods for continuous-time networks or trustworthy onboard classification on AUVs. The math and data look solid enough that a serious editor should send it to referees rather than desk-reject. I would bring it to reading group if we are talking verification of dynamical models or marine autonomy; otherwise maybe. Worth engaging if that intersection is your area; otherwise a quick skim of the tables and Section VI is enough.

Referee Report

2 major / 4 minor

Summary. The paper proposes a reachability-based robustness verification framework for in-situ plankton classifiers on AUVs, combining a falsification pre-check, mixed-monotonicity reachability for a neural ODE block, and star-set propagation for surrounding layers (with refinement). It introduces a compact general neural ODE (GNODE) classifier (pre-ODE conv layers, 32-dim autonomous ODE with ReLU or Tanh, post-ODE FC head) trained on downscaled 8 imes8 imes3 SilCam images from the PyOPIA dataset (7 classes). Robustness is specified as preservation of the correct class label under bounded L∞ perturbations on k pixels; Tables I–II report ROBUS T / NOT ROBUST / UNKNOWN verdicts and runtimes for selected (k, ε) pairs, arguing that the verifier can serve as an automated filter that supplies formal stability guarantees and reduces manual post-processing.

Significance. If the results hold, the work is a useful step toward trustworthy AI for marine robotics: it supplies the first concrete formal certificates (via an independent hybrid reachability engine) for a neural-ODE plankton classifier under environmental noise models, and the authors release trained models and code. The hybrid pipeline (mixed-monotonicity for continuous-time dynamics + NNV-style star sets) and the empirical observation that Tanh is easier to verify than ReLU under full-image attacks are of independent interest to the formal-methods-for-ML community. The operational claim that the framework already acts as a reliable AUV filter remains provisional, however, because certificates are obtained only on a deliberately reduced-resolution model.

major comments (2)

[Section IV-B, Tables I–II, Abstract, Section VI] Section IV-B explicitly states that the 8 imes8 imes3 input resolution and n=32 ODE state are deliberate compactifications of the original CNN architecture of [2], chosen purely for verification tractability (tighter over-approximations, fewer split dimensions). Tables I–II therefore certify only this reduced model. The abstract, introduction and conclusion nevertheless claim that the framework “acts as an automated filter” improving reliability of autonomous sampling and reducing post-processing workload for real SilCam pipelines. Section VI lists higher-resolution verification and formal guarantees for the down-scaling stage as future work, so the transfer assumption is currently unsubstantiated and load-bearing for the application claim.
[Section V, Tables I–II] The experimental demonstration is narrow: Tables I–II cover only a handful of (k,ε) pairs, with several full-image cases returning UNKNOWN after the 7200 s timeout. No systematic sweep of radii, no comparison against a discrete residual-network baseline of comparable size, and no evaluation of how often the falsification pre-check alone already discards non-robust images on a held-out set are provided. Consequently the claim that the framework is “effective” for filtering ambiguous in-situ data rests on a very small sample of successful ROBUS T verdicts.

minor comments (4)

[Section II, III headings] Section headings contain concatenated words without spaces (“NEURALORDINARYDIFFERENTIALEQUATIONS”, “UNDERWATERIMAGEVERIFICATIONFRAMEWORK”, etc.); these should be corrected for readability.
[Figure 2] Figure 2 caption and the surrounding text inconsistently spell “dimesnions” / “dimensions”; also the ODE state dimension is written both as n=32 and “ODE state dimesnions: 32”.
[Section III-B] The falsification sample count of 1000 is justified only by reference to the TNODEV toolbox examples; a short sensitivity statement (or citation of a statistical argument) would strengthen the claim that the pre-check is reliable.
[References] Reference [14] (TNODEV) and [15] are listed as 2026 / arXiv preprints; ensure final versions or DOIs are supplied if available at camera-ready time.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity; certificates are independent computational outputs of a reachability engine applied to trained models, not reductions of fitted inputs or self-definitions.

full rationale

The paper's derivation chain is: train compact GNODE classifiers (ReLU/Tanh variants) on SilCam data via standard PyTorch/torchdiffeq, define L∞ perturbation sets X0 and safe output region S, then run a hybrid reachability pipeline (mixed-monotonicity on the ODE block + star-set on surrounding layers + refinement) that returns ROBUS T / NOT ROBUST / UNKNOWN verdicts. Tables I–II report those empirical certificates. Self-citations ([13]–[15], TNODEV) supply the underlying reachability algorithms and toolbox, which is ordinary reuse of prior method papers; the present claims are the application results and the AUV-filter interpretation, not a re-derivation or uniqueness theorem that forces the verdicts. No parameter is fitted to data and then re-presented as a prediction; no equation is defined in terms of the quantity it purports to prove; the down-scaling choice is explicitly acknowledged as a tractability decision and listed as future work. The chain is therefore self-contained against external benchmarks (the trained weights and the independent verifier runs).

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

The central certificates rest on standard reachability soundness, a deliberate low-resolution architecture chosen for tractability, an empirical noise model, and several hand-chosen verification parameters. No new physical entities are postulated; free parameters are the usual engineering knobs of the verifier and the network.

free parameters (4)

input resolution and ODE state dimension = 8×8×3, n=32
Fixed at 8×8×3 = 192 and n=32 solely for verification tractability (Section IV-B); not derived from data or theory.
falsification sample count = 1000
Set empirically to 1000 random samples from X0 (Section III-B); controls the pre-check’s ability to find counter-examples.
verification timeout = 7200 s
Hard limit of 7200 s after which UNKNOWN is returned (Tables I–II).
L∞ radii ε and attacked-pixel sets P = various discrete pairs
Hand-chosen discrete values (0.01/255 o 10/255, k=1,10,192) that define the robustness queries being certified.

assumptions (3)

standard math Soundness of mixed-monotonicity reachability for the autonomous neural-ODE block and of star-set propagation for the surrounding layers (NNV 2.0).
Invoked throughout Section III-C; the over-approximation Ω(X) ⊇ R(X) is trusted without re-proof.
domain assumption Environmental noise can be adequately modeled as an axis-aligned L∞ box on a chosen subset of pixels of a down-scaled image.
Defines the input set X0 in Section IV-C; real bubble/turbidity artifacts may not be pure L∞.
ad hoc to paper The reduced-resolution classifier preserves the robustness properties that matter for the original high-resolution SilCam pipeline.
Stated as a deliberate design choice in Section IV-B; never formally justified or verified.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Robustness Verification of an Autonomous Underwater Vehicle-based Plankton Classifier." pith.science (2026). https://pith.science/paper/HPT7CE5Q

@misc{pith2026260704453,
  author       = {Pith},
  title        = {Pith review of: Robustness Verification of an Autonomous Underwater Vehicle-based Plankton Classifier},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HPT7CE5Q}},
  note         = {Machine review of arXiv:2607.04453}
}

read the original abstract

The assessment of planktonic standing stocks and microorganism structures is critical for understanding upper ocean biological processes. Currently, autonomous underwater vehicles (AUVs) equipped with in-situ optical imaging and artificial intelligence (AI) methods offer a promising solution for persistent surveillance, mapping and monitoring of planktonic life. However, current AI methods often lack robustness in dynamic, unstructured environments, where environmental noise and non-biological artifacts lead to frequent misclassifications. Standard convolutional neural network (CNN) classifiers often struggle with such conditions, leading to misclassifications that require time-consuming manual validation by marine biologists. To address this issue, we propose a novel robustness verification framework for in-situ plankton classifiers based on reachability analysis. We also introduce a continuous-time neural ordinary differential equation (neural ODE) classification model leveraging the high-resolution imaging capabilities of the SilCam particle imager. In this paper, we demonstrate the effectiveness of the proposed framework by formally verifying the robustness of the neural ODE model against environmental perturbations. We demonstrate that our verification framework acts as an automated filter providing formal guarantees of model stability against ambiguous data, thereby improving the reliability of autonomous sampling and reducing the post-processing workload.

Figures

Figures reproduced from arXiv: 2607.04453 by the authors.

**Figure 1.** Verifier Architecture will each go again through the reachability and verification steps 1 and 2 described above. This partitioning uses heuristics that identify and split the input dimensions that contribute most to the output uncertainty [14]. The verifier repeats this loop, refining the unverified subsets, until either every subset satisfies the specification yielding a ROBUST verdict, or the algorithm times out… view at source ↗

**Figure 2.** Neural ODE model architecture 850 diatom chains, 514 fecal pellets, 671 oil, 479 oily gas particles, and 1931 other. Although copepods represent only a small fraction of the dataset (657 images), the neural ODE classifier still achieves strong copepod classification recognition of 81.1%. We attribute this in part to the parameter efficiency of neural ODE as their weight-sharing, continuousdepth formulation uses fa… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

17 extracted references · 2 linked inside Pith

[2]

Advancing ocean observation with an AI-driven mobile robotic explorer,

A. Saad, A. Stahl, A. V ˚age, E. Davies, T. Nordam, N. Aberle, M. Ludvigsen, G. Johnsen, J. Sousa, and K. Rajan, “Advancing ocean observation with an AI-driven mobile robotic explorer,”Oceanography, vol. 33, no. 3, pp. 50–59, 2020

2020
[1]

The use of wide-band transmittance imaging to size and classify suspended particulate matter in seawater,

E. J. Davies, P. J. Brandvik, F. Leirvik, and R. Nepstad, “The use of wide-band transmittance imaging to size and classify suspended particulate matter in seawater,”Marine pollution bulletin, vol. 115, no. 1-2, pp. 105–114, 2017

2017
[3]

Zooplanktonet: Deep convolutional network for zooplankton classification,

J. Dai, R. Wang, H. Zheng, G. Ji, and X. Qiao, “Zooplanktonet: Deep convolutional network for zooplankton classification,” inOCEANS 2016- Shanghai. IEEE, 2016, pp. 1–6

2016
[4]

PyOPIA: A python ocean particle image analysis toolbox,

E. Davies, A. Nimmo-Smith, R. Nepstad, T. Nordam, U. Bronner, A. Steinvik, S. Giering, M. Masoudi, Z. Liu, P. Helaouetet al., “PyOPIA: A python ocean particle image analysis toolbox,” 2023

2023
[5]

Intriguing properties of neural networks,

C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Good- fellow, and R. Fergus, “Intriguing properties of neural networks,” in International Conference on Learning Representations (ICLR), 2014

2014
[6]

Explaining and harnessing adversarial examples,

I. J. Goodfellow, J. Shlens, and C. Szegedy, “Explaining and harnessing adversarial examples,” inInternational Conference on Learning Repre- sentations (ICLR), 2015

2015
[7]

Neural ordinary differential equations,

R. T. Chen, Y . Rubanova, J. Bettencourt, and D. K. Duvenaud, “Neural ordinary differential equations,”Advances in neural information pro- cessing systems, vol. 31, 2018

2018
[8]

On the robustness to adversarial examples of neural ODE image classifiers,

F. Carrara, R. Caldelli, F. Falchi, and G. Amato, “On the robustness to adversarial examples of neural ODE image classifiers,” in2019 IEEE International Workshop on Information Forensics and Security (WIFS). IEEE, 2019, pp. 1–6

2019

Show all 17 references

[9]

Defending neural ODE image classifiers from adversarial attacks with tolerance randomization,

F. Carrara, R. Caldelli, F. Falchi, and G. Amato, “Defending neural ODE image classifiers from adversarial attacks with tolerance randomization,” inInternational Conference on Pattern Recognition. Springer, 2021, pp. 425–438

2021
[10]

On robustness of neural ordinary differential equations,

H. Yan, J. Du, V . Y . F. Tan, and J. Feng, “On robustness of neural ordinary differential equations,” 2022. [Online]. Available: https://arxiv.org/abs/1910.05513

2022 arXiv
[11]

A stable mapping of nmode,

H. Luo, T. He, and Z. Yi, “A stable mapping of nmode,”Artificial Intelligence Review, vol. 57, no. 5, p. 120, 2024

2024
[12]

Meyer, A

P.-J. Meyer, A. Devonport, and M. Arcak,Interval reachability analysis: Bounding trajectories of uncertain systems with boxes for control and verification. Springer Nature, 2021

2021
[13]

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

A. S. Sayed, P.-J. Meyer, and M. Ghazel, “Bridging neural ODE and resnet: A formal error bound for safety verification,” inInternational Symposium on AI Verification. Springer, 2025, pp. 97–114

2025
[14]

Tnodev: Toolbox for neural ODE verification,

A. S. Sayed, P.-J. Meyer, and M. Ghazel, “Tnodev: Toolbox for neural ODE verification,” 2026. [Online]. Available: https: //arxiv.org/abs/2606.16567

2026 arXiv
[15]

Mixed monotonicity reach- ability analysis of neural ode: A trade-off between tightness and effi- ciency,

A. S. Sayed, P.-J. Meyer, and M. Ghazel, “Mixed monotonicity reach- ability analysis of neural ode: A trade-off between tightness and effi- ciency,”arXiv preprint arXiv:2510.17859, 2025

2025
[16]

NNV 2.0: The neural network verification tool,

D. M. Lopez, S. W. Choi, H.-D. Tran, and T. T. Johnson, “NNV 2.0: The neural network verification tool,” inInternational Conference on Computer Aided Verification. Springer, 2023, pp. 397–412

2023
[17]

torchdiffeq,

R. T. Q. Chen, “torchdiffeq,” 2018. [Online]. Available: https: //github.com/rtqichen/torchdiffeq

2018

Pith tools

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

[1] [2]

Advancing ocean observation with an AI-driven mobile robotic explorer,

A. Saad, A. Stahl, A. V ˚age, E. Davies, T. Nordam, N. Aberle, M. Ludvigsen, G. Johnsen, J. Sousa, and K. Rajan, “Advancing ocean observation with an AI-driven mobile robotic explorer,”Oceanography, vol. 33, no. 3, pp. 50–59, 2020

2020

[2] [1]

The use of wide-band transmittance imaging to size and classify suspended particulate matter in seawater,

E. J. Davies, P. J. Brandvik, F. Leirvik, and R. Nepstad, “The use of wide-band transmittance imaging to size and classify suspended particulate matter in seawater,”Marine pollution bulletin, vol. 115, no. 1-2, pp. 105–114, 2017

2017

[3] [3]

Zooplanktonet: Deep convolutional network for zooplankton classification,

J. Dai, R. Wang, H. Zheng, G. Ji, and X. Qiao, “Zooplanktonet: Deep convolutional network for zooplankton classification,” inOCEANS 2016- Shanghai. IEEE, 2016, pp. 1–6

2016

[4] [4]

PyOPIA: A python ocean particle image analysis toolbox,

E. Davies, A. Nimmo-Smith, R. Nepstad, T. Nordam, U. Bronner, A. Steinvik, S. Giering, M. Masoudi, Z. Liu, P. Helaouetet al., “PyOPIA: A python ocean particle image analysis toolbox,” 2023

2023

[5] [5]

Intriguing properties of neural networks,

C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Good- fellow, and R. Fergus, “Intriguing properties of neural networks,” in International Conference on Learning Representations (ICLR), 2014

2014

[6] [6]

Explaining and harnessing adversarial examples,

I. J. Goodfellow, J. Shlens, and C. Szegedy, “Explaining and harnessing adversarial examples,” inInternational Conference on Learning Repre- sentations (ICLR), 2015

2015

[7] [7]

Neural ordinary differential equations,

R. T. Chen, Y . Rubanova, J. Bettencourt, and D. K. Duvenaud, “Neural ordinary differential equations,”Advances in neural information pro- cessing systems, vol. 31, 2018

2018

[8] [8]

On the robustness to adversarial examples of neural ODE image classifiers,

F. Carrara, R. Caldelli, F. Falchi, and G. Amato, “On the robustness to adversarial examples of neural ODE image classifiers,” in2019 IEEE International Workshop on Information Forensics and Security (WIFS). IEEE, 2019, pp. 1–6

2019