An Adaptive Tensor-Train Decomposition Approach for Efficient Deep Neural Network Compression

In the field of model compression, choosing an appropriate rank for tensor decomposition is pivotal for balancing model compression rate and efficiency. However, this selection, whether done manually or through optimization-based automatic methods, often increases computational complexity. Manual rank selection lacks efficiency and scalability, often requiring extensive trial-and-error, while optimization-based automatic methods significantly increase the computational burden. To address this, we introduce a novel, automatic, and budget-aware rank selection method for efficient model compression, which employs Layer-Wise Imprinting Quantitation (LWIQ). LWIQ quantifies each layer's significance within a neural network by integrating a proxy classifier. This classifier assesses the layer's impact on overall model performance, allowing for a more informed adjustment of tensor rank. Furthermore, our approach includes a scaling factor to cater to varying computational budget constraints. This budget awareness eliminates the need for repetitive rank recalculations for different budget scenarios. Experimental results on the CIFAR-10 dataset show that our LWIQ improved by 63.2$\%$ in rank search efficiency, and the accuracy only dropped by 0.86$\%$ with 3.2x less model size on the ResNet-56 model as compared to the state-of-the-art proxy-based automatic tensor rank selection method.

Formalism for Supporting the Development of Verifiably Safe Medical Guidelines with Statecharts

Improving the effectiveness and safety of patient care is the ultimate objective for medical cyber-physical systems. Many medical best practice guidelines exist, but most of the existing guidelines in handbooks are difficult for medical staff to remember and apply clinically. Furthermore, although the guidelines have gone through clinical validations, validations by medical professionals alone do not provide guarantees for the safety of medical cyber-physical systems. Hence, formal verification is also needed. The paper presents the formal semantics for a framework that we developed to support the development of verifiably safe medical guidelines. The framework allows computer scientists to work together with medical professionals to transform medical best practice guidelines into executable statechart models, Yakindu in particular, so that medical functionalities and properties can be quickly prototyped and validated. Existing formal verification technologies, UPPAAL timed automata in particular, is integrated into the framework to provide formal verification capabilities to verify safety properties. However, some components used/built into the framework, such as the open-source Yakindu statecharts as well as the transformation rules from statecharts to timed automata, do not have built-in semantics. The ambiguity becomes unavoidable unless formal semantics is defined for the framework, which is what the paper is to present.