Pith. sign in

REVIEW 3 major objections 3 minor 24 references

Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks

T0 review · 3 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A Q-network satisfying two self-consistency conditions is a provably safe model-free filter.

desk verdict A correct sufficient-condition theorem and a plausible architecture, but the formal verification claim for the nonlinear benchmarks is not backed by the text. read the letter →

arxiv 2506.15693 v1 pith:J7KPIHI3 submitted 2025-05-27 cs.LG

Jiaxing Li , Hanjiang Hu , Yujie Yang , Changliu Liu This is my paper
classification cs.LG
keywords model-freesafetyfiltersHamilton-JacobireachabilityQvaluefunctionsformalverificationmixed-integerquadraticallyconstrainedprogrammingmultiplicativeneuralnetworksforwardinvariancesafeset
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Learning-based safety filters adapt to complex constraints but usually come with no formal guarantee. This paper claims a sufficient condition that closes that gap: an action-value network $Q(x,u)$ is a certified model-free safety filter if its zero-sublevel set satisfies two properties, which the authors call constraint satisfaction and forward invariance. The paper proposes a multiplicative Q-network, $Q(x,u)=Z_1(x)^{\top}Z_2(x,u)$, whose inner-product structure mirrors the bilinear term in a Hamilton-Jacobi reachability value, and argues this prevents the safe set from collapsing during verification-guided training. It then encodes the two properties as a mixed-integer quadratically constrained program and reports verified, non-empty safe sets on four control benchmarks: double integrator, 2D double integrator, unicycle, and robot arm.

What carries the argument

The load-bearing object is the multiplicative Q-network, defined by $Q(x,u)=Z_1(x)^{\top}Z_2(x,u)$, where $Z_1$ is a state-only branch and $Z_2$ is a state-control branch, with the two embeddings joined by an inner product. This form mirrors the bilinear term $L_gV(x)\,\Delta t\,u$ that appears when the HJ value function is expanded along the dynamics, and the paper argues it is what keeps the zero-sublevel set from shrinking during counterexample-guided fine-tuning. Verification is carried out by encoding each ReLU activation with linear constraints and binary variables and the multiplication layer as the quadratic constraint $y=Z_1(x)^{\top}Z_2(x,u)$, producing a mixed-integer quadratically constrained program whose feasibility is checked with a solver. To certify forward invariance without enumerating the control set, the pipeline trains a policy network $\pi_\phi$ to make $Q(x,\pi_\phi(x))$ small; the check $Q(f(x,u),\pi_\phi(f(x,u)))\le 0$ is a sound sufficient test for the existence of a safe next action, since the minimum over actions is no larger than that value. Pre-activation bounds that make the encoding finite come from interval arithmetic and linear symbolic bound propagation.

What would settle it

Sample the reported verified safe set for the unicycle densely and simulate the closed loop under the trained policy at high precision: finding any pair with $Q(x,u)\le 0$ whose true next state violates the constraint, or for which no candidate action keeps $Q\le 0$, would refute the central soundness claim.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is Theorem 1: a function $Q: X \times U \to \mathbb{R}$ is a valid model-free safety filter whenever (i) $Q(x,u) \le 0$ implies $h(x) \le 0$, and (ii) whenever $Q(x,u) \le 0$, there exists $u'$ with $Q(f(x,u),u') \le 0$. Given those two conditions, the zero-sublevel set $I=\{(x,u) : Q(x,u)\le 0\}$ is a control-dependent safe set, and any trajectory that keeps selecting actions with $Q(x_t,u_t)\le 0$ never leaves the constraint set $\{h\le 0\}$. The paper argues that discounted HJB learning alone does not deliver these conditions, and that the multiplicative network combined with MIQCP verification makes them checkable in practice. The reported experiments show verified safe sets of non-trivial size on all four benchmarks, while a fully connected baseline's verified set collapses to empty on three of them.

Load-bearing premise

The solver's 'no counterexample' answer is only a safety certificate if the mixed-integer program exactly represents the successor map, the policy network, and the safety constraint; for the nonlinear benchmarks the paper does not provide such an encoding, so an infeasible answer may certify only the encoded approximation.

Editorial extensions

