OpenRaiser/Intern-Atlas huggingface dataset:
Double Glueing over Free Exponential: with Measure Theoretic Applications
Venue: arXiv cs.LO 2025
Year: 2025

This paper provides a compact method to lift the free exponential construction of Mellies-Tabareau-Tasson over the Hyland-Schalk double glueing for orthogonality categories. A condition ``reciprocity of orthogonality'' is presented simply enough to lift the free exponential over the double glueing in terms of the orthogonality. Our general method applies to the monoidal category TsK of the s-finite transition kernels with countable biproducts. We show (i) TsK^op has the free exponential, which is shown to be describable in terms of measure theory. (ii) The s-finite transition kernels have an orthogonality between measures and measurable functions in terms of Lebesgue integrals. The orthogonality is reciprocal, hence the free exponential of (i) lifts to the orthogonality category O_I(TsK^op), which subsumes Ehrhard et al's probabilistic coherent spaces as a full subcategory of countable measurable spaces. To lift the free exponential, the measure-theoretic uniform convergence theorem commuting Lebesgue integral and limit plays a crucial role as well as Fubini-Tonelli theorem for double integral in s-finiteness. Our measure-theoretic orthogonality is considered as a continuous version of the orthogonality of the probabilistic coherent spaces for linear logic, and in particular provides a two layered decomposition of Crubille et al's direct free exponential for these spaces.
A survey of Monte Carlo methods for noisy and costly densities with application to reinforcement learning and ABC
Venue: arXiv cs.LG 2025
Year: 2025

This survey gives an overview of Monte Carlo methodologies using surrogate models, for dealing with densities which are intractable, costly, and/or noisy. This type of problem can be found in numerous real-world scenarios, including stochastic optimization and reinforcement learning, where each evaluation of a density function may incur some computationally-expensive or even physical (real-world activity) cost, likely to give different results each time. The surrogate model does not incur this cost, but there are important trade-offs and considerations involved in the choice and design of such methodologies. We classify the different methodologies into three main classes and describe specific instances of algorithms under a unified notation. A modular scheme which encompasses the considered methods is also presented. A range of application scenarios is discussed, with special attention to the likelihood-free setting and reinforcement learning. Several numerical comparisons are also provided.
Automata Linear Dynamic Logic on Finite Traces
Venue: arXiv cs.LO 2025
Year: 2025

Temporal logics are widely used by the Formal Methods and AI communities. Linear Temporal Logic is a popular temporal logic and is valued for its ease of use as well as its balance between expressiveness and complexity. LTL is equivalent in expressiveness to Monadic First-Order Logic and satisfiability for LTL is PSPACE-complete. Linear Dynamic Logic (LDL), another temporal logic, is equivalent to Monadic Second-Order Logic, but its method of satisfiability checking cannot be applied to a nontrivial subset of LDL formulas. Here we introduce Automata Linear Dynamic Logic on Finite Traces (ALDL_f) and show that satisfiability for ALDL_f formulas is in PSPACE. A variant of Linear Dynamic Logic on Finite Traces (LDL_f), ALDL_f combines propositional logic with nondeterministic finite automata (NFA) to express temporal constraints. ALDL$_f$ is equivalent in expressiveness to Monadic Second-Order Logic. This is a gain in expressiveness over LTL at no cost.
Advancing Autonomous Driving: DepthSense with Radar and Spatial Attention
Venue: arXiv cs.RO 2025
Year: 2025

Depth perception is crucial for spatial understanding and has traditionally been achieved through stereoscopic imaging. However, the precision of depth estimation using stereoscopic methods depends on the accurate calibration of binocular vision sensors. Monocular cameras, while more accessible, often suffer from reduced accuracy, especially under challenging imaging conditions. Optical sensors, too, face limitations in adverse environments, leading researchers to explore radar technology as a reliable alternative. Although radar provides coarse but accurate signals, its integration with fine-grained monocular camera data remains underexplored. In this research, we propose DepthSense, a novel radar-assisted monocular depth enhancement approach. DepthSense employs an encoder-decoder architecture, a Radar Residual Network, feature fusion with a spatial attention mechanism, and an ordinal regression layer to deliver precise depth estimations. We conducted extensive experiments on the nuScenes dataset to validate the effectiveness of DepthSense. Our methodology not only surpasses existing approaches in quantitative performance but also reduces parameter complexity and inference times. Our findings demonstrate that DepthSense represents a significant advancement over traditional stereo methods, offering a robust and efficient solution for depth estimation in autonomous driving. By leveraging the complementary strengths of radar and monocular camera data, DepthSense sets a new benchmark in the field, paving the way for more reliable and accurate spatial perception systems.
OMPQ: Orthogonal Mixed Precision Quantization
Venue: arXiv cs.LG 2025
Year: 2025

