{"id":"02dcee14-e61d-4ac0-bc1b-e95a88265bb6","arxiv_id":"2412.13229","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A neuron behavior consistency loss reduces the number of unstable neurons and speeds up formal verification of trained networks across MNIST, Fashion-MNIST, and CIFAR-10.","lead":"Neural network checkers are slow because they must consider every neuron switching on or off. This paper adds a training penalty, neuron behavior consistency, that keeps neuron states stable around a perturbation, and reports faster formal verification on standard image datasets while preserving accuracy.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Cosine-similarity surrogate may not track per-neuron sign instability, leaving the NBC-to-unstable-neuron link unproven; CONDITIONAL verdict stands.","rationale":"The reader's weakest_assumption identifies the same load-bearing concern: the continuous NBC objective at a single adversarial point is an unproven proxy for discrete neuron activation consistency over the whole epsilon-neighborhood. My stress-test sharpens this with a concrete mathematical point: cosine similarity is a global vector alignment, so it provides weak per-neuron gradient signal for sign flips, which are exactly what determine unstable-neuron counts in branch-and-bound verification. The 10-step PGD inner maximization further weakens the min-over-neighborhood approximation, especially for CIFAR-10's high-dimensional inputs. The paper's own conclusion admits the mathematical machinery is not explained, and no correlation analysis between the loss and the verifier's Stable% is provided. These gaps do not refute the empirical results, but they do mean the central causal claim is not established; the evidence is consistent with the method being an implicit regularizer rather than a targeted stabilizer. This matches the reader's CONDITIONAL verdict: the mechanism needs verification, and the empirical claims need corroboration (e.g., code, multiple seeds, larger verification sets). I therefore recommend no change to the reader's verdict. The abstract's overclaim about maintaining verifiability at large radii is a secondary concern already noted by the reader; it does not alter the verdict.","tokens_in":24148,"tokens_out":7263,"duration_ms":71245,"concrete_test":"Train a small network (e.g., M1) with NBC and, at several checkpoints, compute for a fixed test set (a) the NBC loss value and (b) the verifier-computed Stable% (or number of unstable neurons) from alpha,beta-CROWN's initial bounds. Compute the Spearman correlation across checkpoints and across beta values (Table 11 style). If the correlation is weak or negative, the objective is not a faithful proxy for the claimed mechanism. Additionally, train the same architecture with a per-neuron sign-consistency surrogate (e.g., sum of Hinge penalties on pre-activation sign mismatches between x and x') and compare Stable% and TimeU+T; if the surrogate substantially outperforms cosine similarity, the original surrogate is mis-specified and the mechanism is not supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that minimizing the NBC loss reduces unstable neurons and thus speeds up verification. The link is mediated by Algorithm 1's continuous surrogate: cosine similarity of pre-activation vectors plus output KL, evaluated only at a single PGD-found adversarial point per sample (Algorithm 2). Two load-bearing gaps: (i) Cosine similarity is a global alignment measure, not a per-neuron sign-agreement measure; a single hidden neuron sign flip in a layer of m neurons changes cosine similarity by only ~2/m, so the gradient signal for exactly the quantity that determines branch-and-bound branching (unstable neuron count) is weak and indirect. (ii) The min over x' in Eq. (5) is approximated by 10 PGD steps with step epsilon/10, which for high-dimensional CIFAR-10 inputs is unlikely to locate the worst-case inconsistency; the regularizer may fit to easy directions rather than the actual unstable-neuron set at verification time. The paper provides no correlation evidence between the continuous single-point surrogate and the verifier's discrete unstable-neuron count, and the conclusion explicitly defers 'the underlying mathematical machinery' to future work. Without that link, the empirical Stable% gains and speedups, even if reproducible, do not establish the proposed causal mechanism.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes Neuron Behavior Consistency (NBC), a regularization method for training ReLU networks so that neuron activation states are consistent across an input neighborhood. The method combines a cosine-similarity term on hidden-layer pre-activations with a KL term on the output, and the regularizer is evaluated at an adversarial point found by a short PGD run. The authors claim that minimizing this continuous surrogate reduces the number of unstable neurons, tightens neuron bounds, and thereby speeds up branch-and-bound verification while preserving accuracy. The evaluation covers MNIST, Fashion-MNIST, and CIFAR-10 with multiple architectures, comparing against ReLU Stable, TRADES, and Madry adversarial training, and also studies combinations with those baselines. The paper reports higher stable-neuron ratios, higher verified (UNSAT) rates, and lower verification times for NBC-trained networks at moderate radii, with some trade-offs in test accuracy.","tokens_in":24364,"tokens_out":5955,"duration_ms":56544,"significance":"If the empirical claims hold, the paper addresses a practical bottleneck in neural network verification: the exponential branching caused by unstable ReLU neurons. A training regularizer that requires no bound computation and is easy to implement could be a useful tool for verification-friendly training, and the paper's systematic comparison across three datasets and multiple architectures is a strength. The method is also shown to combine with existing adversarial training methods to improve verified rates on larger networks, which is practically relevant. However, the paper's contribution is weakened by a mismatch between the discrete mechanism it invokes (per-neuron sign consistency) and the continuous surrogate it actually optimizes (layer-wise cosine similarity plus output KL), a gap the authors explicitly defer to future work. The empirical results are extensive and internally consistent, but without a demonstrated link between the surrogate and the verifier's unstable-neuron count, the causal explanation of the speedups remains unsubstantiated. The accuracy drops on CIFAR-10 also complicate the claim that the method preserves accuracy.","major_comments":[{"comment":"The centrally claimed mechanism is that minimizing the worst-case NBC over the whole l-infinity neighborhood reduces unstable neurons. However, the minimization in Eq. (5) is only approximated by 10 PGD steps from a single random start (Algorithm 2). For high-dimensional inputs such as CIFAR-10, 10 steps of size epsilon/10 are unlikely to locate the true worst-case inconsistency, so the actual training objective may not be the one stated. This is load-bearing because the reported stable-neuron improvements are attributed to this min-max formulation. The paper should provide evidence that the PGD approximation is adequate, for example by comparing with more PGD steps, multiple restarts, or verifier-computed worst-case points on a subset of tasks, or by reformulating the claim to match the actual computed loss.","section":"Section 3, Eq. (5) and Algorithm 2"},{"comment":"The continuous surrogate in Algorithm 1 computes a cosine similarity between the full pre-activation vectors of each hidden layer. This is a global alignment measure, not a per-neuron sign-agreement measure. A single neuron sign flip in a layer of m neurons changes the cosine similarity by O(1/m) when other activations are unchanged, so the gradient signal for the discrete quantity in Eq. (3) is weak and indirect. The paper does not report any correlation between the continuous NBC value at training time and the verifier's per-neuron unstable-neuron count or the reported Stable% metric. Without such evidence, the claim that minimizing the surrogate reduces unstable neurons is not established. Please add a correlation analysis (e.g., scatter plots or rank correlation between the surrogate and Stable% over checkpoints or models) or replace the surrogate with a per-neuron sign-based penalty to substantiate the mechanism.","section":"Section 3, Algorithm 1"},{"comment":"The abstract and introduction claim that NBC training yields networks that are 'relatively accurate' and preserve accuracy, but the default-training results on CIFAR-10 show substantial accuracy losses. For example, in Table 5, on C2 the NBC model reaches 54.9% test accuracy versus 69.5% for Madry, and on C3 it reaches 64.9% versus 75.5% for Madry. These gaps (about 10-15 percentage points) are not 'comparable' in the usual sense. The RQ3 experiment partially addresses this by matching accuracy ranges, but that experiment uses a different training regime (fine-tuning a pre-trained natural model). Please clarify the conditions under which the accuracy-comparability claim holds, or revise the claim to state that the method trades accuracy for verifiability, with the magnitude of the trade-off depending on the model. This affects the overall 'verification-friendly' contribution as stated.","section":"Section 4, Table 5 (CIFAR-10)"}],"minor_comments":[{"comment":"The sentence after Eq. (4) says 'ε is a hyperparameter that controls the importance of the regularization term,' but the regularization weight in Eq. (4) is β, while ε is the perturbation radius. This is confusing and should be corrected.","section":"Section 3, Eq. (4) and surrounding text"},{"comment":"The paper states that hyperparameter details are in 'supplementary material (Liu et al. 2024b)', where Liu et al. 2024b is the arXiv identifier of this same paper. This self-reference is circular and should be replaced by a separate appendix or a clearly distinct supplementary document.","section":"References and supplementary material"},{"comment":"The training description says 'the same number of training iterations for all datasets, which is 400 iterations,' while the main paper consistently says 400 epochs. Please reconcile the terminology.","section":"Supplementary Material, Detailed Experimental Setup"},{"comment":"The delta rows (e.g., Test Acc. -0.1, -3.9) mix absolute percentage-point changes and relative changes without explicit units. Specifying the units in each caption would improve interpretability.","section":"Tables 2, 6, 7"},{"comment":"The sentence 'we select k images from each of the 10 categories' is ambiguous: is k the number per category or the total number? Given the later values k=100 and k=20, please state explicitly whether these are per-class counts or totals, and report the total number of verification properties used for each dataset.","section":"Section 4, Experimental Setup"},{"comment":"The phrase 'other tools fail to maintain verifiability as the radius increases' refers to other training methods, not verification tools. Please rephrase to avoid confusing the reader.","section":"Abstract and Introduction"},{"comment":"The normalization in Figure 2 (best value set to 100, others scaled proportionally) makes it difficult to judge absolute differences; consider reporting raw values alongside the normalized ones, or using a more standard visualization.","section":"Evaluation, Figure 2"}],"recommendation":"major_revision","confidential_remarks":"The experimental study is extensive and the reported improvements are consistent across datasets, which suggests the method is worth further investigation. The main weakness is the gap between the continuous surrogate and the discrete neuron-stability measure; a correlation analysis between the training-time surrogate and verifier-computed instability would substantially strengthen the causal claim. The accuracy trade-offs on CIFAR-10 should also be presented more candidly. The self-citation to the paper's own arXiv ID as 'supplementary material' is unusual and should be fixed during revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The useful news first: this paper gives the verifiable-AI community a simple, cheap training trick that seems to work. Neuron Behavior Consistency (NBC) adds a cosine-similarity regularizer on hidden-layer pre-activations plus a KL term on the output, evaluated at a PGD-found neighbor, and the experiments show large, consistent gains in stable-neuron ratio and verification time across MNIST, Fashion-MNIST, and CIFAR-10, over several architectures and radii. The gains are not marginal: at large radii where baselines have near-zero stable neurons, NBC keeps 40–80%, and verification time drops by multiples. It also composes cleanly with TRADES, Madry, and ReLU Stable, which is practically useful. The idea is genuinely new relative to ReLU Stable, since it avoids interval bound propagation entirely and uses an adversarial objective instead of a bound-based one. That is a real simplification and worth knowing about.\n\nThe soft spots are real but not disqualifying. The mechanism is asserted more than shown. Minimizing the cosine similarity between whole pre-activation vectors is not the same as minimizing per-neuron sign flips, and the paper does not demonstrate that the continuous surrogate tracks the verifier's discrete unstable-neuron count. The authors themselves defer the mathematical machinery to future work, which is honest but leaves the central causal claim open. Relatedly, the inner minimization is a single 10-step PGD attack, so the regularizer sees one adversarial direction per sample rather than the whole neighborhood. It still works empirically, but the reader cannot tell whether the effect comes from the intended sign-stabilization mechanism or from a blunter side effect like pushing pre-activations away from zero.\n\nThere is also a mild overclaim in the abstract: NBC does not maintain verifiability at the largest radii on the biggest models either; it times out, just less badly than the alternatives. The claims should say \"degrades more gracefully\" rather than \"maintains.\" Minor issues: no code is provided, the SABR comparison uses only 50 verification tasks, and hyperparameters are chosen on a validation set, which is acceptable but means the headline numbers are not fully parameter-free.\n\nMy take: this is a solid empirical paper with an intriguing but unproven mechanism. It deserves a serious referee, not a desk reject. I would ask for one additional experiment correlating the NBC loss with verifier-measured unstable-neuron counts, a clearer statement of where the method still times out, and ideally code. The paper is aimed at verification researchers and practitioners who want a cheap way to make networks more verifiable. I would cite it and bring it to a reading group.","headline":"A practical regularizer that delivers big verification speedups, with an unproven but plausible mechanism—worth refereeing, needs sharper claims.","tokens_in":24900,"tokens_out":1625,"would_cite":true,"duration_ms":18431,"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":"Adding a neuron behavior consistency regularizer at training time makes neural networks verifiably robust with fewer unstable neurons, faster branch-and-bound verification, and comparable accuracy.","keywords":["neuron behavior consistency","verification-friendly neural networks","formal verification","branch-and-bound","ReLU stability","adversarial training","stable neurons","robustness verification"],"falsifier":"Train a network with the NBC loss and then measure the verifier's unstable-neuron ratio on a held-out set while also computing the NBC value; if a network with high NBC (or low NBC loss) does not show a lower unstable-neuron ratio than a network with lower NBC, the link between the surrogate loss and verifier behavior is broken. A more direct test: verify the same properties with a state-of-the-art branch-and-bound verifier on NBC-trained and standard-trained models at matched accuracy; if verification time and UNSAT% are not better for NBC-trained networks, the claim fails.","tokens_in":23940,"feed_emoji":"⚡","tokens_out":3968,"duration_ms":35123,"temperature":0.7,"pith_summary":"This paper argues that a training-time regularizer enforcing neuron behavior consistency makes neural networks dramatically easier to formally verify. The authors claim that by keeping each neuron's pre-activation sign stable across nearby inputs, the trained network has fewer unstable neurons and tighter neuron bounds, which shrinks the branch-and-bound search space. Across MNIST, Fashion-MNIST, and CIFAR-10, with several architectures and perturbation radii, networks trained this way verified faster and at higher rates than those trained with adversarial training or ReLU-stability losses, with comparable accuracy. The method also composes with existing training approaches to improve their verifiability.","feed_headline":"Neuron-stability loss verifies neural nets up to 4.5x faster","feed_subtitle":"Fewer unstable neurons shrink the search space, so larger networks become checkable by formal provers.","key_machinery":"The load-bearing mechanism is the NBC regularizer defined in Eqs. (4)-(5) and Algorithm 1: a continuous approximation to discrete neuron-sign consistency, computed as cosine similarity of pre-activation vectors per hidden layer, weighted by a factor $\\gamma[i]$ that prioritizes smaller layers, plus a KL-divergence term on the output. Algorithm 2 wraps this in an adversarial loop that finds a neighbor $x'$ minimizing NBC, making the regularization target the worst-case neighbor. The paper's argument is that minimizing this loss reduces the verifier's unstable-neuron count and tightens abstract bounds, thus shrinking the exponential search space of branch-and-bound.","core_discovery":"The central claim is that adding a neuron behavior consistency (NBC) term to the training loss produces networks that are robust, accurate enough, and substantially easier for branch-and-bound verifiers. NBC measures whether each neuron's activation state (the sign of its pre-activation value) stays the same for an input and a worst-case neighbor inside an epsilon-ball; because the discrete sign condition is not differentiable, the paper uses a continuous surrogate: cosine similarity between pre-activation vectors at each hidden layer, scaled by layer width, plus KL divergence on the output distribution. The training loss is $CE(f(x), y) - \\beta \\min_{x' \\in C_\\epsilon(x)} NBC(f, x, x')$, with the inner minimization done by PGD-like steps. The paper reports that this reduces the number of unstable neurons and tightens bounds enough to cut verification time by up to 450% and to keep verified rates high even at radii where other methods fail, with accuracy losses on the order of a few percent.","pith_inferences":["NBC could serve as a cheap warm-start for certified training methods, potentially reducing their long training times and gradient-instability issues.","The layer-scaling heuristic $\\gamma[i] = 2^{r[i]}$ suggests a general principle: constrain narrow layers near the input and output to propagate tight bounds; adaptive versions of this weighting could be tested against the fixed heuristic.","Because the surrogate only depends on pre-activations, it may extend to non-ReLU activations and to other verification-friendly modifications such as pruning or quantization, though the paper does not test these settings.","The single-neighbor adversarial minimization could miss harder neighbors inside the epsilon-ball; a multi-neighbor or randomized version might give a stronger proxy, at additional training cost."],"forward_implications":["Networks trained with NBC maintain higher stable neuron ratios across perturbation radii and architectures, which directly shrinks the theoretical upper bound on branching.","Verification time is reduced, with reported speedups of up to 450%, and the advantage grows as the perturbation radius increases.","Combining NBC with existing methods such as TRADES, Madry, and ReLU Stable improves their verification-friendliness, especially for larger networks where other methods lose all verifiability.","Accuracy remains comparable to standard adversarial training while verification improves, a combination that existing methods rarely achieve."],"supporting_citations":[{"why":"Introduces the ReLU Stable loss, the closest baseline that induces ReLU stability during training and the main comparison method.","marker":"(Xiao et al. 2019)"},{"why":"Provides the Madry adversarial training baseline and the PGD attack used to measure empirical robustness.","marker":"(Madry et al. 2018)"},{"why":"Supplies the TRADES baseline for the robustness-accuracy trade-off that NBC is compared against.","marker":"(Zhang et al. 2019b)"},{"why":"Describes the alpha-beta-CROWN verifier used to measure verification time, UNSAT%, and stable neuron ratios.","marker":"(Wang et al. 2021)"},{"why":"Source of the network architectures selected from VNN-COMP for the experiments.","marker":"(Bak, Liu, and Johnson 2021)"},{"why":"Represents the IBP-based certified training approach that NBC is contrasted with as a lighter-weight alternative.","marker":"(Mirman, Gehr, and Vechev 2018)"},{"why":"Provides the IBP regularization method for verified robustness, another certified-training baseline.","marker":"(Gowal et al. 2018)"}],"fun_headline_variants":["Neuron-stability loss makes larger nets formally verifiable","Training for verifiability: consistency beats costly proofs","Neuron consistency yields robust nets that verify in a snap","Cut verification time 4.5x with a neuron-consistency training loss"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The cosine-similarity objective evaluated at one PGD-found neighbor per input faithfully captures whether neurons actually keep their activation states fixed across the whole epsilon-neighborhood, and minimizing it genuinely reduces the unstable neurons counted by the verifier.","fun_headline_variants_meta":{"raw":{"variants":["Neuron-stability loss makes larger nets formally verifiable","Training for verifiability: consistency beats costly proofs","Neuron consistency yields robust nets that verify in a snap","Cut verification time 4.5x with a neuron-consistency training loss"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000571,"raw_usage":{"total_tokens":2677,"prompt_tokens":896,"completion_tokens":1781,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":512,"completion_tokens_details":{"reasoning_tokens":1710}},"tokens_in":512,"tokens_out":1781,"duration_ms":13146,"temperature":1.0,"reasoning_tokens":1710,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T13:41:10.975552+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Train a network with the NBC loss and then measure the verifier's unstable-neuron ratio on a held-out set while also computing the NBC value; if a network with high NBC (or low NBC loss) does not show a lower unstable-neuron ratio than a network with lower NBC, the link between the surrogate loss and verifier behavior is broken. A more direct test: verify the same properties with a state-of-the-art branch-and-bound verifier on NBC-trained and standard-trained models at matched accuracy; if verification time and UNSAT% are not better for NBC-trained networks, the claim fails.","supporting_citations":[{"cited_title":"Y.; Tjeng, V.; Shafiullah, N","cited_arxiv_id":null,"evidence_quote":"Introduces the ReLU Stable loss, the closest baseline that induces ReLU stability during training and the main comparison method."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the Madry adversarial training baseline and the PGD attack used to measure empirical robustness."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Describes the alpha-beta-CROWN verifier used to measure verification time, UNSAT%, and stable neuron ratios."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Represents the IBP-based certified training approach that NBC is contrasted with as a lighter-weight alternative."}],"review_version":1}