{"id":"938d1b78-3129-4dc6-aa78-cabcb4c46840","arxiv_id":"2501.01191","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A sampling-based method constructs interval Markov decision process abstractions for nonlinear stochastic systems, enabling synthesis of control policies with PAC reach-avoid guarantees.","lead":"The paper shows how to build a finite decision model of a nonlinear control system using only sample transitions, noise samples, and a known bound on how fast the dynamics change, then uses that model to synthesize controllers with probability guarantees. It matters because it extends formal, provable controller synthesis to systems whose equations are only partially known.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Equation (10) does not overapproximate λ* outside [1,2]; the action-enabling step can enable actions with target sets too small, breaking the abstraction's soundness guarantee.","rationale":"The paper's central claim (Corollary 10) is that, with high probability over noise samples, the robust value of the data-driven IMDP lower-bounds the reach-avoid probability of a refined policy on the original nonlinear stochastic system. This claim rests on the soundness of the abstraction: for every enabled action and every concrete state in the corresponding region, there must exist a control input steering the nominal dynamics into the action's target set. The action-enabling algorithm in Section 4 is the only mechanism establishing this, and it relies entirely on Eq. (10) to upper-bound the minimal scaling factor λ*. A direct analysis of r_j(x',λ) as the minimum of affine functions shows it is concave, so linear interpolation between λ=1 and λ=2 underestimates λ* whenever the required radius is below r_j(x',1) or above r_j(x',2). In those regimes, the computed λ_i→j can be too small, the union of the sets A_j(x) need not cover R_i, and the implication '∪φ = R_i ⇒ R_i ⊆ Pre(R_j(λ_i→j))' fails. This invalidates Lemma 13 and the PAC policy-synthesis guarantee. The flaw is localized and fixable (binary search for λ*, or clamping to [1,2] with a conservative λ=1), so conditional acceptance is the right disposition rather than rejection. Independent support for the rest of the framework is solid: the Clopper-Pearson interval construction (Theorem 9) is standard, Theorem 7 is correct conditional on a valid λ, and the alternating simulation argument in Appendix A is standard. The reader's weakest_assumption identifies exactly this step; the present stress-test confirms it with a concavity argument and a concrete falsifiability check. A secondary issue, the inconsistent β formula in the experimental section, would also need correction but is not the load-bearing concern for the central guarantee.","tokens_in":20661,"tokens_out":16395,"duration_ms":139164,"concrete_test":"Implement a direct counterexample check: take R_j(λ) = {x : x≤λ, y≤λ, x+y≤λ+1} with center d=(0,0) and x'=(0.5,0.5); compute r_j(x',1) and r_j(x',2), choose C=0.9·r_j(x',1), then compute λ+ via Eq. (10) and λ* by binary search on r_j(x',λ)=C. If λ+ < λ*, the claimed overapproximation is false. Then run Algorithm 1 on the car-parking benchmark and post-verify for every enabled action (s_i, a_j) that each voxel φ⊆R_i is contained in A_j(x) for some sample (x,u,x')∈D_K(R_j) at the chosen λ_i→j; any violation confirms the unsoundness in practice.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Eq. (10) claims λ+ ≥ λ*, where λ* is the minimal scaling such that voxel φ ⊆ A_j(x). Since r_j(x', λ) is the minimum of affine functions of λ (one per polytope facet), it is concave. Linear interpolation between λ=1 and λ=2 therefore lies below r_j on [1,2] and above r_j outside [1,2]. Consequently, λ+ ≥ λ* holds only when the required radius C lies between r_j(x',1) and r_j(x',2). When C < r_j(x',1) (so λ* < 1) or C > r_j(x',2) (so λ* > 2), Eq. (10) yields λ+ ≤ λ*, i.e., a lower bound rather than an upper bound, and λ+ can even be negative. Algorithm 1 then sets λ_i→j = max_φ min_sample λ+ and enables the action whenever λ_i→j ≤ Λ, without re-checking that every voxel is covered at that λ. The computed λ_i→j can be strictly smaller than the true required scaling, so R_j(λ_i→j) is too small, Pre(R_j(λ_i→j)) may not cover R_i, and the policy refinement in Eq. (8) may be undefined for some x. This breaks Lemma 13 and the soundness underpinning Corollary 10. The paper provides no proof of Eq. (10), and the asserted inequality is false in general; a correct implementation would compute λ* by binary search on r_j(x', λ) or clamp λ to [1,2].","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript proposes a data-driven abstraction framework for discrete-time nonlinear stochastic systems with additive noise and unknown noise distribution. It constructs an interval MDP (IMDP) by using forward samples of the nominal dynamics to underapproximate backward reachable sets and to decide which abstract actions are enabled, and by using Clopper-Pearson confidence intervals on noise samples to bound transition probabilities. The authors claim PAC-style lower bounds on concrete reach-avoid probabilities via a probabilistic alternating simulation relation, and they demonstrate the method on an inverted pendulum, a nonlinear oscillator, and a car-parking benchmark. The main theoretical claim is Corollary 10: with probability at least max(0, 1 - beta * |S|^2 * |Act|) over the noise samples, the robust reach-avoid value of the IMDP lower-bounds the reach-avoid probability of the refined policy on the original system.","tokens_in":21000,"tokens_out":13610,"duration_ms":135558,"significance":"If the correctness argument were complete, this would be a useful contribution: it extends sampling-based formal abstraction from linear or known dynamics to Lipschitz nonlinear systems with additive stochastic noise, and the use of Clopper-Pearson intervals over the scenario approach is well motivated by tighter empirical intervals. The paper also ships detailed proofs for Theorems 5, 7, and 9, and the experimental section reports abstraction sizes, runtimes, and comparisons in a reproducible way. However, the central soundness claim currently rests on an unproved and, in general, false inequality in Eq. (10). Because that step is load-bearing for the action-enabling procedure, Lemma 13 and Corollary 10 are not established as written.","major_comments":[{"comment":"The displayed inequality lambda+ >= lambda* is asserted without proof and is false in general. For a fixed sample (x, u, x'), the function r_j(x', lambda) is the distance from x' to the boundary of the scaled polytope R_j(lambda), and because R_j(lambda) is defined by the affine inequalities in Definition 2, r_j(x', lambda) is the minimum of affine functions of lambda and hence concave. Eq. (10) uses the secant line through lambda = 1 and lambda = 2. For a concave function the chord lies below the graph on [1,2] and the extrapolated secant lies above the graph outside [1,2]. Consequently, lambda+ is an upper bound on lambda* only when lambda* lies in [1,2]. When the required radius C = ||J^+(Ri) * (|x - c_phi| + delta_phi)||_infinity is below r_j(x',1) (so lambda* < 1) or above r_j(x',2) (so lambda* > 2), Eq. (10) gives lambda+ <= lambda*, and lambda+ can even be negative. Algorithm 1 then computes lambda_i->j = max_phi min_sample lambda+ and can enable an action at a value of lambda_i->j for which the target set R_j(lambda_i->j) is too small to cover the voxel. In that case the premise of Theorem 7 is not met, the inclusion R_i subset of Pre(R_j(lambda_i->j)) can fail, Lemma 13 breaks down, and the soundness underpinning Corollary 10 is invalidated. A correct implementation should compute lambda* by binary search on r_j(x', lambda), or else use a safe overapproximation that is valid on all of [0, Lambda].","section":"Section 4, Eq. (10)"},{"comment":"The min over samples in Eq. (11), and the subsequent choice of the control input in the policy-refinement paragraph, must be restricted to samples (x, u, x') with x in R_i. As written, Eq. (11) minimizes over all samples in D_K(R_j), and the text says the refined policy chooses the input u attaining the minimal lambda+ over all samples in Eq. (11). If the minimizing sample has x outside R_i, Theorem 7 gives no guarantee that the chosen u steers points in the current voxel into R_j(lambda_i->j), so the refined policy in Eq. (8) may be undefined and condition (2) of Definition 11 may fail. The pseudocode in Algorithm 1 already contains an 'if x in R_i' guard, so this may be a presentation gap rather than an intrinsic flaw, but the formal statements and the policy-refinement argument need to impose the restriction explicitly.","section":"Section 4, Eq. (11) and policy refinement paragraph"}],"minor_comments":[{"comment":"The sentence 'any underapproximation preserves correction of our abstraction' should read 'preserves the correctness of our abstraction'.","section":"Section 3.1"},{"comment":"The notation r_j(x',1) and r_j(x',2) is used before Definition 6 introduces r_j(x', lambda); please state explicitly that these are the radii from Definition 6 evaluated at lambda = 1 and lambda = 2.","section":"Section 4, Eq. (10)"},{"comment":"In the proof of Theorem 5, the maxima are written over x in R^l; this should be over x in R_i, the region under consideration.","section":"Appendix B"},{"comment":"The sentence 'The factor of |S|^2 * |Act| in Theorem 10' should refer to Corollary 10, not Theorem 10.","section":"After Corollary 10"},{"comment":"The phrase 'Since union over phi of phi = R_i' is missing the index set; it should read 'Since union over phi in Phi(R_i) of phi equals R_i'.","section":"Section 4"},{"comment":"The caption uses the notation B^infinity_{r(.)(x')}(x') and A_j(x) without defining the subscript function r(.); aligning this notation with Definition 6 would improve readability.","section":"Figure 1"}],"recommendation":"major_revision","confidential_remarks":"The contribution is appropriate for the venue and the experiments are solid, but the soundness claim is not yet established because of the unproved and generally false inequality in Eq. (10). This is a fixable algorithmic issue: replacing the linear-interpolation formula with a binary search on lambda, or with a provably conservative overapproximation valid on [0, Lambda], would likely resolve the central concern. I therefore do not recommend rejection, but a major revision is needed before the PAC guarantee can be trusted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper extends Badings et al.'s sampling-based IMDP abstraction from linear to nonlinear dynamics by using Lipschitz/Jacobian balls to underapproximate backward reachable sets and Clopper-Pearson intervals to bound transition probabilities. The combination is genuinely new, and the PAC abstraction idea is plausible. Theorems 5 and 7 are proved, and the policy-refinement story is clear.\n\nThe soft spot is Eq. (10), the formula for λ+, which the paper asserts without proof to be an upper bound on the minimal scaling λ* that puts a voxel inside the backward-reachable underapproximation. That assertion is not generally true. The function r_j(x', λ) is the minimum of affine functions of λ, hence concave. Linear interpolation between λ=1 and λ=2 gives a chord that lies below r on [1,2] and above it outside. So λ+ ≥ λ* holds only when the required radius falls between r(1) and r(2). When λ* < 1 or λ* > 2, λ+ can be smaller than λ*, and Algorithm 1 can enable an action with a target set too small to cover the voxel. That breaks Lemma 13 and the soundness of Corollary 10. The fix is straightforward: compute λ* by binary search on r_j(x', λ) (monotone in λ), or clamp λ to [1,2] and check coverage explicitly. I would want to see that correction before trusting the guarantees.\n\nTwo smaller issues. The experiments set β = 1 - 0.05/T per transition, but Corollary 10's union bound uses |S|^2|Act|, not T; the claimed overall confidence of 0.95 does not follow for the IMDPs actually built. No code or data is included, which makes the empirical comparison hard to reproduce.\n\nOverall, the core approach is worth engaging with. The scaling bug is load-bearing but local and repairable. I recommend sending this to serious peer review, with the requirement that the scaling computation be fixed and the beta formula corrected. A careful reader can learn something about data-driven backward reachability even with the flaw.","headline":"Useful data-driven abstraction for nonlinear stochastic systems, but the unproved scaling formula in Eq. (10) can break soundness; fixable with a proper one-dimensional search.","tokens_in":21522,"tokens_out":3967,"would_cite":false,"duration_ms":32952,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93E20","93C10","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Formal control policies for stochastic nonlinear systems can be synthesized from data samples alone, with probably approximately correct reach-avoid guarantees.","keywords":["data-driven abstraction","interval MDP","stochastic nonlinear systems","reach-avoid specification","PAC guarantees","backward reachability","Clopper-Pearson interval","policy synthesis"],"falsifier":"Fix a scalar system, say $f(x)=ax$ with target interval $R_j=[0,1]$, a voxel away from $x'$, and a sample with $x'\\in R_j$; compute $\\lambda^+$ from Eq. (10) and the exact $\\lambda^\\star=\\inf\\{\\lambda: \\phi\\subseteq A_j(x)\\}$ (e.g. by bisection on $r_j(x',\\lambda)$). Exhibit any case with $\\lambda^+<\\lambda^\\star$: then the action-enabling step can enable $a_j$ while the target set is too small, invalidating the soundness of the abstraction that Corollary 10 relies on.","tokens_in":20430,"feed_emoji":"🎛️","tokens_out":13575,"duration_ms":109238,"temperature":0.7,"pith_summary":"Many real-world control tasks involve nonlinear dynamics with unknown stochastic noise, where classical model-based synthesis is impossible. The paper claims that samples of the system's deterministic part and of its noise are enough to build a finite interval Markov decision process (IMDP) abstraction, and that policies synthesized on this abstraction transfer to the original system with a probably approximately correct (PAC) reach-avoid guarantee. The key result is that, with high confidence over the collected samples, the robust reach-avoid value computed on the IMDP is a lower bound on the true probability of the refined policy on the concrete system. This provides a route to formal, guaranteed controller synthesis from black-box data rather than from a known model.","feed_headline":"Sample-based synthesis gives provable reach-avoid controls","feed_subtitle":"Even with unknown dynamics and noise, an interval MDP abstraction turns black-box samples into a formal guarantee.","key_machinery":"The central object is the scaled polytope $R_j(\\lambda)$ --- region $R_j$ shrunk or enlarged about its centre --- which defines an abstract action through its backward reachable preimage $\\mathrm{Pre}(R_j(\\lambda))$. The data-driven mechanism replaces exact preimage computation with the certified underapproximation $A_j(x)=\\{y\\in R_i : \\|J^+(R_i)|x-y|\\|_\\infty\\le r_j(x',\\lambda)\\}$, where $J^+(R_i)$ is the entry-wise maximum absolute Jacobian of $f$ over $R_i$ and $r_j(x',\\lambda)$ is the radius of the largest $L^\\infty$ ball contained in $R_j(\\lambda)$ around a sampled successor $x'$; Theorem 7 guarantees $A_j(x)\\subseteq \\mathrm{Pre}(R_j(\\lambda))$. On the stochastic side, the Clopper--Pearson confidence interval converts counts of noise samples into per-transition probability intervals valid with confidence $1-\\beta$. A probabilistic alternating simulation relation --- a behavioural matching between IMDP and system under a concrete policy --- then lets the abstract robust value compose with the PAC probability intervals to yield the transfer guarantee of Corollary 10.","core_discovery":"For a discrete-time nonlinear system $x_{k+1}=f(x_k,u_k)+w_k$ with differentiable $f$, known local Jacobian bounds $J^+(R_i)$, and unknown additive i.i.d. noise $w_k\\sim\\mathbb{P}$, the paper constructs a finite interval MDP purely from samples of $f$ and of $\\mathbb{P}$. Each abstract action $a_j$ in state $s_i$ corresponds to a target polytope $R_j(\\lambda_{i\\to j})$ scaled around its centre; using the Jacobian bound, every forward sample $(x,u,x')$ with $x'\\in R_j(\\lambda_{i\\to j})$ is inflated into a ball $A_j(x)$ that provably underapproximates the backward reachable set $\\mathrm{Pre}(R_j(\\lambda_{i\\to j}))$ (Theorem 7), and a voxel-covering loop over the region $R_i$ decides when $a_j$ is enabled. Transition probability intervals are obtained by applying the Clopper--Pearson two-sided binomial interval to counts of noise samples (Theorem 9, Eq. (14)). Under the probabilistic alternating simulation relation of Definition 11, Corollary 10 asserts that for every scheduler $\\sigma$ of the IMDP there is a policy $\\pi$ of the concrete system such that, with probability at least $1-\\beta|S|^2|\\mathrm{Act}|$ over the samples, $\\min_{P\\in\\mathcal{P}}\\Pr^{\\mathrm{MI}'}_{\\sigma,P}(S_G,S_U,h) \\le \\Pr^{S}_{\\pi}(X_G,X_U,h)$, i.e., the robust reach-avoid value of the abstraction is a lower bound on the true reach-avoid probability.","pith_inferences":["The same alternating-simulation machinery should extend to specifications beyond reach-avoid, such as safety or $\\omega$-regular objectives, since the relation preserves PCTL-style properties; the paper's proof route is not specific to reach-avoid arithmetic.","Treating the known Jacobian bound $J^+(R_i)$ as a form of model knowledge, a purely sample-only variant would need to estimate these bounds from data, adding a second PAC layer that the current guarantee does not cover.","The voxel-covering structure of Algorithm 1 suggests an adaptive refinement extension: when the action-enabling check fails locally, subdividing only the undercovered voxels would improve the action set at lower sample cost than a global refinement.","A natural follow-up is to compute upper bounds on the reach-avoid probability as well, converting the one-sided lower-bound certificate into an interval-valued guarantee; the probability-interval machinery already yields both sides of each transition interval."],"forward_implications":["For every IMDP scheduler there exists a concrete policy whose reach-avoid probability is at least the robust IMDP value, with confidence $1-\\beta|S|^2|\\mathrm{Act}|$ over the sample set (Corollary 10).","Increasing the number of noise samples $N$ tightens the Clopper--Pearson intervals and raises the guaranteed reach-avoid probability, as the experiments show.","The maximum scaling factor $\\Lambda$ trades abstraction richness for performance: setting $\\Lambda=1$ drops the guaranteed reach-avoid probability to zero on the pendulum and oscillator benchmarks, while larger $\\Lambda$ improves it.","Clopper--Pearson intervals dominate the scenario-approach intervals on all three benchmarks, giving higher reach-avoid guarantees with the same number of samples $N=1{,}000$ or $N=10{,}000$."],"supporting_citations":[{"why":"Supplies the policy-synthesis theorem (Theorem 4/14) that transfers IMDP schedulers to concrete policies via an alternating simulation relation.","marker":"Badings et al. (2023b)"},{"why":"The predecessor IMDP abstraction framework for linear known dynamics; the paper extends it to nonlinear systems and uses it as the scenario-approach baseline.","marker":"Badings et al. (2023a)"},{"why":"Provides the two-sided binomial confidence interval used as Theorem 9 to bound each transition probability.","marker":"Clopper and Pearson (1934)"},{"why":"Establishes that Clopper-Pearson intervals are tighter than scenario-approach intervals, motivating the statistical choice at the core of the method.","marker":"Meggendorfer et al. (2024)"},{"why":"Introduces alternating simulation relations, the correctness foundation for the abstraction in Appendix A.","marker":"Alur et al. (1998)"},{"why":"Gives the robust value iteration algorithm used to compute the optimal IMDP scheduler in Eq. (3).","marker":"Wolff et al. (2012)"},{"why":"Defines interval MDPs, the abstract model on which the entire construction is built.","marker":"Givan et al. (2000)"}],"fun_headline_variants":["Data samples yield formal controllers for noisy nonlinear systems","PAC guarantees for reach-avoid from black-box samples","Interval MDP abstractions from samples ensure formal control","Learn control policies with proofs from noisy data"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole guarantee rests on the unproven claim that Eq. (10) always produces a scaling factor $\\lambda^+$ that overestimates the exact minimal scaling $\\lambda^\\star$ required for a voxel to be covered, and this can fail when the exact scaling is below 1.","fun_headline_variants_meta":{"raw":{"variants":["Data samples yield formal controllers for noisy nonlinear systems","PAC guarantees for reach-avoid from black-box samples","Interval MDP abstractions from samples ensure formal control","Learn control policies with proofs from noisy data"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000526,"raw_usage":{"total_tokens":2604,"prompt_tokens":1072,"completion_tokens":1532,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":688,"completion_tokens_details":{"reasoning_tokens":1472}},"tokens_in":688,"tokens_out":1532,"duration_ms":10210,"temperature":1.0,"reasoning_tokens":1472,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T22:37:37.601718+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Fix a scalar system, say $f(x)=ax$ with target interval $R_j=[0,1]$, a voxel away from $x'$, and a sample with $x'\\in R_j$; compute $\\lambda^+$ from Eq. (10) and the exact $\\lambda^\\star=\\inf\\{\\lambda: \\phi\\subseteq A_j(x)\\}$ (e.g. by bisection on $r_j(x',\\lambda)$). Exhibit any case with $\\lambda^+<\\lambda^\\star$: then the action-enabling step can enable $a_j$ while the target set is too small, invalidating the soundness of the abstraction that Corollary 10 relies on.","supporting_citations":[{"cited_title":"Henzinger, Orna Kupferman, and Moshe Y","cited_arxiv_id":null,"evidence_quote":"Introduces alternating simulation relations, the correctness foundation for the abstraction in Appendix A."},{"cited_title":"Leach, and Thomas L","cited_arxiv_id":null,"evidence_quote":"Defines interval MDPs, the abstract model on which the entire construction is built."}],"review_version":1}