OpenRaiser/Intern-Atlas huggingface dataset:
Relating Answer Set Programming and Many-sorted Logics for Formal Verification
Venue: arXiv cs.LO 2025
Year: 2025

Answer Set Programming (ASP) is an important logic programming paradigm within the field of Knowledge Representation and Reasoning. As a concise, human-readable, declarative language, ASP is an excellent tool for developing trustworthy (especially, artificially intelligent) software systems. However, formally verifying ASP programs offers some unique challenges, such as 1. a lack of modularity (the meanings of rules are difficult to define in isolation from the enclosing program), 2. the ground-and-solve semantics (the meanings of rules are dependent on the input data with which the program is grounded), and 3. limitations of existing tools. My research agenda has been focused on addressing these three issues with the intention of making ASP verification an accessible, routine task that is regularly performed alongside program development. In this vein, I have investigated alternative semantics for ASP based on translations into the logic of here-and-there and many-sorted first-order logic. These semantics promote a modular understanding of logic programs, bypass grounding, and enable us to use automated theorem provers to automatically verify properties of programs.
A Category-Theoretic Perspective on Approximation Fixpoint Theory
Venue: arXiv cs.LO 2025
Year: 2025

Approximation Fixpoint Theory (AFT) was founded in the early 2000s by Denecker, Marek, and Truszczyński as an abstract algebraic framework to study the semantics of non-monotonic logics. Since its early successes, the potential of AFT as a unifying semantic framework has become widely recognised, and the interest in AFT has gradually increased, with applications now ranging from foundations of database theory to abstract argumentation. The non-monotonic constructive processes that occur in many more areas of computer science, together with their associated semantic structures, can be successfully studied using AFT, which greatly simplifies their characterizations. The goal of my research is to take a step towards the lifting of AFT into a more general framework for constructive knowledge.
Early Validation of High-level Requirements on Cyber-Physical Systems
Venue: arXiv cs.LO 2025
Year: 2025

The overarching, broad topic of my research are advancements in the area of safety-critical, cyber-physical systems (CPS) development with emphasis on validation and verification. The particular focus of my research is the early validation of high-level requirements on CPS. My current approach for tackling this problem is transforming the requirements into Event Calculus and subsequently reasoning about them using ASP solvers such as the grounding-free s(CASP). Below, I discuss my research, its current state, and the open issues that are still left to tackle. The first results of my work will be presented in a paper that was accepted for ICLP'24, which is my first paper in this area.
Oracle Separations for RPH
Venue: arXiv cs.CC 2025
Year: 2025

While theoretical computer science primarily works with discrete models of computation, like the Turing machine and the wordRAM, there are many scenarios in which introducing real computation models is more adequate. We want to compare real models of computation with discrete models of computation. We do this by means of oracle separation results. We define the notion of a real Turing machine as an extension of the (binary) Turing machine by adding a real tape. Using those machines, we define and study the real polynomial hierarchy RPH. We are interested in RPH as the first level of the hierarchy corresponds to the well-known complexity class ER. It is known that $NP \subseteq ER \subseteq PSPACE$ and furthermore $PH \subseteq RPH \subseteq PSPACE$. We are interested to know if any of those inclusions are tight. In the absence of unconditional separations of complexity classes, we turn to oracle separation. We develop a technique that allows us to transform oracle separation results from the binary world to the real world. As applications, we show there are oracles such that: - $RPH^O$ proper subset of $PSPACE^O$, - $Σ_{k+1}^O$ not contained in $Σ_kR^O$, for all $k\geq 0$, - $Σ_kR^O$ proper subset of $Σ_{k+1}R^O$, for all $k\geq 0$, - $BQP^O$ not contained in $RPH^O$. Our results hint that ER is strictly contained in PSPACE and that there is a separation between the different levels of the real polynomial hierarchy. We also bound the power of real computations by showing that NP-hard problems are unlikely to be solvable using polynomial time on a realRAM. Furthermore, our oracle separations hint that polynomial-time quantum computing cannot be simulated on an efficient real Turing machine.
Towards Seamless Hierarchical Federated Learning under Intermittent Client Participation: A Stagewise Decision-Making Methodology
Venue: arXiv cs.LG 2025
Year: 2025

