Source-linked AI summary
Extreme Learning Machine-based Barrier Function Synthesis
Ahan Basu, Mahathi Anand, Pushpak Jagtap
TL;DR
Synthesizing non-conservative barrier certificates is challenging when system dynamics are unknown, while neural approaches can be computationally costly and difficult to verify robustly. The paper uses ELM-based barriers with convex optimization and Lipschitz-based grid verification. In two case studies, it reports reduced computation time and sample requirements compared with neural methods.
Problem
Barrier-certificate synthesis is challenging when system dynamics are unknown, and neural approaches face costly training and verification with sensitivity to optimization settings.
Source: §1 · pp. 1–2Method
The paper synthesizes ELM-based barriers for unknown discrete-time systems using convex output-weight optimization and Lipschitz-based grid verification.
Source: §1 · p. 2, §3.1 · p. 4Results
Takeaways & Limitations
Lipschitz bounds support post-hoc verification from finite grid samples, with validity guarantees over the state set when the stated condition holds.
Source: §1 · p. 2, §3.2 · p. 5Choosing a smaller ε can bring η closer to zero, but increases sample count and computation time.
Source: §3.2 · p. 5
Abstract
from arXiv · showhide
Deep learning methods like neural networks have greatly simplified the computation of safety certificates for complex nonlinear systems with unknown dynamics. However, due to the data-driven nature of these certificates and the complex architecture of neural networks, computation time as well as robustness guarantees across unseen data remain a challenge. This work aims to formally verify safety properties of discrete-time unknown systems by synthesizing extreme learning machine (ELM)-based barrier certificates. Compared to neural network counterparts, this approach greatly improves convergence guarantees and computational time due to its architectural simplicity and the convex nature of the underlying optimization problem. By minimizing the Lipschitz constant of the candidate barrier, we present a grid-based sampling technique to formally verify its validity using the minimum number of samples required. We demonstrate through numerical examples the effectiveness of our approach, and compare with traditional deep-learning based certificate synthesis to highlight its benefits.
1 Introduction
Barrier certificates can guarantee safety, but synthesizing useful certificates is difficult when dynamics are unknown and traditional optimization or neural-network approaches are computationally demanding. This work proposes ELM-based synthesis with convex optimization and Lipschitz-based formal verification.
1 Introduction
- Barrier certificates separate safe and unsafe regions and provide sufficient conditions for trajectories to avoid unsafe configurations.Traditional template-based synthesis can be computationally complex, especially for nonlinear dynamics.Source: §1 · p. 1
- Unknown system dynamics often prevent model-based synthesis, while neural approaches face costly training and verification and sensitivity to optimization settings.The cited approaches learn from data, but backpropagation over large state-space regions and MILP, SMT, or SDP verification can scale poorly.Source: §1 · pp. 1–2
- ELM-based barrier conditions are affine in the learned output weights, yielding a convex formulation without learning the system dynamics.The method bounds the candidate barrier's Lipschitz constant and uses grid samples for post-hoc validity guarantees over the state set.Source: §1 · p. 2
- Two case studies and comparisons with neural methods demonstrate the approach's effectiveness, including reduced computation time and samples required for formal guarantees.The authors report that hidden ELM weights are fixed while output weights are learned.Source: §1 · p. 2
2 Preliminaries and Problem Formulation
The paper formulates safety verification for unknown discrete-time systems using barrier certificates, then parameterizes the certificate as an ELM so its conditions can be optimized convexly. It connects finite data-based training to safety guarantees over the state space.
2.1 System Definition
- For an unknown discrete-time system, a black-box model supplies next states for queried states, enabling finite samples while the goal is to keep trajectories from initial states outside the unsafe set.The system is represented by state space X, initial set X0, and state-update map f.Source: §2.1 · p. 2
2.2 Barrier Certificates
- A barrier certificate satisfying the initial, unsafe-set, and non-increase conditions guarantees that trajectories from X0 avoid XU.The conditions require B(x) ≤ 0 on X0, B(x) > 0 on XU, and B(f(x)) − B(x) ≤ 0 on X.Source: §2.2 · pp. 2–3
- The zero-level set of B separates safe and unsafe regions, and non-increase along trajectories prevents crossing into the unsafe region.For unknown dynamics, the map f in the non-increase condition makes direct certificate computation intractable.Source: §2.2 · p. 3
- For known dynamics, certificates are commonly synthesized with fixed templates and SOS or SMT methods; unknown-dynamics neural approaches use non-convex backpropagation and may have initialization-sensitive convergence.The paper proposes an ELM formulation to recast synthesis as a convex program.Source: §2.2 · p. 3
2.3 Extreme Learning Machine
- An ELM is a single-hidden-layer feedforward network whose hidden weights and biases are randomly preselected while output weights are learned.The formulation uses Lipschitz-bounded activation functions.Source: §2.3 · p. 3
2.4 Problem Formulation
- The synthesis problem is to construct an ELM-parameterized barrier certifying that a system starting in X0 never reaches XU.The system dynamics map is unknown.Source: §2.4 · p. 3
- Because the hidden layer is fixed, barrier conditions are affine in the output weights and can be optimized by a convex program, permitting global optima when feasible.The method uses finitely many data samples while seeking formal guarantees over the continuous state space.Source: §2.4 · p. 3
3 ELM-based Barrier Certificate Synthesis
The section trains an ELM barrier from finite grid samples, then uses Lipschitz bounds to state when the candidate is valid over the continuous state space. Its guarantee depends on zero training loss and a condition relating the slack, grid spacing, and system and barrier Lipschitz constants.
3.1 Formulation of Loss Function
- Grid-cover representative points form the training datasets, and a convex weighted loss encodes barrier conditions with slack η and strict unsafe-set separation δ.Zero loss satisfies the barrier conditions at sampled points.Source: §3.1 · p. 4
3.2 Correctness Guarantees for ELM-Barrier Certificates
- Normalizing the random hidden-layer weights and minimizing the output-weight norm reduces the ELM barrier’s Lipschitz bound.The bound is L_bar = ||W̄|| × |β| × L_φ, with ||W̄|| = 1.Source: §3.1 · p. 4, §3.2 · p. 5
- η + Lε ≤ 0 makes the zero-loss ELM a valid barrier and guarantees system safety, provided the dynamics satisfy the known-Lipschitz assumption.Here L = L_bar(L_x + 1); the proof extends sampled constraints to the continuous state space.Source: §3.2 · p. 5
- Choosing η closer to zero requires smaller grid spacing, which increases sample count and computation time.The section identifies this as a trade-off in selecting the verification margin.Source: §3.2 · p. 5
4 Case Studies
The case studies apply the ELM-barrier workflow to a simple pendulum and a magnetic levitator. Both examples report formal verification, with the magnetic levitator also showing negative barrier values along controlled trajectories.
4 Case Studies
- Both case studies use Algorithm 1 to train and verify the ELM barrier, solving the quadratic program with HiGHS in Python 3.10.The reported computations ran on Windows with an Intel Core i7-14700 CPU and 32 GB RAM.Source: §4 · pp. 5–6
4.1 Simple Pendulum System
- The pendulum certificate is formally verified with L_barr=0.033; more than 50 hidden neurons suffice, while verification success requires many samples.The example uses 50 hidden neurons and ε=0.00123; the barrier level sets and a sample trajectory are shown in Figure 1.Source: §4.1 · p. 6, Figure 1 · p. 6
4.2 Magnetic Levitator System
- The magnetic-levitator certificate is formally verified with L_barr=0.2209, and its barrier values stay negative along the controlled trajectories.The example uses 60 hidden neurons and ε=0.002759; Figure 2 shows trajectories from different initial conditions and barrier values over time.Source: §4.2 · p. 7, Figure 2 · p. 7
5 Comparison with Related Approaches
The comparison contrasts ELM synthesis with SOS-, scenario-optimization-, and neural-network-based methods. It reports lower computation time and fewer verification samples for ELM than neural barrier methods, alongside theoretical trade-offs with other approaches.
5.1 Theoretical Comparison
- Theoretical comparison describes ELM as applicable to general unknown nonlinear dynamics and higher-dimensional systems, while contrasting its convex programming with limits of SOS, scenario, and neural methods.SOS depends on known dynamics and semidefinite programming; scenario optimization depends on basis functions and does not use convex programming, while neural methods involve backpropagation.Source: §5.1 · p. 8
5.2 Quantitative Comparison
- ELM is reported to require less computation time and fewer verification samples than neural barrier methods, with comparisons based on 10 random-initialization trials.The authors attribute the sample reduction relative to to minimizing the barrier's Lipschitz constant rather than predefining it.Source: §5.2 · p. 8
6 Conclusion and Future Work
The conclusion presents ELM-based barrier synthesis as a convex formulation with Lipschitz-based post-hoc validity guarantees, evaluated in two case studies and benchmark comparisons with neural approaches. Future work includes controller synthesis and extension to interconnected systems.
6 Conclusion and Future Work
- The proposed ELM barrier formulation uses a Lipschitz-based post-hoc validity guarantee and is validated in two case studies against neural barrier synthesis approaches.Future work includes controller synthesis and extension to interconnected systems.Source: §6 · p. 8