Abstract

Vision-based neural network controllers have shown promising results in autonomous lane-following tasks, but verifying their safety properties remains a significant challenge due to the high dimensionality of image inputs. This thesis designs an approach to enable formal verification of vision-based lane-following controllers by first developing an end-to-end autonomous system combining deep learning-based lane detection with reinforcement learning control. To enable formal verification, we introduce a generator-based framework that bridges the gap between high-dimensional image space and low-dimensional vehicle states, allowing us to leverage existing verification tools while maintaining the vision-based nature of the controller.

We further enhance our verification framework through certified training techniques and propose a multi-controller architecture that provides stronger safety guarantees. Experiments in the CARLA simulator demonstrate that our approaches can effectively verify the safety properties of vision-based controllers across various driving scenarios, while maintaining performance in lane-following tasks. The results demonstrate that our proposed methods can successfully address the challenge of verifying neural network controllers that operate directly on high-dimensional visual inputs.

Committee Chair

Yevgeniy Vorobeychik

Committee Members

Christopher Gill Nathan Jacobs Hussein Sibai

Degree

Master of Science (MS)

Author's Department

Computer Science & Engineering

Author's School

McKelvey School of Engineering

Document Type

Thesis

Date of Award

Winter 12-2024

Language

English (en)

Author's ORCID

https://orcid.org/0009-0002-2845-4728

Download

Included in

Engineering Commons

Share

COinS