To bridge the ever increasing gap between deep neural networks' complexity and hardware capability, network quantization has attracted more and more research attention. The latest trend of mixed precision quantization takes advantage of hardware's multiple bit-width arithmetic operations to unleash the full potential of network quantization. However, this also results in a difficult integer programming formulation, and forces most existing approaches to use an extremely time-consuming search process even with various relaxations. Instead of solving a problem of the original integer programming, we propose to optimize a proxy metric, the concept of network orthogonality, which is highly correlated with the loss of the integer programming but also easy to optimize with linear programming. This approach reduces the search time and required data amount by orders of magnitude, with little compromise on quantization accuracy. Specifically, we achieve 72.08% Top-1 accuracy on ResNet-18 with 6.7Mb, which does not require any searching iterations. Given the high efficiency and low data dependency of our algorithm, we used it for the post-training quantization, which achieve 71.27% Top-1 accuracy on MobileNetV2 with only 1.5Mb. Our code is available at https://github.com/MAC-AutoML/OMPQ.
Autonomous Cooperative Transportation System involving Multi-Aerial Robots with Variable Attachment Mechanism
Venue: arXiv cs.RO 2025
Year: 2025

Cooperative transportation by multi-aerial robots has the potential to support various payloads and improve failsafe against dropping. Furthermore, changing the attachment positions of robots according payload characteristics increases the stability of transportation. However, there are almost no transportation systems capable of scaling to the payload weight and size and changing the optimal attachment positions. To address this issue, we propose a cooperative transportation system comprising autonomously executable software and suitable hardware, covering the entire process, from pre-takeoff setting to controlled flight. The proposed system decides the formation of the attachment positions by prioritizing controllability based on the center of gravity obtained from Bayesian estimations with robot pairs. We investigated the cooperative transportation of an unknown payload larger than that of whole carrier robots through numerical simulations. Furthermore, we performed cooperative transportation of an unknown payload (with a weight of about 3.2 kg and maximum length of 1.76 m) using eight robots. The proposed system was found to be versatile with regard to handling unknown payloads with different shapes and center-of-gravity positions.
A Novel Open Set Energy-based Flow Classifier for Network Intrusion Detection
Venue: arXiv cs.CR 2025
Year: 2025

Several machine learning-based Network Intrusion Detection Systems (NIDS) have been proposed in recent years. Still, most of them were developed and evaluated under the assumption that the training context is similar to the test context. This assumption is false in real networks, given the emergence of new attacks and variants of known attacks. To deal with this reality, the open set recognition field, which is the most general task of recognizing classes not seen during training in any domain, began to gain importance in machine learning based NIDS research. Yet, existing solutions are often bound to high temporal complexities and performance bottlenecks. In this work, we propose an algorithm to be used in NIDS that performs open set recognition. Our proposal is an adaptation of the single-class Energy-based Flow Classifier (EFC), which proved to be an algorithm with strong generalization capability and low computational cost. The new version of EFC correctly classifies not only known attacks, but also unknown ones, and differs from other proposals from the literature by presenting a single layer with low temporal complexity. Our proposal was evaluated against well-established multi-class algorithms and as an open set classifier. It proved to be an accurate classifier in both evaluations, similar to the state of the art. As a conclusion of our work, we consider EFC a promising algorithm to be used in NIDS for its high performance and applicability in real networks.
HyperQB: A Bounded Model Checker for Hyperproperties
Venue: arXiv cs.LO 2025
Year: 2025

We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.
Scalable Multi-Agent Reinforcement Learning for Residential Load Scheduling under Data Governance
Venue: arXiv cs.MA 2025
Year: 2025

As a data-driven approach, multi-agent reinforcement learning (MARL) has made remarkable advances in solving cooperative residential load scheduling problems. However, centralized training, the most common paradigm for MARL, limits large-scale deployment in communication-constrained cloud-edge environments. As a remedy, distributed training shows unparalleled advantages in real-world applications but still faces challenge with system scalability, e.g., the high cost of communication overhead during coordinating individual agents, and needs to comply with data governance in terms of privacy. In this work, we propose a novel MARL solution to address these two practical issues. Our proposed approach is based on actor-critic methods, where the global critic is a learned function of individual critics computed solely based on local observations of households. This scheme preserves household privacy completely and significantly reduces communication cost. Simulation experiments demonstrate that the proposed framework achieves comparable performance to the state-of-the-art actor-critic framework without data governance and communication constraints.
Score-based Generative Neural Networks for Large-Scale Optimal Transport
Venue: arXiv cs.LG 2025
Year: 2025

