SMT-Based Translation Validation for Machine Learning Compiler

EasyChair Preprint no. 8632

Abstract

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

@Booklet{EasyChair:8632,
  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}}