{"id":"c3e943cb-1f09-4ef0-8b58-a6764fdee45c","arxiv_id":"2507.17703","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"The authors reformulate joint synthesis of a piecewise stochastic control barrier function and a safe controller as a single dual linear program claimed to have zero duality gap.","lead":"This paper presents a linear-programming method to simultaneously synthesize a piecewise constant safety barrier and a safe controller for discrete-time nonlinear stochastic systems with additive noise. If correct, it would let engineers compute formal probabilistic safety guarantees for controlled stochastic systems in minutes using standard LP solvers.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The polyhedral representation in (17) replaces the universal requirement 'for all x in X_i' in (13)/(15d) with an existential variable \\tilde{z}_i, invalidating the zero-gap LP equivalence and the formal safety guarantee.","rationale":"The reader's weakest assumption correctly identifies the unproven equivalence between the semi-infinite constraints (13)/(15d) and the polyhedral representation (17). My analysis strengthens this: the equivalence is not just missing a proof, it is actually incorrect because (17) uses an existential variable \\tilde{z}_i, whereas (13) imposes a universal condition over x in each cell. The proof of Theorem 2 derives KKT conditions with respect to \\tilde{z}_i, which is only meaningful if \\tilde{z}_i is an optimization variable, reinforcing that the LP solves a relaxed problem. The provided concrete test would expose this unsoundness on a minimal example: the original constraint is infeasible, but the LP in Theorem 2 would find a feasible solution. Because the core idea of PWC s-CBF synthesis is salvageable (e.g., by replacing the existential \\tilde{z}_i with constraints at the vertices of each cell), I agree with the reader's CONDITIONAL verdict rather than outright rejection. The paper must provide a correct derivation of the polyhedral representation or a different convexification, along with a complete proof of zero duality gap, before the formal safety guarantee can be accepted.","tokens_in":13591,"tokens_out":8087,"duration_ms":81690,"concrete_test":"Construct a one-dimensional cell X_i = [-1,1] with a single transition j whose affine bounds from Lemma 1 are T_ij(x,u) = 0.5x and \\overline{T_ij}(x,u) = -0.5x (they satisfy the soundness condition for some kernel). The original constraint (13) requires T_ij in [0.5x, -0.5x] for all x in [-1,1], which is empty. The polyhedral representation (17) with \\tilde{z}_i = [x, u] and x in [-1,1] admits T_ij = 0 by choosing x = 0. Implement the LP from Theorem 2 for this minimal instance (K=1, U=[0,1], any dynamics consistent with these bounds). If the LP returns a feasible solution with a positive safety bound, it solves a strict relaxation of (13), demonstrating that the claimed equivalence in Theorem 2 is false.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central claim is that the minimax problem in Theorem 1 is solved exactly by the dual LP in Theorem 2. The proof hinges on representing the semi-infinite constraint (15d), which requires the transition kernel bounds to hold for all x in each partition cell X_i, as the polyhedral set (17). This conversion is not merely unproven; it is incorrect. In (13), for fixed u, the feasible transition vectors T_i are those satisfying T_ij(x,u) <= T_ij <= \\overline{T_ij}(x,u) for every x in X_i, i.e., T_i must lie in the intersection over x of the corresponding intervals. In (17), the authors introduce decision variables x'_i, x''_i >= 0, set \\tilde{z}_i = [x'_i - x''_i, u_i], and impose the affine bounds for that single \\tilde{z}_i. This defines the projection of a polyhedron, which is the union over x of the intervals, not the intersection. The universal quantifier has been swapped for an existential one. Consequently, the LP in Theorem 2 solves a relaxed problem: it may pick, for each cell, an x that makes the barrier condition easiest to satisfy, while other x in the same cell violate (8c). The safety bound (9) therefore is not a guaranteed lower bound. The stationarity condition (19e) with respect to \\tilde{z}_i further confirms that \\tilde{z}_i is treated as an optimization variable, which is only valid for the relaxed problem. This is a load-bearing flaw: the zero-gap equivalence and the formal safety guarantee both collapse unless the polyhedral representation is corrected (e.g., by imposing the affine bounds at all vertices of X_i).","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a method for jointly synthesizing a piecewise constant stochastic control barrier function and a piecewise constant feedback controller for discrete-time nonlinear stochastic systems with additive Gaussian noise and bounded continuous controls. The synthesis problem is formulated as a minimax optimization over the barrier values, controller values, and transition-kernel bounds, and the paper claims that this minimax problem can be solved exactly by a dual linear program with zero duality gap, yielding a formally guaranteed lower bound on probabilistic safety. The method uses interval bound propagation to obtain affine lower and upper bounds on transition kernels over partition cells, then constructs a dual LP whose constraints are derived from the original semi-infinite constraints. The paper reports case studies on 2D linear, 3D temperature-regulation, and 4D unicycle models, with safety probabilities matching or exceeding a 0.95 threshold.","tokens_in":13911,"tokens_out":9637,"duration_ms":105732,"significance":"The problem addressed is important: simultaneous synthesis of a barrier certificate and a safe controller for stochastic systems with continuous control sets is genuinely challenging, and an exact, tractable LP formulation would be a valuable contribution. The interval-bound-propagation idea in Lemma 1 is sensible, and the experimental evaluation covers relevant benchmarks of increasing dimension. However, the central claim of an exact zero-gap conversion is not established by the manuscript. The proposed polyhedral representation in Section V replaces a universal quantifier over states with an existential variable, so the LP in Theorem 2 solves a relaxed problem. Consequently, the formal safety lower bound in (9) is not guaranteed by the LP solution, and the reported safety probabilities are not supported by the theory. The paper is not publishable in its current form.","major_comments":[{"comment":"The representation of P_i(u_i) in (17) is not equivalent to the set defined in (13). In (13), the affine bounds T_ij(x,u_i) ≤ T_ij ≤ T̄_ij(x,u_i) must hold for every x ∈ X_i, which is an intersection over x of interval constraints. In (17), the same affine bounds are evaluated at the single existential variable ẑ_i = [x'_i−x''_i, u_i], so the represented set is a union over admissible (x,u_i) of the interval constraints. This swaps a universal quantifier for an existential one. Consequently, Theorem 2 solves a relaxed problem in which the optimizer can choose, for each cell, the state x that makes the barrier condition easiest to satisfy, while other states in the same cell may violate (8c). The safety lower bound (9) is therefore not guaranteed by the LP solution. The stationarity condition (19e), which treats ẑ_i as an optimization variable, further confirms that the LP is solving the relaxed problem rather than enforcing the original universal constraint.","section":"V, Eq. (17)"},{"comment":"The proof does not justify the claimed zero duality gap. The inner problem after (18) is an LP only for a fixed value of ẑ_i; the outer minimization over u_i, equivalently over ẑ_i, is not shown to preserve the convex structure needed for the KKT reduction to a single LP. The stationarity condition ∂L/∂ẑ_i = 0 is asserted without taking into account the box constraints (19f); if λ_i^T H̃^{p2}_i ≠ 0, the minimizing ẑ_i would lie on the boundary of its box, and the dual would require additional dual variables for those bound constraints. The cited references on bilevel optimization do not supply the missing equivalence, and no argument is given that strong duality holds for the joint minimax problem rather than only for the inner maximization at a fixed ẑ_i.","section":"V, Theorem 2 proof"},{"comment":"The final LP (19) does not determine the control u_i. After imposing the stationarity condition (19e), the variable ẑ_i appears only in the separate bound constraints (19f) and is otherwise absent from the objective and from all other constraints. Thus the LP solution yields no information about the optimal control values u_i, and the paper provides no procedure to recover the PWC controller π(x) = u_i for x ∈ X_i. The theorem statement claims that the LP returns an optimal solution (b*,u*,β*,η*) of the problem in Theorem 1, but without a recovery map for u_i, this claim is incomplete and unsupported.","section":"V, Theorem 2"},{"comment":"Theorem 1's formulation is ambiguous: in (14) the inner maximization is written as max over T of η+Nβ, but η and β are outer decision variables, so the maximization is vacuous as written; the intended robust interpretation, in which the constraints must hold for all T ∈ P(u), is not made explicit. Additionally, Theorem 2 imposes the constraint 0 ≤ b_i ≤ 1 in (19a), which is absent from Theorem 1 and from Definition 2, and no argument is given that this restriction is without loss of optimality. Since the paper claims an exact equivalence, these points need to be clarified or proved.","section":"IV, V (Eq. (14) and (19a))"}],"minor_comments":[{"comment":"The stated dimension of h_i, R^{2(K+n+m+1)×1}, does not match the displayed vector, which has 2(K+n+m+2) rows; please correct the dimensions.","section":"V, Eq. (17)"},{"comment":"The bounds ẑ^⊥_i and ẑ^⊤_i in (17) and (19f) are never explicitly defined; please specify the lower and upper bounds on the state component x ∈ X_i and the control component u ∈ U.","section":"V, Eq. (17)"},{"comment":"The conclusion states that the method handles 'non-additive dynamics', but the model in (1) has additive noise; the intended meaning is likely nonlinear dynamics, and the wording should be corrected.","section":"VII Conclusion"},{"comment":"The table reports P_s as a lower bound from (9), but the text sometimes refers to it as 'the probability of safety'; please consistently distinguish the theoretical lower bound from the empirical Monte Carlo frequency.","section":"VI, Table I"},{"comment":"The extension to the infinite horizon claims that setting β_i = 0 for all i suffices, but feasibility of the barrier condition (15c) under β_i = 0 is not discussed and may be restrictive; please comment on this.","section":"Remark 3"}],"recommendation":"reject","confidential_remarks":"The central equivalence claim is invalid as stated because the polyhedral representation in (17) replaces a universal quantifier over x with an existential variable, so the LP in Theorem 2 solves a relaxed problem and the formal safety guarantee is not delivered. This is a load-bearing error, not a presentation issue. The paper might be salvageable with a substantially revised derivation that correctly encodes the universal constraints, but that is beyond a minor revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The core idea here is worth taking seriously: jointly synthesize a piecewise constant stochastic control barrier function and a feedback controller as a single LP. That's a genuinely useful target, and the PWC construction from the authors' earlier work is a sensible way to make the functional optimization concrete. The use of interval bound propagation to get affine under-approximations of the transition kernel is also nice, and the experiments on the linear, temperature, and unicycle examples show the method can produce safe-looking controllers quickly for modest dimensions. The paper is clearly written and the authors are open about the dependence on their prior PWC s-CBF result.\n\nThe problem is the main theorem. The step from (13)/(15d) to the polyhedral set in (17) is not just missing a proof; it is wrong in a load-bearing way. In (13), the feasible transition kernels require the bounds on T_ij to hold for every x in X_i; that is an intersection over x of the intervals. In (17), the authors introduce \tilde{z}_i = [x'_i - x''_i, u_i] as an optimization variable and impose the affine bounds for that single point. That is an existential quantifier: the LP may pick, for each cell, an x that makes the barrier condition easiest to satisfy, while other x in the same cell violate (8c). The LP is therefore solving a relaxed problem, not the minimax problem in Theorem 1. The zero-gap equivalence claimed in Theorem 2 collapses, and the safety lower bound in (9) is not certified for the synthesized controller. The stationarity condition (19e) with respect to \tilde{z}_i confirms that \tilde{z}_i is a free decision variable, which only makes sense for the relaxed problem.\n\nThere are smaller issues too. The proof of Theorem 2 is a sketch: the Lagrangian is written for the inner max, but the KKT argument never properly justifies strong duality for the combined problem, and the recovery of the optimal controller u_i from the LP solution is not spelled out (u_i is buried in \tilde{z}_i, but the constraints on it are only the box bounds). The experiments would also be stronger with a baseline comparison and error bars; the Monte Carlo results are encouraging but don't substitute for a correct certificate.\n\nNone of this is fatal to the underlying approach. The idea is plausible and could be repaired, for example by imposing the affine bounds at all vertices of each cell or by using a genuinely uniform bound. But as it stands, the central claim of exact simultaneous synthesis is not supported. This is exactly the kind of paper a serious referee should see: the problem is relevant, the approach is promising, and a rigorous revision could turn it into a solid contribution. I'd send it back for major revision rather than reject it outright.","headline":"The paper's PWC synthesis idea is attractive, but its central zero-gap LP theorem is invalid as written because the polyhedral representation in (17) swaps 'for all x' for 'exists x', so the formal safety guarantee does not follow.","tokens_in":14452,"tokens_out":3177,"would_cite":false,"duration_ms":36579,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93C55","93E20","90C05","93D30"],"pacs":[],"model":"deepseek-v4-flash","headline":"For stochastic nonlinear systems, a barrier certificate and a safe controller can be synthesized together by solving a single linear program, with no loss from convexification.","keywords":["control barrier functions","stochastic systems","piecewise constant functions","minimax optimization","dual linear programming","probabilistic safety","formal synthesis","transition kernel bounds"],"falsifier":"Pick a one-dimensional nonlinear system with a single partition cell, run the proposed LP, then sample a dense grid inside that cell and directly evaluate the original barrier inequality (8c) using numerical integration of the Gaussian transition kernel at the LP's chosen control. If any sampled x violates (8c), the polyhedral reformulation in (17) is not equivalent to the semi-infinite constraint, and the zero-gap claim cannot hold as stated.","tokens_in":13352,"feed_emoji":"🛡️","tokens_out":9092,"duration_ms":95458,"temperature":0.7,"pith_summary":"The paper tries to establish that, for discrete-time nonlinear stochastic systems with additive noise, a safe feedback controller and a piecewise constant barrier certificate can be synthesized together by solving one linear program. The key claim is that the natural minimax formulation—choose the barrier and controller to minimize the safety bound while an adversary chooses transition probabilities consistent with the dynamics—has a zero-gap dual, meaning the LP's optimum equals the original problem's optimum and no accuracy is sacrificed. If correct, the method delivers a certificate with a formal probabilistic safety guarantee, a lower bound on the probability of staying inside the safe set, without needing the barrier or controller to be fixed in advance, and it scales with standard LP solvers. This matters because most prior approaches fix one of the two objects and optimize only the other.","feed_headline":"Zero-gap LP gives barrier and controller at once","feed_subtitle":"For stochastic nonlinear systems, one optimization formally bounds the probability of staying safe.","key_machinery":"The load-bearing object is the piecewise constant stochastic control barrier function (s-CBF): $B(x) = b_i$ inside partition cell $X_i$ and $B(x) = 1$ on the unsafe set, paired with a per-cell constant controller $\\pi(x) = u_i$. Its defining condition (8c) replaces the hard expectation inequality by a sum over transition probabilities, and those probabilities are approximated from above and below by affine functions of $(x,u_i)$ via interval bound propagation. The resulting set of feasible transition vectors is a simplex, which lets the synthesis problem be written as a minimax optimization. The conversion in (17) introduces a composed vector $\\tilde{z}_i = [x, u_i]$ to express the per-cell transition-kernel constraints as a finite set of linear inequalities, and the KKT conditions then collapse the bilevel structure into one LP.","core_discovery":"The central discovery is the reduction of joint stochastic control barrier synthesis to a minimax program that is losslessly solved as a dual LP. For a K-cell axis-aligned partition of the whitened safe set, the transition probability from any cell to every other cell has an exact expression in terms of error functions. Replacing that nonlinear expression by sound affine lower and upper bounds, computed by interval bound propagation, makes the set of admissible transition kernels a simplex, and the barrier condition becomes a linear constraint in the barrier values, the per-cell controls, and an auxiliary transition vector. Theorem 2 claims the resulting LP has the same optimal value as the minimax problem, i.e., zero duality gap, so the optimal barrier and piecewise constant controller are obtained together, and Corollary 1 yields the formal safety bound $P_s \\geq 1 - (\\eta + N \\max_i \\beta_i)$.","pith_inferences":["If the zero-gap equivalence holds, the same dualization pattern should transfer to other supermartingale certificates, such as reach-avoid or moment bounds, wherever the transition kernel can be enclosed by affine bounds.","The polyhedral conversion via $\\tilde{z}_i$ is the step most likely to be sensitive to partition geometry; testing it on non-rectangular cells or cells with loose affine bounds would reveal whether the equivalence extends beyond the paper's hyper-rectangle constructions.","The dual LP could double as a verification tool: freeze the per-cell controls of an arbitrary candidate controller and optimize only the barrier values, yielding either a safety certificate or a refutation for that controller.","Comparing the formal lower bound against empirical Monte Carlo safety rates would quantify conservatism and guide adaptive partitioning as the natural next step."],"forward_implications":["For a given partition with $K$ cells, one LP run produces both the barrier values and the controller, with no iterative scheme and no pre-specified barrier.","The returned pair gives a formal lower bound on $N$-step probabilistic safety; if $1 - (\\eta + N \\max_i \\beta_i)$ meets the required threshold, the system is certified safe.","As the partition is refined, the safety probability achieved by the piecewise constant controller approaches the best value attainable by continuous s-CBFs, under the paper's convergence argument.","The method applies to nonlinear dynamics with additive Gaussian noise and bounded continuous control sets, and the affine-bounding step extends to any continuous and differentiable transition kernel.","The LP has $O(K^2)$ variables and constraints, so moderate partitions are solvable with standard LP solvers; the paper reports certificates for 2D, 3D, and 4D benchmark systems."],"supporting_citations":[{"why":"Supplies the piecewise stochastic barrier function framework, the safety bound that Corollary 1 inherits, and the convergence result as partition size grows.","marker":"[11]"},{"why":"Provides the exact transition kernel formula for hyper-rectangular cells and the interval Markov decision process context the paper extends to continuous action spaces.","marker":"[18]"},{"why":"Establishes that the transition kernel induces a unique probability measure for the stochastic system, grounding the definition of probabilistic safety.","marker":"[25]"},{"why":"Gives the lower bound $P_s \\geq 1 - (\\eta + \\beta N)$ that connects a valid s-CBF to probabilistic safety.","marker":"[27]"},{"why":"Supplies the backward-mode linear relaxation theorem used to prove that the affine bounds in Lemma 1 are sound.","marker":"[30]"},{"why":"Provides the interval bound propagation technique used to compute affine transition kernel bounds.","marker":"[28]"},{"why":"Background for Lagrangian duality and the convex optimization arguments invoked in the dual LP proof.","marker":"[31]"},{"why":"Supports rewriting the convex bilevel optimization as a single LP via KKT conditions.","marker":"[34]"}],"fun_headline_variants":["Zero-gap LP yields barrier and controller jointly","Exactly solved minimax for safe stochastic control","One LP gives safety certificate and controller","Zero-duality-gap LP for stochastic safety","Barrier and controller from a single LP"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The entire argument rests on the unproved claim that 'this inequality must hold for every point x inside a grid cell' can be exactly rewritten as a finite set of linear inequalities involving one representative point, so that any solution of the linear program automatically satisfies the original barrier condition at every x.","fun_headline_variants_meta":{"raw":{"variants":["Zero-gap LP yields barrier and controller jointly","Exactly solved minimax for safe stochastic control","One LP gives safety certificate and controller","Zero-duality-gap LP for stochastic safety","Barrier and controller from a single LP"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000126,"raw_usage":{"total_tokens":1038,"prompt_tokens":803,"completion_tokens":235,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":419,"completion_tokens_details":{"reasoning_tokens":168}},"tokens_in":419,"tokens_out":235,"duration_ms":2751,"temperature":1.0,"reasoning_tokens":168,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T18:19:40.897858+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Pick a one-dimensional nonlinear system with a single partition cell, run the proposed LP, then sample a dense grid inside that cell and directly evaluate the original barrier inequality (8c) using numerical integration of the Gaussian transition kernel at the LP's chosen control. If any sampled x violates (8c), the polyhedral reformulation in (17) is not equivalent to the semi-infinite constraint, and the zero-gap claim cannot hold as stated.","supporting_citations":[{"cited_title":"Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems,","cited_arxiv_id":null,"evidence_quote":"Provides the exact transition kernel formula for hyper-rectangular cells and the interval Markov decision process context the paper extends to continuous action spaces."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes that the transition kernel induces a unique probability measure for the stochastic system, grounding the definition of probabilistic safety."},{"cited_title":"Automatic Perturbation Analy- sis for Scalable Certified Robustness and Beyond,","cited_arxiv_id":null,"evidence_quote":"Supplies the backward-mode linear relaxation theorem used to prove that the affine bounds in Lemma 1 are sound."},{"cited_title":"Efficient Neural Network Robustness Certification with General Acti- vation Functions,","cited_arxiv_id":null,"evidence_quote":"Provides the interval bound propagation technique used to compute affine transition kernel bounds."},{"cited_title":"A Review on Bilevel Optimization: From Classical to Evolutionary Approaches and Applications,","cited_arxiv_id":null,"evidence_quote":"Supports rewriting the convex bilevel optimization as a single LP via KKT conditions."}],"review_version":1}