If this is right

  • A verified network's zero-sublevel set is an invariant safe set: starting with any pair with $Q(x_0,u_0)\le 0$, repeatedly picking actions with $Q(x_t,u_t)\le 0$ keeps the state forever in $\{h\le 0\}$, with no online use of the dynamics model.
  • The trained policy $\pi_\phi$ provides a witness for forward invariance during verification, so the pipeline never needs exhaustive control search to certify that a safe continuation exists.
  • The multiplicative architecture is what prevents safe-set collapse: the paper reports that the fully connected baseline's verified safe set is empty on the unicycle and robot arm tasks, while the proposed network keeps a verified set on all four benchmarks.
  • The certified safe set is sound but conservative: for the double integrator it lies strictly inside the true maximum safe invariant set computed from the HJB equation, so the guarantee is not a completeness result.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The soundness of the nonlinear benchmarks rests on an encoding of the successor map, the policy network, and the safety constraint inside the mixed-integer program that the paper does not exhibit; until such an encoding is supplied, the unicycle and robot-arm results are best read as certificates of the encoded program.
  • Because the two conditions are sufficient but not necessary, a verification scheme with a tighter relaxation of $\min_{u'}Q$ could certify larger safe sets for the same learned network, separating approximation loss from the network's actual safety margin.
  • The multiplicative parameterization is not tied to safety filters; it could plausibly improve verifiable training of other value-based certificates, such as Lyapunov or contraction functions, wherever bilinear state-control terms appear.
  • Comparing the verified unicycle set against a dense grid-computed Hamilton-Jacobi reachable set would quantify the conservativeness added by each pipeline stage and provide a direct test of the verification soundness claim.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 3 minor

Summary. The paper proposes verifiable sufficient conditions for a learned action-value function Q to act as a model-free safety filter: constraint satisfaction and forward invariance. It introduces a multiplicative Q-network architecture intended to mitigate zero-sublevel-set shrinkage, and a post-hoc certification pipeline based on mixed-integer quadratically constrained programming (MIQCP), with adversarial fine-tuning using counterexamples. Experiments report verified safe-set sizes on four benchmarks: double integrator, 2D double integrator, unicycle, and robot arm.

Significance. If the certification pipeline were fully specified, this would be a valuable contribution. Theorem 1 is a correct sufficient condition, and the post-hoc verification approach is not circular with respect to the fitted parameters: the certificate is checked after training and can only be conservative. The multiplicative Q-network is a reasonable architectural response to a real empirical problem. However, the core claim that the pipeline 'successfully synthesizes formally verified, model-free safety certificates' is not supported for the nonlinear benchmarks, because the verification query is not instantiated for the dynamics, the constraint, or the policy network. The theoretical result is sound, but the experimental certification claim needs substantial additional support.

major comments (3)
  1. [IV-C] The MIQCP formulation in equations (20a)-(20n) and the earlier query (15) encode only the multiplicative Q-network: the ReLU activations, the bilinear product, and the inequalities Q(x,u)<=0 and h(x)>=0. The text states that the forward-invariance check 'follows the same constraint encoding and replacing h(x) with Q(f(x,u), pi_phi(f(x,u)))', but no encoding is given for the dynamics f, the constraint h, or the policy network pi_phi. For the unicycle, f contains cos and sin terms; for the robot arm, h involves trigonometric functions of joint angles. Gurobi 11.0.2 does not support transcendental functions, and the paper provides no sound polynomial or trigonometric enclosure with rigorous error bounds. Consequently, the infeasibility results reported in Section IV-C and the verified safe-set sizes in Table I for the unicycle (0.6900) and robot arm (0.4957) cannot be taken as certificates of the original continuous conditions. This is load-bearing because the central claim of the paper is the existence of formally verified certificates.
  2. [IV-C] Definition 6 defines a violation through strict inequalities (y1<0, y2>0), while the concrete MIQCP in (20m)-(20n) uses the non-strict conditions Q(x,u)<=0 and h(x)>=0. These are not logically equivalent: a counterexample with Q(x,u)=0 and h(x)>0 is included in the MIQCP but excluded from the formal feasibility condition. The paper should state the exact non-strict formulation of the feasibility problem and prove that checking it is equivalent to the sufficient conditions in Theorem 1. As written, the formal definition and the executed verification query may be checking different properties.
  3. [IV-C, IV-D] The replacement of min_{u'} Q(f(x,u),u') by Q(f(x,u), pi_phi(f(x,u))) in the verification query is underspecified. The sound direction is clear: verifying Q(f(x,u), pi_phi(f(x,u)))<=0 implies the minimum is <=0. But a query that reports a 'violation' when Q(f(x,u), pi_phi(f(x,u)))>0 is not a violation of forward invariance, because another control could achieve a non-positive value. The paper must state the universally quantified condition being checked, specify how the policy network appears in the MIQCP (including its ReLU encoding), and explain how an infeasibility result from that query certifies the original condition. This is needed for both the double integrator and the nonlinear benchmarks.
minor comments (3)
  1. [IV-B] Equation (9) introduces V(f(x,u)) without defining the state-value function V in the context of Q; the derivation from (9) to (11) is informal and should be clarified or removed if it is only motivational.
  2. [Definition 5 / Theorem 1] Definition 5 requires h(xt)<0 for all t, while Theorem 1's proof only establishes h(xt)<=0 under constraint satisfaction. The strict-versus-non-strict distinction should be made consistent.
  3. [V-B / Table I] No experimental variation or seed information is reported; Table I and Figure 2 present single-run safe-set sizes, so the reader cannot assess the variability of the proposed method or the claim that the baseline 'cannot be verified without collapsing.'

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the safety-filter conditions, the MIQCP formulation, and the policy lower-bound argument are self-contained; the nonlinear-dynamics encoding gap is a soundness risk, not a circular reduction.

full rationale

Theorem 1 states sufficient conditions for a Q-function to be a model-free safety filter and proves them directly from Definition 4; it does not import its conclusion from a fitted parameter or from a self-citation. The verification pipeline checks the two conditions post hoc on the trained network, and the policy network πϕ is used only through the sound implication Q(x',πϕ(x')) ≤ 0 ⇒ min_u' Q(x',u') ≤ 0, which holds for any policy and therefore cannot force the certificate by construction. Self-citations ([22], [7], [8], [20]) are used as software/tooling or as background on verification-guided training, not as the authority for the paper's central mathematical claim. The one serious concern in the manuscript is that equations (15) and (20) only spell out the ReLU and bilinear-product encoding of Q; for the unicycle and robot arm benchmarks no rigorous MIQCP encoding of f(x,u), h(x), or πϕ is provided, so the reported 'verified' sets for those tasks may not certify the original continuous conditions. That is a soundness/completeness gap in the instantiation, not a circularity: the sufficient conditions remain independent of the learning procedure, and no prediction is defined in terms of the fitted network values. Hence the circularity score is 0.

