{"id":"e3d78249-4eaf-47f8-b62e-de05f47b2414","arxiv_id":"2411.14163","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"A case study shows that differentiable-logic training improves local robustness of a small path-centring network, but current verifiers fail on the regression architecture and the title's 'formally verified' claim is not achieved.","lead":"This paper describes a small experiment in which a neural network was trained to find the centre of a LEGO track from a camera image, with logical robustness constraints added to training. The authors found the constraints improved constraint satisfaction, but the verification tools they tried could not complete a formal robustness check on this regression network.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The claimed benefit of constrained training rests on training-set curves; without a held-out split or multiple seeds, the report's central positive finding is not yet supported.","rationale":"The reader's conditional verdict is appropriate. The most load-bearing part of the paper's message is the empirical comparison in §4.1: it is the only positive evidence for the differentiable-logic pipeline, and the title/abstract leverage it into a 'guarantee'. The paper never states a data split, and the curves in Fig. 5 are plausibly training metrics; Section 3.4 explains that PGD counterexamples are generated during training, so improvement on those training inputs is expected and does not demonstrate robustness on new images. Since the dataset has only 385 images and batch size 16, overfitting is a real risk. A rerun with held-out images and multiple seeds would settle this. Separately, the formal-verification portion is honestly reported as a failure, and §4.3 appropriately warns that local properties give no unseen-data guarantees; so the phrase 'verified network' in the title/abstract should be softened. My concern is not that the authors are hiding results; it is that the paper's central empirical inference is not yet grounded in the figures as presented. This overlaps with the reader's call for error bars and artifacts, but I locate the problem more specifically in the missing held-out evaluation of the constraint-accuracy claim.","tokens_in":10409,"tokens_out":6329,"duration_ms":64354,"concrete_test":"Rerun both vanilla and constrained training on the public dataset with at least 5 seeds and a fixed 80/20 stratified split, recording constraint accuracy and max output deviation for Eq. (2) on held-out images only. If the constrained model's held-out constraint accuracy and adversarial deviation are not consistently better than vanilla across seeds, the paper's empirical claim reduces to a training-set artifact.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The narrowed central claim is that Gödel-logic constraints improve constraint accuracy and adversarial robustness (§4.1). The only quantitative support is Fig. 5 (loss and constraint accuracy vs epoch) and a single adversarial image at epoch 45 (Fig. 4). No train/validation/test split is described; the dataset is 385 images (§3.2), and both runs use batch size 16. Because the constraint-loss loop generates PGD counterexamples from the training set (§3.4), a training-set curve can improve simply by overfitting to those counterexamples. Without held-out images or multiple seeds, \"constrained-training improves robustness\" is indistinguishable from \"constrained-training memorizes the training adversarial examples.\" Separately, the title and abstract claim a \"formally verified\" network, but §4.2 reports that every DNNV backend either failed or returned unknown, and NNV only produced loose intervals for one image; no tool certified Eq. (2). The honest §4.3 caveat does not repair the mismatch between those statements and the title/abstract.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper reports a case study on training a small convolutional regression network for JetBot road-following using a custom 385-image LEGO dataset, comparing standard training with training augmented by Gödel fuzzy-logic robustness constraints. It then attempts formal verification of a local robustness property using α,β-CROWN, DNNV, and NNV, and reports lessons learned. The paper claims improved constraint accuracy and adversarial robustness from constrained training, while documenting that none of the verifiers successfully certified the property: DNNV backends failed or returned unknown, and NNV produced only very loose output intervals.","tokens_in":10511,"tokens_out":4882,"duration_ms":44286,"significance":"If the claims are appropriately scoped, the experience report has value for the verification community: it documents concrete tool failures on a regression network with max-pooling and tanh layers, makes a small dataset publicly available, and provides a falsifiable negative data point about the current readiness of neural-network verifiers for this class of networks. However, the positive claim that constrained training improves robustness is not yet supported by the evidence as presented, and the title and abstract substantially overstate the degree of formal verification achieved. With revision, this can be a solid experience report; in its current form the central claims need rebalancing.","major_comments":[{"comment":"The title and abstract promise a “formally verified neural network” and describe “guaranteeing the behaviour of the neural network after training”, but the body reports that no verifier certified Eq. (2): DNNV’s BaB and Reluplex failed on unsupported computation graphs, ERAN returned unknown, nnenum returned a generic error, and NNV’s estimateNetworkOutputBounds produced intervals far too wide to certify δ=0.1 (Listing 2 and Table 2). The paper itself notes in §4.1, citing [12], that training with constraints does not guarantee their satisfaction. The title and abstract should be revised to match the experience-report outcome, for example by saying the work explores the use of differentiable logics and reports on verification attempts, rather than claiming a verified network.","section":"Abstract; §4.2"},{"comment":"The central positive finding—that constrained training improves constraint accuracy and adversarial robustness—rests on training-set loss/constraint-accuracy curves and a single adversarial image at epoch 45. No train/validation/test split is described; the dataset is 385 images (§3.2) and both runs use batch size 16. Since the PGD counterexamples used in constraint training are generated from the training set (§3.4), an improved training-set curve is compatible with the model memorizing those counterexamples rather than learning a generalizable robustness property. To support the generalization claim, the authors should evaluate on held-out images, report results over multiple seeds, or explicitly reframe the observation as training-set constraint accuracy without generalization language.","section":"§4.1; Figs. 4 and 5"},{"comment":"The robustness property Eq. (2) is presented as a “basic safety property”, but no argument connects the chosen parameters (ε=48/255, δ=0.1) or the output-coordinate deviation to the actual navigation behaviour of the JetBot, such as track width, vehicle speed, or control-loop sensitivity. Without such a connection, Eq. (2) is a local Lipschitz-style condition whose satisfaction or violation has no demonstrated safety implication. The paper itself acknowledges in §4.3 that verification is local to data points and provides no guarantees for unseen data; the property should be scoped accordingly and its status as a safety property either justified with a concrete argument or softened.","section":"§3.4; Eq. (2)"}],"minor_comments":[{"comment":"The text says NNV provides a “relatively simplier interface”; the intended word is “simpler”.","section":"§4.2"},{"comment":"The sentence “the estimateNetworkOutputBounds function does return any tighter bounds for the network’s output” appears to be missing the word “not”, since Table 2 shows the bounds are not tight enough to certify the property.","section":"§4.2; Table 2"},{"comment":"The caption “Vanilla constrained-training” should include a comma or dash to separate the two legend entries.","section":"Fig. 5 caption"},{"comment":"The claim that “the choice of a logic does not have a major impact” is based on the authors’ own preprint [10], which is listed as under review; this should be stated explicitly so readers can weigh the evidence.","section":"§1; reference [10]"},{"comment":"The paper states that α,β-CROWN was “not suitable for the verification of regression tasks without modification” but gives no detail on the modification needed; adding a sentence on the specific limitation encountered would make the observation more actionable.","section":"§4.2"}],"recommendation":"major_revision","confidential_remarks":"The paper is a workshop experience report and the topic is within scope for a formal-methods-for-autonomous-systems venue. The main concern is the mismatch between the title/abstract and the reported verification failure, together with the absence of held-out evaluation for the constrained-training benefit; both are fixable in revision. The self-citation [10] is reasonable but should be flagged as unpublished. I would not recommend rejection because the documented tool failures and the public dataset are useful contributions if the claims are rebalanced."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nIf you need a concrete data point on how poorly the current verifier ecosystem handles regression networks, this paper is useful. The authors trained a small CNN to find a track centre, then tried to verify a local robustness property with a stack of tools (DNNV backends, NNV) and nearly everything failed. That observation is legitimate and reproducible, and the writing is candid: Section 4.3 says flat out that verification was not completed and local properties give no guarantee on unseen data.\n\nWhat's new: a public 385-image LEGO road dataset and a record of verifier failures on a regression architecture with max-pooling and tanh. The lessons about tool installation and unsupported layers are worth having.\n\nThe problems are in the packaging and the one quantitative claim. The title and abstract say 'formally verified' and 'guaranteeing the behaviour', which the body contradicts. No verifier succeeded; they admit it. So the headline is wrong. The other issue is the claim that constrained training improves robustness. The only evidence is a training-set curve and one adversarial image, with no held-out split, no multiple seeds, and no error bars. Since the constraint loss uses PGD counterexamples from the training set, the improvement could be memorization. This is not enough to support the claim.\n\nAlso, only the dataset is public; the training code, weights, and verification scripts aren't released, so the 'experience' is not fully reproducible.\n\nOverall, this is a workshop-grade experience report. It deserves a serious referee because the verifier-failure data is credible and useful, but it needs heavy revision: fix the claims, add proper evaluation, and release the artifacts. I'd cite it only for the tooling gap, not for the training comparison.","headline":"An honest workshop report on why regression-network verification is hard, but the abstract oversells the result and the training benefit is not demonstrated.","tokens_in":11116,"tokens_out":3660,"would_cite":false,"duration_ms":32085,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This experience report argues that training a small path-centring regression network with differentiable-logic constraints improves its local adversarial robustness, but that none of the verifiers tried could formally verify the trained…","keywords":["neural network verification","experience report","differentiable logics","Gödel fuzzy logic","adversarial robustness","autonomous navigation","regression network","formal verification tools"],"falsifier":"A concrete observation that would settle whether the central claim is right: search a held-out dataset image $x_0$ for a perturbation $x$ with $\\|x_0 - x\\|_\\infty \\le 48/255$ that moves either output coordinate by more than $0.1$; finding one refutes the robustness property at that point, and since the paper reports no verifier could decide the property, a successful decision either way would directly test its conclusion about verification tooling.","tokens_in":10148,"feed_emoji":"🚗","tokens_out":9315,"duration_ms":83171,"temperature":0.7,"pith_summary":"The paper is an experience report from a case study on building a formally verified neural network for autonomous navigation. The authors train a small regression network to locate the track centre from camera images of a small robot car, and try to make it correct by construction by adding Gödel fuzzy-logic translations of a local robustness property as extra loss terms. They report that constrained training improves constraint accuracy and adversarial robustness compared with vanilla training, but that training with constraints does not guarantee the property holds. The verification half of the case study did not succeed: every verifier tried either crashed, returned unknown, or reported unsupported operations, mainly because the network is a regression network with max-pooling and tanh layers. A sympathetic reading is that the paper establishes the promise of differentiable-logic training and the current gap in verification tooling for such networks.","feed_headline":"No verifier could prove this robot-car network safe","feed_subtitle":"Logic-based training improved robustness, but every verifier tried failed on the regression network.","key_machinery":"The load-bearing mechanism is the translation of the robustness constraint into a differentiable loss term using Gödel fuzzy logic, with conjunction as min, disjunction as max, and implication $x \\to y$ as 1 if $x < y$ else $y$; a projected-gradient-descent search inside the $\\epsilon$-ball supplies a worst-case counterexample for the constraint, and adaptive loss balancing weighs the logical loss against the mean-squared-error loss. This turns the verification property into an extra training objective, so the network is pushed toward satisfying it during learning. The second half of the machinery is the network architecture itself: a small convolutional regression net with max-pooling and a final tanh layer, chosen for tractability but precisely the features that make post-training verification fail.","core_discovery":"The central claim, stated on the paper's own terms, is that the loop of differentiable-logic training followed by formal verification is a plausible pipeline for safety properties in autonomous navigation, and that the bottleneck is tooling, not the training idea. Concretely, they show that adding the constraint $\\forall x.\\ \\|x_0 - x\\|_\\infty \\le \\epsilon \\Rightarrow \\|N(x_0) - N(x)\\|_\\infty \\le \\delta$ as a Gödel fuzzy-logic loss term, with $\\epsilon = 48/255$ and $\\delta = 0.1$, raises constraint accuracy and adversarial robustness relative to vanilla training. They do not claim the constrained network is verified; in fact they report that one verifier was unsuitable for regression tasks, and through a unified verifier interface the attempted verifiers all failed or returned unknown, while a bound-estimation toolbox produced wide, unhelpful intervals. The discovery is an experience-level one: verification tools currently support classification networks with ReLU activations but not regression networks containing max-pooling and tanh, and verification remains local to data points, giving no guarantees on unseen images.","pith_inferences":["The report leaves implicit that swapping max-pooling for strided convolutions and the tanh output for a piecewise-linear activation would likely bring the architecture into the fragment current verifiers support; re-running the same experiment on that architecture is a direct test of this reading.","A stronger safety case would replace the pointwise local robustness property with a global Lipschitz bound over the set of images the car can actually encounter, addressing the paper's own caveat that local checks give no guarantees on unseen data.","Because the constrained training uses adversarial examples only for the constraint loss and not for the mean-squared-error term, a head-to-head comparison with ordinary adversarial training on the same network would isolate whether the logic-based loss is what drives the robustness gain."],"forward_implications":["Training with differentiable-logic robustness constraints, as implemented here, improves constraint accuracy and adversarial robustness relative to standard training on the same data.","Adding constraints during training does not by itself guarantee that the network satisfies them after training, so a separate verification step remains necessary.","For regression networks with max-pooling and tanh layers, currently available verifiers do not produce a verification result; they error out or return unknown, so verification-friendly architectures are a prerequisite.","Formal verification of such networks is local to input data points; it does not provide guarantees on unseen images, limiting the safety case for real deployment.","The estimated output bounds from the bound-estimation tool were too wide to certify robustness even at small perturbations."],"supporting_citations":[{"why":"defines the local robustness property that the paper adopts as Eq. (2) and later tries to verify.","marker":"[5]"},{"why":"introduces the differentiable-logic approach of turning logical constraints into extra loss terms, which the constrained training is built on.","marker":"[9]"},{"why":"supplies the training code and prior differentiable-logic comparison that the paper's constrained-training runs reuse.","marker":"[10]"},{"why":"backs the paper's statement that training with constraints does not guarantee their satisfaction, motivating the verification attempt.","marker":"[12]"},{"why":"provides the projected-gradient-descent method used to find worst-case counterexamples of the constraint during training.","marker":"[22]"},{"why":"provides the unified verifier interface through which the paper attempts post-training verification and records the failures.","marker":"[30]"},{"why":"provides the bound-estimation toolbox whose wide output intervals are reported against input perturbations.","marker":"[40]"},{"why":"supports the explanation that max-pooling layers are too complicated for current verifiers, explaining the failures.","marker":"[39]"}],"fun_headline_variants":["Verifiers fail on robot-car network, but logic training helps","Logic-based training passes, but no verifier proves the robot-car net","Robot-car neural net: logic training improves robustness, verification fails","No verifier can prove this autonomous navigation net safe, but logic training helps"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the local robustness property used in Eq. (2)—keeping the predicted track centre within $\\delta = 0.1$ output units for any input perturbation of at most $\\epsilon = 48/255$—is a meaningful safety condition for keeping the robot on the track, and that local checks on data points transfer to real operation.","fun_headline_variants_meta":{"raw":{"variants":["Verifiers fail on robot-car network, but logic training helps","Logic-based training passes, but no verifier proves the robot-car net","Robot-car neural net: logic training improves robustness, verification fails","No verifier can prove this autonomous navigation net safe, but logic training helps"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000739,"raw_usage":{"total_tokens":3261,"prompt_tokens":864,"completion_tokens":2397,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":480,"completion_tokens_details":{"reasoning_tokens":2321}},"tokens_in":480,"tokens_out":2397,"duration_ms":15368,"temperature":1.0,"reasoning_tokens":2321,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:27:18.185100+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A concrete observation that would settle whether the central claim is right: search a held-out dataset image $x_0$ for a perturbation $x$ with $\\|x_0 - x\\|_\\infty \\le 48/255$ that moves either output coordinate by more than $0.1$; finding one refutes the robustness property at that point, and since the paper reports no verifier could decide the property, a successful decision either way would directly test its conclusion about verification tooling.","supporting_citations":[{"cited_title":"In: Proceedings of the 36th International Conference on Machine Learning, PMLR, pp","cited_arxiv_id":null,"evidence_quote":"introduces the differentiable-logic approach of turning logical constraints into extra loss terms, which the constrained training is built on."},{"cited_title":"In: International Conference on Learning Representations","cited_arxiv_id":null,"evidence_quote":"provides the projected-gradient-descent method used to find worst-case counterexamples of the constraint during training."}],"review_version":1}