We consider the fundamental problem of sampling the optimal transport coupling between given source and target distributions. In certain cases, the optimal transport plan takes the form of a one-to-one mapping from the source support to the target support, but learning or even approximating such a map is computationally challenging for large and high-dimensional datasets due to the high cost of linear programming routines and an intrinsic curse of dimensionality. We study instead the Sinkhorn problem, a regularized form of optimal transport whose solutions are couplings between the source and the target distribution. We introduce a novel framework for learning the Sinkhorn coupling between two distributions in the form of a score-based generative model. Conditioned on source data, our procedure iterates Langevin Dynamics to sample target data according to the regularized optimal coupling. Key to this approach is a neural network parametrization of the Sinkhorn problem, and we prove convergence of gradient descent with respect to network parameters in this formulation. We demonstrate its empirical success on a variety of large scale optimal transport tasks.
5G Traffic Prediction with Time Series Analysis
Venue: arXiv cs.LG 2025
Year: 2025

In today's day and age, a mobile phone has become a basic requirement needed for anyone to thrive. With the cellular traffic demand increasing so dramatically, it is now necessary to accurately predict the user traffic in cellular networks, so as to improve the performance in terms of resource allocation and utilisation. Since traffic learning and prediction is a classical and appealing field, which still yields many meaningful results, there has been an increasing interest in leveraging Machine Learning tools to analyse the total traffic served in a given region, to optimise the operation of the network. With the help of this project, we seek to exploit the traffic history by using it to predict the nature and occurrence of future traffic. Furthermore, we classify the traffic into particular application types, to increase our understanding of the nature of the traffic. By leveraging the power of machine learning and identifying its usefulness in the field of cellular networks we try to achieve three main objectives - classification of the application generating the traffic, prediction of packet arrival intensity and burst occurrence. The design of the prediction and classification system is done using Long Short Term Memory (LSTM) model. The LSTM predictor developed in this experiment would return the number of uplink packets and also estimate the probability of burst occurrence in the specified future time interval. For the purpose of classification, the regression layer in our LSTM prediction model is replaced by a softmax classifier which is used to classify the application generating the cellular traffic into one of the four applications including surfing, video calling, voice calling, and video streaming.
The Sigma-max System Induced from Randomness & Fuzziness and its Application in Time Series Prediction
Venue: arXiv cs.AI 2025
Year: 2025

This paper managed to induce probability theory (sigma system) and possibility theory (max system) respectively from the clearly-defined randomness and fuzziness, while focusing the question why the key axiom of "maxitivity" is adopted for possibility measure. Such an objective is achieved by following three steps: a) the establishment of mathematical definitions of randomness and fuzziness; b) the development of intuitive definition of possibility as measure of fuzziness based on compatibility interpretation; c) the abstraction of the axiomatic definitions of probability/ possibility from their intuitive definitions, by taking advantage of properties of the well-defined randomness and fuzziness. We derived the conclusion that "max" is the only but un-strict disjunctive operator that is applicable across the fuzzy event space, and is an exact operator for extracting the value from the fuzzy sample space that leads to the largest possibility of one. Then a demonstration example of stock price prediction is presented, which confirms that max inference indeed exhibits distinctive performance, with an improvement up to 18.99%, over sigma inference for the investigated application. Our work provides a physical foundation for the axiomatic definition of possibility for the measure of fuzziness, which hopefully would facilitate wider adoption of possibility theory in practice.
QuantumNAT: Quantum Noise-Aware Training with Noise Injection, Quantization and Normalization
Venue: arXiv cs.LG 2025
Year: 2025

