Wed 11 May 2022 03:15 - 03:20 at ICSE room 4-odd hours - Validation and Verification 2 Chair(s): Grischa Liebel
Deep learning has been increasingly adopted in many application areas. To construct valid deep learning models, developers must conform to certain computational constraints by carefully selecting appropriate neural architectures and hyperparameter values. For example, the kernel size hyperparameter of the 2D convolution operator cannot be overlarge to ensure that the height and width of the output tensor remain positive. Because model construction is largely manual and lacks necessary tooling support, it is possible to violate those constraints and raise type errors of deep learning models, causing either runtime exceptions or wrong output results. In this paper, we propose Refty, a refinement type-based tool for statically checking the validity of deep learning models ahead of job execution. Refty refines each type of deep learning operator with framework-independent logical formulae that describe the computational constraints on both tensors and hyperparameters. Given the neural architecture and hyperparameter domains of a model, Refty visits every operator, generates a set of constraints that the model should satisfy, and utilizes an SMT solver for solving the constraints. We have evaluated Refty on both individual operators and representative real-world models with various hyperparameter values under PyTorch and TensorFlow. We also compare it with an existing shape-checking tool. The experimental results show that Refty finds all the type errors and achieves 100% Precision and Recall, demonstrating its effectiveness.
Tue 10 MayDisplayed time zone: Eastern Time (US & Canada) change
Wed 11 MayDisplayed time zone: Eastern Time (US & Canada) change
03:00 - 04:00 | Validation and Verification 2Technical Track / Journal-First Papers at ICSE room 4-odd hours Chair(s): Grischa Liebel Reykjavik University | ||
03:00 5mTalk | Verification of Consistency between Process Models, Object Life Cycles, and Context-dependent Semantic Specifications Journal-First Papers Ralph Hoch Institute of Computer Technology, TU Wien, Christoph Luckeneder Vienna University of Technology, Roman Popp TU Wien, Vienna, Austria, Hermann Kaindl Institute of Computer Technology, TU Wien Link to publication DOI Pre-print Media Attached | ||
03:05 5mTalk | Verification of ORM-based Controllers by Summary Inference Technical Track Geetam Chawla Indian Insitute of Science, Bangalore, Navneet Aman Indian Institute of Science, Bangalore, Raghavan Komondoor IISc Bengaluru, Ashish Shashikant Bokil Indian Institute of Science, Bangalore, Nilesh Ramesh Kharat Indian Institute of Science, Bangalore Pre-print Media Attached | ||
03:10 5mTalk | Data-Driven Loop Bound Learning for Termination Analysis Technical Track DOI Pre-print Media Attached | ||
03:15 5mTalk | Refty: Refinement Types for Valid Deep Learning Models Technical Track Yanjie Gao Microsoft Research, lizhengxian Microsoft Research, Haoxiang Lin Microsoft Research, Hongyu Zhang University of Newcastle, Ming Wu Shanghai Tree-Graph Blockchain Research Institute, Mao Yang Microsoft Research DOI Pre-print Media Attached | ||
03:20 5mTalk | GraphFuzz: Library API Fuzzing with Lifetime-aware Dataflow Graphs Technical Track DOI Pre-print Media Attached | ||
03:25 5mTalk | MOREST: Model-based RESTful API Testing with Execution Feedback Technical Track Yi Liu Nanyang Technological University, Yuekang Li Nanyang Technological University, Gelei Deng Nanyang Technological University, Yang Liu Nanyang Technological University, Ruiyuan Wan Huawei Inc., Runchao Wu Huawei Inc., Dandan Ji Huawei Inc., Shiheng Xu Huawei Inc., Minli Bao Huawei Inc. Pre-print Media Attached |