SMT-Based Translation Validation for Machine Learning Compiler

EasyChair Preprint 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: Deep Learning Compiler, Machine Learning Compiler, Satisfiability Modulo Theory, Translation Validation, compiler verification

@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 8632},
  year      = {EasyChair, 2022}}