Timothy Wang

Timothy Wang, Romain Jobredeaux, Marc Pantel et al.

The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety critical roles. There is a considerable body of mathematical proofs on on-line optimization programs which can be leveraged to assist in the development and verification of their implementation. In this paper, we demonstrate how theoretical proofs of real-time optimization algorithms can be used to describe functional properties at the level of the code, thereby making it accessible for the formal methods community. The running example used in this paper is a generic semi-definite programming (SDP) solver. Semi-definite programs can encode a wide variety of optimization problems and can be solved in polynomial time at a given accuracy. We describe a top-to-down approach that transforms a high-level analysis of the algorithm into useful code annotations. We formulate some general remarks about how such a task can be incorporated into a convex programming autocoder. We then take a first step towards the automatic verification of the optimization program by identifying key issues to be adressed in future work.

Timothy Wang, Romain Jobredeaux, E. Feron

We present the concept of a unified graphical environment for expressing the semantics of control systems. The graphical control system design environment in Simulink already allows engineers to insert a variety of assertions aimed the verification and validation of the control software. We propose extensions to a Simulink-like environment's annotation capabilities to include formal control system stability, performance properties and their proofs. We provide a conceptual description of a tool, that takes in a Simulink-like diagram of the control system as the input, and generates a graphically annotated control system diagram as the output. The annotations can either be inserted by the user or generated automatically by a third party control analysis software such as IQC$β$ or $μ$-tool. We finally describe how the graphical representation of the system and its properties can be translated to annotated programs in a programming language used in verification and validation such as Lustre or C.

Justin Zhao, Timothy Wang, Wael Abid et al.

Low Rank Adaptation (LoRA) has emerged as one of the most widely adopted methods for Parameter Efficient Fine-Tuning (PEFT) of Large Language Models (LLMs). LoRA reduces the number of trainable parameters and memory usage while achieving comparable performance to full fine-tuning. We aim to assess the viability of training and serving LLMs fine-tuned with LoRA in real-world applications. First, we measure the quality of LLMs fine-tuned with quantized low rank adapters across 10 base models and 31 tasks for a total of 310 models. We find that 4-bit LoRA fine-tuned models outperform base models by 34 points and GPT-4 by 10 points on average. Second, we investigate the most effective base models for fine-tuning and assess the correlative and predictive capacities of task complexity heuristics in forecasting the outcomes of fine-tuning. Finally, we evaluate the latency and concurrency capabilities of LoRAX, an open-source Multi-LoRA inference server that facilitates the deployment of multiple LoRA fine-tuned models on a single GPU using shared base model weights and dynamic adapter loading. LoRAX powers LoRA Land, a web application that hosts 25 LoRA fine-tuned Mistral-7B LLMs on a single NVIDIA A100 GPU with 80GB memory. LoRA Land highlights the quality and cost-effectiveness of employing multiple specialized LLMs over a single, general-purpose LLM.

Timothy Wang, Romain Jobredeaux, Heber Herencia et al.

This article describes a fully automated, credible autocoding chain for control systems. The framework generates code, along with guarantees of high level functional properties which can be independently verified. It relies on domain specific knowledge and fomal methods of analysis to address a context of heightened safety requirements for critical embedded systems and ever-increasing costs of verification and validation. The platform strives to bridge the semantic gap between domain expert and code verification expert. First, a graphical dataflow language is extended with annotation symbols enabling the control engineer to express high level properties of its control law within the framework of a familiar language. An existing autocoder is enhanced to both generate the code implementing the initial design, but also to carry high level properties down to annotations at the level of the code. Finally, using customized code analysis tools, certificates are generated which guarantee the correctness of the annotations with respect to the code, and can be verified using existing static analysis tools. Only a subset of properties and controllers are handled at this point.