OpenRaiser/Intern-Atlas huggingface dataset:
A unit-based symbolic execution method for detecting memory corruption vulnerabilities in executable codes
Venue: arXiv cs.CR 2025
Year: 2025

Memory corruption is a serious class of software vulnerabilities, which requires careful attention to be detected and removed from applications before getting exploited and harming the system users. Symbolic execution is a well-known method for analyzing programs and detecting various vulnerabilities, e.g., memory corruption. Although this method is sound and complete in theory, it faces some challenges, such as path explosion, when applied to real-world complex programs. In this paper, we present a method for improving the efficiency of symbolic execution and detecting four classes of memory corruption vulnerabilities in executable codes, i.e., heap-based buffer overflow, stack-based buffer overflow, use-after-free, and double-free. We perform symbolic execution only on test units rather than the whole program to lower the chance of path explosion. In our method, test units are considered parts of the program's code, which might contain vulnerable statements and are statically identified based on the specifications of memory corruption vulnerabilities. Then, each test unit is symbolically executed to calculate path and vulnerability constraints of each statement of the unit, which determine the conditions on unit input data for executing that statement or activating vulnerabilities in it, respectively. Solving these constraints gives us input values for the test unit, which execute the desired statements and reveal vulnerabilities in them. Finally, we use machine learning to approximate the correlation between system and unit input data. Thereby, we generate system inputs that enter the program, reach vulnerable instructions in the desired test unit, and reveal vulnerabilities in them. This method is implemented as a plugin for angr framework and evaluated using a group of benchmark programs. The experiments show its superiority over similar tools in accuracy and performance.
Revisiting the Fast Fourier Transform in Rocq
Venue: arXiv cs.LO 2025
Year: 2025

This notes explains how a standard algorithm that constructs the discrete Fourier transform has been formalised and proved correct in the Coq proof assistant using the SSReflect extension.
Online matching with delays and stochastic arrival times
Venue: arXiv cs.DS 2025
Year: 2025

