OpenRaiser/Intern-Atlas huggingface dataset:
A $d^{1/2+o(1)}$ Monotonicity Tester for Boolean Functions on $d$-Dimensional Hypergrids
Venue: arXiv cs.DS 2025
Year: 2025

Monotonicity testing of Boolean functions on the hypergrid, $f:[n]^d \to \{0,1\}$, is a classic topic in property testing. Determining the non-adaptive complexity of this problem is an important open question. For arbitrary $n$, [Black-Chakrabarty-Seshadhri, SODA 2020] describe a tester with query complexity $\widetilde{O}(\varepsilon^{-4/3}d^{5/6})$. This complexity is independent of $n$, but has a suboptimal dependence on $d$. Recently, [Braverman-Khot-Kindler-Minzer, ITCS 2023] and [Black-Chakrabarty-Seshadhri, STOC 2023] describe $\widetilde{O}(\varepsilon^{-2} n^3\sqrt{d})$ and $\widetilde{O}(\varepsilon^{-2} n\sqrt{d})$-query testers, respectively. These testers have an almost optimal dependence on $d$, but a suboptimal polynomial dependence on $n$. In this paper, we describe a non-adaptive, one-sided monotonicity tester with query complexity $O(\varepsilon^{-2} d^{1/2 + o(1)})$, independent of $n$. Up to the $d^{o(1)}$-factors, our result resolves the non-adaptive complexity of monotonicity testing for Boolean functions on hypergrids. The independence of $n$ yields a non-adaptive, one-sided $O(\varepsilon^{-2} d^{1/2 + o(1)})$-query monotonicity tester for Boolean functions $f:\mathbb{R}^d \to \{0,1\}$ associated with an arbitrary product measure.
Torch-Choice: A PyTorch Package for Large-Scale Choice Modeling with Python
Venue: arXiv cs.LG 2025
Year: 2025

The $\texttt{torch-choice}$ is an open-source library for flexible, fast choice modeling with Python and PyTorch. $\texttt{torch-choice}$ provides a $\texttt{ChoiceDataset}$ data structure to manage databases flexibly and memory-efficiently. The paper demonstrates constructing a $\texttt{ChoiceDataset}$ from databases of various formats and functionalities of $\texttt{ChoiceDataset}$. The package implements two widely used models, namely the multinomial logit and nested logit models, and supports regularization during model estimation. The package incorporates the option to take advantage of GPUs for estimation, allowing it to scale to massive datasets while being computationally efficient. Models can be initialized using either R-style formula strings or Python dictionaries. We conclude with a comparison of the computational efficiencies of $\texttt{torch-choice}$ and $\texttt{mlogit}$ in R as (1) the number of observations increases, (2) the number of covariates increases, and (3) the expansion of item sets. Finally, we demonstrate the scalability of $\texttt{torch-choice}$ on large-scale datasets.
Self-Supervised Siamese Autoencoders
Venue: arXiv cs.LG 2025
Year: 2025

In contrast to fully-supervised models, self-supervised representation learning only needs a fraction of data to be labeled and often achieves the same or even higher downstream performance. The goal is to pre-train deep neural networks on a self-supervised task, making them able to extract meaningful features from raw input data afterwards. Previously, autoencoders and Siamese networks have been successfully employed as feature extractors for tasks such as image classification. However, both have their individual shortcomings and benefits. In this paper, we combine their complementary strengths by proposing a new method called SidAE (Siamese denoising autoencoder). Using an image classification downstream task, we show that our model outperforms two self-supervised baselines across multiple data sets and scenarios. Crucially, this includes conditions in which only a small amount of labeled data is available. Empirically, the Siamese component has more impact, but the denoising autoencoder is nevertheless necessary to improve performance.
TBDetector:Transformer-Based Detector for Advanced Persistent Threats with Provenance Graph
Venue: arXiv cs.CR 2025
Year: 2025

