{"id":"9b32a542-7805-43dc-a382-4a8df3e0ab9c","arxiv_id":"2502.03765","paper_version":2,"verdict":"REJECT","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"high","formal_verification":"none","parameter_count":3,"one_line_summary":"The authors present a Leaky ReLU substitute for class-K∞ functions and a Union of Invariant Sets method that merges PWA barrier-function certificates from several linear α choices into one larger invariant set.","lead":"The paper proposes using Leaky ReLU functions instead of general class-K∞ comparison functions in barrier-function conditions, and then merging several separately computed invariant sets into one larger certified set. The practical interest is in making safety certificates for ReLU-based controllers larger and easier to compute, but the main mathematical claim does not hold as stated.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1 is false: a bounded C1 h and locally Lipschitz f satisfying (6) with alpha(h)=sqrt(h) need not admit any Leaky ReLU, so the bounded-ratio assertion in (8) is the load-bearing error.","rationale":"The reader's weakest_assumption correctly identifies the bounded-ratio step. The counterexample removes any doubt: it satisfies every stated hypothesis of Theorem 1 but violates the conclusion, so the theorem cannot be repaired by interpreting the proof charitably. A Lipschitz assumption on alpha near zero would restore the bounded ratio, but the paper does not state it, and the examples do not test it. The UIS lemma may still produce sufficient unions of linearly certified invariant sets, but that does not rescue the paper's advertised claim that a fixed two-parameter Leaky ReLU can replace arbitrary class K-infinity functions. Because the theorem is false as stated and the later construction explicitly invokes it, the reader's REJECT verdict is appropriate; no adjustment is needed.","tokens_in":9836,"tokens_out":20185,"duration_ms":212229,"concrete_test":"Evaluate the written counterexample analytically or in a CAS: for D=R, h=1/(1+e^x), f=(1+e^x)^(3/2)/e^x, alpha(h)=sqrt(h). Verify that h' f + alpha(h)=0 for all x, confirming that (a) holds. Then fix alpha_m=1 and compute at x=10: h is about 4.54e-5, and L_f h + h = -sqrt(h)+h is about -0.00669, which is negative. Since the same inequality is negative for every alpha_m once h<1/alpha_m^2, this single family of evaluations disproves Theorem 1.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is the equivalence in Theorem 1. Its proof requires, at equation (8), that alpha(h(x))/h(x) is bounded above on the set 0<h<=hmax merely because alpha and h are finite. This is false for valid extended class K-infinity functions with unbounded derivative near zero, e.g., alpha(h)=sign(h)sqrt(|h|), for which alpha(h)/h = 1/sqrt(h) tends to infinity as h goes to 0+. The failure is not hypothetical. On D=R, take h(x)=1/(1+e^x) (bounded, C-infinity, 0<h<=1) and f(x)=(1+e^x)^(3/2)/e^x (smooth, hence locally Lipschitz). Then h'(x)f(x) = -1/sqrt(1+e^x) = -sqrt(h(x)), so (6) holds with equality for alpha(h)=sqrt(h). Yet for any 0<alpha1<=alpha_m, at any point with h(x)<1/alpha_m^2, L_f h + alpha_m h = -sqrt(h)+alpha_m h < 0. Since h(x) goes to 0 as x goes to infinity, such points exist, so no Leaky ReLU parameters satisfy (6). Thus (a) does not imply (b), and the UIS construction cannot rely on Theorem 1 as a general equivalence; a Lipschitz-type condition on alpha near h=0 would be needed but is neither stated nor proved.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a framework for constructing piecewise-affine (PWA) barrier functions and invariant sets for dynamical systems identified by ReLU neural networks. The main theoretical contribution is Theorem 1, which claims that validity of a barrier condition (6) with some extended class-K∞ function α is equivalent to validity with a Leaky ReLU α of the form α(h)=α_m σ(α_1/α_m)(h). Building on this, the authors introduce a Union of Invariant Sets (UIS) method: multiple invariant sets S^(i), each certified by a linear α_i h via the earlier optimization (17), are combined into one set S = ∪_i S^(i), with a max-of-barriers PWA function as the certificate and a Leaky ReLU class-K∞ function. The paper includes two numerical examples and makes the code publicly available.","tokens_in":10180,"tokens_out":9237,"duration_ms":91287,"significance":"If the theoretical claims were correct, the paper would offer a practical way to avoid searching over class-K∞ functions and to enlarge invariant sets without additional computational cost, and the UIS idea is conceptually appealing. Credit should be given for making the code available and for the clear algorithmic presentation of the union construction. However, the central theorem is false as stated, and the proof of Lemma 1 has gaps concerning the PWA representation and the behavior at non-differentiable points and outside the set. These issues are load-bearing for the paper's main message, and the numerical examples are demonstrations rather than substitutes for proof.","major_comments":[{"comment":"The implication (a)⇒(b) is false. The proof asserts that α(h(x))/h(x) is bounded above on the set 0 < h(x) ≤ h_max merely because both α(h(x)) and h(x) are finite. This fails for valid extended class-K∞ functions whose ratio α(h)/h diverges near h=0, e.g., α(h)=sign(h)√|h|. A concrete counterexample within all the stated smoothness assumptions is: D=[0,1], h(x)=x^2 (so 0≤h≤1), f(x)=-1/2, and α(h)=sign(h)√|h|. Then L_f h = h'(x)f(x) = 2x·(-1/2) = -x = -√h(x), so (6) holds with equality. Yet for any Leaky ReLU with slopes 0<α_1≤α_m, condition (6) on h>0 reads -√h + α_m h ≥ 0, i.e., -x + α_m x^2 ≥ 0 for all x∈[0,1]. For 0 < x < 1/α_m this quantity is negative, so no Leaky ReLU parameters satisfy (6). Thus boundedness of h and finiteness of α do not imply the bounded-ratio condition used in (8) and (10); a Lipschitz-type condition on α near h=0 is needed but is neither stated nor proved.","section":"Theorem 1, Eq. (8)-(10)"},{"comment":"The product partition P = P_1 × ⋯ × P_m defined in (21) does not necessarily refine the active regions of the max function h(x,P,α)=max_i h^(i)(x). On a cell of P, each h^(i) is affine, but the pointwise maximum of several affine functions is generally not affine on the cell; the active index changes at the hyperplanes where h^(i)=h^(j), and those hyperplanes need not be part of the product partition. Consequently, the proof's assertion that 'we defined P to ensure that in each cell, we have only one affine function h_i(x,P,α)' is not justified, and the resulting h is not shown to be PWA in the sense of (1). A correct construction would require a common refinement of P_1,…,P_m together with the comparison hyperplanes {x : h^(i)(x)=h^(j)(x)}, and the proof does not provide or analyze such a refinement.","section":"Lemma 1, Eq. (21) and its proof"},{"comment":"The proof explicitly omits the demonstration that h(x,P,α)<0 for all x∉S ('Due to brevity, the proof of h(x,P,α)<0 for x∉S is eliminated'), and it defers all non-differentiable points to Proposition 2 of [15]. Both omissions are load-bearing: the negative-side argument around Eq. (26) uses h(x,P,α)<0, and condition (6) must hold for every x∈D, including the non-differentiable boundaries of the max function. The paper neither states the hypotheses required for Proposition 2 of [15] nor verifies them for the particular h in (19). As written, the proof establishes (6) only at differentiable points and under the extra assumption that S is exactly the superlevel set of h, which is part of what is left unproved.","section":"Lemma 1, proof of part 2"}],"minor_comments":[{"comment":"The sentence 'Equation (6) makes set S an asymptotically set in D' appears to be a typo; it should read 'asymptotically stable set' or 'asymptotically attractive set'.","section":"Definition 3"},{"comment":"In the statement of Theorem 1, the Leaky ReLU is written as α(x)=α_m σ(α_1/α_m)(x), but α should be a function of h(x), namely α(h)=α_m σ(α_1/α_m)(h). The current notation makes α a function of the state x, which is inconsistent with the barrier condition (6) in which α is evaluated at h(x).","section":"Theorem 1"},{"comment":"The while condition 'P_N i=1 τbi ≠ 0' is a typo; it should be '∑_i τ_bi ≠ 0'.","section":"Algorithm 1"},{"comment":"The description of the ReLU neural network approximation of the inverted pendulum is incomplete: no training data, network training procedure, or approximation-error bound is provided, so the reader cannot verify that the computed invariant set is valid for the true nonlinear dynamics rather than only for the identified PWA model.","section":"Example 1"}],"recommendation":"reject","confidential_remarks":"The central theorem of the paper is false as stated, and the counterexample is simple and robust. The UIS construction may be salvageable with a correct PWA refinement and a complete proof for the max barrier function, but that would require a substantial rewrite of the theoretical core. The current version should be rejected; the authors may benefit from seeing the counterexample before resubmitting a revised version."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: the union-of-invariant-sets idea is valid and useful, but Theorem 1 is false as stated. The stress-test counterexample is correct, and the paper's central equivalence claim does not survive it.\n\nWhat's actually new: the procedural UIS method—unioning multiple invariant sets obtained from different linear α values and then representing the combined set with a max-of-barriers plus a Leaky ReLU comparison function. That is a reasonable, practical extension of your earlier vertex-based approach, and the code is publicly available. The examples do show larger invariant sets than single-α selections. And the union of certified invariant sets is trivially forward-invariant; that part of Lemma 1 is fine.\n\nWhere it breaks: the proof of Theorem 1 asserts that α(h)/h is bounded near h=0 because α and h are finite. That is false for extended class K∞ functions like α(h)=sign(h)√|h|, where the ratio diverges. The stress-test example with h(x)=1/(1+e^x) and f(x)=(1+e^x)^(3/2)/e^x gives a smooth system satisfying (6) with α=√h, yet no Leaky ReLU slopes satisfy the inequality for all x because near h=0 the term −√h dominates any linear α_m h. So (a) does not imply (b). The theorem needs a Lipschitz condition on α near zero, which is neither stated nor proved. This matters because Theorem 1 is used to justify replacing arbitrary α with Leaky ReLU; without it, the UIS barrier construction can still be argued directly from the linear α_i, but the paper's claimed generality is unsupported.\n\nSecondary issues: Lemma 1's proof skips the h<0 case and defers nonsmooth points to [15] without checking its conditions. That is sloppy but repairable. The numerical examples are demonstrations, not proofs, and they don't fix the theory.\n\nBottom line: the UIS method is salvageable—drop or substantially weaken Theorem 1, and prove the max barrier validity directly from the individual linear α_i. As written, the paper overclaims. I would send it to peer review, expecting major revision, because the algorithmic idea and code deserve expert scrutiny, but the current Theorem 1 cannot stand.","headline":"UIS union argument is valid, but Theorem 1 is false as stated and the paper's main equivalence claim needs major repair.","tokens_in":10712,"tokens_out":3282,"would_cite":false,"duration_ms":33181,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93C10","93D30"],"pacs":[],"model":"deepseek-v4-flash","headline":"A Leaky ReLU with two slopes can replace arbitrary K∞ comparison functions in barrier-function safety certificates, and unions of invariant sets can be certified by taking pointwise maxima.","keywords":["barrier functions","Leaky ReLU","class K-infinity functions","piecewise affine systems","ReLU neural networks","invariant sets","forward invariance","safety verification"],"falsifier":"Construct a bounded, continuously differentiable h and a PWA dynamics where condition (6) holds with α(h)=sign(h)√|h|, an extended class K∞ function, but for every pair 0<α_1≤α_m the inequality L_f h ≥ −α_m σ(α_1/α_m)(h) is violated at some point arbitrarily close to the boundary h=0; if such a case exists, Theorem 1's equivalence is false as stated.","tokens_in":9593,"feed_emoji":"🛡️","tokens_out":5039,"duration_ms":46090,"temperature":0.7,"pith_summary":"The paper tries to establish that in barrier-function safety analysis for ReLU-neural-network and piecewise-affine systems, the extended class K∞ comparison function in the barrier condition can be replaced by a fixed-shape Leaky ReLU without losing any certified invariant set. If true, safety analysts can stop searching over arbitrary nonlinear comparison functions and instead tune two slopes, one for the positive side of the barrier and one for the negative. The paper also proposes the Union of Invariant Sets (UIS) method, which merges invariant sets obtained from several linear comparison functions into a single piecewise-affine barrier function whose superlevel set is their union. The authors demonstrate on inverted-pendulum and barrier-certificate examples that the union can be larger than any individual set.","feed_headline":"Leaky ReLU can replace K∞ in safety barrier proofs","feed_subtitle":"Two slopes certify the same invariant sets as arbitrary comparison functions, cutting the search cost.","key_machinery":"The load-bearing identity is the ratio bound α(h(x))/h(x) at equation (8) and its negative-side analogue at equation (10), which converts any class K∞ comparison function into a two-slope Leaky ReLU. The second piece is the max-of-barrier-functions construction h(x)=max_i $h^{{(i)}}$(x) over a product partition, with α(x)=α_max σ(α_min/α_max)(x), which turns individual invariant sets into a single certified union.","core_discovery":"The central claim is Theorem 1: for a bounded, continuously differentiable h, the existence of any extended class K∞ function α satisfying L_f h ≥ −α(h) is equivalent to the existence of a Leaky ReLU α(x)=α_m σ(α_1/α_m)(x) — with slopes 0<α_1≤α_m and σ(α_1/α_m)(x)=x for x≥0, (α_1/α_m)x for x<0 — satisfying the same inequality. The proof argues that finiteness of h and α(h) forces the ratio α(h)/h to be bounded above for h>0 and bounded below for h<0, so one can pick a dominating positive slope α_m and a smaller slope α_1. The paper then uses this equivalence to justify combining barrier functions from multiple linear α values by taking their pointwise maximum, yielding a PWA barrier function with Leaky ReLU α that certifies the union of the individual invariant sets.","pith_inferences":["Theorem 1's equivalence is local in shape near h=0; for comparison functions that vanish faster than linearly, such as sign(h)√|h|, the ratio bound fails and no finite-slope Leaky ReLU can dominate, so the equivalence as stated appears to require an additional regularity assumption.","The UIS max construction suggests a general recipe: any finite collection of valid barrier functions with comparable slopes can be merged by pointwise max, which might extend to non-ReLU nonlinear systems on compact sets, as the paper hints in Remark 2.","A testable extension is to treat the Leaky ReLU slopes α_1 and α_m as decision variables in the optimization (17) rather than choosing them by bisection, using the UIS certification to validate the result and potentially recovering larger invariant sets."],"forward_implications":["If Theorem 1 holds, barrier-function synthesis (17) can be run with a fixed Leaky ReLU shape instead of searching over K∞ functions, reducing the search to two slopes.","The UIS method yields a certified invariant set that contains every individual set from the chosen α values (Corollary 1), so it never performs worse than the previous best single-α approach and can be strictly larger.","The resulting PWA barrier function is compatible with the same partition-based optimization framework, so no new machinery beyond a product partition and a pointwise max is needed.","Because the Leaky ReLU is non-smooth, validity at non-differentiable points rests on the nonsmooth barrier-function framework, extending the method to systems where the active barrier switches."],"supporting_citations":[{"why":"Provides the prior PWA barrier function optimization with linear α that UIS extends and compares against.","marker":"[14]"},{"why":"Supplies the nonsmooth barrier function result used to justify the pointwise-max barrier function at non-differentiable points.","marker":"[15]"},{"why":"Gives the definitions of forward invariance and barrier function underlying condition (6).","marker":"[16]"},{"why":"Provides the vector-field refinement approach used in Algorithm 1 when boundary constraints are violated.","marker":"[17]"},{"why":"Serves as the barrier-certificate synthesis baseline for the second example.","marker":"[18]"},{"why":"Establishes the PWA representation of ReLU networks used to justify the differentiability assumption in Assumption 2.","marker":"[11]"}],"fun_headline_variants":["Leaky ReLU matches any K∞ in barrier proofs","Proof: Leaky ReLU and K∞ are interchangeable","Simpler barrier functions: Leaky ReLU suffices","Unite invariant sets with Leaky ReLU barriers","One slope pair does any barrier check"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof of Theorem 1 assumes that for the given class K∞ function α, the ratio α(h)/h stays bounded as h approaches zero from either side; this fails for functions like sign(h)√|h|, where the ratio blows up.","fun_headline_variants_meta":{"raw":{"variants":["Leaky ReLU matches any K∞ in barrier proofs","Proof: Leaky ReLU and K∞ are interchangeable","Simpler barrier functions: Leaky ReLU suffices","Unite invariant sets with Leaky ReLU barriers","One slope pair does any barrier check"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000677,"raw_usage":{"total_tokens":3069,"prompt_tokens":928,"completion_tokens":2141,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":544,"completion_tokens_details":{"reasoning_tokens":2065}},"tokens_in":544,"tokens_out":2141,"duration_ms":14331,"temperature":1.0,"reasoning_tokens":2065,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T00:50:47.700924+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a bounded, continuously differentiable h and a PWA dynamics where condition (6) holds with α(h)=sign(h)√|h|, an extended class K∞ function, but for every pair 0<α_1≤α_m the inequality L_f h ≥ −α_m σ(α_1/α_m)(h) is violated at some point arbitrarily close to the boundary h=0; if such a case exists, Theorem 1's equivalence is false as stated.","supporting_citations":[{"cited_title":"Invariant set estimation for piece- wise affine dynamical systems using piecewise affine barrier function,","cited_arxiv_id":null,"evidence_quote":"Provides the prior PWA barrier function optimization with linear α that UIS extends and compares against."},{"cited_title":"Nonsmooth barrier func- tions with applications to multi-robot systems,","cited_arxiv_id":null,"evidence_quote":"Supplies the nonsmooth barrier function result used to justify the pointwise-max barrier function at non-differentiable points."},{"cited_title":"Automated stability analysis of piecewise affine dynamics using vertices,","cited_arxiv_id":null,"evidence_quote":"Provides the vector-field refinement approach used in Algorithm 1 when boundary constraints are violated."},{"cited_title":"Synthesizing relu neural networks with two hidden layers as barrier certificates for hybrid systems,","cited_arxiv_id":null,"evidence_quote":"Serves as the barrier-certificate synthesis baseline for the second example."},{"cited_title":"Stability analysis and controller synthesis using single-hidden-layer relu neural networks,","cited_arxiv_id":null,"evidence_quote":"Establishes the PWA representation of ReLU networks used to justify the differentiability assumption in Assumption 2."}],"review_version":1}