Umeå University's logo

The paper studies how code generation by LLMs can be combined with formal verification to produce critical embedded software. The first contribution is a general framework, spec2code, in which LLMs are combined with different types of critics that produce feedback for iterative backprompting and fine-tuning. The second contribution presents a first feasibility study, where a minimalistic instantiation of spec2code, without iterative backprompting and fine-tuning, is empirically evaluated using three industrial case studies from the heavy vehicle manufacturer Scania. The goal is to automatically generate industrial-quality code from specifications only. Different combinations of formal ACSL specifications and natural language specifications are explored. The results indicate that formally correct code can be generated even without the application of iterative backprompting and fine-tuning.

Recent advancements in machine learning, particularly in the field of adversarial training, have underscored the necessity for models that are not only accurate but also robust against adversarial attacks. However, a critical challenge lies in the unequal vulnerability of different classes within these models, often leading to a 'weakest-link' phenomenon where certain classes are more susceptible to adversarial perturbations. This paper presents a novel approach to improving the robustness of machine learning models against adversarial attacks, focusing on classes identified as vulnerable. The core of our methodology involves generating adversarial examples specifically tailored to these vulnerable classes, a process we term class-specific perturbations. We integrate this adversarial training into the learning process, aiming to enhance the model's robustness specifically for these at-risk classes. Motivated by this finding, we propose Balanced Adversarial Training (BAT) to facilitate adversarial training for the vulnerable class. Experimental evaluations across different datasets show that our proposed framework not only improves the robustness of the vulnerable class against adversarial attacks but also maintains overall model performance. Our work highlights the importance of moving beyond average accuracy, which is particularly important in safety-critical applications.

This work introduces the notion of intermediate concepts based on levels structure to aid explainability for black-box models. The levels structure is a hierarchical structure in which each level corresponds to features of a dataset (i.e., a player-set partition). The level of coarseness increases from the trivial set, which only comprises singletons, to the set, which only contains the grand coalition. In addition, it is possible to establish meronomies, i.e., part-whole relationships, via a domain expert that can be utilised to generate explanations at an abstract level. We illustrate the usability of this approach in a real-world car model example and the Titanic dataset, where intermediate concepts aid in explainability at different levels of abstraction.

This work investigates the relationship between adversarial robustness and the local Lipschitz constant in ensemble neural network frameworks, namely bagging and stacking. Capitalising on this, we introduce an ensemble neural network design that improves both accuracy and adversarial resilience. We theoretically obtain the local Lipschitz constants for both ensembles, offering insights into their susceptibility to adversarial attacks and identifying architectures optimal for adversarial defense. Notably, our approach negates the need for specific adversarial attack and accommodates any number of pre-trained networks for an ensemble architecture. Evaluations on the MNIST and CIFAR-10 datasets against white-box attacks, specifically FGSM and PGD, show our approach is adversarially robust compared to standalone networks and vanilla ensemble architectures.