Federated Learning (FL) offers a pioneering distributed learning paradigm that enables devices/clients to build a shared global model. This global model is obtained through frequent model transmissions between clients and a central server, which may cause high latency, energy consumption, and congestion over backhaul links. To overcome these drawbacks, Hierarchical Federated Learning (HFL) has emerged, which organizes clients into multiple clusters and utilizes edge nodes (e.g., edge servers) for intermediate model aggregations between clients and the central server. Current research on HFL mainly focus on enhancing model accuracy, latency, and energy consumption in scenarios with a stable/fixed set of clients. However, addressing the dynamic availability of clients -- a critical aspect of real-world scenarios -- remains underexplored. This study delves into optimizing client selection and client-to-edge associations in HFL under intermittent client participation so as to minimize overall system costs (i.e., delay and energy), while achieving fast model convergence. We unveil that achieving this goal involves solving a complex NP-hard problem. To tackle this, we propose a stagewise methodology that splits the solution into two stages, referred to as Plan A and Plan B. Plan A focuses on identifying long-term clients with high chance of participation in subsequent model training rounds. Plan B serves as a backup, selecting alternative clients when long-term clients are unavailable during model training rounds. This stagewise methodology offers a fresh perspective on client selection that can enhance both HFL and conventional FL via enabling low-overhead decision-making processes. Through evaluations on MNIST and CIFAR-10 datasets, we show that our methodology outperforms existing benchmarks in terms of model accuracy and system costs.
KET-RAG: A Cost-Efficient Multi-Granular Indexing Framework for Graph-RAG
Venue: arXiv cs.IR 2025
Year: 2025

Graph-RAG constructs a knowledge graph from text chunks to improve retrieval in Large Language Model (LLM)-based question answering. It is particularly useful in domains such as biomedicine, law, and political science, where retrieval often requires multi-hop reasoning over proprietary documents. Some existing Graph-RAG systems construct KNN graphs based on text chunk relevance, but this coarse-grained approach fails to capture entity relationships within texts, leading to sub-par retrieval and generation quality. To address this, recent solutions leverage LLMs to extract entities and relationships from text chunks, constructing triplet-based knowledge graphs. However, this approach incurs significant indexing costs, especially for large document collections. To ensure a good result accuracy while reducing the indexing cost, we propose KET-RAG, a multi-granular indexing framework. KET-RAG first identifies a small set of key text chunks and leverages an LLM to construct a knowledge graph skeleton. It then builds a text-keyword bipartite graph from all text chunks, serving as a lightweight alternative to a full knowledge graph. During retrieval, KET-RAG searches both structures: it follows the local search strategy of existing Graph-RAG systems on the skeleton while mimicking this search on the bipartite graph to improve retrieval quality. We evaluate 13 solutions on three real-world datasets, demonstrating that KET-RAG outperforms all competitors in indexing cost, retrieval effectiveness, and generation quality. Notably, it achieves comparable or superior retrieval quality to Microsoft's Graph-RAG while reducing indexing costs by over an order of magnitude. Additionally, it improves the generation quality by up to 32.4% while lowering indexing costs by around 20%.
Full Swap Regret and Discretized Calibration
Venue: arXiv cs.LG 2025
Year: 2025

