{"id":"1168d361-4646-4d9d-9883-02b300158672","arxiv_id":"2502.05510","paper_version":3,"verdict":"REJECT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":4,"one_line_summary":"A data-driven algorithm synthesizes reachability, safety, and reach-while-avoid certificates with PAC-style bounds, using a compression set built during non-convex loss minimization.","lead":"The authors learn neural-network certificates for reachability, safety, and reach-while-avoid properties from sampled trajectories of discrete-time systems. They attach probabilistic guarantees to these certificates using scenario optimization and a compression set computed during training.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Zero value of the discretized loss (26) does not imply the continuous certificate conditions (3)-(6) because no grid error bound is given, so Theorem 1's PAC guarantee does not follow for the implemented algorithm.","rationale":"The reader's weakest assumption identifies the same load-bearing concern I find: the implemented algorithm checks certificate conditions only on finite grids and on the boundary of X, with no quantitative error bound connecting zero discretized loss to the continuous conditions that Theorem 1 and Definition 1 require. This is not a minor technicality: the entire PAC guarantee is conditional on the output VN being a genuine certificate. If (3)-(6) hold only on the sampled grid, the property φ may fail on a new trajectory that passes through a region where V violates a condition between grid points, and the first inclusion in (21) would not hold. The paper's phrasing that the grid is 'dense enough' (Section 4.3) is an assertion, not a proof; no Lipschitz constant, no resolution-dependent error bound, and no independent verification step is supplied. I also considered whether Assumption 2's preference/non-associativity properties could be the weakest point; the proofs in Appendix A.2 are somewhat informal, particularly the repeated-sample argument, but they are secondary because even a fully rigorous compression proof would not repair the missing link from discretized loss to continuous certificate. Credit is due for the constructive compression-set mechanism and the conditional Theorem 1, which appears internally plausible. However, the paper's stated contribution—model-free PAC guarantees for reachability, safety, and RWA certificates—is not supported by the implemented algorithm as written. The gap is likely reparable (e.g., by adding a sound continuous-domain verification step or a Lipschitz-based grid refinement bound), but the current manuscript does not contain such a step, so I recommend keeping the REJECT verdict.","tokens_in":24110,"tokens_out":4137,"duration_ms":45863,"concrete_test":"Take the trained neural-network certificate returned by Algorithm 2 for the §6.1 reachability case and run a sound verifier (e.g., interval bound propagation or an SMT solver over the network's activation functions) to check conditions (3)-(6) on the continuous sets X_I, X\\X_G, ∂X_G, and a sufficiently large bounded box in R^n\\X. Report the maximum violation found. Because Eq. (26) only checks finitely many points, any found violation directly disproves the claim that zero discretized loss certifies ψ_s; a successful verifier would show the gap is only a missing formalization, not an actual failure.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that Algorithm 2, via Theorem 1, provides a PAC guarantee that a new trajectory satisfies φ. This requires the constructed V to satisfy the continuous certificate conditions: ψ_s^reach = (3)-(6) and ψ_Δ^reach = (7) for all sampled trajectories. Section 4.3 replaces the integrals defining l_s in (25) by a summation over finite deterministic grids, Eq. (26), and checks condition (6) only on the boundary ∂X. The text states the grids are 'dense enough' but gives no error bound, no Lipschitz estimate for V, and no post-hoc verification step. Hence a returned V with zero loss (28) is only known to satisfy inequalities at finitely many points and on ∂X, not over X\\X_G, ∂X_G, X_I, or R^n\\X. For example, a continuous function can be non-positive on a grid in X\\X_G yet positive between grid points, violating (5); or it can be positive on ∂X but negative in an arbitrarily thin layer just outside X, violating (6). Since Definition 1 and the first inclusion in (21) rely on V actually satisfying ψ_s and ψ_Δ, the implication 'zero loss ⇒ property φ' is not established. The compression-set argument of Theorem 1 is conditional on an algorithm whose output is a true certificate; as implemented, that precondition is unverified. This is a load-bearing gap in the paper as written, independent of the plausibility of Assumption 2's preference/non-associativity properties.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a data-driven method for synthesizing neural-network certificates for reachability, safety, and reach-while-avoid properties of deterministic discrete-time systems. It encodes certificate conditions as a loss function, introduces Algorithm 1 as a subgradient-descent procedure that simultaneously builds a compression set, and Algorithm 2 as a discarding mechanism to drive the loss to zero. The main theoretical result, Theorem 1, uses compression-based scenario theory to give a PAC-style bound on the probability that a new trajectory violates the certificate conditions and thereby the underlying property. The paper reports numerical experiments on benchmark systems, including a comparison with the scenario-optimization approach of [34], and states that code is publicly available.","tokens_in":24410,"tokens_out":11822,"duration_ms":136807,"significance":"If fully established, the contribution would be significant: it aims to provide model-free probabilistic verification guarantees without requiring Lipschitz constants of the dynamics, and it gives a constructive, iterative mechanism for computing compression sets in a non-convex setting. The explicit comparison with [34] and the availability of code are strengths. The value of the paper is, however, conditional on closing the gap between the continuous certificate conditions used in the theory and the finite, grid-based loss actually minimized in the implementation, and on a correct proof that the discarding algorithm indeed produces a compression set.","major_comments":[{"comment":"The replacement of the integrals in (25) by the finite sums in (26), with the exterior-positivity condition checked only on the boundary ∂X, is not supported by any error analysis. The text states that the grid is 'dense enough' but gives no Lipschitz estimate for V_θ and no post-verification step. A continuous function can satisfy (26) and yet violate (5) between grid points, or violate (6) in an arbitrarily thin layer just outside X. Since Theorem 1 and Definition 1 require V to satisfy the continuous conditions ψ_s and ψ_Δ, the implication 'zero discretized loss ⇒ property φ' is not established for the implemented algorithm.","section":"Section 4.3, Eq. (26)"},{"comment":"The proof that R_N is a compression set for Algorithm 2 is not valid as written. To show A_2(R_N)=A_2({ξ_i}), the proof re-runs Algorithm 2 on R_N and asserts that the first call to Algorithm 1 returns C_1; however, that first call is fed with R_N rather than the original multiset, and Proposition 4 only guarantees that C_1 is a compression set for the original invocation. No argument is given that Algorithm 1 on R_N produces the same sequence of sets C_i and the same final parameter vector. Without a correct proof that R_N is a compression set, Theorem 1 cannot be invoked with R_N for Algorithm 2.","section":"Section 4.2 and Appendix A.3, Proposition 5(2)"},{"comment":"Theorem 1 is stated under the hypothesis V_N = A({ξ_i}) satisfies ψ_s and all sampled conditions ψ_Δ(ξ_i). Algorithm 2, however, terminates when the loss is zero only on the remaining set D, and samples in R_N are removed precisely because their loss may be positive. The paper does not explain how the final certificate satisfies the theorem's hypothesis, nor why the first inclusion in (21) remains valid for an algorithm that discards violating samples. A separate argument is needed to justify that a new violating trajectory still implies a change of the compression set.","section":"Section 3.2, Theorem 1 and Eq. (21)"}],"minor_comments":[{"comment":"The notation '⋀_{i=0}^N ψ_Δ(ξ_i)' appears to have an indexing typo; it should presumably be i=1,...,N.","section":"Theorem 1 statement"},{"comment":"Section 2.1 states that X is bounded, while Property 2 says the safety property may be constructed for unbounded X; these statements should be reconciled.","section":"Section 2.1 and Property 2"},{"comment":"The sample-dependent loss l_Δ contains the term sup_{x∈X_I} V_θ(x), but the implementation of this supremum over a continuous set is not discussed; presumably it is also discretized, and this should be stated explicitly.","section":"Section 4.3, Eq. (27)"},{"comment":"The sentence 'the approach of [34] with 10^19 samples results in a confidence of at least 10^{-30}' appears to invert the intended statement; a confidence should be close to one, while a risk level would be small.","section":"Section 6.4"},{"comment":"The phrase 'by Certificate 1' should presumably read 'by Proposition 1'.","section":"Section 4.3"}],"recommendation":"major_revision","confidential_remarks":"The scenario-optimization framework in the paper is interesting and the comparison with [34] is useful. However, the current version should not be accepted because the central guarantee is not connected to the implemented discretized loss, and because the proof that Algorithm 2 constructs a compression set appears incomplete. Both issues are load-bearing for the paper's main claim and require substantial additional work rather than copy-editing."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: the compression-set construction is the real contribution here; the PAC wrapper is borrowed and the implementation has a load-bearing gap in Section 4.3 that the authors wave past.\n\nWhat's new: Algorithm 1's way of building a compression set inside a subgradient-descent loop with jump exploration is a genuine advance over pick-to-learn. Proposition 4's argument that the compression set reproduces the same iterates is plausible, and the preference/non-associativity proof is non-trivial. The comparison with [34] (Lipschitz-requiring, exponential-in-dimension) is fair, and the code is available. The numerical work shows the method handles 8D and partially unsafe systems, which is useful evidence.\n\nWhere it goes soft: Theorem 1 is conditional on the algorithm returning V that satisfies the continuous certificate conditions psi_s and psi_Delta on all sampled trajectories. But Section 4.3 replaces the state integrals in (25) with finite grid sums (26), and enforces the outside-X positivity only on the boundary. Zero value of (26) only tells you the inequalities hold on the grid and boundary; it says nothing about gaps between grid points or a thin layer just outside X. The paper says the grid is 'dense enough' but gives no Lipschitz estimate for V, no grid-error bound, and no post-hoc verification. Without that, the implication 'zero discrete loss => certificate => property' fails, so the PAC guarantee in Theorem 1 does not attach to the actual output of Algorithm 2. This is not a small technicality: it is the bridge from the theorem's precondition to the deployed algorithm.\n\nThe rest of the theory looks internally consistent; the compression argument in Theorem 1 is standard scenario theory applied correctly. The flaw is concentrated in one section and is likely reparable - add a Lipschitz bound for the network and choose the grid accordingly, or add a verification oracle that checks the continuous conditions on a dense set. Citation patterns are fine; the closest work in [34] and [35] is discussed honestly.\n\nWho this is for: people working in data-driven verification and scenario optimization. The compression mechanism is worth knowing even if the current guarantees are not yet airtight. I would send it to peer review, but flag the Section 4.3 gap as a major-revision issue. The authors need to either prove a grid-error bound or restructure the claim to a finite-sample certificate.","headline":"The compression-set construction is genuinely new, but the missing grid-error analysis leaves the PAC certificate guarantee unsupported for the implemented method.","tokens_in":24920,"tokens_out":2199,"would_cite":false,"duration_ms":23584,"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":"Sampled trajectories alone can yield reachability, safety, and reach-while-avoid certificates whose PAC risk is set by a compression set, not state dimension.","keywords":["certificate synthesis","reachability","safety","reach-while-avoid","PAC guarantees","compression set","scenario approach","non-convex optimization"],"falsifier":"Construct a smooth scalar function whose sampled loss (26) is zero on the deterministic grids described in Section 4.3 but whose true value violates one of the continuous conditions, for example a sublevel well inside $X_G$ that sits between grid points and dips below $-\\delta$; existence of such a function would refute the dense-grid implication and hence the premise of Theorem 1. Concretely, one can run the method and then check the returned certificate with a dense adaptive search or global optimizer; any violation found outside the training grid is a direct falsifier.","tokens_in":23877,"feed_emoji":"🛡️","tokens_out":12018,"duration_ms":111506,"temperature":0.7,"pith_summary":"The paper tries to establish that verification certificates for discrete-time dynamical systems can be learned from a finite collection of trajectories, with no model of the dynamics and no knowledge of its Lipschitz constant. The properties covered are reachability, safety, and reach-while-avoid; for each, a scalar function $V$ is trained by minimizing a loss whose zero value encodes the certificate conditions. The accompanying guarantee, Theorem 1, is PAC in nature: with confidence at least $1-\\beta$, the probability that a newly drawn trajectory violates the certificate conditions—and hence the property—is at most $\\epsilon(C_N,\\beta,N)$, where $C_N$ is the number of training trajectories in a compression set. A compression set is a subset of the data that would produce the exact same certificate as the full dataset, and its size, rather than state dimension, controls the risk bound. The paper also provides the algorithms that construct the certificate and the compression set simultaneously, so the guarantee is usable in practice.","feed_headline":"Trajectories alone certify safety, reachability and reach-while-avoid","feed_subtitle":"No model or Lipschitz constant needed; the guarantee tracks task complexity, not state dimension.","key_machinery":"The central object is the compression set: a subset $C_N$ of the training trajectories which, when used as the algorithm's input, returns the same certificate $V_N$ as the full dataset. Its cardinality $C_N = |C_N|$ enters the risk formula (19), so smaller compression sets give tighter PAC guarantees. Algorithm 1 is the constructive mechanism: it performs subgradient descent on the worst-case loss and, when it finds a training sample whose subgradient is misaligned with the current descent direction, it 'jumps' along that subgradient and adds the sample to $C_N$; the paper proves that this creates a genuine compression set. Algorithm 2 wraps Algorithm 1, discarding each returned compression set from the training pool until the worst-case loss reaches zero, at the cost of a larger final compression set. The loss functions (25)–(27) translate the certificate conditions—initial-set, goal-set, unsafe-set, outside-domain, and along-trajectory decrease constraints—into integrals over the relevant regions, with the integrals approximated in implementation by sums over deterministic grids.","core_discovery":"On the paper's own terms, the central claim is a theorem about any certificate-synthesis algorithm that satisfies two structural properties: preference and non-associativity (Assumption 2). Theorem 1 states that if such an algorithm returns a certificate $V_N$ satisfying the certificate conditions on all $N$ sampled trajectories, then, with confidence at least $1-\\beta$, the probability that a new trajectory violates those conditions—and therefore the property $\\varphi$—is bounded by $\\epsilon(C_N,\\beta,N)$, the solution of equation (19) evaluated at the compression-set cardinality. The proof routes the violation probability through the probability that a new sample changes the compression set, which the paper controls via a compression-generalization result. The paper then claims that its own Algorithm 1, a subgradient-descent scheme with deliberate jumps triggered by misaligned subgradients, terminates, returns a compression set, and satisfies Assumption 2 (Proposition 4), and that Algorithm 2, which discards compression sets until the loss reaches zero, does the same (Proposition 5). If these propositions hold, the PAC bound applies to the certificates actually constructed in the numerical studies, including the partially unsafe example where classical exact methods cannot give a certificate.","pith_inferences":["The paper leaves implicit that the 'dense enough' grid in Section 4.3 is doing logical work: if a counterexample could hide between grid points, the validity implication from the discretized loss (26) to the continuous conditions (3)–(6) would break, so an error bound or post-hoc verification would turn the method into a fully rigorous one.","A testable extension suggested by the framework is to use the learned certificate itself to search for violations: since the certificate defines level sets, one can run a global optimizer over $V$ on each region and check the continuous conditions, converting the grid assumption into a verifiable certificate.","The same compression-set construction should transfer to other non-convex learning-with-guarantees tasks beyond dynamical-system verification, because Algorithm 1 only relies on subgradients and a worst-case loss over samples.","The PAC guarantee is relative to the distribution of initial conditions used for sampling; an adversarial or unknown initial-state distribution would require additional robustness machinery not present in the paper."],"forward_implications":["A direct corollary is that property verification becomes model-free: only sampled trajectories are needed, not the system equations, so the method applies to black-box or simulation-only systems.","Because the risk bound depends on compression-set size rather than exponentially on state-space dimension, the guarantees can remain informative for higher-dimensional systems where grid-based and Lipschitz-based scenario bounds become vacuous.","The discarding mechanism lets the method produce a probabilistic certificate even when some sampled trajectories enter the unsafe set, a case in which exact certificate synthesis would simply fail.","The certificate itself, not just a yes/no property answer, is made available, which the paper identifies as a step toward control synthesis.","The compression-set computation is constructive for a non-convex optimization program, extending a mechanism that was previously a general meta-algorithm to a concrete subgradient-descent instance."],"supporting_citations":[{"why":"Supplies the compression-set generalization theorem whose risk formula (19) is used directly in the proof of Theorem 1.","marker":"[14]"},{"why":"Provides the pick-to-learn meta-algorithm that Algorithm 1 instantiates as a concrete subgradient-descent procedure.","marker":"[35]"},{"why":"The closest alternative approach, which requires Lipschitz constants and convexity; the paper compares its guarantees and sample counts against this approach.","marker":"[34]"},{"why":"Gives the direct-property PAC bound stated as Proposition 6, used as the baseline when no certificate is constructed.","marker":"[7]"},{"why":"Supplies a priori compression bounds for convex programs that motivate the a posteriori route taken here.","marker":"[11]"},{"why":"Provides the wait-and-judge a posteriori compression perspective underlying the risk evaluation.","marker":"[13]"},{"why":"Supplies the sampling-and-discarding idea on which Algorithm 2 is based.","marker":"[44]"},{"why":"Establishes that non-convex scenario problems generally lack non-trivial a priori compression bounds, motivating the constructive approach.","marker":"[15]"}],"fun_headline_variants":["Data-driven certificates: PAC guarantees from past trajectories","Learn safety certificates from data with compression-based PAC bounds","No model? No problem: certificates from trajectories alone","Compression enables PAC certificates for dynamical systems","Trajectory-only certificates with probabilistic validity"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The argument stands on the assumption that a certificate whose discretized loss (26) is zero on a finite grid, with the outside-domain condition checked only on the boundary of $X$, satisfies the exact continuous certificate conditions over the whole state space; the paper states the grid is 'dense enough' but offers no error bound or verification step for that implication.","fun_headline_variants_meta":{"raw":{"variants":["Data-driven certificates: PAC guarantees from past trajectories","Learn safety certificates from data with compression-based PAC bounds","No model? No problem: certificates from trajectories alone","Compression enables PAC certificates for dynamical systems","Trajectory-only certificates with probabilistic validity"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000222,"raw_usage":{"total_tokens":1503,"prompt_tokens":1044,"completion_tokens":459,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":660,"completion_tokens_details":{"reasoning_tokens":388}},"tokens_in":660,"tokens_out":459,"duration_ms":5237,"temperature":1.0,"reasoning_tokens":388,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-08T19:03:14.393271+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a smooth scalar function whose sampled loss (26) is zero on the deterministic grids described in Section 4.3 but whose true value violates one of the continuous conditions, for example a sublevel well inside $X_G$ that sits between grid points and dips below $-\\delta$; existence of such a function would refute the dense-grid implication and hence the premise of Theorem 1. Concretely, one can run the method and then check the returned certificate with a dense adaptive search or global optimizer; any violation found outside the training grid is a direct falsifier.","supporting_citations":[{"cited_title":"Campi and Simone Garatti","cited_arxiv_id":null,"evidence_quote":"Supplies the compression-set generalization theorem whose risk formula (19) is used directly in the proof of Theorem 1."},{"cited_title":"Campi, and Simone Garatti","cited_arxiv_id":null,"evidence_quote":"Provides the pick-to-learn meta-algorithm that Algorithm 1 instantiates as a concrete subgradient-descent procedure."},{"cited_title":"Formal Verification of Unknown Discrete- and Continuous-Time Systems: A Data- Driven Approach","cited_arxiv_id":null,"evidence_quote":"The closest alternative approach, which requires Lipschitz constants and convexity; the paper compares its guarantees and sample counts against this approach."},{"cited_title":"Badings, Murat Cubuktepe, Nils Jansen, Sebastia n Junges, Joost-Pieter Katoen, and Ufuk Topcu","cited_arxiv_id":null,"evidence_quote":"Gives the direct-property PAC bound stated as Proposition 6, used as the baseline when no certificate is constructed."},{"cited_title":"Campi and Simone Garatti","cited_arxiv_id":null,"evidence_quote":"Supplies a priori compression bounds for convex programs that motivate the a posteriori route taken here."},{"cited_title":"Campi and Simone Garatti","cited_arxiv_id":null,"evidence_quote":"Provides the wait-and-judge a posteriori compression perspective underlying the risk evaluation."},{"cited_title":"On the Exact Feasibility of Convex Scenario Programs With Discarded Constraints","cited_arxiv_id":null,"evidence_quote":"Supplies the sampling-and-discarding idea on which Algorithm 2 is based."},{"cited_title":"A General Scenario Theory for Nonconvex Optimization and Decision Making","cited_arxiv_id":null,"evidence_quote":"Establishes that non-convex scenario problems generally lack non-trivial a priori compression bounds, motivating the constructive approach."}],"review_version":1}