APT detection is difficult to detect due to the long-term latency, covert and slow multistage attack patterns of Advanced Persistent Threat (APT). To tackle these issues, we propose TBDetector, a transformer-based advanced persistent threat detection method for APT attack detection. Considering that provenance graphs provide rich historical information and have the powerful attacks historic correlation ability to identify anomalous activities, TBDetector employs provenance analysis for APT detection, which summarizes long-running system execution with space efficiency and utilizes transformer with self-attention based encoder-decoder to extract long-term contextual features of system states to detect slow-acting attacks. Furthermore, we further introduce anomaly scores to investigate the anomaly of different system states, where each state is calculated with an anomaly score corresponding to its similarity score and isolation score. To evaluate the effectiveness of the proposed method, we have conducted experiments on five public datasets, i.e., streamspot, cadets, shellshock, clearscope, and wget_baseline. Experimental results and comparisons with state-of-the-art methods have exhibited better performance of our proposed method.
Polymorphic Coverage Types
Venue: arXiv cs.PL 2025
Year: 2025

Test input generators are an important part of property-based testing (PBT) frameworks, and a key expectation is that they be capable of producing all acceptable elements that satisfy both the function's input type and the generator-provided constraints. However, it is not readily apparent how to validate whether a particular generator's output satisfies this coverage requirement. In practice, developers typically rely on manual inspection and post-mortem analysis of test runs to determine whether a generator provides sufficient coverage; these approaches are error-prone and difficult to scale as generators grow more complex. To address this problem, we present a new refinement-type-based verification procedure for validating the coverage provided by input test generators, based on a novel interpretation of types that embeds "must-style" underapproximate reasoning principles as a fundamental part of the type system. In our formulation, the types associated with expressions capture the set of values guaranteed to be produced by the expression, rather than the usual interpretation in which types represent the set of values an expression may produce. We formalize the notion of coverage types in a rich core language supporting higher-order functions and inductive datatypes. To better support real-world test generators, we extend this type system with type and qualifier polymorphism, enabling static verification of coverage guarantees for test input generators constructed using the monadic combinators found in most PBT frameworks. Finally, we have implemented a coverage type checker for OCaml programs based on this core calculus and present a detailed evaluation of its utility using a corpus of benchmarks drawn from both the PBT literature and open-source projects.
CRISP: Curriculum Inducing Primitive Informed Subgoal Prediction for Hierarchical Reinforcement Learning
Venue: arXiv cs.LG 2025
Year: 2025

Hierarchical reinforcement learning (HRL) leverages temporal abstraction to efficiently tackle complex long-horizon tasks. However, HRL often collapses because the continual updates of the low-level primitive make earlier sub-goals issued by the high-level policy obsolete, introducing non-stationarity that destabilizes training. We propose CRISP, a curriculum-driven framework that tackles this instability with three key ingredients: (1) primitive-informed parsing (PIP), which adaptively re-labels a handful of expert demonstrations to always generate reachable subgoals by the current low-level primitive, (2) an inverse-reinforcement-learning regularizer that steers the high-level policy toward the expert-induced subgoal distribution and stabilizes learning, and (3) a unified training loop that leverages these components to boost sample efficiency. Across six sparse-reward robotic navigation and manipulation benchmarks, CRISP improves success rates by more than 40% over strong hierarchical and flat baselines and successfully transfers to real-world tasks, demonstrating the promise of curriculum-based HRL for practical scenarios.
ZigzagNetVis: Suggesting temporal resolutions for graph visualization using zigzag persistence
Venue: arXiv cs.HC 2025
Year: 2025

