{"id":"78acd5b7-da75-4fdc-814d-ca447869fe46","arxiv_id":"2505.00622","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A case study shows that combining Marabou/Vehicle with CORA can partially verify neural-network controllers for Alsomitra-inspired gliders, but practical guarantees remain out of reach.","lead":"Researchers tested two families of neural-network verification tools on a new problem: keeping a seed-shaped gliding drone close to a target trajectory. They found the tools can partially verify such controllers, but the guarantees are too weak for real use and robustness training helped only in some settings.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The claimed benefit of adversarial training is not established: verification comparisons lack a regression-matched control, so the paper's central empirical claim is unsupported as presented.","rationale":"Reader's verdict of CONDITIONAL matches my read. The most load-bearing weak point is not external model fidelity but the internal comparison: the paper's only quantitative evidence for the proposed training method is a comparison of two networks that are not controlled for regression accuracy. The paper acknowledges this in Section 9.1 but does not repair it. Because the headline claim in the abstract is that 'training methods do improve performance and robustness,' a confounded comparison is directly relevant. The model-fidelity question, while important, applies equally to every verification case study built on simulation and would not change the paper's main tool-integration lessons; the regression confound, however, invalidates the reported success of the proposed method if it lands. The reader explicitly noted the confound in the rationale, so agreement is partial: we differ on which is the weakest assumption. I therefore keep the CONDITIONAL verdict, with the condition made explicit: add a regression-matched control and report held-out test robustness before claiming improvement.","tokens_in":14954,"tokens_out":6304,"duration_ms":59667,"concrete_test":"Train, say, five naive and five adversarially trained networks from the same initializations with identical architecture, data, and epoch counts; compute held-out RMSE and R2 on a test split. Select one naive and one adversarial network whose held-out R2 is statistically indistinguishable (or, to be conservative, where the naive network has higher R2). Re-run Property 1 (Table 1) and the CORA reachability experiment (Fig. 7) on this matched pair. If the y* improvement and reachability success persist, the concern is resolved. If they vanish, the central claim must be weakened to 'adversarial training changes verification behavior,' with no demonstrated advantage.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing evidence for the central claim is the comparison between 'naive' and 'adversarially trained' controllers in Table 1 and Fig. 7. The two networks are not matched on regression quality. Section 9.1 concedes: 'A better comparison could be made using NNs with equivalent regression performance on a test set of data, using a coefficient such as R2.' Without a held-out RMSE/R2 report, the Property 1 improvement (y* from 46 to 30) and the CORA reachability success could simply reflect that the adversarial network is a better fit to the PID training data, not that Lipschitz-regularized training improves verifiable robustness. The other results do not remove the confound: Property 2 is unchanged, Property 3 fails for all networks, Property 4 is 0 for all, and Property 5 is evaluated only on training data (§7.2), where the adversarial network is worse than the naive network for (epsilon, L*) = (0.01, 1e-5) and (0.01, 1e-4) in Table 2. Since the abstract's claim that 'training methods do improve performance and robustness' rests on exactly these comparisons, the central empirical claim is not yet supported. The reader's model-fidelity concern is real but secondary: if the simplified quasi-steady model is unvalidated, the verified properties describe a simulation, but the tool-integration and benchmark lessons could still hold; the regression confound, by contrast, directly undermines the reported success of the paper's proposed training method.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a verification case study for a centimetre-scale Alsomitra-inspired gliding drone controlled by a neural network. The authors formulate an ideal safety/adherence property (following a linear target trajectory), then distill it into properties expressible in Vehicle/Marabou and CORA. They propose a regression adaptation of PGD-based adversarial training with a dynamic Lipschitz penalty, and compare a 'naive' network with an adversarially trained network and with property-driven-trained networks from a companion paper. The reported results are mixed: one global property improves under adversarial training (Property 1, y* from 46 to 30), another is unchanged, one fails for all networks, one is trivially easy, and a local robustness property is evaluated only on training data. The CORA reachability experiment shows the adversarial network reaching the goal region while the naive network does not. The paper concludes that a combination of existing tools and the proposed training methods could support this class of benchmarks once tool limitations are overcome.","tokens_in":15243,"tokens_out":7874,"duration_ms":76917,"significance":"If the claims are sustained, the paper provides a useful first end-to-end verification benchmark for a regression-controlled bio-inspired glider, with transferable lessons about normalization, relational properties, and reachability set explosion. The paper is commendably candid about tool shortcomings and about its own limitations, and the public release of verification artifacts is a strength. The main empirical claim about adversarial training improving performance and robustness is, however, not established by the data as presented: the comparison is confounded by differences in regression quality, and the local robustness property is evaluated on training data. The case-study and tool-integration contributions are worthwhile, but the central empirical conclusion needs either re-supporting or substantial weakening.","major_comments":[{"comment":"The central comparison between the naive and adversarially trained networks is not matched on regression quality. Section 9.1 explicitly concedes that 'A better comparison could be made using NNs with equivalent regression performance on a test set of data, using a coefficient such as R2.' The reported improvements — Property 1 y* from 46 to 30 in Table 1 and the CORA reachability success in Fig. 7 — are therefore compatible with the alternative explanation that the adversarial network is simply a better regressor on the training distribution. This is load-bearing because the abstract states that the investigated training methods improve performance and robustness. Please report held-out RMSE and R^2 for every network used in Tables 1-2 and Fig. 7, and either re-run the verification with regression-matched networks or explicitly restrict the claim to 'the tested networks were verified at least as well under the chosen properties.'","section":"Sects. 7.3, 8.2, 9.1; Tables 1-2, Fig. 7"},{"comment":"Property 5 is evaluated only with respect to the training dataset, which is the same data used to train both networks. Robustness measured on training points can reflect memorization rather than generalizable robustness, so the statement in Section 7.3 that 'Table 2 shows a marginal improvement in robustness performance' is not supported for unseen states. In addition, the naive network timed out for the epsilon=0.01 cells, so the adversarial network's 0% and 13.6% success rates in those cells have no naive baseline. Please re-evaluate Property 5 on a held-out test set, or at a minimum report the timeouts symmetrically and avoid interpreting cells that have no baseline as evidence of improvement or regression.","section":"Sect. 7.2, Eq. (25), Table 2"},{"comment":"The dynamics used throughout are a simplification of the falling-plate model: Eq. (1) replaces tan alpha by x2/x1, and Section 3.2 constrains the angle of attack to [-pi/2,0]. The paper gives no quantitative validation that this simplified plant preserves the trajectories of the original model [24] or of real Alsomitra seeds. Since every verified property and reachable set in Sects. 7-8 concerns this simplified plant, the verification results are about a simulation model, not the physical drone; the title, abstract, and contributions should be adjusted accordingly. A concrete fix is to bound the error |tan alpha - x2/x1| over the reachable state space and to state explicitly that the case study certifies the simplified model, with the fidelity of that model listed as an assumption rather than an established fact.","section":"Sect. 3.2, Eq. (1), Table 3 (Appendix)"},{"comment":"Property 4 is reported as y*=0 for every network. With the premise -x5 <= x6 <= -x5 + y*, setting y*=0 restricts the antecedent to a single line x6=-x5, which may be an empty or measure-zero subset of the valid input space, making the property vacuously true or trivially easy. The text says Property 4 'succeeded for all y* values' but does not discuss satisfiability of the antecedent. Please report whether the premise is satisfiable for each y*, and if the success is vacuous, remove or reframe the property so that Table 1 is not read as evidence of good behaviour.","section":"Sect. 7.1, Property 4, Table 1"}],"minor_comments":[{"comment":"The displayed formula contains (2y1+1)^4 ± (2y1+1)^4, which would make the two terms identical; the appendix version uses (2ℓCM/ℓ+1)^4 ± (2ℓCM/ℓ−1)^4, so the main-text equation is missing the sign change in the second factor. Please correct.","section":"Eq. (10)"},{"comment":"The roles of epsilon rows and L* columns are not explicitly labeled in the table body; add a header such as 'epsilon \\ L*' so that the orientation is unambiguous.","section":"Table 2"},{"comment":"Report quantitative bounds of the reachable sets (for example, the maximal |x6+x5| over the final reachable set) rather than only the plot, so the reader can assess how close the adversarial controller comes to the target trajectory.","section":"Fig. 7"},{"comment":"The DL2 and Gödel Logic PDT networks are not described in this paper and Section 9.1 notes differences in network structure; state their training hyperparameters and architecture or omit them from Tables 1 if they are not directly comparable.","section":"Sect. 6 and Sect. 9.1"},{"comment":"The text says 'All relevant files are publicly available here' but no URL appears in the manuscript; add the repository link for reproducibility.","section":"Sect. 1.1"},{"comment":"The expression 'x ! i - x ! i + 6' is confusing; clarify that the network is doubled in onnx format and that indices 0-5 and 6-11 correspond to the same six states, so that the perturbation bound is expressed in the doubled-index representation.","section":"Listing 3"}],"recommendation":"major_revision","confidential_remarks":"The paper is a useful case-study report and the tool-engineering lessons are likely to be of interest to the verification community. The regression confound identified in Section 9.1 is the main obstacle: it directly undermines the abstract's claim that the training methods improve performance and robustness. The fix — adding regression-matched baselines or materially weakening the claim — is within the scope of a revision, so I do not recommend rejection. The model-fidelity issue is secondary but should nonetheless be acknowledged more prominently in the revised framing."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. First, the paper gives the verification community something it doesn't have: an end-to-end case study of a bio-inspired glider controller, with relational safety properties, regression rather than classification networks, and a documented list of tool shortcomings (normalization, relational property support, reachability set explosion). That part is real and useful. Second, the headline empirical claim — that the proposed Lipschitz-PGD adversarial training improves performance and robustness — is not actually established by the evidence as presented. The comparison between the naive and adversarial networks is not matched for regression quality; the paper itself concedes in Section 9.1 that a proper comparison would need NNs with equivalent regression performance on a test set using R2. Without that, the Property 1 improvement (y* from 46 to 30) and the CORA reachability success in Fig. 7 could just reflect that the adversarially trained net is a better fit to the PID data. Table 2 is mixed: for (epsilon, L*) = (0.01, 1e-5) and (0.01, 1e-4) the adversarial net is worse than the naive one. So the abstract's 'training methods do improve performance and robustness' is a step beyond what the paper supports.\n\nWhat the paper does well: it is honest about its own limitations, documents the workarounds in detail (doubling the ONNX network for relational properties, splitting initial sets in CORA, adding normalization layers), and positions the case study as a challenge for future tools rather than claiming victory. The relational property formalizations and the regression adaptation of PGD are worth building on. The data and code are supposed to be public, though I could not find a working repository link in the text — that should be fixed.\n\nThe soft spots are proportionate to the claims. The model-fidelity issue (quasi-steady falling plate, angle-of-attack approximation, no wind-tunnel validation) means the verified properties are about a simulation, not the physical drone. That is not fatal for a benchmark paper, but the authors should be explicit that this is the case. The bigger issue is the regression confound, which is recognized but not addressed. Property 5 is evaluated on training data, so it tells you about in-sample robustness, not generalization. Timers and empty cells in Table 2 suggest scalability limitations that are discussed.\n\nWho is this for? Verification researchers and tool developers, especially those working on VNN-COMP/ARCH-COMP style benchmarks. They will get useful lessons even if the central empirical claim is weak.\n\nMy recommendation: send it to peer review, not desk reject. It deserves a serious referee. The referee should ask for a regression-matched control (or at least RMSE/R2 on a held-out set), a working public repo link, and a toned-down abstract/claim. After that, it's a useful benchmark case study.","headline":"A genuinely useful new benchmark case study with an unsupported headline claim about adversarial training; deserves peer review and a regression-matched control.","tokens_in":15837,"tokens_out":2520,"would_cite":true,"duration_ms":24273,"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":"This paper shows that existing verification tools, combined with a new regression-specific adversarial-training method, can verify trajectory-adherence properties of an Alsomitra-inspired glider controller, yet the verified guarantees…","keywords":["neural network verification","reachability analysis","adversarial training","regression control","gliding microdrone","Alsomitra","Lipschitz robustness","closed-loop control"],"falsifier":"Compare the verified envelopes against wind-tunnel or free-flight measurements of an Alsomitra-inspired glider using the same controller: record the actual deviation from the target trajectory $x_6 = -x_5$ over 20 seconds. If real trajectories exceed the verified $y^*$ values or fail to reach the CORA goal region from the initial set $x_1=1, x_2=0, x_3=0, x_4=0, x_5=0, x_6\\in[1.43,4.29]$, then the claim that these properties apply to the physical drone is falsified; a cheaper check is to integrate the full unsimplified dynamics model and compare against the simplified equations used for verification.","tokens_in":14724,"feed_emoji":"🛩️","tokens_out":7421,"duration_ms":71619,"temperature":0.7,"pith_summary":"This paper argues that existing neural-network verification tools, combined with a new adversarial training scheme for regression networks, can verify safety-relevant properties of an Alsomitra-inspired gliding-drone controller, but only within a tightly constrained envelope. The drone is modelled as a falling plate with a displaced centre of mass, and the controller is a small ReLU network trained by behaviour cloning to follow a linear trajectory. The authors reduce an ideal infinite-horizon specification to five static properties checked with one verifier and a finite-horizon reachability property checked with another. Their central positive result is that adversarially trained controllers satisfy the first global property with $y^* = 30$ instead of $y^* = 46$, and reach the goal corridor after 20 seconds when the naive controller does not, while the verified guarantees remain too coarse for practical use.","feed_headline":"Adversarial training narrows verified glider error from y*=46 to 30","feed_subtitle":"Property checks and reachability show the trained controller reaches the goal corridor in 20 seconds, with clear limits.","key_machinery":"The load-bearing object is the quasi-steady aerodynamic model of a falling plate with a displaced centre of mass, taken from the literature and simplified for tractability by replacing $\\tan\\alpha$ with $x_2/x_1$ and constraining the pitch angle so that reachability computations can run. The second mechanism is the closed-loop controller: a $6\\times 6 \\times 4 \\times 1$ ReLU network, trained on PID-generated regression data, whose single output actuates the centre-of-mass displacement. The third mechanism is adversarial training for regression: PGD with an RMSE loss augmented by a dynamically computed Lipschitz penalty that penalises large output-to-input gradient ratios. The argument is carried by pairing these trained networks with two verification pipelines: relational, regression-oriented properties in Vehicle/Marabou, and zonotope-based reachability in CORA, where a zonotope is a convex set representation that over-approximates all states reachable under the dynamics.","core_discovery":"On the paper's own terms, the discovery is that this class of benchmarks — continuous regression control with complex nonlinear dynamics — is not yet directly verifiable, but a pragmatic pipeline can be assembled from existing tools. The ideal property, that the drone always stays within distance $y^*$ of the target line $x_6 = -x_5$ after some time, is split into two tasks: Vehicle/Marabou checks that the controller never commands a large deviation under relational constraints on the input state, and CORA checks that all trajectories from a small initial interval reach a goal region around the line within 20 seconds. Adversarial training using projected gradient descent with an RMSE loss augmented by a Lipschitz penalty yields networks that pass stricter versions of those properties than naively trained networks. The authors are explicit that the verified $y^*$ values are too large and the reachable initial sets too small for the guarantees to be immediately useful; the contribution is the first end-to-end demonstration that the tools can be adapted to this problem class, plus a catalogue of what must change.","pith_inferences":["Editorial inference: the regression adversarial-training scheme is plant-agnostic and should transfer directly to other passively falling or gliding microflyers, such as dandelion-inspired designs, provided their dynamics can be written as a tractable model.","Editorial inference: a sharper test of the robustness claim would compare naive and adversarial networks matched on regression accuracy ($R^2$), since the paper notes the reachability gap could partly reflect regression performance rather than robustness alone.","Editorial inference: if validation data ever confirm the simplified aerodynamics, the same pipeline would turn these coarse envelopes into flight-relevant guarantees; until then, the paper's transferable contribution is the catalogue of tool gaps: normalisation, relational properties, multi-network queries, and derivative complexity."],"forward_implications":["Verifying a continuous regression controller in practice today means splitting the ideal property: static relational checks on the network plus finite-horizon reachability on the closed loop.","Adversarial training with a Lipschitz penalty improves the verification outcome on the first trajectory-adherence property, with $y^*$ dropping from 46 to 30, and lets the adversarial controller reach the goal corridor in 20 seconds where the naive controller does not.","The guarantees obtained are not yet deployment-grade: the verified $y^*$ values are large and the reachable initial sets are zero-width in five dimensions, so this is a proof of principle rather than a certification.","Tool development priorities follow directly from the case study: native input normalisation, relational properties that name multiple network outputs, support for multiple network calls, and cheaper Jacobian and Hessian approximations for reachability.","Regression-focused robustness training generalises the usual classification-oriented property-driven training, so the same scheme can be applied to other regression control tasks with nonlinear closed-loop dynamics."],"supporting_citations":[{"why":"Supplies the falling-plate dynamics with a displaced centre of mass that define the drone plant.","marker":"[24]"},{"why":"Is the SMT verifier used to check the static relational properties on the controller.","marker":"[20]"},{"why":"Is the specification language used to encode properties 1-5 in a form the verifier can read.","marker":"[10]"},{"why":"Provides CORA's zonotope reachability machinery used for the 20-second goal-region property.","marker":"[2]"},{"why":"Defines standard and Lipschitz robustness and supplies the theoretical basis for the adversarial regression loss.","marker":"[6]"},{"why":"Defines the benchmark whose initial-set and goal-region structure the CORA specification follows.","marker":"[25]"},{"why":"Is the competition context that motivates the reachability formalisation and comparison.","marker":"[15]"},{"why":"Is the benchmark context that motivates the static-property formalisation and comparison.","marker":"[5]"}],"fun_headline_variants":["Neural glider controller verified via hybrid VNN pipeline","Adversarial training boosts verifiable robustness in glider drones","Verifying NN glider control: Vehicle and CORA team up","Case study shows VNN tools can verify drone controllers—with limits","Gliding drone NN verification: pipeline works, guarantees still small"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The verification results concern the simplified quasi-steady aerodynamic equations, so if those equations do not faithfully represent a real Alsomitra-inspired drone — and no wind-tunnel or field validation is given — every verified property is only about a simulation rather than the drone.","fun_headline_variants_meta":{"raw":{"variants":["Neural glider controller verified via hybrid VNN pipeline","Adversarial training boosts verifiable robustness in glider drones","Verifying NN glider control: Vehicle and CORA team up","Case study shows VNN tools can verify drone controllers—with limits","Gliding drone NN verification: pipeline works, guarantees still small"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000377,"raw_usage":{"total_tokens":2045,"prompt_tokens":1023,"completion_tokens":1022,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":639,"completion_tokens_details":{"reasoning_tokens":935}},"tokens_in":639,"tokens_out":1022,"duration_ms":11407,"temperature":1.0,"reasoning_tokens":935,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T04:37:56.937565+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compare the verified envelopes against wind-tunnel or free-flight measurements of an Alsomitra-inspired glider using the same controller: record the actual deviation from the target trajectory $x_6 = -x_5$ over 20 seconds. If real trajectories exceed the verified $y^*$ values or fail to reach the CORA goal region from the initial set $x_1=1, x_2=0, x_3=0, x_4=0, x_5=0, x_6\\in[1.43,4.29]$, then the claim that these properties apply to the physical drone is falsified; a cheaper check is to integrate the full unsimplified dynamics model and compare against the simplified equations used for verification.","supporting_citations":[{"cited_title":"443– 452 (2019)","cited_arxiv_id":null,"evidence_quote":"Is the SMT verifier used to check the static relational properties on the controller."},{"cited_title":"github.io/tutorial/","cited_arxiv_id":null,"evidence_quote":"Is the specification language used to encode properties 1-5 in a form the verifier can read."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides CORA's zonotope reachability machinery used for the 20-second goal-region property."},{"cited_title":"Computer Aided Verification pp","cited_arxiv_id":null,"evidence_quote":"Defines standard and Lipschitz robustness and supplies the theoretical basis for the adversarial regression loss."},{"cited_title":"EPiC Series in Computing103, 64–121 (2024),https://easychair.org/ publications/paper/WsgX","cited_arxiv_id":null,"evidence_quote":"Defines the benchmark whose initial-set and goal-region structure the CORA specification follows."},{"cited_title":"workshop on applied verification for continuous and hybrid systems","cited_arxiv_id":null,"evidence_quote":"Is the competition context that motivates the reachability formalisation and comparison."}],"review_version":1}