Paper deep dive
Robustness Verification of an Autonomous Underwater Vehicle-based Plankton Classifier
Abdelrahman Sayed Sayed, Pierre-Jean Meyer, Asgeir J. Sørensen, Mohamed Ghazel
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 87%
Last extracted: 7/7/2026, 1:43:18 PM
Summary
This paper introduces a robustness verification framework for AUV-based plankton classifiers, utilizing neural ordinary differential equations (Neural ODEs) and reachability analysis to formally guarantee classification stability against environmental perturbations, thereby reducing manual validation efforts by marine biologists.
Entities (8)
Relation Signals (7)
Robustness Verification Framework → verifies → Neural ODE Classifier
confidence 95% · propose a novel robustness verification framework for in-situ plankton classifiers... formally verifying the robustness of the neural ODE model
Autonomous Underwater Vehicle → equippedwith → SilCam Particle Imager
confidence 90% · autonomous underwater vehicles (AUVs) equipped with in-situ optical imaging... SilCam
Neural ODE Classifier → leverages → Reachability Analysis
confidence 90% · based on reachability analysis... formally verifying the robustness
NNV 2.0 → implements → Star-set Propagation
confidence 85% · propagated with the star-set method of NNV 2.0
Robustness Verification Framework → reducesmanualvalidationfor → Marine Biologists
confidence 85% · reducing the post-processing workload... manual validation by marine biologists
Neural ODE Classifier → outperforms → Convolutional Neural Network
confidence 80% · Standard convolutional neural network (CNN) classifiers often struggle... neural ODE have emerged as a powerful and robust alternative.
PyOPIA Toolbox → provides → Plankton Dataset
confidence 80% · used the in-situ SilCam images collected through the PyOPIA ocean particle image analysis toolbox
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2607.04453v1
- Canonical: https://arxiv.org/abs/2607.04453v1
Trouble viewing inline? Open PDF directly →
Full Text
24,111 characters extracted from source content.
Expand or collapse full text
Robustness Verification of an Autonomous Underwater Vehicle-based Plankton Classifier †thanks: This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie COFUND grant agreement no. 101034248. This work is partly funded by SFI HARVEST, 309661 by the Research Council of Norway. Abdelrahman Sayed Sayed Pierre-Jean Meyer Asgeir J. Sørensen Mohamed Ghazel 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. I Introduction The growing interest in assessing and monitoring planktonic standing stocks and microorganism structures in the upper water column (mesopelagic zone) is critical for understanding the impact of climate change on ocean processes. To achieve continuous systematic ecosystem surveillance and monitoring, the oceanographic community is increasingly relying on autonomous underwater vehicles (AUVs) equipped with advanced optical sensors, such as the SilCam [7], and Artificial Intelligence (AI)-based tools. These AUVs enable high-resolution imaging and intelligent onboard sampling [12], significantly accelerating the detection and classification of microorganisms while simultaneously reducing the operational cost of deploying fleets of research vessels. Currently, the automated classification of in-situ plankton imagery is mostly dependent on convolutional neural networks (CNNs), including task-specific architectures such as ZooplanktoNet [5], and in-situ imaging and analysis pipelines built around the SilCam imager [7] and PyOPIA toolbox [6]. However, deploying AI-based classification models in uncertain and unstructured underwater environments raises significant challenges. Compared to controlled laboratory settings, in-situ ocean imaging is affected by dynamic environmental noise, turbidity, and particularly by gas bubbles generated by the AUV’s own motion. These appear as bright artifacts overlaid on the imaged particles and, hence, routinely trigger misclassifications. To bridge the gap between reliable autonomy and AI-based classification models whose behaviour can be trusted, there is a need for rigorous verification tools that can certify the stability of classifiers against such environmental perturbations. While current CNN-based classifiers are static models often vulnerable to adversarial perturbations [16, 8], neural ordinary differential equations (neural ODE) [4] have emerged as a powerful and robust alternative. Modeled as a continuous-time system, they have been empirically shown to be naturally more robust against some adversarial attacks [1, 2, 17, 10]. Beyond such empirical robustness, formal verification provides provable guarantees on the classifier’s behaviour over an entire set of perturbed inputs. Among well-known formal methods, reachability-based techniques propagate an input set layer-by-layer to over-approximate the reachable outputs [11]. However, recent tools target mostly feed-forward ReLU networks, and certifying the continuous-time dynamics of a neural ODE remains mostly unexplored [13]. In this work, we propose a novel robustness verification framework for AUV-based plankton classifiers. Namely, we leverage the robustness properties of neural ODE and reachability analysis to formally guarantee the stability of classification results against specific noise thresholds. By integrating this verifier into the AUV processing pipeline, we aim to automatically filter ambiguous data and misclassifications, thereby enhancing the reliability of in-situ ocean observation. Section I first introduces the neural ODE model class we consider. Section I presents the verification framework, Section IV describes the experimental setup and problem definition, and Section V reports the verification results. I Neural Ordinary Differential Equations A neural ODE [4] models a continuous-depth transformation of a hidden state z(t)∈ℝnz(t) ^n as the solution to an initial value problem dz(t)dt=f(z(t),t,θ),z(t0)=z0, dz(t)dt=f (z(t),t,θ ), z(t_0)=z_0, (1) where the vector field f is a neural network that is parameterized by trainable weights θ. The model output is obtained by integrating (1) from t0t_0 to a final time tft_f, z(tf)=z0+∫t0tff(z(t),t,θ)t,z(t_f)=z_0+ _t_0^t_ff (z(t),t,θ )\,dt, which is evaluated numerically with an ODE solver. Replacing the discrete stack of residual layers of a standard neural network by continuous dynamics (1) is what gives neural ODE their smooth and stability-related robustness properties [17]. In practice, the ODE block does not act on the raw input but is embedded between neural network layers, yielding what we refer to as a general neural ODE (GNODE). In a formal way, a GNODE classifier is the composition =gpost∘Φ∘gpre:ℝm→ℝc,N=g_post g_pre:R^m ^c, (2) where gpre:ℝm→ℝng_pre:R^m ^n is a feature-extraction network mapping an input (an image in our case) to the ODE initial state z0=gpre(x)z_0=g_pre(x), Φ:z0↦z(tf) :z_0 z(t_f) is the flow obtained by integrating (1), and gpost:ℝn→ℝcg_post:R^n ^c is a classification head mapping the terminal state to the c class scores. We consider the autonomous GNODE, where the vector field f is a feed-forward network independent of t. In our model, f is a single hidden-layer network dz(t)dt=W2σ(W1z(t)+b1)+b2, dz(t)dt=W_2\,σ\! (W_1z(t)+b_1 )+b_2, (3) where σ is an element-wise activation function and W1,W2,b1,b2W_1,W_2,b_1,b_2 are the trainable parameters of the ODE block. In the architecture used throughout this paper (Section IV), the state dimension is n=32n=32 and σ is either the hyperbolic tangent (Tanh) or the rectified linear unit (ReLU) activation function. Figure 1: Verifier Architecture I Underwater Image Verification Framework The architecture of the proposed verifier is illustrated in Figure 1. The framework is designed to formally guarantee that a classified image from in-situ images remains robust against environmental or user induced perturbations. This process is divided into two main phases: an initial falsification check and a rigorous verification and refinement loop. I-A Initialization and Robustness Specification First, we define an initial input set 0X_0 (representing an in-situ image with perturbation noise) and a desired classification S (the region of the output space corresponding to the correct class label). The goal is to prove that for all x∈0x _0, the classified output of the model remains within S. I-B Image Falsification Check This preliminary check avoids the unnecessary computational cost of full reachability analysis. The verifier generates 10001000 random samples from the entire input set 0X_0 (i.e., the set of all potential noisy variations of the image) and evaluates the neural ODE classifier against the specification. This sample count was set empirically across the examples presented in the TNODEV toolbox [15], and is large enough to reliably expose specification-violating inputs in this pre-check. The outcome of this check determines the next step: • Counter-example found: if any sample violates the desired classification S, the verification process terminates, returning a NOT ROBUST verdict, indicating that the classifier is not robust for this image. • No counter-example: if no violation is detected among the samples, the verifier proceeds to the verification and refinement loop. I-C Image Verification and Refinement In this phase, the verifier iteratively proves that the robustness specification S is satisfied for the input image set 0X_0 using reachability analysis. As illustrated in Figure 1, this loop consists of three main blocks: 1. Reachability Block: the verifier propagates the input set 0X_0 through the layers of the neural ODE classifier to compute a guaranteed over-approximation Ω(0)⊇ℛ(0) (X_0) (X_0) of the exact output reachable set ℛ(0)=(x):x∈0R(X_0)=\N(x):x _0\. The ODE block is handled with continuous time mixed-monotonicity reachability, as discussed in [14], while the surrounding pre-ODE convolutional and post-ODE fully-connected layers are propagated with the star-set method of NNV 2.0 [9] in a hybrid pipeline. 2. Verification Check: the resulting over-approximation is checked against S, and if Ω(0)⊂ (X_0) (i.e., the correct class score remains dominant over the entire set), the current image subset is verified. 3. Refinement Block: if the check returns false, the input set is partitioned into smaller subsets (in our case, shaped as intervals, i.e. axis-aligned hyperrectangles), which 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 [15]. 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 and thus returns the verdict UNKNOWN. An UNKNOWN verdict is not a failure of the method, but simply the standard inconclusive outcome of sound but incomplete reachability-based verifiers such as NNV 2.0 [9], as the over-approximation is too loose to produce a verdict on the robustness specification within the allocated computation time limit. We discuss its operational interpretation in Section V. IV Experimental Setup The neural ODE networks were trained in PyTorch using the torchdiffeq adjoint ODE solver [3], on a desktop with an AMD Ryzen™ 9 5950X CPU (16 cores, 32 threads), 96 GB of RAM, and a NVIDIA GeForce RTX 5080 GPU with 16 GB of VRAM. The trained neural ODE models are available at the following repository: https://github.com/ab-sayed/Robustness-Verification-of-an-AUV-based-Plankton-Classifier IV-A Underwater Plankton Dataset We used the in-situ SilCam images collected through the PyOPIA ocean particle image analysis toolbox [6]. The dataset contains 77 plankton classes (bubble, copepod, diatom chains, fecal pellets, oil, oily gas particles, and other) for a total of 77387738 images, distributed as 26362636 bubbles, 657657 copepods, 850850 diatom chains, 514514 fecal pellets, 671671 oil, 479479 oily gas particles, and 19311931 other. Although copepods represent only a small fraction of the dataset (657657 images), the neural ODE classifier still achieves strong copepod classification recognition of 81.1%81.1\%. We attribute this in part to the parameter efficiency of neural ODE as their weight-sharing, continuous-depth formulation uses far fewer parameters compared to an equivalent discrete network [4], which reduces the risk of overfitting on under-represented classes. IV-B Classifier Architectures Our neural ODE classifier illustrated in Figure 2 follows the in-situ plankton classification architecture of the CNN classifier introduced in [12], but adopts a compact and verifiable architecture in which the deep convolutional stack is reduced and the core nonlinear transformation is realized by a neural ODE block. From an input image 8×8×38× 8× 3 (192192 dimension), two pre-ODE feature-extraction blocks (2D convolution, batch normalization, and activation function σ) reduce the input to a flattened 3232-dimensional feature vector. This vector is the initial state z0z_0 of the ODE layer defined in (3) with state dimension n=32n=32. The integrated state z(tf)z(t_f) is then passed to a post-ODE classification block of two fully-connected layers (6464 then 77 units), producing the score over the 77 classes. The reduced input resolution and compact ODE state are deliberate choices made primarily for verification tractability, as a smaller input dimension (8×8×3=1928× 8× 3=192) and state dimension (n=32n=32) yield tighter reachable set over-approximations and fewer dimensions to split during refinement, which together lower the verification cost. These dimensions are not the product of a heuristic architecture search, as they follow from a direct compaction of the original CNN classifier [12], reducing its convolutional stack and replacing the core nonlinear transformation with the neural ODE block. Figure 2: Neural ODE model architecture We evaluate two variants of this architecture that share the same structure and differ only in the activation function σ used in the feature-extraction, ODE, and post-ODE layers: IV-B1 Neural ODE-based classifier with ReLU The variant using the ReLU activation, σ(s)=max(0,s)σ(s)= (0,s). IV-B2 Neural ODE-based classifier with Tanh The variant using the Tanh activation, σ(s)=tanh(s)σ(s)= (s). IV-C Problem Definition Let :ℝm→ℝcN:R^m ^c denote the trained neural ODE classifier mapping an input image to class scores, with input values m=8×8×3=192m=8× 8× 3=192 and classes c=7c=7. Let x⋆∈ℝmx ^m be a nominal image that is correctly classified, with true label ℓ=argmaxj∈1,…,cj(x⋆). = _j∈\1,…,c\N_j(x ). Perturbation strategy We model environmental noise as a bounded L∞L_∞ perturbation applied to a subset P⊆1,…,mP \1,…,m\ of k=|P|k=|P| pixels, with magnitude ε expressed in normalized intensity units (i.e., ε=α/255 =α/255). This induces the input set 0=x∈ℝm:∀i∈P,|xi−xi⋆|≤ε;∀i∉P,xi=xi⋆,X_0= \x ^m\;:\;∀ i∈ P,|x_i-x _i|≤ ;∀ i∉ P,x_i=x _i\ \, which is an axis-aligned box (hyperrectangle). We consider k∈1,…,192k∈\1,…,192\ attacked pixels, ranging from a single-pixel perturbation to the full 192192-pixel image, over a range of L∞L_∞ radii ε . Robustness specification Robustness requires that the correct label ℓ remain dominant over the entire perturbation set. The safe output region is =y∈ℝc:yℓ>yj∀j≠ℓ.S= \y ^c\;:\;y_ >y_j\ \ ∀ j≠ \. Verification goal The classifier is certified robust for x⋆x under perturbation (ε,P)( ,P) if and only if every reachable output keeps ℓ dominant, i.e. (0)⊆.N(X_0) . The verifier in Section I returns ROBUST when this inclusion is proven, NOT ROBUST when a counter-example is found by the falsification check, and UNKNOWN when neither verdict is established within the allocated time limit. V Verification Results Tables I and I report the verification verdicts and runtimes for the ReLU and Tanh variants across different perturbation settings as mentioned in Section IV-C. Table I: Robustness verification results for neural ODE-based classifier with ReLU activation Pixels Attacked Noise (L∞L_∞) Verdict Time 1 / 192 0.1/255 ROBUST 128.1 s 1 / 192 0.5/255 ROBUST 104.2 s 10 / 192 0.1/255 ROBUST 104.8 s 192 / 192 0.01/255 ROBUST 108.9 s 192 / 192 5/255 NOT ROBUST 0 s 192 / 192 10/255 NOT ROBUST 0 s 192 / 192 1/255 Unknown 7200 s 192 / 192 0.05/255 Unknown 7200 s Table I: Robustness verification results for neural ODE-based classifier with Tanh activation Pixels Attacked Noise (L∞L_∞) Verdict Time 1 / 192 0.1/255 ROBUST 119.2 s 1 / 192 0.5/255 ROBUST 101.4 s 10 / 192 0.1/255 ROBUST 105.2 s 192 / 192 0.01/255 ROBUST 113.1 s 192 / 192 5/255 NOT ROBUST 0 s 192 / 192 10/255 NOT ROBUST 0 s 192 / 192 1/255 Unknown 7200 s 192 / 192 0.05/255 ROBUST 105.2 s Localized perturbations For sparse perturbations affecting a single pixel or ten pixels (k∈1,10k∈\1,10\), both variants are certified ROBUST across all tested radii, with verification verdicts reached within approximately 100100–130130 seconds. This indicates that the classifier is provably robust to the localized corruptions typically of small bubbles or sensor noise that affect only a few pixels of some region of interest. Full-image perturbations When every pixel is perturbed (k=192k=192), the verdict depends strongly on the perturbation radius ε . At a small radius (ε=0.01/255 =0.01/255) both variants remain ROBUST (around 109109 and 113113 s), certifying stability against uniform low-intensity noise across the whole image. At large radii (ε∈5/255,10/255 ∈\5/255,10/255\) both variants are immediately reported NOT ROBUST as the falsification check finds a counter-example at essentially zero cost (0 s), and therefore no reachability computation is initiated. This highlights the practical value of the cheap falsification pre-check, which discards clearly non-robust cases without consuming much computation time. The role of the activation functions At ε=1/255 =1/255 (full image attack), both variants return UNKNOWN after the allocated timeout of 72007200 s, meaning that the over-approximation is too loose to prove the robustness specification, and refinement does not close this gap within the fixed time limit. At the smaller radius ε=0.05/255 =0.05/255, the two activations diverge, as the Tanh variant is certified ROBUST in 105.2105.2 s, while the ReLU variant exhausts the allocated time duration. This contrast reflects a verifiability advantage of the smooth Tanh activation function dynamics, as its bounded derivative (tanh′(s)=sech2(s)∈(0,1] (s)=sech^2(s)∈(0,1]) yields tighter Jacobian and mixed-monotonicity bounds and avoids the combinatorial case-splitting that the piecewise-linear ReLU induces in the star-set reachability of the post-ODE layers. VI Conclusion and Future Work We presented a reachability-based robustness verification framework for AUV-based plankton classifiers and introduced a compact neural ODE classifier for in-situ SilCam imagery. By combining mixed-monotonicity reachability for the continuous-time ODE block with star-set propagation for the surrounding layers, the framework provides formal guarantees that a classified image remains correctly classified under bounded L∞L_∞ perturbations, acting as an automated filter that reduces the manual post-processing burden on marine biologists. Our results further indicate that the Tanh activation function can be easier to verify than ReLU in the harder settings of full-image perturbation, which is a relevant observation when designing classifiers intended to be formally certified. Future work includes extending the verification to higher input resolutions, deriving formal guarantees for the image downscaling stage preceding the classifier, and integrating the verifier into the onboard AUV processing pipeline for real-time filtering of ambiguous detections. VII Acknowledgements We acknowledge the support from Ahmed Abdelgayed throughout all phases of this work. We would like to thank Emlyn J. Davies and Raymond Nepstad from SINTEF Ocean for the initial discussions and feedback at the start of this work. References [1] F. Carrara, R. Caldelli, F. Falchi, and G. Amato (2019) On the robustness to adversarial examples of neural ODE image classifiers. In 2019 IEEE International Workshop on Information Forensics and Security (WIFS), p. 1–6. Cited by: §I. [2] F. Carrara, R. Caldelli, F. Falchi, and G. Amato (2021) Defending neural ODE image classifiers from adversarial attacks with tolerance randomization. In International Conference on Pattern Recognition, p. 425–438. Cited by: §I. [3] R. T. Q. Chen (2018) Torchdiffeq. External Links: Link Cited by: §IV. [4] R. T. Chen, Y. Rubanova, J. Bettencourt, and D. K. Duvenaud (2018) Neural ordinary differential equations. Advances in neural information processing systems 31. Cited by: §I, §I, §IV-A. [5] J. Dai, R. Wang, H. Zheng, G. Ji, and X. Qiao (2016) ZooplanktoNet: deep convolutional network for zooplankton classification. In OCEANS 2016-Shanghai, p. 1–6. Cited by: §I. [6] E. Davies, A. Nimmo-Smith, R. Nepstad, T. Nordam, U. Bronner, A. Steinvik, S. Giering, M. Masoudi, Z. Liu, P. Helaouet, et al. (2023) PyOPIA: a python ocean particle image analysis toolbox. Cited by: §I, §IV-A. [7] E. J. Davies, P. J. Brandvik, F. Leirvik, and R. Nepstad (2017) The use of wide-band transmittance imaging to size and classify suspended particulate matter in seawater. Marine pollution bulletin 115 (1-2), p. 105–114. Cited by: §I. [8] I. J. Goodfellow, J. Shlens, and C. Szegedy (2015) Explaining and harnessing adversarial examples. In International Conference on Learning Representations (ICLR), Cited by: §I. [9] D. M. Lopez, S. W. Choi, H. Tran, and T. T. Johnson (2023) NNV 2.0: the neural network verification tool. In International Conference on Computer Aided Verification, p. 397–412. Cited by: item 1, §I-C. [10] H. Luo, T. He, and Z. Yi (2024) A stable mapping of nmode. Artificial Intelligence Review 57 (5), p. 120. Cited by: §I. [11] P. Meyer, A. Devonport, and M. Arcak (2021) Interval reachability analysis: bounding trajectories of uncertain systems with boxes for control and verification. Springer Nature. Cited by: §I. [12] A. Saad, A. Stahl, A. Våge, E. Davies, T. Nordam, N. Aberle, M. Ludvigsen, G. Johnsen, J. Sousa, and K. Rajan (2020) Advancing ocean observation with an AI-driven mobile robotic explorer. Oceanography 33 (3), p. 50–59. Cited by: §I, §IV-B. [13] A. S. Sayed, P. Meyer, and M. Ghazel (2025) Bridging neural ODE and resnet: a formal error bound for safety verification. In International Symposium on AI Verification, p. 97–114. Cited by: §I. [14] A. S. Sayed, P. Meyer, and M. Ghazel (2025) Mixed monotonicity reachability analysis of neural ode: a trade-off between tightness and efficiency. arXiv preprint arXiv:2510.17859. Cited by: item 1. [15] A. S. Sayed, P. Meyer, and M. Ghazel (2026) TNODEV: toolbox for neural ODE verification. External Links: 2606.16567, Link Cited by: item 3, §I-B. [16] C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fergus (2014) Intriguing properties of neural networks. In International Conference on Learning Representations (ICLR), Cited by: §I. [17] H. Yan, J. Du, V. Y. F. Tan, and J. Feng (2022) On robustness of neural ordinary differential equations. External Links: 1910.05513, Link Cited by: §I, §I.