Assumptions & free parameters 4 free parameters · 6 assumptions · 0 invented entities

The formal guarantee rests on the MIQCP being an exact representation of Theorem 1's conditions. The ledger shows that the paper only specifies the encoding for the Q network itself in equation (20). The dynamics, constraint, and policy encodings are missing assumptions for the nonlinear benchmarks, so the empirical 'verified' claims are not backed by a complete derivation.

free parameters (4)
  • MIQCP solver tolerance and time limit
    The paper does not report Gurobi tolerances or time limits; the 'verified' status depends on solver infeasibility proofs whose floating-point rigor is unstated.
  • safe set size measure
    Table I and Figure 2 report 'safe set size' percentages without defining the underlying measure or sampling procedure, so the numbers are not reproducible.
  • network hyperparameters (hidden sizes 32/32, embedding 8)
    Chosen by hand; they affect MIQCP tractability and the reported safe-set sizes, though not the theoretical soundness of Theorem 1.
  • discount factor gamma
    Used in the pretraining loss in equation (8); its value is not reported and it shapes which Q network the fine-tuning starts from.
assumptions (6)
  • domain assumption Dynamics f is deterministic, bounded, Lipschitz, and known exactly for verification.
    Equation (1) and the verification queries (12)-(15) assume exact access to f; for the unicycle benchmark this trigonometric dynamics must be encoded in the MIQCP, which is not shown.
  • domain assumption Constraint h is piecewise smooth with closed, connected zero-sublevel set and is exactly representable in MIQCP.
    Section III assumes h is piecewise smooth; Section IV-C encodes h(x) in the constraint satisfaction query but no encoding for nonlinear h, such as distance constraints, is given.
  • standard math The ReLU encoding in equations (20c)-(20k) with pre-activation bounds exactly represents the Q network.
    The big-M constraints rely on valid lower and upper bounds; this is standard but requires the bounds to be true bounds, which is not proven in the paper.
  • ad hoc to paper Nonlinear dynamics f and nonlinear constraints can be represented exactly or with sound bounds inside the MIQCP.
    The experiments include a unicycle with trigonometric dynamics and nonlinear constraints, but no such encoding or sound approximation is described in Section IV-C or V.
  • ad hoc to paper The policy network pi_phi is encoded in the verification MIQCP and is guaranteed to produce controls in U.
    Definition 7 and the forward invariance query require evaluating Q(f(x,u), pi_phi(f(x,u))); the paper does not specify how pi_phi is encoded or how U-feasibility of its outputs is enforced.
  • domain assumption Gurobi solves the MIQCP to global optimality and can certify infeasibility.
    The verification pipeline treats a solver 'infeasible' answer as proof that no counterexample exists; numerical tolerances and the nonconvexity of the bilinear product are not discussed.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks." pith.science (2026). https://pith.science/paper/J7KPIHI3