Parameterized Quantum Circuits (PQC) are promising towards quantum advantage on near-term quantum hardware. However, due to the large quantum noises (errors), the performance of PQC models has a severe degradation on real quantum devices. Take Quantum Neural Network (QNN) as an example, the accuracy gap between noise-free simulation and noisy results on IBMQ-Yorktown for MNIST-4 classification is over 60%. Existing noise mitigation methods are general ones without leveraging unique characteristics of PQC; on the other hand, existing PQC work does not consider noise effect. To this end, we present QuantumNAT, a PQC-specific framework to perform noise-aware optimizations in both training and inference stages to improve robustness. We experimentally observe that the effect of quantum noise to PQC measurement outcome is a linear map from noise-free outcome with a scaling and a shift factor. Motivated by that, we propose post-measurement normalization to mitigate the feature distribution differences between noise-free and noisy scenarios. Furthermore, to improve the robustness against noise, we propose noise injection to the training process by inserting quantum error gates to PQC according to realistic noise models of quantum hardware. Finally, post-measurement quantization is introduced to quantize the measurement outcomes to discrete values, achieving the denoising effect. Extensive experiments on 8 classification tasks using 6 quantum devices demonstrate that QuantumNAT improves accuracy by up to 43%, and achieves over 94% 2-class, 80% 4-class, and 34% 10-class classification accuracy measured on real quantum computers. The code for construction and noise-aware training of PQC is available in the TorchQuantum library.
A Fast Horizon Detector and a New Annotated Dataset for Maritime Video Processing
Venue: arXiv cs.CV 2025
Year: 2025

Accurate and fast sea horizon detection is vital for tasks in autonomous navigation and maritime security, such as video stabilization, target region reduction, precise tracking, and obstacle avoidance. This paper introduces a novel sea horizon detector from RGB videos, focusing on rapid and effective sea noise suppression while preserving weak horizon edges. Line fitting methods are subsequently employed on filtered edges for horizon detection. We address the filtering problem by extracting line segments with a very low edge threshold, ensuring the detection of line segments even in low-contrast horizon conditions. We show that horizon line segments have simple and relevant properties in RGB images, which we exploit to suppress noisy segments. Then we use the surviving segments to construct a filtered edge map and infer the horizon from the filtered edges. We propose a careful incorporation of temporal information for horizon inference and experimentally show its effectiveness. We address the computational constraint by providing a vectorized implementation for efficient CPU execution, and leveraging image downsizing with minimal loss of accuracy on the original size. Moreover, we contribute a public horizon line dataset to enrich existing data resources. Our algorithm's performance is rigorously evaluated against state-of-the-art methods, and its components are validated through ablation experiments. Source code and dataset files are available at: https://github.com/Zardoua-Yassir/A_fast_horizon_detector_and_a_new_annotated_dataset_for_maritime_video_processing
3rd Place Solution for VisDA 2021 Challenge -- Universally Domain Adaptive Image Recognition
Venue: arXiv cs.CV 2025
Year: 2025

The Visual Domain Adaptation (VisDA) 2021 Challenge calls for unsupervised domain adaptation (UDA) methods that can deal with both input distribution shift and label set variance between the source and target domains. In this report, we introduce a universal domain adaptation (UniDA) method by aggregating several popular feature extraction and domain adaptation schemes. First, we utilize VOLO, a Transformer-based architecture with state-of-the-art performance in several visual tasks, as the backbone to extract effective feature representations. Second, we modify the open-set classifier of OVANet to recognize the unknown class with competitive accuracy and robustness. As shown in the leaderboard, our proposed UniDA method ranks the 3rd place with 48.49% ACC and 70.8% AUROC in the VisDA 2021 Challenge.
Tracing Content Requirements in Financial Documents using Multi-granularity Text Analysis
Venue: arXiv cs.IR 2025
Year: 2025

The completeness (in terms of content) of financial documents is a fundamental requirement for investment funds. To ensure completeness, financial regulators have to spend significant time carefully checking every financial document based on relevant content requirements, which prescribe the information types to be included in financial documents (e.g., the description of shares' issue conditions and procedures). However, existing techniques provide limited support to help regulators automatically identify the text chunks related to financial information types, due to the complexity of financial documents. In this paper, we propose FITI to trace content requirements in financial documents with multi-granularity text analysis. Given a new financial document, FITI first selects a set of candidate sentences for efficient information type identification. Then, to rank candidate sentences, FITI uses a combination of rule-based and data-centric approaches, by leveraging information retrieval (IR) and machine learning (ML) techniques that analyze the words, sentences, and contexts related to an information type. Finally, a heuristic-based selector, which considers both the sentence ranking and domain-specific phrases, determines a list of sentences corresponding to each information type. We evaluated FITI by assessing its effectiveness in tracing financial content requirements in 100 real-world financial documents. Experimental results show that FITI is able to provide accurate identification with average precision, recall, and F1-score values of 0.824, 0.646, and 0.716, respectively. The overall accuracy of FITI significantly outperforms the best baseline (based on a transformer language model) by 0.266 in terms of F1-score. Furthermore, FITI can help regulators detect about 80% of missing information types in financial documents