This paper presents a new research direction for the Min-cost Perfect Matching with Delays (MPMD) - a problem introduced by Emek et al. (STOC'16). In the original version of this problem, we are given an $n$-point metric space, where requests arrive in an online fashion. The goal is to minimise the matching cost for an even number of requests. However, contrary to traditional online matching problems, a request does not have to be paired immediately at the time of its arrival. Instead, the decision of whether to match a request can be postponed for time $t$ at a delay cost of $t$. For this reason, the goal of the MPMD is to minimise the overall sum of distance and delay costs. Interestingly, for adversarially generated requests, no online algorithm can achieve a competitive ratio better than $O(\log n/\log \log n)$ (Ashlagi et al., APPROX/RANDOM'17). Here, we consider a stochastic version of the MPMD problem where the input requests follow a Poisson arrival process. For such a problem, we show that the above lower bound can be improved by presenting two deterministic online algorithms, which, in expectation, are constant-competitive. The first one is a simple greedy algorithm that matches any two requests once the sum of their delay costs exceeds their connection cost, i.e., the distance between them. The second algorithm builds on the tools used to analyse the first one in order to obtain even better performance guarantees. This result is rather surprising as the greedy approach for the adversarial model achieves a competitive ratio of $Ω(m^{\log \frac{3}{2}+\varepsilon})$, where $m$ denotes the number of requests served (Azar et al., TOCS'20). Finally, we prove that it is possible to obtain similar results for the general case when the delay cost follows an arbitrary positive and non-decreasing function, as well as for the MPMD variant with penalties to clear pending requests.
Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting
Venue: arXiv cs.LO 2025
Year: 2025

At the core of the quest for a logic for PTime is a mismatch between algorithms making arbitrary choices and isomorphism-invariant logics. One approach to overcome this problem is witnessed symmetric choice. It allows for choices from definable orbits which are certified by definable witnessing automorphisms. We consider the extension of fixed-point logic with counting (IFPC) with witnessed symmetric choice (IFPC+WSC) and a further extension with an interpretation operator (IFPC+WSC+I). The latter operator evaluates a subformula in the structure defined by an interpretation. This structure possibly has other automorphisms exploitable by the WSC-operator. For similar extensions of pure fixed-point logic (IFP) it is known that IFP+WSCI simulates counting which IFP+WSC fails to do. For IFPC+WSC it is unknown whether the interpretation operator increases expressiveness and thus allows studying the relation between WSC and interpretations beyond counting. We separate IFPC+WSC from IFPC+WSCI by showing that IFPC+WSC is not closed under FO-interpretations. By the same argument, we answer an open question of Dawar and Richerby regarding non-witnessed symmetric choice in IFP. Additionally, we prove that nesting WSC-operators increases the expressiveness using the so-called CFI graphs. We show that if IFPC+WSC+I canonizes a particular class of base graphs, then it also canonizes the corresponding CFI graphs. This differs from various other logics, where CFI graphs provide difficult instances.
A "New Ara" for Vector Computing: An Open Source Highly Efficient RISC-V V 1.0 Vector Processor Design
Venue: arXiv cs.AR 2025
Year: 2025

Vector architectures are gaining traction for highly efficient processing of data-parallel workloads, driven by all major ISAs (RISC-V, Arm, Intel), and boosted by landmark chips, like the Arm SVE-based Fujitsu A64FX, powering the TOP500 leader Fugaku. The RISC-V V extension has recently reached 1.0-Frozen status. Here, we present its first open-source implementation, discuss the new specification's impact on the micro-architecture of a lane-based design, and provide insights on performance-oriented design of coupled scalar-vector processors. Our system achieves comparable/better PPA than state-of-the-art vector engines that implement older RVV versions: 15% better area, 6% improved throughput, and FPU utilization >98.5% on crucial kernels.
Inferring Past Human Actions in Homes with Abductive Reasoning
Venue: arXiv cs.CV 2025
Year: 2025

Abductive reasoning aims to make the most likely inference for a given set of incomplete observations. In this paper, we introduce "Abductive Past Action Inference", a novel research task aimed at identifying the past actions performed by individuals within homes to reach specific states captured in a single image, using abductive inference. The research explores three key abductive inference problems: past action set prediction, past action sequence prediction, and abductive past action verification. We introduce several models tailored for abductive past action inference, including a relational graph neural network, a relational bilinear pooling model, and a relational transformer model. Notably, the newly proposed object-relational bilinear graph encoder-decoder (BiGED) model emerges as the most effective among all methods evaluated, demonstrating good proficiency in handling the intricacies of the Action Genome dataset. The contributions of this research significantly advance the ability of deep learning models to reason about current scene evidence and make highly plausible inferences about past human actions. This advancement enables a deeper understanding of events and behaviors, which can enhance decision-making and improve system capabilities across various real-world applications such as Human-Robot Interaction and Elderly Care and Health Monitoring. Code and data available at https://github.com/LUNAProject22/AAR
Composable Coresets for Constrained Determinant Maximization and Beyond
Venue: arXiv cs.DS 2025
Year: 2025

We study algorithms for construction of composable coresets for the task of Determinant Maximization under partition constraint. Given a point set $V\subset \mathbb{R}^d$ that is partitioned into $s$ groups $V_1,\cdots, V_s$, and integers $k_1,...,k_s$, where $k=\sum_i k_i$, the goal is to pick $k_i$ points from group $V_i$ such that the overall determinant of the picked $k$ points is maximized. Determinant Maximization and its constrained variants have gained a lot of interest for modeling diversity, and have found applications in the context of data summarization. When the cardinality $k$ of the selected set is greater than the dimension $d$, we show a peeling algorithm that gives us a composable coreset of size $kd$ with a provably optimal approximation factor of $d^{O(d)}.$ When $k\leq d$, we show a simple coreset construction with optimal size and approximation factor. As a further application of our technique, we get a composable coreset for determinant maximization under the more general laminar matroid constraints, and a composable coreset for unconstrained determinant maximization in a previously unresolved regime. Our results generalize to all strongly Rayleigh distributions and to several other experimental design problems. As an application, we improve the runtime of the practical local-search based algorithm of [Anari-Vuong--COLT'22] for determinantal maximization under partition constraint from $O(n^{2^s}k^{2^s})$ to $O(n k^{2^s})$, making it only linear on the number of points $n$.
DeepTrace: Learning to Optimize Contact Tracing in Epidemic Networks with Graph Neural Networks
Venue: arXiv cs.SI 2025
Year: 2025

Digital contact tracing aims to curb epidemics by identifying and mitigating public health emergencies through technology. Backward contact tracing, which tracks the sources of infection, proved crucial in places like Japan for identifying COVID-19 infections from superspreading events. This paper presents a novel perspective of digital contact tracing as online graph exploration and addresses the forward and backward contact tracing problem as a maximum-likelihood (ML) estimation problem using iterative epidemic network data sampling. The challenge lies in the combinatorial complexity and rapid spread of infections. We introduce DeepTrace, an algorithm based on a Graph Neural Network (GNN) that iteratively updates its estimations as new contact tracing data is collected, learning to optimize the maximum likelihood estimation by utilizing topological features to accelerate learning and improve convergence. The contact tracing process combines either BFS or DFS to expand the network and trace the infection source, ensuring comprehensive and efficient exploration. Additionally, the GNN model is fine-tuned through a two-phase approach: pre-training with synthetic networks to approximate likelihood probabilities and fine-tuning with high-quality data to refine the model. Using COVID-19 variant data, we illustrate that DeepTrace surpasses current methods in identifying superspreaders, providing a robust basis for a scalable digital contact tracing strategy.
Polynomial Identity Testing via Evaluation of Rational Functions
Venue: arXiv cs.CC 2025
Year: 2025

$ \newcommand{\ie}{i.\,e.} $We introduce a hitting set generator for Polynomial Identity Testing based on evaluations of low-degree univariate rational functions at abscissas associated with the variables. We establish an equivalence up to rescaling with a generator introduced by Shpilka and Volkovich, which has a similar structure but uses multivariate polynomials. We initiate a systematic analytic study of the power of hitting set generators by characterizing their vanishing ideals, \ie, the sets of polynomials that they fail to hit. We provide two such characterizations for our generator. First, we develop a small collection of polynomials that jointly produce the vanishing ideal. As corollaries, we obtain tight bounds on the minimum degree, sparseness, and partition class size of set-multilinearity in the vanishing ideal. Second, inspired by a connection to alternating algebra, we develop a structured deterministic membership test for the multilinear part of the vanishing ideal. We present a derivation based on alternating algebra along with the required background, as well as one in terms of zero substitutions and partial derivatives, avoiding the need for alternating algebra. As evidence of the utility of our analytic approach, we rederive known derandomization results based on the generator by Shpilka and Volkovich and present a new application in derandomization / lower bounds for read-once oblivious algebraic branching programs.
UniASM: Binary Code Similarity Detection without Fine-tuning
Venue: arXiv cs.CR 2025
Year: 2025

Binary code similarity detection (BCSD) is widely used in various binary analysis tasks such as vulnerability search, malware detection, clone detection, and patch analysis. Recent studies have shown that the learning-based binary code embedding models perform better than the traditional feature-based approaches. However, previous studies have not delved deeply into the key factors that affect model performance. In this paper, we design extensive ablation studies to explore these influencing factors. The experimental results have provided us with many new insights. We have made innovations in both code representation and model selection: we propose a novel rich-semantic function representation technique to ensure the model captures the intricate nuances of binary code, and we introduce the first UniLM-based binary code embedding model, named UniASM, which includes two newly designed training tasks to learn representations of binary functions. The experimental results show that UniASM outperforms the state-of-the-art (SOTA) approaches on the evaluation datasets. The average scores of Recall@1 on cross-compilers, cross-optimization-levels, and cross-obfuscations have improved by 12.7%, 8.5%, and 22.3%, respectively, compared to the best of the baseline methods. Besides, in the real-world task of known vulnerability search, UniASM outperforms all the current baselines.
Decoding Neural Signals: Invasive BMI Review
Venue: arXiv cs.HC 2025
Year: 2025

Human civilization has witnessed transformative technological milestones, from ancient fire lighting to the internet era. This chapter delves into the invasive brain machine interface (BMI), a pioneering technology poised to be a defining chapter in our progress. Beyond aiding medical conditions, invasive BMI promises far reaching impacts across diverse technologies and aspects of life. The exploration begins by unraveling the biological and engineering principles essential for BMI implementation. The chapter comprehensively analyzes potential applications, methodologies for detecting and decoding brain signals, and options for stimulating signals within the human brain. It concludes with a discussion on the multifaceted challenges and opportunities for the continued development of invasive BMI. This chapter not only provides a profound understanding of the foundational elements of invasive BMI but also serves as a guide through its applications, intricacies, and potential societal implications. Navigating neurobiology, engineering innovations, and the evolving landscape of human AI symbiosis, the chapter sheds light on the promises and hurdles that define the future of invasive BMI.
Care for the Mind Amid Chronic Diseases: An Interpretable AI Approach Using IoT
Venue: arXiv cs.AI 2025
Year: 2025

Health sensing for chronic disease management creates immense benefits for social welfare. Existing health sensing studies primarily focus on the prediction of physical chronic diseases. Depression, a widespread complication of chronic diseases, is however understudied. We draw on the medical literature to support depression detection using motion sensor data. To connect humans in this decision-making, safeguard trust, and ensure algorithm transparency, we develop an interpretable deep learning model: Temporal Prototype Network (TempPNet). TempPNet is built upon the emergent prototype learning models. To accommodate the temporal characteristic of sensor data and the progressive property of depression, TempPNet differs from existing prototype learning models in its capability of capturing temporal progressions of prototypes. Extensive empirical analyses using real-world motion sensor data show that TempPNet outperforms state-of-the-art benchmarks in depression detection. Moreover, TempPNet interprets its decision by visualizing the temporal progression of depression and its corresponding symptoms detected from sensor data. We further employ a user study and a medical expert panel to demonstrate its superiority over the benchmarks in interpretability. This study offers an algorithmic solution for impactful social good -- collaborative care of chronic diseases and depression in health sensing. Methodologically, it contributes to extant literature with a novel interpretable deep learning model for depression detection from sensor data. Patients, doctors, and caregivers can deploy our model on mobile devices to monitor patients' depression risks in real-time. Our model's interpretability also allows human experts to participate in the decision-making by reviewing the interpretation and making informed interventions.
ADEPT: A DEbiasing PrompT Framework
Venue: arXiv cs.CL 2025
Year: 2025

Several works have proven that finetuning is an applicable approach for debiasing contextualized word embeddings. Similarly, discrete prompts with semantic meanings have shown to be effective in debiasing tasks. With unfixed mathematical representation at the token level, continuous prompts usually surpass discrete ones at providing a pre-trained language model (PLM) with additional task-specific information. Despite this, relatively few efforts have been made to debias PLMs by prompt tuning with continuous prompts compared to its discrete counterpart. Furthermore, for most debiasing methods that alter a PLM's original parameters, a major problem is the need to not only decrease the bias in the PLM but also to ensure that the PLM does not lose its representation ability. Finetuning methods typically have a hard time maintaining this balance, as they tend to violently remove meanings of attribute words. In this paper, we propose ADEPT, a method to debias PLMs using prompt tuning while maintaining the delicate balance between removing biases and ensuring representation ability. To achieve this, we propose a new training criterion inspired by manifold learning and equip it with an explicit debiasing term to optimize prompt tuning. In addition, we conduct several experiments with regard to the reliability, quality, and quantity of a previously proposed attribute training corpus in order to obtain a clearer prototype of a certain attribute, which indicates the attribute's position and relative distances to other words on the manifold. We evaluate ADEPT on several widely acknowledged debiasing benchmarks and downstream tasks, and find that it achieves competitive results while maintaining (and in some cases even improving) the PLM's representation ability. We further visualize words' correlation before and after debiasing a PLM, and give some possible explanations for the visible effects.
Efficient Image Generation with Variadic Attention Heads
Venue: arXiv cs.CV 2025
Year: 2025

While the integration of transformers in vision models have yielded significant improvements on vision tasks they still require significant amounts of computation for both training and inference. Restricted attention mechanisms significantly reduce these computational burdens but come at the cost of losing either global or local coherence. We propose a simple, yet powerful method to reduce these trade-offs: allow the attention heads of a single transformer to attend to multiple receptive fields. We demonstrate our method utilizing Neighborhood Attention (NA) and integrate it into a StyleGAN based architecture for image generation. With this work, dubbed StyleNAT, we are able to achieve a FID of 2.05 on FFHQ, a 6% improvement over StyleGAN-XL, while utilizing 28% fewer parameters and with 4$\times$ the throughput capacity. StyleNAT achieves the Pareto Frontier on FFHQ-256 and demonstrates powerful and efficient image generation on other datasets. Our code and model checkpoints are publicly available at: https://github.com/SHI-Labs/StyleNAT
Unrealizability Logic
Venue: arXiv cs.PL 2025
Year: 2025

We consider the problem of establishing that a program-synthesis problem is unrealizable (i.e., has no solution in a given search space of programs). Prior work on unrealizability has developed some automatic techniques to establish that a problem is unrealizable; however, these techniques are all black-box, meaning that they conceal the reasoning behind why a synthesis problem is unrealizable. In this paper, we present a Hoare-style reasoning system, called unrealizability logic for establishing that a program-synthesis problem is unrealizable. To the best of our knowledge, unrealizability logic is the first proof system for overapproximating the execution of an infinite set of imperative programs. The logic provides a general, logical system for building checkable proofs about unrealizability. Similar to how Hoare logic distills the fundamental concepts behind algorithms and tools to prove the correctness of programs, unrealizability logic distills into a single logical system the fundamental concepts that were hidden within prior tools capable of establishing that a program-synthesis problem is unrealizable.
Complete Decomposition of Symmetric Tensors in Linear Time and Polylogarithmic Precision
Venue: arXiv cs.DS 2025
Year: 2025

We study symmetric tensor decompositions, i.e. decompositions of the input symmetric tensor T of order 3 as sum of r 3rd-order tensor powers of u_i where u_i are vectors in \C^n. In order to obtain efficient decomposition algorithms, it is necessary to require additional properties from the u_i. In this paper we assume that the u_i are linearly independent. This implies that r is at most n, i.e., the decomposition of T is undercomplete. We will moreover assume that r=n (we plan to extend this work to the case where r is strictly less than n in a forthcoming paper). We give a randomized algorithm for the following problem: given T, an accuracy parameter epsilon, and an upper bound B on the condition number of the tensor, output vectors u'_i such that u_i and u'_i differ by at most epsilon (in the l_2 norm and up to permutation and multiplication by phases) with high probability. The main novel features of our algorithm are: (1) We provide the first algorithm for this problem that works in the computation model of finite arithmetic and requires only poly-logarithmic (in n, B and 1/epsilon) many bits of precision. (2) Moreover, this is also the first algorithm that runs in linear time in the size of the input tensor. It requires O(n^3) arithmetic operations for all accuracy parameters epsilon = 1/poly(n).