@misc{pith2026250615693,
  author       = {Pith},
  title        = {Pith review of: Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/J7KPIHI3}},
  note         = {Machine review of arXiv:2506.15693}
}
read the original abstract

Recent learning-based safety filters have outperformed conventional methods, such as hand-crafted Control Barrier Functions (CBFs), by effectively adapting to complex constraints. However, these learning-based approaches lack formal safety guarantees. In this work, we introduce a verifiable model-free safety filter based on Hamilton-Jacobi reachability analysis. Our primary contributions include: 1) extending verifiable self-consistency properties for Q value functions, 2) proposing a multiplicative Q-network structure to mitigate zero-sublevel-set shrinkage issues, and 3) developing a verification pipeline capable of soundly verifying these self-consistency properties. Our proposed approach successfully synthesizes formally verified, model-free safety certificates across four standard safe-control benchmarks.

Figures

Figures reproduced from arXiv: 2506.15693 by the authors.

Figure 1
Figure 1. Illustration of the verification pipeline toward a certified model-free safety filter. The pipeline consists of four stages: [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Safe control set size for each task at different stages [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Verified safe sets for (a) double integrator, we also demonstrate the ground truth safe set of double integrator with the [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

24 extracted references · 20 canonical work pages

  1. [1]

    Control barrier functions: Theory and applications

    Aaron D Ames, Samuel Coogan, Magnus Egerstedt, Gennaro No- tomista, Koushil Sreenath, and Paulo Tabuada. Control barrier functions: Theory and applications. In 2019 18th European control conference (ECC), pages 3420–3431. Ieee, 2019

    work page 2019

  2. [2]

    Robust control barrier–value functions for safety- critical control

    Jason J Choi, Donggun Lee, Koushil Sreenath, Claire J Tomlin, and Sylvia L Herbert. Robust control barrier–value functions for safety- critical control. In 2021 60th IEEE Conference on Decision and Control (CDC), pages 6814–6821. IEEE, 2021

    work page 2021

  3. [3]

    Safe control with learned certificates: A survey of neural lyapunov, barrier, and contrac- tion methods for robotics and control

    Charles Dawson, Sicun Gao, and Chuchu Fan. Safe control with learned certificates: A survey of neural lyapunov, barrier, and contrac- tion methods for robotics and control. IEEE Transactions on Robotics, 39(3):1749–1767, 2023

    2023

  4. [4]

    Fisac, Neil F

    Jaime F. Fisac, Neil F. Lugovoy, Vicenc ¸ Rubies-Royo, Shromona Ghosh, and Claire J. Tomlin. Bridging hamilton-jacobi safety analysis and reinforcement learning. In Proceedings of the 2019 International Conference on Robotics and Automation (ICRA) , pages 8550–8556, 2019

    work page 2019

  5. [5]

    Hamilton-Jacobi Reachability in Reinforcement Learning: A Survey

    Milan Ganai, Sicun Gao, and Sylvia Herbert. Hamilton-jacobi reachability in reinforcement learning: A survey. arXiv preprint arXiv:2407.09645, 2024

    work page Pith review arXiv 2024

  6. [6]

    Learning to be safe: Deep rl with a safety critic

    Yang Gao, Eric Jang, and Sergey Levine. Learning to be safe: Deep rl with a safety critic. arXiv preprint arXiv:2010.14603 , 2020

    arXiv 2010

  7. [7]

    Real-time safe control of neural network dynamic models with sound approximation

    Hanjiang Hu, Jianglin Lan, and Changliu Liu. Real-time safe control of neural network dynamic models with sound approximation. In 6th Annual Learning for Dynamics & Control Conference , pages 92–103. PMLR, 2024

    work page 2024

  8. [8]

    Verification of neural control barrier functions with symbolic derivative bounds propagation

    Hanjiang Hu, Yujie Yang, Tianhao Wei, and Changliu Liu. Verification of neural control barrier functions with symbolic derivative bounds propagation. In 8th Annual Conference on Robot Learning , 2024

    work page 2024

Show all 24 references
  1. [9]

    Factorized bi- linear models for image recognition

    Yanghao Li, Naiyan Wang, Jiaying Liu, and Xiaodi Hou. Factorized bi- linear models for image recognition. arXiv preprint arXiv:1611.05709, 2016

    2016 arXiv

  2. [10]

    Kochenderfer

    Changliu Liu, Tomer Arnon, Christopher Lazarus, Clark Barrett, and Mykel J. Kochenderfer. Algorithms for verifying deep neural networks. abs/1903.06758, 2019

    1903 arXiv

  3. [11]

    Control in a safe set: Ad- dressing safety in human-robot interactions

    Changliu Liu and Masayoshi Tomizuka. Control in a safe set: Ad- dressing safety in human-robot interactions. In Dynamic Systems and Control Conference, volume 46209, page V003T42A003. American Society of Mechanical Engineers, 2014

    2014

  4. [12]

    The flexible, extensible and efficient toolbox of level set methods

    Ian M Mitchell. The flexible, extensible and efficient toolbox of level set methods. Journal of Scientific Computing , 35:300–329, 2008

    2008

  5. [13]

    A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games

    Ian M Mitchell, Alexandre M Bayen, and Claire J Tomlin. A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games. IEEE Transactions on automatic control , 50(7):947–957, 2005

    2005

  6. [14]

    Rawlings, David Q

    James B. Rawlings, David Q. Mayne, and Moritz M. Diehl. Model Predictive Control: Theory, Computation, and Design . Nob Hill Publishing, Madison, Wisconsin, 2nd edition, 2017

    2017

  7. [15]

    Vicenc ¸ Rubies-Royo, David Fridovich-Keil, Sylvia Herbert, and Claire J. Tomlin. A classification-based approach for approximate reachability. In Proceedings of the 2019 International Conference on Robotics and Automation (ICRA) , pages 8550–8556, 2019

    2019

  8. [16]

    Q-learning-based model-free safety filter

    Guo Ning Sue, Yogita Choudhary, Richard Desatnik, Carmel Majidi, John Dolan, and Guanya Shi. Q-learning-based model-free safety filter. arXiv preprint arXiv:2411.19809 , November 2024

    2024 arXiv

  9. [17]

    Evaluating robustness of neural networks with mixed integer programming, 2019

    Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming, 2019

    2019

  10. [18]

    Refining control barrier functions through hamilton-jacobi reachability

    Sander Tonkens and Sylvia Herbert. Refining control barrier functions through hamilton-jacobi reachability. in 2022 ieee. In RSJ Interna- tional Conference on Intelligent Robots and Systems (IROS) , pages 13355–13362

    2022

  11. [19]

    Safe control algorithms using energy functions: A unified framework, benchmark, and new directions

    Tianhao Wei and Changliu Liu. Safe control algorithms using energy functions: A unified framework, benchmark, and new directions. In IEEE Conference on Decision and Control , pages 238–243. IEEE, 2019

    2019

  12. [20]

    Yun, Hanjiang Hu, Peizhi Niu, Xusheng Luo, and Changliu Liu

    Tianhao Wei, Luca Marzari, Kai S. Yun, Hanjiang Hu, Peizhi Niu, Xusheng Luo, and Changliu Liu. Modelverification.jl: a compre- hensive toolbox for formally verifying deep neural networks. arXiv preprint arXiv:2407.01639, 2024

    2024 arXiv

  13. [21]

    High-order control barrier functions

    Wei Xiao and Calin Belta. High-order control barrier functions. IEEE Transactions on Automatic Control , 67(7):3655–3662, 2021

    2021

  14. [22]

    Scalable synthesis of formally verified neural value function for hamilton-jacobi reachability analysis

    Yujie Yang, Hanjiang Hu, Tianhao Wei, Shengbo Eben Li, and Changliu Liu. Scalable synthesis of formally verified neural value function for hamilton-jacobi reachability analysis. arXiv preprint arXiv:2407.20532, 2024. Accessed: 2025-02-20

    2024 arXiv

  15. [23]

    Efficient neural network robustness certification with general activation functions, 2018

    Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions, 2018

    2018

  16. [24]

    Safety index synthesis via sum-of-squares programming

    Weiye Zhao, Tairan He, Tianhao Wei, Simin Liu, and Changliu Liu. Safety index synthesis via sum-of-squares programming. In 2023 American Control Conference (ACC) , pages 732–737. IEEE, 2023

    2023

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.