Download PDFOpen PDF in browser

SMT-Based Translation Validation for Machine Learning Compiler

EasyChair Preprint no. 8632

21 pagesDate: August 10, 2022


Machine learning compilers are large software containing complex transformations for deep learning models, and any buggy transformation may cause a crash or silently bring a regression to the prediction accuracy and performance. This paper proposes an SMT-based translation validation framework for Multi-Level IR (MLIR), a compiler framework used by many deep learning compilers. It proposes an SMT encoding tailored for translation validation that is an over-approximation of the FP arithmetic and reduction operations. It performs abstraction refinement if validation fails. We also propose a new approach for encoding arithmetic properties of reductions in SMT. We found mismatches between the specification and implementation of MLIR, and validated high-level transformations for SqueezeNet, MobileNet, and text_classification with proper splitting.

Keyphrases: compiler verification, Deep Learning Compiler, Machine Learning Compiler, Satisfiability Modulo Theory, Translation Validation

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Seongwon Bang and Seunghyeon Nam and Inwhan Chun and Ho Young Jhoo and Juneyoung Lee},
  title = {SMT-Based Translation Validation for Machine Learning Compiler},
  howpublished = {EasyChair Preprint no. 8632},

  year = {EasyChair, 2022}}
Download PDFOpen PDF in browser