We study the problem of minimizing swap regret in structured normal-form games. Players have a very large (potentially infinite) number of pure actions, but each action has an embedding into $d$-dimensional space and payoffs are given by bilinear functions of these embeddings. We provide an efficient learning algorithm for this setting that incurs at most $\tilde{O}(T^{(d+1)/(d+3)})$ swap regret after $T$ rounds. To achieve this, we introduce a new online learning problem we call \emph{full swap regret minimization}. In this problem, a learner repeatedly takes a (randomized) action in a bounded convex $d$-dimensional action set $\mathcal{K}$ and then receives a loss from the adversary, with the goal of minimizing their regret with respect to the \emph{worst-case} swap function mapping $\mathcal{K}$ to $\mathcal{K}$. For varied assumptions about the convexity and smoothness of the loss functions, we design algorithms with full swap regret bounds ranging from $O(T^{d/(d+2)})$ to $O(T^{(d+1)/(d+2)})$. Finally, we apply these tools to the problem of online forecasting to minimize calibration error, showing that several notions of calibration can be viewed as specific instances of full swap regret. In particular, we design efficient algorithms for online forecasting that guarantee at most $O(T^{1/3})$ $\ell_2$-calibration error and $O(\max(\sqrt{εT}, T^{1/3}))$ \emph{discretized-calibration} error (when the forecaster is restricted to predicting multiples of $ε$).
ThunderServe: High-performance and Cost-efficient LLM Serving in Cloud Environments
Venue: arXiv cs.DC 2025
Year: 2025

Recent developments in large language models (LLMs) have demonstrated their remarkable proficiency in a range of tasks. Compared to in-house homogeneous GPU clusters, deploying LLMs in cloud environments with diverse types of GPUs is crucial for addressing the GPU shortage problem and being more cost-effective. However, the diversity of network environments and various GPU types on the cloud bring difficulties to achieving high-performance serving. In this work, we propose ThunderServe, a high-performance and cost-efficient LLM serving system for heterogeneous cloud environments. We introduce a novel scheduling algorithm, which optimizes the deployment plan of LLM serving to accommodate the heterogeneous resource and network bandwidth conditions in cloud environments. Furthermore, we propose a lightweight re-scheduling mechanism, designed to adapt to fluctuating online conditions (e.g., node failures, workload shifts) without the need for costly restarts of ongoing services. Empirical results in both heterogeneous cloud and homogeneous in-house environments reveal that ThunderServe delivers up to a 2.1$\times$ and on average a $1.7\times$ increase in throughput and achieves up to a 2.5$\times$ and on average a $1.5\times$ reduction in latency deadlines compared with state-of-the-art systems given the same price budget, suggesting opting for cloud services provides a more cost-efficient solution.
This looks like what? Challenges and Future Research Directions for Part-Prototype Models
Venue: arXiv cs.LG 2025
Year: 2025

The growing interest in eXplainable Artificial Intelligence (XAI) has prompted research into models with built-in interpretability, the most prominent of which are part-prototype models. Part-Prototype Models (PPMs) make decisions by comparing an input image to a set of learned prototypes, providing human-understandable explanations in the form of ``this looks like that''. Despite their inherent interpretability, PPMS are not yet considered a valuable alternative to post-hoc models. In this survey, we investigate the reasons for this and provide directions for future research. We analyze papers from 2019 to 2024, and derive a taxonomy of the challenges that current PPMS face. Our analysis shows that the open challenges are quite diverse. The main concern is the quality and quantity of prototypes. Other concerns are the lack of generalization to a variety of tasks and contexts, and general methodological issues, including non-standardized evaluation. We provide ideas for future research in five broad directions: improving predictive performance, developing novel architectures grounded in theory, establishing frameworks for human-AI collaboration, aligning models with humans, and establishing metrics and benchmarks for evaluation. We hope that this survey will stimulate research and promote intrinsically interpretable models for application domains. Our list of surveyed papers is available at https://github.com/aix-group/ppm-survey.
Revisiting Topological Interference Management: A Learning-to-Code on Graphs Perspective
Venue: arXiv cs.IT 2025
Year: 2025