Temporal graphs are commonly used to represent complex systems and track the evolution of their constituents over time. Visualizing these graphs is crucial as it allows one to quickly identify anomalies, trends, patterns, and other properties that facilitate better decision-making. In this context, selecting an appropriate temporal resolution is essential for constructing and visually analyzing the layout. The choice of resolution is particularly important, especially when dealing with temporally sparse graphs. In such cases, changing the temporal resolution by grouping events (i.e., edges) from consecutive timestamps -- a technique known as timeslicing -- can aid in the analysis and reveal patterns that might not be discernible otherwise. However, selecting an appropriate temporal resolution is a challenging task. In this paper, we propose ZigzagNetVis, a methodology that suggests temporal resolutions potentially relevant for analyzing a given graph, i.e., resolutions that lead to substantial topological changes in the graph structure. ZigzagNetVis achieves this by leveraging zigzag persistent homology, a well-established technique from Topological Data Analysis (TDA). To improve visual graph analysis, ZigzagNetVis incorporates the colored barcode, a novel timeline-based visualization inspired by persistence barcodes commonly used in TDA. We also contribute with a web-based system prototype that implements suggestion methodology and visualization tools. Finally, we demonstrate the usefulness and effectiveness of ZigzagNetVis through a usage scenario, a user study with 27 participants, and a detailed quantitative evaluation.
Decidability of Querying First-Order Theories via Countermodels of Finite Width
Venue: arXiv cs.LO 2025
Year: 2025

We propose a generic framework for establishing the decidability of a wide range of logical entailment problems (briefly called querying), based on the existence of countermodels that are structurally simple, gauged by certain types of width measures (with treewidth and cliquewidth as popular examples). As an important special case of our framework, we identify logics exhibiting width-finite finitely universal model sets, warranting decidable entailment for a wide range of homomorphism-closed queries, subsuming a diverse set of practically relevant query languages. As a particularly powerful width measure, we propose to employ Blumensath's partitionwidth, which subsumes various other commonly considered width measures and exhibits highly favorable computational and structural properties. Focusing on the formalism of existential rules as a popular showcase, we explain how finite partitionwidth sets of rules subsume other known abstract decidable classes but - leveraging existing notions of stratification - also cover a wide range of new rulesets. We expose natural limitations for fitting the class of finite unification sets into our picture and suggest several options for remedy.
MedAlpaca -- An Open-Source Collection of Medical Conversational AI Models and Training Data
Venue: arXiv cs.CL 2025
Year: 2025

As large language models (LLMs) like OpenAI's GPT series continue to make strides, we witness the emergence of artificial intelligence applications in an ever-expanding range of fields. In medicine, these LLMs hold considerable promise for improving medical workflows, diagnostics, patient care, and education. Yet, there is an urgent need for open-source models that can be deployed on-premises to safeguard patient privacy. In our work, we present an innovative dataset consisting of over 160,000 entries, specifically crafted to fine-tune LLMs for effective medical applications. We investigate the impact of fine-tuning these datasets on publicly accessible pre-trained LLMs, and subsequently, we juxtapose the performance of pre-trained-only models against the fine-tuned models concerning the examinations that future medical doctors must pass to achieve certification.
ATHEENA: A Toolflow for Hardware Early-Exit Network Automation
Venue: arXiv cs.AR 2025
Year: 2025

The continued need for improvements in accuracy, throughput, and efficiency of Deep Neural Networks has resulted in a multitude of methods that make the most of custom architectures on FPGAs. These include the creation of hand-crafted networks and the use of quantization and pruning to reduce extraneous network parameters. However, with the potential of static solutions already well exploited, we propose to shift the focus to using the varying difficulty of individual data samples to further improve efficiency and reduce average compute for classification. Input-dependent computation allows for the network to make runtime decisions to finish a task early if the result meets a confidence threshold. Early-Exit network architectures have become an increasingly popular way to implement such behaviour in software. We create: A Toolflow for Hardware Early-Exit Network Automation (ATHEENA), an automated FPGA toolflow that leverages the probability of samples exiting early from such networks to scale the resources allocated to different sections of the network. The toolflow uses the data-flow model of fpgaConvNet, extended to support Early-Exit networks as well as Design Space Exploration to optimize the generated streaming architecture hardware with the goal of increasing throughput/reducing area while maintaining accuracy. Experimental results on three different networks demonstrate a throughput increase of $2.00\times$ to $2.78\times$ compared to an optimized baseline network implementation with no early exits. Additionally, the toolflow can achieve a throughput matching the same baseline with as low as $46\%$ of the resources the baseline requires.
MFGLib: A Library for Mean-Field Games
Venue: arXiv cs.GT 2025
Year: 2025

