{"id":"32e1204b-4c15-40df-be46-7c18823f4dd8","arxiv_id":"2411.11310","paper_version":1,"verdict":"REJECT","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":5,"one_line_summary":"The simulation gap between a nominal model and a high-fidelity simulator is quantified as a state and input dependent bound via convex optimization and Lipschitz constants, then used for symbolic controller synthesis.","lead":"This paper proposes a data-driven way to quantify the gap between a simple mathematical model and a high-fidelity robot simulator, and then to fold that gap into controller design as a bounded disturbance. The goal is a formal guarantee that controllers verified on the simple model will still meet safety specifications in simulation or on the real robot.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Reported pendulum gap function γ2 is negative on part of X, contradicting Theorem 4.1 and invalidating the central formal guarantee.","rationale":"The reader's weakest_assumption focused on underestimation of the Lipschitz constants and the unverified coverage condition (3.3). Those are legitimate concerns: Theorem 4.1 requires L_1_i and L_2_i to be upper bounds on the true Lipschitz constants, and finite-data estimates are generally lower bounds unless additional coverage or global information is used. However, the most decisive issue is simpler and internal to the paper: the stated γ_2 polynomial takes negative values over X, directly contradicting the nonnegativity required of a simulation-gap function and hence invalidating Theorem 4.1 for the pendulum example. This does not rely on unknown simulator behavior or external estimation procedures; all reported numbers suffice. The SCP in (3.5) constrains only sampled points, so extrapolation to all x∈X can violate the intended bound. The paper does not verify that the coverage condition (3.3) holds, does not certify the Lipschitz constants, and does not enforce nonnegativity of the final γ_i. These are not mere presentation issues; they undermine the claimed 100% guarantee. Given the internal contradiction, the REJECT verdict stands. I chose 'partial' agreement because the reader identified the negative gap in the rationale but selected a different weakest_assumption; my load-bearing concern is the negative γ_2, which is more directly falsifiable.","tokens_in":10709,"tokens_out":5487,"duration_ms":46192,"concrete_test":"Evaluate the reported closed-form γ_2 from §6.1 at the four vertices of X=[−0.2,0.2]×[−0.5,0.5], e.g., compute γ_2(−0.2,0.5)=−0.5657(0.04)−0.0139(0.25)−0.0482(−0.1)+0.1809(−0.2)−0.0022(0.5)+0.0495≈−0.0091. If any vertex yields a negative value, the bound in Theorem 4.1 is false. To confirm repair, rerun the SCP with an explicit nonnegativity constraint q_i^T p_i(x,u)+L^(i)ε ≥0 over a dense grid covering X (or using sum-of-squares verification), and recompute L_1_i and L_2_i as certified upper Lipschitz constants per [NZ23]; the corrected γ_i must be nonnegative everywhere on X for both i=1,2.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 4.1 claims that for all x∈X and u∈U, |f̂_i(x,u)−f_i(x,u)| ≤ q_i^T p_i(x,u)+L^(i)ε, so the right-hand side defines the nonnegative simulation-gap function γ_i. In the pendulum case study (§6.1), the reported γ_2 is γ_2(x,u)=−0.5657x_1^2−0.0139x_2^2−0.0482x_1x_2+0.1809x_1−0.0022x_2+0.0495. At x=(−0.2,0.5), which lies in the stated state set X=[−0.2,0.2]×[−0.5,0.5], this evaluates to approximately −0.0091. Since |f̂_2(x,u)−f_2(x,u)| is always nonnegative, an upper bound that is negative cannot hold. This is an internal contradiction: every coefficient is reported in the paper, and the check requires only arithmetic. The quadratic is strictly concave (Hessian determinant ≈0.029>0 with negative leading diagonal), so its minimum over the rectangular box is attained at a vertex; the vertex (−0.2,0.5) indeed gives a negative value. Thus the central guarantee of a bounded, nonnegative simulation gap fails for the paper's own data. The likely source is that the SCP in (3.5) only enforces constraints at sampled points x_r, with no mechanism ensuring the extrapolated expression remains nonnegative over all of X, and no verification of the coverage condition (3.3) or of the Lipschitz estimates as true upper bounds is provided. Because the subsequent controller synthesis in (5.1) relies on this upper bound, the demonstrated invariance satisfaction in PyBullet is not backed by the claimed formal result.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a data-driven framework for quantifying the mismatch between a nominal discrete-time model f and a high-fidelity simulator model fhat by constructing a state- and input-dependent simulation-gap function gamma. The main result, Theorem 4.1, gives a Lipschitz-corrected pointwise upper bound on |fhat_i(x,u)-f_i(x,u)| under Assumption 1 and a coverage condition (3.3). This bound is then used in a robust/symbolic controller synthesis problem (5.1). Two case studies are presented: a pendulum in PyBullet and a Turtlebot in Gazebo, for which symbolic controllers are synthesized to enforce invariance and reach-while-avoid specifications, respectively.","tokens_in":11177,"tokens_out":13263,"duration_ms":124168,"significance":"The conceptual idea of treating the sim-to-real gap as a formally bounded, state/input-dependent disturbance is appealing and potentially useful for combining data-driven modeling with established robust and symbolic control techniques. The proof of Theorem 4.1 is concise and valid under its assumptions, and the convex scenario program in (3.5) is practical. The authors also report all fitted coefficients explicitly, which is good practice and makes independent arithmetic checks possible. However, the central numerical support is currently invalid: the reported pendulum gap function gamma_2 is negative on part of the state space, directly contradicting Theorem 4.1, and the key assumptions of the theorem (coverage of X by epsilon-balls and valid global Lipschitz constants) are not verified. The contribution can be considered significant only after these issues are resolved.","major_comments":[{"comment":"The reported pendulum gap function gamma_2 is negative at x=(-0.2,0.5), which lies in X=[-0.2,0.2]x[-0.5,0.5]. Using the coefficients reported in Section 6.1, gamma_2(-0.2,0.5) = -0.5657(0.04) - 0.0139(0.25) - 0.0482(-0.1) + 0.1809(-0.2) - 0.0022(0.5) + 0.0495, which evaluates to approximately -0.0091. Since the left-hand side of (4.1) is an absolute value and hence nonnegative, an upper bound that is negative cannot hold. This is an internal contradiction with Theorem 4.1, and it follows from the authors' own reported numbers. The origin is that the SCP in (3.5) enforces q_i^T p_i(x,u) only at sampled points and provides no mechanism to keep the extrapolated expression, after adding L^(i) epsilon, nonnegative over the whole box X. This invalidates the claimed formal guarantee for the pendulum case study.","section":"Section 6.1, Eq. (4.1)"},{"comment":"The proof of Theorem 4.1 depends critically on the coverage condition X subset of union of X_r from (3.3) and on L1_i and L2_i being valid Lipschitz constants. Neither is verified in the manuscript. The Lipschitz constants are reported as outputs of Algorithm 1 of [NZ23], but no argument establishes that they are true global upper bounds. In the pendulum example, the reported L2_2 = 0.168 is inconsistent with the fitted quadratic q_2^T p_2, whose gradient has norm close to 0.4 at points in X; a valid global Lipschitz constant must be at least the maximum gradient norm. If the Lipschitz constants are underestimated, the L^(i) epsilon correction in (4.1) is not valid. Similarly, no evidence is shown that the epsilon-balls around the N sampled points actually cover the full state set X. The authors should provide certificates for both conditions, or the hypotheses of Theorem 4.1 are not established.","section":"Section 4, Assumption 1 and Eq. (3.3)"},{"comment":"The controller synthesis in (5.1) treats gamma as a deterministic, state- and input-dependent disturbance bound. Because the reported gamma_2 is negative on part of X for the pendulum, the invariance satisfaction shown in Fig. 2 is not a consequence of the claimed formal bound; at best it demonstrates the behavior on particular trajectories. The paper's central claim that the simulator mismatch is formally quantified therefore lacks at least one valid complete example. A revision should include a case study in which the reported gamma is nonnegative on the entire state space and in which Assumption 1 and the coverage condition are explicitly verified.","section":"Section 5 and Section 6.1"}],"minor_comments":[{"comment":"The constant term in gamma_2 is reported as 0.0495, whereas the listed q_2^(7) = 0.0081 plus L^(2) epsilon, with L^(2) = 7.2331 + 0.1680 and epsilon = 0.0022, gives about 0.0244; this numerical inconsistency should be clarified.","section":"Section 6.1"},{"comment":"The caption of Fig. 5 refers to the 'Pybullet model' hitting obstacles, but the Turtlebot experiment is carried out in Gazebo; this should be corrected.","section":"Section 6.2 / Fig. 5"},{"comment":"In item (ii), the text says 'high-fidelity simulator Sigma', but Sigma is the nominal model; the intended symbol is probably RhatSigma.","section":"Problem 2.2"},{"comment":"The basis functions p_i^{(l)} are not formally defined in the optimization formulation; although the reported gamma functions let the reader infer them for the examples, a precise definition would improve reproducibility.","section":"Section 3"},{"comment":"There are minor typographical inconsistencies, including 'Algorithm-1' for 'Algorithm 1', and inconsistent capitalization of PyBullet/Pybullet.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The main theorem is valid under its assumptions, and the deficiencies in the numerical case studies--nonnegativity of gamma, verified coverage, and certified Lipschitz constants--can in principle be repaired within the proposed framework. I therefore recommend major revision rather than rejection. If the authors cannot supply those certificates in a revised version, the paper should then be rejected."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The idea here is genuinely useful: instead of scalar or probabilistic sim2real gaps, they construct a state/input-dependent gap function with a deterministic finite-sample certificate, then feed it into symbolic controller synthesis. That framing is new relative to the cited work, and the SCP formulation in (3.5) plus the Lipschitz-extension argument in Theorem 4.1 is a clean way to get a formal bound from finitely many simulator queries. The paper is also honest about the role of the simulator as a stand-in for reality, which is a reasonable position.\n\nThe problem is that the numerical results contradict the theorem. Theorem 4.1 guarantees a nonnegative upper bound for |f_hat_i - f_i| over all of X. The reported gamma_2 for the pendulum is a strictly concave quadratic that takes a negative value at x = (-0.2, 0.5), which is inside the stated state set. That is not a subtle issue; it means the central formal guarantee fails for the paper's own data. The likely cause is that the SCP only constrains the gap function at sampled points, and neither the coverage condition (3.3) nor the Lipschitz constants L1_2, L2_2 are ever verified as true upper bounds. The reported L2_2 = 0.168 also looks too small given the fitted quadratic's gradients over X. So the theorem is mathematically valid under Assumption 1, but the paper does not demonstrate that Assumption 1 holds, and in fact provides evidence that it does not.\n\nThere is also some circularity: the gap function is fit to data and then used to show the same simulator satisfies a specification; the formal contribution is the certificate for the fit, not an independent prediction. That is a moderate concern, but the conceptual contribution survives it.\n\nThe case-study comparison is additionally confounded by using different initial conditions with and without the gap function, which the authors acknowledge. This makes the empirical demonstration weaker than it looks, though not dishonest.\n\nBottom line: the framework is worth engaging with and likely repairable, but the paper as submitted claims a guarantee its own example violates. A serious referee should see it, but the authors need to fix the numerical verification—either recompute the constants, verify the coverage condition, or restrict X to where the gap function is actually nonnegative—before publication. I would not cite this version, but I would read a revised one.","headline":"A coherent formal framework for bounding sim2real gaps, but the paper's own pendulum numbers contradict the central guarantee—reject as-is, though the idea deserves referee time.","tokens_in":666,"tokens_out":757,"would_cite":false,"duration_ms":16209,"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":"This paper claims the sim-to-real gap can be turned into a formal, state-dependent error bound computed from simulator data.","keywords":["simulation gap","Sim2Real transfer","data-driven control","formal guarantees","symbolic control","scenario convex program","Lipschitz constants","bounded disturbance"],"falsifier":"Take a dense grid of state-input pairs that were not used when solving the scenario program, evaluate the simulator and the nominal model at each pair, and check whether $\\left|\\hat{f}_i(x,u) - f_i(x,u)\\right| \\le q_i^\\top p_i(x,u) + L^{(i)}\\epsilon$ holds everywhere; a single violation falsifies Theorem 4.1. A quicker check computes $\\sup_{x \\in X} \\|\\nabla_x \\gamma_2(x,u)\\|$ for the pendulum's reported gap and compares it with the claimed $L^{(2)}_2 = 0.168$; the fitted $\\gamma_2$ has gradients with norm up to about $0.43$, which would already contradict the Lipschitz constant used in the bound.","tokens_in":10534,"feed_emoji":"🤖","tokens_out":11421,"duration_ms":89952,"temperature":0.7,"pith_summary":"This paper tries to convert the sim-to-real gap from an informal worry into a computed, provable bound. It defines a simulation-gap function $\\gamma(x,u)$ that, for every state $x$ and input $u$, upper-bounds the difference between a simple nominal model's next-state map and a high-fidelity simulator's map. The function is learned from finitely many simulator samples by solving one convex scenario program per state dimension, and a Lipschitz argument extends the sampled bound to the entire state set. Once the gap is known, the simulator can be treated as the nominal model with a bounded, state- and input-dependent disturbance, so controllers synthesized for that disturbed model carry a guarantee that the specification holds in simulation. Because modern simulators are assumed to track reality closely, the paper presents this as a route to controllers that can move from simulation to a real system without losing their formal guarantees.","feed_headline":"Sim-to-real error gets a proven state-dependent bound","feed_subtitle":"A convex program turns simulator data into a bounded error term, letting a simple model control the simulator.","key_machinery":"The load-bearing object is the simulation-gap function $\\gamma(x,u) = (\\gamma_1(x,u), \\dots, \\gamma_n(x,u))$, with $\\gamma_i(x,u) := q_i^\\top p_i(x,u) + L^{(i)}\\epsilon$. The coefficient vector $q_i$ is obtained from the scenario convex program (3.5): minimize $\\eta_i$ subject to $q_i^\\top p_i(x_r,u) \\le \\eta_i$ and $\\left|\\hat{f}_i(x_r,u) - f_i(x_r,u)\\right| \\le q_i^\\top p_i(x_r,u)$ on the sampled points $x_r$. The basis functions $p_i(x,u)$ are user-chosen but the program is convex in $q_i$, so it is solvable in practice. The step that gives the result its formal force is the Lipschitz extension in Theorem 4.1: a bound verified on finitely many $\\epsilon$-balls around the samples is pushed to all of $X$ at the cost of the additive term $L^{(i)}\\epsilon$. On the controller side, the machinery turns the gap into a bounded disturbance by representing the simulator as $f(x,u) + [-\\gamma(x,u), \\gamma(x,u)]$, a form for which established robust and symbolic control techniques apply.","core_discovery":"The central claim is Theorem 4.1: suppose the pointwise error $\\left| \\hat{f}_i(x,u) - f_i(x,u)\\right|$ and the chosen parametric bound $q_i^\\top p_i(x,u)$ are both Lipschitz continuous in $x$ with constants $L^{(i)}_1$ and $L^{(i)}_2$. Then, from the solution of the scenario convex program in (3.5), one obtains for every $x \\in X$ and every $u \\in U$ the inequality $\\left| \\hat{f}_i(x,u) - f_i(x,u)\\right| \\le q_i^\\top p_i(x,u) + L^{(i)} \\epsilon$, with $L^{(i)} = L^{(i)}_1 + L^{(i)}_2$ and $\\epsilon$ the radius of the sample balls that cover $X$. The right-hand side is the simulation-gap function $\\gamma_i(x,u)$. The program minimizes the tightest such upper bound over the sampled points, and the Lipschitz term extends that guarantee to the unsampled region. As a consequence, the simulator model is represented as the nominal model plus a bounded, state- and input-dependent disturbance, so a controller that enforces a specification for that disturbed system also enforces it for the simulator; under the paper's Real-to-Sim fidelity assumption, the same controller is then credible for the real system.","pith_inferences":["Editorial inference: the same Lipschitz-extension scheme could certify gap functions from online trajectory data instead of an exhaustive state grid, provided the visited $\\epsilon$-balls cover the region of interest; this would make the method applicable when simulator queries are expensive.","Editorial inference: the reported Lipschitz constants are numerically checkable against the fitted gap functions; for the pendulum, comparing the supremum of $\\nabla_x \\gamma_2$ over $X$ with the stated $L^{(2)}_2 = 0.168$ (the fitted $\\gamma_2$ has gradients with norm up to roughly $0.43$) would give a direct pre-deployment test of whether the claimed bound can hold.","Editorial inference: the gap function could serve as a simulator-fidelity certificate: a simulator is adequate for a given model and specification exactly when the synthesis problem with the gap term remains feasible, and this could be used to select among available simulators.","Editorial inference: adapting the argument to stochastic simulators would mean replacing the Lipschitz extension with a probabilistic or robust version, which would soften the 100%-correctness claim; the paper does not take that step."],"forward_implications":["If the bound is correct, a controller synthesized for the nominal model with the gap function added satisfies the given specification in the high-fidelity simulator; the pendulum case shows an invariance specification that fails without the gap and holds with it.","Smaller sampling radii produce tighter gap functions, at the cost of more simulation data and more computation; the paper's table shows the maximum gap decreasing as $\\epsilon$ shrinks.","The guarantee is deterministic rather than probabilistic, covering every state and input in the bounded sets, which the paper positions against earlier sim-to-real gap quantities that carried only probabilistic guarantees.","The method lets a deliberately crude kinematic model (the Turtlebot unicycle model) absorb unmodeled physics such as mass, friction, and inertia into the gap term, so the same controller meets a reach-while-avoid specification in the Gazebo simulator.","If the high-fidelity simulator is a faithful stand-in for the real robot, the same controller can be deployed on the real system with the specification already guaranteed in simulation."],"supporting_citations":[{"why":"Supplies the data-driven scenario convex program and Algorithm 1 for estimating the Lipschitz constants that the theorem requires.","marker":"[NZ23]"},{"why":"Provides the method used in the paper to estimate the Lipschitz constants $L^{(i)}_1$ and $L^{(i)}_2$ from finite data, which enter the bound's $\\epsilon$ term.","marker":"[WZ96]"},{"why":"Defines feedback refinement relations and symbolic controller synthesis, the technique used to design the controller for the nominal-model-plus-gap system.","marker":"[RWR17]"},{"why":"Provides the SCOTS toolbox used to implement the symbolic controllers in both case studies.","marker":"[RZ16]"},{"why":"Prior work that quantifies the sim2real gap as a numerical value with a probabilistic guarantee; the paper contrasts its own state- and input-dependent, 100%-correctness gap against it.","marker":"[AUA23]"},{"why":"Supplies the PyBullet simulator used to collect high-fidelity pendulum data.","marker":"[CB21]"},{"why":"Supplies the Gazebo simulator used to collect high-fidelity Turtlebot data.","marker":"[KH04]"}],"fun_headline_variants":["Data-driven bound quantifies sim-to-real gap formally","Rigorous sim-gap bounds for trustworthy real-world control","Turning simulator data into a provable control bound","Formal guarantee: simulator error is a bounded disturbance"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The guarantee rests on the assumption that the simulator-vs-model error and the fitted gap function both change at a known, finite rate over the entire state region, and that the sampled balls truly cover that region; if the true error changes faster than the estimated rate or a region is left uncovered, the uniform bound can fail.","fun_headline_variants_meta":{"raw":{"variants":["Data-driven bound quantifies sim-to-real gap formally","Rigorous sim-gap bounds for trustworthy real-world control","Turning simulator data into a provable control bound","Formal guarantee: simulator error is a bounded disturbance"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001327,"raw_usage":{"total_tokens":5417,"prompt_tokens":979,"completion_tokens":4438,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":595,"completion_tokens_details":{"reasoning_tokens":4386}},"tokens_in":595,"tokens_out":4438,"duration_ms":28845,"temperature":1.0,"reasoning_tokens":4386,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T18:40:44.115263+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a dense grid of state-input pairs that were not used when solving the scenario program, evaluate the simulator and the nominal model at each pair, and check whether $\\left|\\hat{f}_i(x,u) - f_i(x,u)\\right| \\le q_i^\\top p_i(x,u) + L^{(i)}\\epsilon$ holds everywhere; a single violation falsifies Theorem 4.1. A quicker check computes $\\sup_{x \\in X} \\|\\nabla_x \\gamma_2(x,u)\\|$ for the pendulum's reported gap and compares it with the claimed $L^{(2)}_2 = 0.168$; the fitted $\\gamma_2$ has gradients with norm up to about $0.43$, which would already contradict the Lipschitz constant used in the bound.","supporting_citations":[],"review_version":1}