The advance of topological interference management (TIM) has been one of the driving forces of recent developments in network information theory. However, state-of-the-art coding schemes for TIM are usually handcrafted for specific families of network topologies, relying critically on experts' domain knowledge and sophisticated treatments. The lack of systematic and automatic generation of solutions inevitably restricts their potential wider applications to wireless communication systems, due to the limited generalizability of coding schemes to wider network configurations. To address such an issue, this work makes the first attempt to advocate revisiting topological interference alignment (IA) from a novel learning-to-code perspective. Specifically, we recast the one-to-one and subspace IA conditions as vector assignment policies and propose a unifying learning-to-code on graphs (LCG) framework by leveraging graph neural networks (GNNs) for capturing topological structures and reinforcement learning (RL) for decision-making of IA beamforming vector assignment. Interestingly, the proposed LCG framework is capable of recovering known one-to-one scalar/vector IA solutions for a significantly wider range of network topologies, and more remarkably of discovering new subspace IA coding schemes for multiple-antenna cases that are challenging to be handcrafted. The extensive experiments demonstrate that the LCG framework is an effective way to automatically produce systematic coding solutions to the TIM instances with arbitrary network topologies, and at the same time, the underlying learning algorithm is efficient with respect to online inference time and possesses excellent generalizability and transferability for practical deployment.
Language Agents as Digital Representatives in Collective Decision-Making
Venue: arXiv cs.LG 2025
Year: 2025

Consider the process of collective decision-making, in which a group of individuals interactively select a preferred outcome from among a universe of alternatives. In this context, "representation" is the activity of making an individual's preferences present in the process via participation by a proxy agent -- i.e. their "representative". To this end, learned models of human behavior have the potential to fill this role, with practical implications for multi-agent scenario studies and mechanism design. In this work, we investigate the possibility of training \textit{language agents} to behave in the capacity of representatives of human agents, appropriately expressing the preferences of those individuals whom they stand for. First, we formalize the setting of \textit{collective decision-making} -- as the episodic process of interaction between a group of agents and a decision mechanism. On this basis, we then formalize the problem of \textit{digital representation} -- as the simulation of an agent's behavior to yield equivalent outcomes from the mechanism. Finally, we conduct an empirical case study in the setting of \textit{consensus-finding} among diverse humans, and demonstrate the feasibility of fine-tuning large language models to act as digital representatives.
SQuARE: Sequential Question Answering Reasoning Engine for Enhanced Chain-of-Thought in Large Language Models
Venue: arXiv cs.CL 2025
Year: 2025

In the rapidly evolving field of Natural Language Processing, Large Language Models (LLMs) are tasked with increasingly complex reasoning challenges. Traditional methods like chain-of-thought prompting have shown promise but often fall short in fully leveraging a model's reasoning capabilities. This paper introduces SQuARE (Sequential Question Answering Reasoning Engine), a novel prompting technique designed to improve reasoning through a self-interrogation paradigm. Building upon CoT frameworks, SQuARE prompts models to generate and resolve multiple auxiliary questions before tackling the main query, promoting a more thorough exploration of various aspects of a topic. Our expansive evaluations, conducted with Llama 3 and GPT-4o models across multiple question-answering datasets, demonstrate that SQuARE significantly surpasses traditional CoT prompts and existing rephrase-and-respond methods. By systematically decomposing queries, SQuARE advances LLM capabilities in reasoning tasks. The code is publicly available at https://github.com/IntelLabs/RAG-FiT/tree/square.
Human noise at the fingertip: Positional (non)control under varying haptic $\times$ musical conditions (Appendices included)
Venue: arXiv cs.HC 2025
Year: 2025

As technologies and interfaces for the instrumental control of musical sound get ever better at tracking aspects of human position and motion in space, a fundamental problem emerges: Unintended or even counter-intentional control may result when humans themselves become a source of positional noise. A clear case of what is meant by this is the "stillness movement" of a body part occurring despite the simultaneous explicit intention for that body part to remain still. In this paper, we present the results of a randomized, controlled experiment investigating this phenomenon along a vertical axis relative to the human fingertip. The results include characterizations of both the spatial distribution and frequency distribution of the stillness movement observed. Also included are results indicating a possible role for constant forces and viscosities in reducing stillness movement amplitude, thereby potentially enabling the implementation of more positional control of musical sound within the same available spatial range. Importantly, the above is summarized in a form that is directly interpretable for anyone designing technologies, interactions, or performances that involve fingertip control of musical sound. Also, a complete data set of the experimental results is included in the separate Appendices to this paper, again in a format that is directly interpretable.
PenTest++: Elevating Ethical Hacking with AI and Automation
Venue: arXiv cs.CR 2025
Year: 2025