Mean-field games (MFGs) are limiting models to approximate $N$-player games, with a number of applications. Despite the ever-growing numerical literature on computation of MFGs, there is no library that allows researchers and practitioners to easily create and solve their own MFG problems. The purpose of this document is to introduce MFGLib, an open-source Python library for solving general MFGs with a user-friendly and customizable interface. It serves as a handy tool for creating and analyzing generic MFG environments, along with embedded auto-tuners for all implemented algorithms. The package is distributed under the MIT license and the source code and documentation can be found at https://github.com/radar-research-lab/MFGLib/.
Random Reed-Solomon Codes Achieve List-Decoding Capacity With Linear-Sized Alphabets
Venue: arXiv cs.IT 2025
Year: 2025

Reed-Solomon codes are a classic family of error-correcting codes consisting of evaluations of low-degree polynomials over a finite field on some sequence of distinct field elements. They are widely known for their optimal unique-decoding capabilities, but their list-decoding capabilities are not fully understood. Given the prevalence of Reed-Solomon codes, a fundamental question in coding theory is determining if Reed-Solomon codes can optimally achieve list-decoding capacity. A recent breakthrough by Brakensiek, Gopi, and Makam established that Reed-Solomon codes are combinatorially list-decodable all the way to capacity. However, their results hold for randomly-punctured Reed-Solomon codes over an exponentially large field size $2^{O(n)}$, where $n$ is the block length of the code. A natural question is whether Reed-Solomon codes can still achieve capacity over smaller fields. We show that Reed-Solomon codes are list-decodable to capacity with linear field size $O(n)$, which is evidently optimal up to a constant factor. Our techniques also show that random linear codes are list-decodable up to capacity with optimal list-size $O(1/\varepsilon)$ and near-optimal alphabet size $2^{O(1/\varepsilon^2)}$, where $\varepsilon$ is the gap to capacity. As far as we are aware, list-decoding up to capacity with optimal list-size $O(1/\varepsilon)$ was not known to be achievable with any linear code over a constant alphabet size (even non-constructively), and it was also not known to be achievable for random linear codes over any alphabet size. With our proof, which maintains a hypergraph perspective of the list-decoding problem, we include an alternate presentation of ideas from Brakensiek, Gopi, and Makam that more directly connects the list-decoding problem to the GM-MDS theorem via a hypergraph orientation theorem.
EPLKG: Efficient Prompt Learning with Knowledge Graph
Venue: arXiv cs.AI 2025
Year: 2025

Large-scale pre-trained models such as CLIP excel in transferability and robust generalization across diverse datasets. However, adapting these models to new datasets or domains is computationally costly, especially in low-resource or few-shot settings, and existing prompt-learning methods often lack interpretability. We introduce Efficient Prompt Learning with Knowledge Graph (EPLKG), which uses a knowledge graph to curate diverse, interpretable prompts and, where KG coverage is limited, augments this bank with LLM-generated human-readable visual descriptions. EPLKG operates entirely on cached CLIP image and text embeddings and employs a lightweight Gumbel-Softmax module to select a single prompt per image-class pair, enabling low-memory, fast training. Across 11 benchmarks, EPLKG reduces per-image training time by up to 45 percent and peak GPU memory by around 30 to 40 percent compared to strong prompt-learning baselines, while keeping the average base-new harmonic-mean accuracy within 2 percentage points, thereby improving the efficiency of model adaptation without sacrificing competitive performance or interpretability.
An Efficient Algorithm for Solving the 2-MAXSAT Problem
Venue: arXiv cs.CC 2025
Year: 2025

