RISS 학술연구정보서비스

검색
다국어 입력

http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.

변환된 중국어를 복사하여 사용하시면 됩니다.

예시)
  • 中文 을 입력하시려면 zhongwen을 입력하시고 space를누르시면됩니다.
  • 北京 을 입력하시려면 beijing을 입력하시고 space를 누르시면 됩니다.
닫기
    인기검색어 순위 펼치기

    RISS 인기검색어

      검색결과 좁혀 보기

      선택해제

      오늘 본 자료

      • 오늘 본 자료가 없습니다.
      더보기
      • Neural Network Verification for Nonlinear Systems

        Sidrane, Chelsea Rose ProQuest Dissertations & Theses Stanford Universit 2022 해외박사(DDOD)

        RANK : 2591

        Machine learning has proven useful in a wide variety of domains from computer vision to control of autonomous systems. However, if we want to use neural networks in safety critical systems such as vehicles and aircraft, we need reliability guarantees. We turn to formal methods to verify that neural networks do not have unexpected behavior, such as misclassifying an image after a small amount of random noise is added. Within formal methods, there is a small but growing body of work focused on neural network verification. However, most of this work only reasons about neural networks in isolation, when in reality, neural networks are often used within large, complex systems. We build on this literature to verify neural networks operating within nonlinear systems.Our first contribution is to enable the use of mixed-integer linear programming for verification of systems containing both ReLU neural networks and smooth nonlinear functions. Mixed-integer linear programming is a common tool used for verifying neural networks with ReLU activation functions, and while effective, does not natively permit the use of nonlinear functions. We introduce an algorithm to overapproximate arbitrary nonlinear functions using piecewise linear constraints. These piecewise linear constraints can be encoded into a mixed-integer linear program, allowing verification of systems containing both ReLU neural networks and nonlinear functions. We use a special kind of approximation known as overapproximation which allows us to make sound claims about the original nonlinear system when we verify the overapproximate system.The next two contributions of this thesis are to apply the overapproximation algorithm to two different neural network verification settings: verifying inverse model neural networks and verifying neural network control policies. Frequently appearing in a variety of domains from medical imaging to state estimation, inverse problems involve reconstructing an underlying state from observations. The model mapping states to observations can be nonlinear and stochastic, making the inverse problem difficult. Neural networks are ideal candidates for solving inverse problems because they are very flexible and can be trained from data. However, inverse model neural networks lack built-in accuracy guarantees. We introduce a method to solve for verified upper bounds on the error of an inverse model neural network.The next verification setting we address is verifying neural network control policies for nonlinear dynamical systems. A control policy directs a dynamical system to perform a desired task such as moving to a target location. When a dynamical system is highly nonlinear and difficult to control, traditional control approaches may become computationally intractable. In contrast, neural network control policies are fast to execute. However, neural network control policies lack the stability, safety, and convergence guarantees that are often available to more traditional control approaches. In order to assess the safety and performance of neural network control policies, we introduce a method to perform finite time reachability analysis. Reachability analysis reasons about the set of states reachable by the dynamical system over time and whether that set of states is unsafe or is guaranteed to reach a goal.The final contribution of this thesis is the release of three open source software packages implementing methods described herein. The field of formal verification for neural networks is small and the release of open source software will allow it to grow more quickly as it makes iteration upon prior work easier.Overall, this thesis contributes ideas, methods, and tools to build confidence in deep learning systems. This area will continue to grow in importance as deep learning continues to find new applications.

      연관 검색어 추천

      이 검색어로 많이 본 자료

      활용도 높은 자료

      해외이동버튼