Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal description of ML models for unambiguous implementation

Adrien Gauffriau, Iryna De Albuquerque Silva, Claire Pagetti

TL;DR

The paper tackles the need for certifiable ML model deployment in safety-critical aeronautics by introducing a formal, framework-agnostic description that preserves semantics on hardware. It extends the Neural Network Exchange Format (NNEF) with an execution model based on Petri nets and adds multi-item support for distribution across HW/SW items, including data exchanges via graphitem and variablesync. A colored Petri-net semantics is provided to ensure semantics preservation when partitioning a model into multiple items, and a Jetson Xavier TX demonstration with manual C++/CUDA code generation validates both semantic and functional integrity, along with timing measurements. This approach yields traceable, predictable deployment suitable for DO-178C-like processes and offers a pathway toward standardized aeronautics-oriented model exchange with rigorous semantics."

Abstract

Implementing deep neural networks in safety critical systems, in particular in the aeronautical domain, will require to offer adequate specification paradigms to preserve the semantics of the trained model on the final hardware platform. We propose to extend the nnef language in order to allow traceable distribution and parallelisation optimizations of a trained model. We show how such a specification can be implemented in cuda on a Xavier platform.

Formal description of ML models for unambiguous implementation

TL;DR

The paper tackles the need for certifiable ML model deployment in safety-critical aeronautics by introducing a formal, framework-agnostic description that preserves semantics on hardware. It extends the Neural Network Exchange Format (NNEF) with an execution model based on Petri nets and adds multi-item support for distribution across HW/SW items, including data exchanges via graphitem and variablesync. A colored Petri-net semantics is provided to ensure semantics preservation when partitioning a model into multiple items, and a Jetson Xavier TX demonstration with manual C++/CUDA code generation validates both semantic and functional integrity, along with timing measurements. This approach yields traceable, predictable deployment suitable for DO-178C-like processes and offers a pathway toward standardized aeronautics-oriented model exchange with rigorous semantics."

Abstract

Implementing deep neural networks in safety critical systems, in particular in the aeronautical domain, will require to offer adequate specification paradigms to preserve the semantics of the trained model on the final hardware platform. We propose to extend the nnef language in order to allow traceable distribution and parallelisation optimizations of a trained model. We show how such a specification can be implemented in cuda on a Xavier platform.
Paper Structure (24 sections, 3 equations, 9 figures)

This paper contains 24 sections, 3 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Context
  3. Assurance development process
  4. Contributions
  5. Format of description -- nnef
  6. Brief Reminder on Neural Network
  7. Neural Network Description in nnef
  8. Max Pooling Layer Semantics
  9. nnef Execution Model Semantics
  10. Is distribution needed?
  11. nnef extension for multiple items
  12. Extension for item splitting
  13. Splitting an nnef description into multi-item descriptions
  14. Petri-based semantic
  15. Implementation and experiments
  16. ...and 9 more sections

Figures (9)

  • Figure 1: Left part: current ML deployment practice and right part: proposed aeronautical practice.
  • Figure 2: LeNet-5 neural network
  • Figure 3: Translation of one instruction
  • Figure 4: nnef semantics of the LeNet-5 express with Petri net. Initial marking
  • Figure 5: Petri associated to DNN of listing \ref{['completeMLMD']}. Initial marking
  • ...and 4 more figures

Theorems & Definitions (17)

  • Definition 1: Feed-forward Deep Neural Network
  • Definition 2: Predecessors / successors of a layer
  • Definition 3: Function associated to a FDNN
  • Example 1: Single-path feed-forward deep neural network
  • Remark 1
  • Example 2
  • Definition 4: Padding associated function -- $\mathcal{P}_{p,v}$
  • Definition 5: Pooling layer associated function -- $\mathcal{P}\emph{ool}_{k,s}$
  • Example 3
  • Remark 2
  • ...and 7 more