Jordi Planes

This paper presents TRACE-CS2, a framework for explainable course scheduling that builds on TRACE-CS. It combines a SAT-based contrastive explainer with a large language model for natural language interaction. We identify three limitations of TRACE-CS: reporting infeasibility when there exists possible schedules; accepting only one positive and one negative literal per query; and a limited schedule diversification. TRACE-CS2 addresses these limitations by incorporating: a three-step local/global feasibility check; multi-literal queries; and SAT model enumeration. On a benchmark of 600 contrastive queries, TRACE-CS2 reaches better accuracy and may produce more distinct schedules.

End-to-end machine learning malware detectors are vulnerable to adversarial EXEmples, carefully-crafted malicious programs that evade detection through minimal perturbations. Such attacks typically operate by either replacing unused content (patch attacks), or injecting new patterns (content-injection attacks). To counter these attacks, recent research has focused on certification methods for end-to-end models that aim to prove robustness guarantees within bounded perturbation sizes. However, existing approaches (i) are not robust against content-injection manipulations and (ii) provide only probabilistic guarantees for perturbations that are negligible relative to the overall program size. Hence, in this paper we address these limitations through a novel deterministic certification schema based on (de)randomized smoothing. Our defense splits each executable into non-overlapping chunks and classifies them independently. The final decision is obtained via majority voting across all chunks, ensuring that localized modifications, such as injected or patched code, influence only a limited subset of chunks and have minimal impact in the overall classification. This design guarantees that each chunk either contains or does not contain an adversarial perturbation, enabling us to (i) handle manipulations occurring at arbitrary locations within the program, and (ii) compute deterministic estimates of the perturbation magnitude required to evade detection. We demonstrate the effectiveness of our certification schema through extensive experimental analysis, comparing our defense against a range of state-of-the-art attacks and defenses. The results show that our approach achieves unmatched robustness across all tested attack scenarios, substantially outperforming competing defenses.

Hydrogen arises as an alternative to decarbonize heavy industries, yet its production remains either expensive or environmentally harmful, prompting the exploration of waste-to-hydrogen gasification as a viable solution. This study addresses the challenges in accurately modeling the gasification reactor, a critical step in waste-to-hydrogen conversion, by confronting issues such as the inherent diversity of biomass and the complex interactions among its constituent properties using Artificial Intelligence. To address these challenges, we propose a methodology that integrates Physics-Informed Neural Networks, merging experimental data with physical principles to develop robust and adaptive models to predict syngas composition. Preliminary results indicate improvements in model accuracy over other models, achieving high predictive accuracies with an R2 value of 0.96 for the syngas composition, as well as greater scalability compared to existing approaches in this field.

Shapley values find a growing number of uses in different fields of knowledge, including machine learning, game theory, but also analysis of inconsistency, analysis and query answering in databases, among others. The complexity of computing Shapley values is most often unwieldy. As a result, approximate methods have been devised in the past. Some of the proposed methods are amenable to large-scale parallelization. This paper investigates the use of Spark for accelerating the approximate computation of Shapley values, namely in settings where this computation is extremely time-consuming.

The uses of machine learning (ML) have snowballed in recent years. In many cases, ML models are highly complex, and their operation is beyond the understanding of human decision-makers. Nevertheless, some uses of ML models involve high-stakes and safety-critical applications. Explainable artificial intelligence (XAI) aims to help human decision-makers in understanding the operation of such complex ML models, thus eliciting trust in their operation. Unfortunately, the majority of past XAI work is based on informal approaches, that offer no guarantees of rigor. Unsurprisingly, there exists comprehensive experimental and theoretical evidence confirming that informal methods of XAI can provide human-decision makers with erroneous information. Logic-based XAI represents a rigorous approach to explainability; it is model-based and offers the strongest guarantees of rigor of computed explanations. However, a well-known drawback of logic-based XAI is the complexity of logic reasoning, especially for highly complex ML models. Recent work proposed distance-restricted explanations, i.e. explanations that are rigorous provided the distance to a given input is small enough. Distance-restricted explainability is tightly related with adversarial robustness, and it has been shown to scale for moderately complex ML models, but the number of inputs still represents a key limiting factor. This paper investigates novel algorithms for scaling up the performance of logic-based explainers when computing and enumerating ML model explanations with a large number of inputs.

In the recent years, there has been a strong concern over the robustness of machine learning systems, specially when working in critical systems. One of such critical domains is cybersecurity, and a particular example is malware detection. This works aims to provide a formal technique to check the robustness of neural networks applied to the detection of malware. The technique is based on the automatic translation of the neural network to an equivalent set of equations that can be subsequently rigorously analyzed with respect to certain conditions for its input and output. That is, given a particular input for the neural network, check if there exist slight variations of such an input that can modify the output of the neural network. As a case study, we present preliminary results of a robustness analysis for a neural network that detects Windows PE malware. The results of the robustness analysis can be used to certify the robustness of the classifier or for improving such a classifier by fixing the flaws detected.

Deep learning-based malware detectors have been shown to be susceptible to adversarial malware examples, i.e. malware examples that have been deliberately manipulated in order to avoid detection. In light of the vulnerability of deep learning detectors to subtle input file modifications, we propose a practical defense against adversarial malware examples inspired by (de)randomized smoothing. In this work, we reduce the chances of sampling adversarial content injected by malware authors by selecting correlated subsets of bytes, rather than using Gaussian noise to randomize inputs like in the Computer Vision domain. During training, our chunk-based smoothing scheme trains a base classifier to make classifications on a subset of contiguous bytes or chunk of bytes. At test time, a large number of chunks are then classified by a base classifier and the consensus among these classifications is then reported as the final prediction. We propose two strategies to determine the location of the chunks used for classification: 1) randomly selecting the locations of the chunks and 2) selecting contiguous adjacent chunks. To showcase the effectiveness of our approach, we have trained two classifiers with our chunk-based smoothing schemes on the BODMAS dataset. Our findings reveal that the chunk-based smoothing classifiers exhibit greater resilience against adversarial malware examples generated with state-of-the-art evasion attacks, outperforming a non-smoothed classifier and a randomized smoothing-based classifier by a great margin.

Malware detectors based on machine learning (ML) have been shown to be susceptible to adversarial malware examples. However, current methods to generate adversarial malware examples still have their limits. They either rely on detailed model information (gradient-based attacks), or on detailed outputs of the model - such as class probabilities (score-based attacks), neither of which are available in real-world scenarios. Alternatively, adversarial examples might be crafted using only the label assigned by the detector (label-based attack) to train a substitute network or an agent using reinforcement learning. Nonetheless, label-based attacks might require querying a black-box system from a small number to thousands of times, depending on the approach, which might not be feasible against malware detectors.This work presents a novel query-free approach to craft adversarial malware examples to evade ML-based malware detectors. To this end, we have devised a GAN-based framework to generate adversarial malware examples that look similar to benign executables in the feature space. To demonstrate the suitability of our approach we have applied the GAN-based attack to three common types of features usually employed by static ML-based malware detectors: (1) Byte histogram features, (2) API-based features, and (3) String-based features. Results show that our model-agnostic approach performs on par with MalGAN, while generating more realistic adversarial malware examples without requiring any query to the malware detectors. Furthermore, we have tested the generated adversarial examples against state-of-the-art multimodal and deep learning malware detectors, showing a decrease in detection performance, as well as a decrease in the average number of detections by the antimalware engines in VirusTotal.