Traditional ethical hacking relies on skilled professionals and time-intensive command management, which limits its scalability and efficiency. To address these challenges, we introduce PenTest++, an AI-augmented system that integrates automation with generative AI (GenAI) to optimise ethical hacking workflows. Developed in a controlled virtual environment, PenTest++ streamlines critical penetration testing tasks, including reconnaissance, scanning, enumeration, exploitation, and documentation, while maintaining a modular and adaptable design. The system balances automation with human oversight, ensuring informed decision-making at key stages, and offers significant benefits such as enhanced efficiency, scalability, and adaptability. However, it also raises ethical considerations, including privacy concerns and the risks of AI-generated inaccuracies (hallucinations). This research underscores the potential of AI-driven systems like PenTest++ to complement human expertise in cybersecurity by automating routine tasks, enabling professionals to focus on strategic decision-making. By incorporating robust ethical safeguards and promoting ongoing refinement, PenTest++ demonstrates how AI can be responsibly harnessed to address operational and ethical challenges in the evolving cybersecurity landscape.
SteROI-D: System Design and Mapping for Stereo Depth Inference on Regions of Interest
Venue: arXiv cs.CV 2025
Year: 2025

Machine learning algorithms have enabled high quality stereo depth estimation to run on Augmented and Virtual Reality (AR/VR) devices. However, high energy consumption across the full image processing stack prevents stereo depth algorithms from running effectively on battery-limited devices. This paper introduces SteROI-D, a full stereo depth system paired with a mapping methodology. SteROI-D exploits Region-of-Interest (ROI) and temporal sparsity at the system level to save energy. SteROI-D's flexible and heterogeneous compute fabric supports diverse ROIs. Importantly, we introduce a systematic mapping methodology to effectively handle dynamic ROIs, thereby maximizing energy savings. Using these techniques, our 28nm prototype SteROI-D design achieves up to 4.35x reduction in total system energy compared to a baseline ASIC.
Diffusing DeBias: Synthetic Bias Amplification for Model Debiasing
Venue: arXiv cs.LG 2025
Year: 2025

Deep learning model effectiveness in classification tasks is often challenged by the quality and quantity of training data whenever they are affected by strong spurious correlations between specific attributes and target labels. This results in a form of bias affecting training data, which typically leads to unrecoverable weak generalization in prediction. This paper aims at facing this problem by leveraging bias amplification with generated synthetic data: we introduce Diffusing DeBias (DDB), a novel approach acting as a plug-in for common methods of unsupervised model debiasing exploiting the inherent bias-learning tendency of diffusion models in data generation. Specifically, our approach adopts conditional diffusion models to generate synthetic bias-aligned images, which replace the original training set for learning an effective bias amplifier model that we subsequently incorporate into an end-to-end and a two-step unsupervised debiasing approach. By tackling the fundamental issue of bias-conflicting training samples memorization in learning auxiliary models, typical of this type of techniques, our proposed method beats current state-of-the-art in multiple benchmark datasets, demonstrating its potential as a versatile and effective tool for tackling bias in deep learning models. Code is available at https://github.com/Malga-Vision/DiffusingDeBias
MDCrow: Automating Molecular Dynamics Workflows with Large Language Models
Venue: arXiv cs.AI 2025
Year: 2025

Molecular dynamics (MD) simulations are essential for understanding biomolecular systems but remain challenging to automate. Recent advances in large language models (LLM) have demonstrated success in automating complex scientific tasks using LLM-based agents. In this paper, we introduce MDCrow, an agentic LLM assistant capable of automating MD workflows. MDCrow uses chain-of-thought over 40 expert-designed tools for handling and processing files, setting up simulations, analyzing the simulation outputs, and retrieving relevant information from literature and databases. We assess MDCrow's performance across 25 tasks of varying required subtasks and difficulty, and we evaluate the agent's robustness to both difficulty and prompt style. \texttt{gpt-4o} is able to complete complex tasks with low variance, followed closely by \texttt{llama3-405b}, a compelling open-source model. While prompt style does not influence the best models' performance, it has significant effects on smaller models.