{"id":"a4e977da-beff-44d0-bd94-f1972bce778a","arxiv_id":"2506.06679","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"A convex optimization method, based on a probabilistic reformulation of control inputs, computes and iteratively enlarges controlled reach-avoid sets for discrete-time polynomial systems.","lead":"This paper computes controlled reach-avoid sets for discrete-time polynomial systems by treating control inputs as random variables and using convex optimization. It adds an iterative epsilon-greedy refinement that, in the examples, finds larger safe reachable regions than a direct greedy baseline.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Appendix equation (17) misprints the ϵ-greedy constraint: it subtracts the uniform integral, uses reversed limits, and uses ε instead of δ, so Algorithm 1 as published is not a sound encoding of Proposition 3.","rationale":"I focused on the appendix misprint rather than the reader's open-set assumption because the open-set condition is an explicit hypothesis of the paper's formal problem (Section II-A defines X={h<0}, T={g<0}), and Theorem 1's proof is sound under that hypothesis. The open/closed issue is a scope limitation worth noting, but it does not invalidate the central theorem as stated. The printed SDP (17), however, is a concrete error in the algorithm's implementation. Algorithm 1's line 5 relies on solving (17); if (17) does not encode Proposition 3's constraint, then the paper's central algorithm cannot be certified or reproduced from the text. The reader did note a 'typo in the key appendix equation' but treated it as a presentation issue; I treat it as the most load-bearing concern because it directly affects the soundness of the constructive part of the contribution. The test is unambiguous: re-derive the SDP and run both versions on Example 2. I do not propose changing the verdict: CONDITIONAL remains appropriate, with the condition being that the appendix equation be corrected and the corrected version validated. I also agree with the reader's secondary points about missing code, error bars, and the distinction from [26], but those are not load-bearing for the mathematical claim.","tokens_in":22077,"tokens_out":37364,"duration_ms":379762,"concrete_test":"Re-derive the SOS encoding of (12) for m=1 by computing the polynomial ∫_{ũ0(x)−δ}^{ũ0(x)+δ} v(f(x,u)) du and ∫_U v(f(x,u)) du explicitly, and compare with (17). Then run two instances of Example 2 with ε=0.5, δ=0.1: one using the literal printed (17) and one using the corrected plus-sign/δ-limits version. If only the corrected version reproduces the reported CRAS {x|−0.0290<x<0.9480} and the literal version fails to satisfy (12) (e.g., max_u v(f(x,u))−λv(x)<0 for some x∈X\\T), the misprint is confirmed as the cause. This settles whether Algorithm 1's expansion step is sound as published.","verdict_should_be":"UNCHANGED","load_bearing_attack":"In Appendix A, the SOS encoding (17) of Proposition 3's constraint (12) is misprinted. Proposition 3 requires, for all x∈X\\T, (1−ε)/Z ∫_{ũ0(x)−δ}^{ũ0(x)+δ} v(f(x,u)) du + ε/Z ∫_U v(f(x,u)) du ≥ λv(x), with Z=(1−ε)(2δ)^m+ε·vol(U). As printed, (17) instead contains (1−ε)/Z ∫_{ũ0(x)+ε}^{ũ0(x)−ε} v(f(x,u)) du − ε/Z ∫_U v(f(x,u)) du − λv(x)+s1h−s2g ∈ P[x]. The minus sign before the ε/Z integral, the use of ε rather than δ as the box half-width, and the reversed integration limits mean the SDP (17) is not a relaxation of (12). A solver that consumes (17) literally could return a v that satisfies a much weaker or vacuous constraint, so Algorithm 1's certified expansion step (line 5) is unsupported by the published text. The same reversed-limit notation appears in Proposition 3's displayed formula, although the proof's normalization check (1−ε)/Z ∫_{box} du + ε/Z ∫_U du = 1 shows the intended limits are ũ0(x)−δ to ũ0(x)+δ. This is likely a typographical error, but it is load-bearing: the correctness of Algorithm 1 as documented depends on (17) matching (12).","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a convex-optimization framework for computing controlled reach-avoid sets (CRASs) of discrete-time polynomial systems. The central idea is to view control inputs as i.i.d. random variables with a distribution satisfying Assumption 1 and to prove (Theorem 1) that a CRAS is equivalent to a 0-reach-avoid set in this probabilistic sense. Based on this equivalence, the paper formulates an SOS program (8) that inner-approximates a CRAS by searching for a polynomial Lyapunov-like function. It then proposes an iterative algorithm (Algorithm 1), inspired by the epsilon-greedy strategy from reinforcement learning, that updates the control distribution to enlarge the certified set; the iterative condition is stated as Proposition 3 and encoded as the SOS program (17) in Appendix A. The paper reports experiments on several benchmarks, including safety verification comparisons with Fossil and DeepICBC.","tokens_in":22387,"tokens_out":7786,"duration_ms":79021,"significance":"If the central equivalence and the SOS relaxations are correct, the paper makes a valuable contribution: it gives a convex (SOS) route to CRAS computation for discrete-time polynomial systems, a problem where the standard Lyapunov-like conditions are non-convex due to composition with the control input. Theorem 1 is a genuine equivalence result and its proof is essentially sound under the stated open-set assumptions. The SOS program (8) correctly implements Proposition 2 via Putinar-type arguments, and the reported results, including a 12-dimensional safety verification in 4.9 seconds, are impressive. The main weakness is that the iterative expansion step, which is a primary contribution, is documented incorrectly: the SOS encoding (17) does not match the condition (12), so Algorithm 1 as published is not a sound implementation of the paper's own Proposition 3. The paper also relies on Proposition 1 without proof and makes an empirical, rather than proven, claim of iterative enlargement.","major_comments":[{"comment":"The SOS program (17) is not a relaxation of the constraint (12) stated in Proposition 3. As printed, (17) contains a minus sign before the term (ε/Z)∫_U v(f(x,u)) du, whereas (12) requires a plus sign; (17) uses ε as the box half-width, whereas (12) uses δ; and both (12) and (17) display reversed integration limits (ũ0(x)+ε to ũ0(x)−ε instead of ũ0(x)−δ to ũ0(x)+δ). The normalization check in the proof of Proposition 3 confirms that the intended limits are ũ0(x)−δ to ũ0(x)+δ. Because Algorithm 1, line 5, instructs the solver to use (17), the published algorithm does not correctly encode the proposed epsilon-greedy condition. This is a load-bearing error: it must be corrected, and the experiments should be re-run or explicitly confirmed to have used the corrected formula.","section":"Appendix A, Eq. (17); Section IV, Proposition 3"},{"comment":"Proposition 1 is stated without proof and without a precise reference to a theorem in [44]. Since Proposition 3 and hence the iterative expansion step reduce the new condition to Proposition 1, the correctness of the expansion phase rests on a result that the reader cannot verify from the manuscript. Please either include a proof of Proposition 1 or cite an exact theorem statement from [44] that covers this discrete-time controlled setting.","section":"Section II-B, Proposition 1"},{"comment":"The paper claims that Algorithm 1 'computes larger CRASs' and that the epsilon-greedy strategy 'expands' the CRAS, but no monotonicity or convergence theorem is provided for the sequence of sets {x∈X | v_k(x)>0}. The final output is the union of per-iteration CRASs, which is itself a CRAS provided each iterate v_k satisfies the certified condition; however, the paper does not state this union property, and the empirical volume growth is not guaranteed by any proved result. Moreover, line 6 of Algorithm 1 simply says 'update ε' without specifying the update rule, while the examples use different schedules (ε_{t+1}=0.8ε_t, ε_{t+1}=0.5ε_t, etc.). Please state precisely what guarantee is claimed and specify or parameterize the update rule.","section":"Section IV, Algorithm 1"}],"minor_comments":[{"comment":"The Monte Carlo volume estimates γ = N/10^6 are point estimates without confidence intervals; reporting values such as 0.9070 to four decimals overstates the precision of a random sample. Please include standard errors or confidence intervals.","section":"Section V"},{"comment":"The equivalence in Theorem 1 relies on the safe and target sets being open (strict inequalities h(x)<0, g(x)<0). It would be helpful to state explicitly that closed or half-open specifications require a different argument or an additional assumption, since many practical reach-avoid specifications use closed sets.","section":"Section II-A"},{"comment":"The definition is titled 'p-reach-void sets' but the intended term is 'p-reach-avoid sets'; please fix this typo.","section":"Definition 2"},{"comment":"The sentence 'the MOSEK solver fails when a higher-order polynomial is used as controller templates' is unclear: it should specify which scenario failed (e.g., which degree and sampling setup) and whether the reported results were obtained despite this failure.","section":"Example 5"},{"comment":"The notation for the perturbed policy is inconsistent: the text introduces π'_0 but later writes ϕ^{π'}_{x0}(t); please unify the notation.","section":"Theorem 1 proof"}],"recommendation":"major_revision","confidential_remarks":"The central equivalence theorem and the SOS formulation (8) appear to be sound and are a credible contribution. The blocking issue is the misprinted encoding of the epsilon-greedy condition: as published, Algorithm 1 is not a sound implementation of the paper's own Proposition 3, so the iterative expansion claim cannot be accepted on the basis of the manuscript. This is a localized, fixable error, so I recommend major revision rather than rejection. Please also ensure that the reported experiments were actually run with the corrected SOS program (17) and state this explicitly in the revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe bottom line: the core argument holds up. The equivalence between CRASs and probabilistic 0-reach-avoid sets for discrete-time polynomial systems is correct under the stated assumptions, and the convex SOS relaxation that follows is sound. The paper deserves a serious referee, but it needs a corrected appendix before it is treated as fully reproducible.\n\nWhat is actually new: replacing the nonconvex max-condition in the CRAS characterization with an expectation under a full-support input distribution is a simple but genuine trick. Theorem 1's proof is valid for open safe and target sets and Lipschitz dynamics; the open-tube argument gives positive probability, and the converse is immediate. The SOS program (8) is a standard relaxation and is sound. The epsilon-greedy iterative refinement in Algorithm 1 is a reasonable sufficient-condition heuristic, and the experiments show it often enlarges the certified set. The safety-verification extension to a 12-dimensional example in 4.9 seconds is genuinely nice evidence of scalability, even without released code.\n\nSoft spots, in proportion. The biggest issue is the appendix: equation (17), which encodes Proposition 3, is misprinted. It has a minus sign on the uniform integral, reversed integration limits, and uses epsilon instead of delta as the box half-width. A solver that consumes (17) literally is not solving the constraint in Proposition 3, so Algorithm 1's line 5 is unsupported by the published text. I believe it is a typo—the intended expression is clear from Proposition 3 and its proof—but it is load-bearing and must be fixed. Second, Proposition 1 and Lemma 1 are cited without proof; both appear sound, and Lemma 1 is from the same group's prior work, but the paper should either prove or more carefully state these. Third, the open-set assumption on X and T is real: many practical specifications are closed or half-open, and the equivalence may fail there. The paper does not discuss this limitation. Fourth, the iterative expansion has no formal monotonicity guarantee; returning the union of certified sets sidesteps the issue, but the text should say so. Finally, the Monte Carlo volume estimates come without error bars, so the reported expansions should be read with some skepticism.\n\nOverall, this is a solid subfield contribution, not a breakthrough, and the novelty relative to the authors' own prior reach-avoid work is modest. But the equivalence result and the convex formulation are worth having. I would send it to a referee who can check the appendix carefully and ask for a corrected (17), proof sketches for the cited lemmas, and a discussion of the open-set limitation.\n\nVerdict: deserves peer review.","headline":"A correct and useful probabilistic reformulation of CRASs, marred by a load-bearing typo in the key appendix equation that needs fixing before the method is reproducible.","tokens_in":22963,"tokens_out":3492,"would_cite":true,"duration_ms":34580,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93C55","90C22","93B03","93D30"],"pacs":[],"model":"deepseek-v4-flash","headline":"Randomizing control inputs turns discrete-time reach-avoid computation into convex optimization.","keywords":["controlled reach-avoid sets","discrete-time polynomial systems","sum-of-squares optimization","semidefinite programming","epsilon-greedy","0-reach-avoid sets","safety verification","Lyapunov-like functions"],"falsifier":"Construct a discrete-time polynomial system with a closed safe set where the only successful control sequence is forced to lie on the boundary of the control set for every step. Under any full-support distribution the probability of drawing exactly that sequence is zero, so the 0-reach-avoid set is empty while the CRAS is nonempty; finding such an example would disprove the claimed equivalence outside the open-set assumption.","tokens_in":21853,"feed_emoji":"🎯","tokens_out":6151,"duration_ms":55394,"temperature":0.7,"pith_summary":"This paper aims to show that controlled reach-avoid sets (CRASs) for discrete-time polynomial systems—the initial states from which some control policy can steer the system into a target set without leaving a safe set—can be inner-approximated by solving a convex optimization problem. The idea is to treat the control inputs as random variables drawn from any distribution with full support on the control set. Under that probabilistic lens, the paper proves that a CRAS is exactly a 0-reach-avoid set: a state is in the set precisely when the probability of a safe journey to the target is strictly positive. The Lyapunov-like inequalities that characterize such sets become sum-of-squares constraints after the maximum over controls is replaced by an expectation, which removes the nonlinear coupling that previously blocked convex computation for discrete-time systems. An iterative epsilon-greedy update of the control distribution then expands the certified set.","feed_headline":"Randomizing controls makes reach-avoid sets convex","feed_subtitle":"A sum-of-squares program computes controlled reach-avoid sets; an epsilon-greedy loop enlarges them.","key_machinery":"The machinery is the probabilistic replacement of the control variable: control inputs $u$ are drawn i.i.d. from a fixed distribution, and the maximum over $u$ in the Lyapunov-like condition is replaced by an expectation $\\mathbb{E}[v(f(x,u))]$. This removes the nonlinear composition terms such as $u^2$ and $u^3$ that made discrete-time certificate synthesis non-convex, because the expectation is linear in $v$. The epsilon-greedy refinement replaces the fixed distribution by a state-dependent mixture concentrated on a $\\delta$-neighborhood of a fitted approximate optimal controller, with weight $1-\\epsilon$, plus a uniform exploration term with weight $\\epsilon$; the resulting inequality (12) is still convex in $v$ and can be encoded as the SOS program (17). Together these transformations turn CRAS computation into a sequence of semidefinite programs.","core_discovery":"The central claim is Theorem 1: under Assumption 1, a controlled reach-avoid set $R$ and a probabilistic 0-reach-avoid set $R_0$ coincide. Since the safe and target sets are open and the dynamics are polynomial, hence locally Lipschitz, a successful finite control sequence has an open neighborhood of control perturbations that still succeeds, so any full-support distribution gives the successful event strictly positive probability. Consequently the hard search over control policies can be replaced by the search for a bounded function $v$ satisfying $\\mathbb{E}[v(f(x,u))] - \\lambda v(x) \\geq 0$ on the safe set minus the target and $v(x) \\leq 0$ on the boundary region, which is convex in $v$. Encoding $v$ and the multipliers as sum-of-squares polynomials yields the semidefinite program (8), whose region $\\{x \\in X : v(x) > 0\\}$ is an inner approximation of the CRAS. The paper further claims that iterating with a state-dependent epsilon-greedy distribution—mostly concentrating probability near a fitted optimal controller while retaining small exploration weight elsewhere—enlarges the certified set, and that the resulting method verifies a 12-dimensional safety benchmark in seconds.","pith_inferences":["If the equivalence is right, the hard part of CRAS computation is not the policy search but the choice of the control distribution; tuning the distribution or the epsilon schedule should be as important as raising the polynomial degree of $v$.","The open-set assumption suggests a testable boundary case: practical specifications with closed safe sets may need a limiting argument or a modified theorem.","The epsilon-greedy iteration resembles a homotopy from the uniform-distribution certificate to a local controller-based certificate; viewed this way, it could be extended to other certificate classes such as control Lyapunov functions for stabilization.","The Monte Carlo volume estimates and grid sampling for controller fitting introduce statistical error that the theory does not yet quantify; a falsifier could compare the SOS-certified set against exact dynamic programming on low-dimensional benchmarks."],"forward_implications":["CRASs for discrete-time polynomial systems can be inner-approximated by a single convex sum-of-squares program, avoiding the non-convex search for feedback controllers.","The initial certified set can be enlarged by iteratively updating the control distribution with an epsilon-greedy rule; each iteration solves another convex program.","The probabilistic reformulation extends to control barrier certificates for safety verification, and the paper reports successful verification of benchmarks up to 12 dimensions, including one in 4.9 seconds.","Because the expectation condition implies the maximum condition, any certificate found by the method is also valid for the original CRAS definition.","The method is presented as the first sum-of-squares approach tailored to CRASs for discrete-time polynomial systems."],"supporting_citations":[{"why":"Defines p-reach-avoid sets and supplies the probabilistic viewpoint that the paper builds on.","marker":"[39]"},{"why":"Supplies the Lyapunov-like expectation condition (Lemma 1) used to certify 0-reach-avoid sets.","marker":"[37]"},{"why":"Supplies the max-based Lyapunov-like condition that Proposition 1 adapts to CRASs and that the expectation condition implies.","marker":"[44]"},{"why":"Baseline certificate-synthesis toolchain used for comparison in the safety-verification experiments.","marker":"[13]"},{"why":"Baseline certificate method used for comparison in the safety-verification experiments.","marker":"[27]"},{"why":"Invoked to justify decreasing epsilon in the iterative epsilon-greedy strategy.","marker":"[42]"},{"why":"Used to compute the one-step over-approximation $\\hat{X}$ needed in the SOS programs.","marker":"[40]"},{"why":"Earlier iterative CRAS method that the paper positions its discrete-time approach against.","marker":"[26]"}],"fun_headline_variants":["Convex optimization computes reach-avoid sets via randomization","Randomize controls to certify safety sets","Epsilon-greedy loop enlarges verified reach-avoid sets","Probabilistic trick makes reach-avoid sets convex","SOS program finds safe initial states"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof hinges on the safe and target sets being open, so that around a successful trajectory there is a whole tube of successful control sequences; if those sets are closed or half-open, the equivalence between a CRAS and a 0-reach-avoid set may break.","fun_headline_variants_meta":{"raw":{"variants":["Convex optimization computes reach-avoid sets via randomization","Randomize controls to certify safety sets","Epsilon-greedy loop enlarges verified reach-avoid sets","Probabilistic trick makes reach-avoid sets convex","SOS program finds safe initial states"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000188,"raw_usage":{"total_tokens":1373,"prompt_tokens":1026,"completion_tokens":347,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":642,"completion_tokens_details":{"reasoning_tokens":274}},"tokens_in":642,"tokens_out":347,"duration_ms":3887,"temperature":1.0,"reasoning_tokens":274,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T05:53:40.693824+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a discrete-time polynomial system with a closed safe set where the only successful control sequence is forced to lie on the boundary of the control set for every step. Under any full-support distribution the probability of drawing exactly that sequence is zero, so the 0-reach-avoid set is empty while the CRAS is nonempty; finding such an example would disprove the claimed equivalence outside the open-set assumption.","supporting_citations":[{"cited_title":"In: 2021 American Control Conference (ACC)","cited_arxiv_id":null,"evidence_quote":"Defines p-reach-avoid sets and supplies the probabilistic viewpoint that the paper builds on."},{"cited_title":"IEEE Transactions on Automatic Control68(8), 4682–4694 (2022)","cited_arxiv_id":null,"evidence_quote":"Supplies the max-based Lyapunov-like condition that Proposition 1 adapts to CRASs and that the expectation condition implies."},{"cited_title":"IEEE Transactions on Reliability (2024)","cited_arxiv_id":null,"evidence_quote":"Baseline certificate method used for comparison in the safety-verification experiments."},{"cited_title":"Advances in Neural Information Processing Systems36(2024)","cited_arxiv_id":null,"evidence_quote":"Invoked to justify decreasing epsilon in the iterative epsilon-greedy strategy."},{"cited_title":"In: 2020 59th IEEE Conference on Decision and Control (CDC)","cited_arxiv_id":null,"evidence_quote":"Used to compute the one-step over-approximation $\\hat{X}$ needed in the SOS programs."},{"cited_title":"In: 2024 American Control Conference (ACC)","cited_arxiv_id":null,"evidence_quote":"Earlier iterative CRAS method that the paper positions its discrete-time approach against."}],"review_version":1}