Scaling Mixed-Integer Programming for Certification of Neural Network Controllers Using Bounds Tightening
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866929697620754432 |
|---|---|
| author | Sosnin, Philip Tsay, Calvin |
| author_facet | Sosnin, Philip Tsay, Calvin |
| contents | Neural networks offer a computationally efficient approximation of model predictive control, but they lack guarantees on the resulting controlled system's properties. Formal certification of neural networks is crucial for ensuring safety, particularly in safety-critical domains such as autonomous vehicles. One approach to formally certify properties of neural networks is to solve a mixed-integer program based on the network. This approach suffers from scalability issues due to the complexity of solving the resulting mixed-integer programs. Nevertheless, these issues can be (partially) mitigated via bound-tightening techniques prior to forming the mixed-integer program, which results in tighter formulations and faster optimisation. This paper presents bound-tightening techniques in the context of neural network explicit control policies. Bound tightening is particularly important when considering problems spanning multiple time steps of a controlled system, as the bounds must be propagated through the problem depth. Several strategies for bound tightening are evaluated in terms of both computational complexity and tightness of the bounds. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_17874 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Scaling Mixed-Integer Programming for Certification of Neural Network Controllers Using Bounds Tightening Sosnin, Philip Tsay, Calvin Optimization and Control Neural networks offer a computationally efficient approximation of model predictive control, but they lack guarantees on the resulting controlled system's properties. Formal certification of neural networks is crucial for ensuring safety, particularly in safety-critical domains such as autonomous vehicles. One approach to formally certify properties of neural networks is to solve a mixed-integer program based on the network. This approach suffers from scalability issues due to the complexity of solving the resulting mixed-integer programs. Nevertheless, these issues can be (partially) mitigated via bound-tightening techniques prior to forming the mixed-integer program, which results in tighter formulations and faster optimisation. This paper presents bound-tightening techniques in the context of neural network explicit control policies. Bound tightening is particularly important when considering problems spanning multiple time steps of a controlled system, as the bounds must be propagated through the problem depth. Several strategies for bound tightening are evaluated in terms of both computational complexity and tightness of the bounds. |
| title | Scaling Mixed-Integer Programming for Certification of Neural Network Controllers Using Bounds Tightening |
| topic | Optimization and Control |
| url | https://arxiv.org/abs/2403.17874 |