By the MAXSAT problem, we are given a set $V$ of $m$ variables and a collection $C$ of $n$ clauses over $V$, i.e., a conjunctive normal form ($\textit{CNF}$) formula. We will seek a truth assignment to maximize the number of satisfied clauses in $C$. This problem is $\textit{NP}$-complete even for its restricted version, the 2-maxsat problem, by which every clause contains at most 2 literals. In this paper, we discuss an efficient algorithm to solve this problem. Its main idea is to transform the 2-maxsat problem into a related problem of maximizing satisfied conjunctions in a disjunctive normal form ($\textit{DNF}$) formula $D$. We then represent all those truth assignments for a conjunction $d$ as a graph (called a $p$*-graph), under each of which $d$ evaluates to $\textit{true}$, and organize all the $p$*-graphs for the conjunctions in $D$ into a trie-like structure. By exploring the structure and recursively its substructures (with each corresponding to a subgraph dynamically built up by integrating some $p$*-subgraphs), the algorithm can find a maximum set of satisfied conjunctions in $D$ in polynomial time. Its worst-case time complexity is bounded by O($n^2m^4$). This provides in fact a proof of $P$ = $\textit{NP}$.
HPSCAN: Human Perception-Based Scattered Data Clustering
Venue: arXiv cs.LG 2025
Year: 2025

Cluster separation is a task typically tackled by widely used clustering techniques, such as k-means or DBSCAN. However, these algorithms are based on non-perceptual metrics, and our experiments demonstrate that their output does not reflect human cluster perception. To bridge the gap between human cluster perception and machine-computed clusters, we propose HPSCAN, a learning strategy that operates directly on scattered data. To learn perceptual cluster separation on such data, we crowdsourced the labeling of 7,320 bivariate (scatterplot) datasets to 384 human participants. We train our HPSCAN model on these human-annotated data. Instead of rendering these data as scatterplot images, we used their x and y point coordinates as input to a modified PointNet++ architecture, enabling direct inference on point clouds. In this work, we provide details on how we collected our dataset, report statistics of the resulting annotations, and investigate the perceptual agreement of cluster separation for real-world data. We also report the training and evaluation protocol for HPSCAN and introduce a novel metric, that measures the accuracy between a clustering technique and a group of human annotators. We explore predicting point-wise human agreement to detect ambiguities. Finally, we compare our approach to ten established clustering techniques and demonstrate that HPSCAN is capable of generalizing to unseen and out-of-scope data.
LostPaw: Finding Lost Pets using a Contrastive Learning-based Transformer with Visual Input
Venue: arXiv cs.CV 2025
Year: 2025

Losing pets can be highly distressing for pet owners, and finding a lost pet is often challenging and time-consuming. An artificial intelligence-based application can significantly improve the speed and accuracy of finding lost pets. To facilitate such an application, this study introduces a contrastive neural network model capable of accurately distinguishing between images of pets. The model was trained on a large dataset of dog images and evaluated through 3-fold cross-validation. Following 350 epochs of training, the model achieved a test accuracy of 90%. Furthermore, overfitting was avoided, as the test accuracy closely matched the training accuracy. Our findings suggest that contrastive neural network models hold promise as a tool for locating lost pets. This paper presents the foundational framework for a potential web application designed to assist users in locating their missing pets. The application will allow users to upload images of their lost pets and provide notifications when matching images are identified within its image database. This functionality aims to enhance the efficiency and accuracy with which pet owners can search for and reunite with their beloved animals.
Fully Automatic Neural Network Reduction for Formal Verification
Venue: arXiv cs.LG 2025
Year: 2025

Formal verification of neural networks is essential before their deployment in safety-critical applications. However, existing methods for formally verifying neural networks are not yet scalable enough to handle practical problems under strict time constraints. We address this challenge by introducing a fully automatic and sound reduction of neural networks using reachability analysis. The soundness ensures that the verification of the reduced network entails the verification of the original network. Our sound reduction approach is applicable to neural networks with any type of element-wise activation function, such as ReLU, sigmoid, and tanh. The network reduction is computed on the fly while simultaneously verifying the original network and its specification. All parameters are automatically tuned to minimize the network size without compromising verifiability. We further show the applicability of our approach to convolutional neural networks by explicitly exploiting similar neighboring pixels. Our evaluation shows that our approach reduces large neural networks to a fraction of the original number of neurons and thus shortens the verification time to a similar degree.