OpenRaiser/Intern-Atlas huggingface dataset:
Soteria: Efficient Symbolic Execution as a Functional Library
Venue: arXiv cs.PL 2025
Year: 2025

Symbolic execution (SE) tools often rely on intermediate languages (ILs) to support multiple programming languages, promising reusability and efficiency. In practice, this approach introduces trade-offs between performance, accuracy, and language feature support. We argue that building SE engines \emph{directly} for each source language is both simpler and more effective. We present Soteria, a lightweight OCaml library for writing SE engines in a functional style, without compromising on performance, accuracy or feature support. Soteria enables developers to construct SE engines that operate directly over source-language semantics, offering \emph{configurability}, compositional reasoning, and ease of implementation. Using Soteria, we develop Soteria$^{\text{Rust}}$, the \emph{first} Rust SE engine supporting Tree Borrows (the intricate aliasing model of Rust), and Soteria$^{\text{C}}$, a compositional SE engine for C. Both tools are competitive with or outperform state-of-the-art tools such as Kani, Pulse, CBMC and Gillian-C in performance and the number of bugs detected. We formalise the theoretical foundations of Soteria and prove its soundness, demonstrating that sound, efficient, accurate, and expressive SE can be achieved without the compromises of ILs.
Gromov-Wasserstein Graph Coarsening
Venue: arXiv cs.LG 2025
Year: 2025

We study the problem of graph coarsening within the Gromov-Wasserstein geometry. Specifically, we propose two algorithms that leverage a novel representation of the distortion induced by merging pairs of nodes. The first method, termed Greedy Pair Coarsening (GPC), iteratively merges pairs of nodes that locally minimize a measure of distortion until the desired size is achieved. The second method, termed $k$-means Greedy Pair Coarsening (KGPC), leverages clustering based on pairwise distortion metrics to directly merge clusters of nodes. We provide conditions guaranteeing optimal coarsening for our methods and validate their performance on six large-scale datasets and a downstream clustering task. Results show that the proposed methods outperform existing approaches on a wide range of parameters and scenarios.
Design and Performance Analysis of Hybrid FSO/THz Relay with Aerial RIS for Future NTN-Integrated 6G Wireless Communications
Venue: arXiv cs.IT 2025
Year: 2025

In the context of emerging sixth-generation (6G) wireless networks, reconfigurable intelligent surfaces (RISs) are gaining prominence for their ability to intelligently control electromagnetic wave propagation and enhance backhaul communication performance. In this paper, we propose a novel dual-hop wireless network, where the first hop consists of a hybrid free-space optics (FSO) / terahertz (THz) link, and the second hop incorporates an aerial RIS-based radio frequency (RF) link. To provide a comprehensive performance evaluation, a comparative analysis of two switching strategies is conducted: (1) hard switching and (2) soft switching. Novel closed-form expressions are derived for key performance metrics, including outage probability and bit error rate. These expressions are then utilized to investigate the impact of various system parameters. Our proposed hybrid model demonstrates a 52.54% performance improvement over the traditional RF-FSO framework. Moreover, the integration of an aerial RIS in the second hop enhances system performance by 41.39%. Numerical findings suggest that strategically placing the aerial RIS at a lower altitude and maintaining an equal, shorter distance from both communication endpoints significantly improves overall system performance. To analyze the response under high signal-to-noise ratio (SNR) conditions, asymptotic analysis is performed, and the diversity order of the system is determined. Finally, the analytical results are validated through a Monte Carlo simulation.
CENIC: Convex Error-controlled Numerical Integration for Contact
Venue: arXiv cs.RO 2025
Year: 2025

State-of-the-art robotics simulators operate in discrete time. This requires users to choose a time step, which is both critical and challenging: large steps can produce non-physical artifacts, while small steps force the simulation to run slowly. Continuous-time error-controlled integration avoids such issues by automatically adjusting the time step to achieve a desired accuracy. But existing error-controlled integrators struggle with the stiff dynamics of contact, and cannot meet the speed and scalability requirements of modern robotics workflows. We introduce CENIC, a new continuous-time integrator that brings together recent advances in convex time-stepping and error-controlled integration, inheriting benefits from both continuous integration and discrete time-stepping. CENIC runs at fast real-time rates comparable to discrete-time robotics simulators like MuJoCo, Drake and Isaac Sim, while also providing guarantees on accuracy and convergence.
Dual-Arm Whole-Body Motion Planning: Leveraging Overlapping Kinematic Chains
Venue: arXiv cs.RO 2025
Year: 2025

High degree-of-freedom dual-arm robots are becoming increasingly common due to their morphology enabling them to operate effectively in human environments. However, motion planning in real-time within unknown, changing environments remains a challenge for such robots due to the high dimensionality of the configuration space and the complex collision-avoidance constraints that must be obeyed. In this work, we propose a novel way to alleviate the curse of dimensionality by leveraging the structure imposed by shared joints (e.g. torso joints) in a dual-arm robot. First, we build two dynamic roadmaps (DRM) for each kinematic chain (i.e. left arm + torso, right arm + torso) with specific structure induced by the shared joints. Then, we show that we can leverage this structure to efficiently search through the composition of the two roadmaps and largely sidestep the curse of dimensionality. Finally, we run several experiments in a real-world grocery store with this motion planner on a 19 DoF mobile manipulation robot executing a grocery fulfillment task, achieving 0.4s average planning times with 99.9% success rate across more than 2000 motion plans.
Random Permutations in Computational Complexity
Venue: arXiv cs.CC 2025
Year: 2025

Classical results of Bennett and Gill (1981) show that with probability 1, $P^A \neq NP^A$ relative to a random oracle $A$, and with probability 1, $P^π\neq NP^π\cap coNP^π$ relative to a random permutation $π$. Whether $P^A = NP^A \cap coNP^A$ holds relative to a random oracle $A$ remains open. While the random oracle separation has been extended to specific individually random oracles--such as Martin-Löf random or resource-bounded random oracles--no analogous result is known for individually random permutations. We introduce a new resource-bounded measure framework for analyzing individually random permutations. We define permutation martingales and permutation betting games that characterize measure-zero sets in the space of permutations, enabling formal definitions of resource-bounded random permutations. Our main result shows that $P^π\neq NP^π\cap coNP^π$ for every polynomial-time betting-game random permutation $π$. This is the first separation result relative to individually random permutations, rather than an almost-everywhere separation. We also strengthen a quantum separation of Bennett, Bernstein, Brassard, and Vazirani (1997) by showing that $NP^π\cap coNP^π\not\subseteq BQP^π$ for every polynomial-space random permutation $π$. We investigate the relationship between random permutations and random oracles. We prove that random oracles are polynomial-time reducible from random permutations. The converse--whether every random permutation is reducible from a random oracle--remains open. We show that if $NP \cap coNP$ is not a measurable subset of $EXP$, then $P^A \neq NP^A \cap coNP^A$ holds with probability 1 relative to a random oracle $A$. Conversely, establishing this random oracle separation with time-bounded measure would imply $BPP$ is a measure 0 subset of $EXP$.
Tracing AG Codes: Toward Meeting the Gilbert-Varshamov Bound
Venue: arXiv cs.IT 2025
Year: 2025

One of the oldest problems in coding theory is to match the Gilbert-Varshamov bound with explicit binary codes. Over larger-yet still constant-sized-fields, algebraic-geometry codes are known to beat the GV bound. In this work, we leverage this phenomenon by taking traces of AG codes. Our hope is that the margin by which AG codes exceed the GV bound will withstand the parameter loss incurred by taking the trace from a constant field extension to the binary field. In contrast to concatenation, the usual alphabet-reduction method, our analysis of trace-of-AG (TAG) codes uses the AG codes' algebraic structure throughout - including in the alphabet-reduction step. Our main technical contribution is a Hasse-Weil-type theorem that is well-suited for the analysis of TAG codes. The classical theorem (and its Grothendieck trace-formula extension) are inadequate in this setting. Although we do not obtain improved constructions, we show that a constant-factor strengthening of our bound would suffice. We also analyze the limitations of TAG codes under our bound and prove that, in the high-distance regime, they are inferior to code concatenation. Our Hasse-Weil-type theorem holds in far greater generality than is needed for analyzing TAG codes. In particular, we derive new estimates for exponential sums.
DT-NVS: Diffusion Transformers for Novel View Synthesis
Venue: arXiv cs.CV 2025
Year: 2025

Generating novel views of a natural scene, e.g., every-day scenes both indoors and outdoors, from a single view is an under-explored problem, even though it is an organic extension to the object-centric novel view synthesis. Existing diffusion-based approaches focus rather on small camera movements in real scenes or only consider unnatural object-centric scenes, limiting their potential applications in real-world settings. In this paper we move away from these constrained regimes and propose a 3D diffusion model trained with image-only losses on a large-scale dataset of real-world, multi-category, unaligned, and casually acquired videos of everyday scenes. We propose DT-NVS, a 3D-aware diffusion model for generalized novel view synthesis that exploits a transformer-based architecture backbone. We make significant contributions to transformer and self-attention architectures to translate images to 3d representations, and novel camera conditioning strategies to allow training on real-world unaligned datasets. In addition, we introduce a novel training paradigm swapping the role of reference frame between the conditioning image and the sampled noisy input. We evaluate our approach on the 3D task of generalized novel view synthesis from a single input image and show improvements over state-of-the-art 3D aware diffusion models and deterministic approaches, while generating diverse outputs.
3D Guard-Layer: An Integrated Agentic AI Safety System for Edge Artificial Intelligence
Venue: arXiv cs.AR 2025
Year: 2025

AI systems have found a wide range of real-world applications in recent years. The adoption of edge artificial intelligence, embedding AI directly into edge devices, is rapidly growing. Despite the implementation of guardrails and safety mechanisms, security vulnerabilities and challenges have become increasingly prevalent in this domain, posing a significant barrier to the practical deployment and safety of AI systems. This paper proposes an agentic AI safety architecture that leverages 3D to integrate a dedicated safety layer. It introduces an adaptive AI safety infrastructure capable of dynamically learning and mitigating attacks against the AI system. The system leverages the inherent advantages of co-location with the edge computing hardware to continuously monitor, detect and proactively mitigate threats to the AI system. The integration of local processing and learning capabilities enhances resilience against emerging network-based attacks while simultaneously improving system reliability, modularity, and performance, all with minimal cost and 3D integration overhead.
Decomposition of Small Transformer Models
Venue: arXiv cs.LG 2025
Year: 2025

Recent work in mechanistic interpretability has shown that decomposing models in parameter space may yield clean handles for analysis and intervention. Previous methods have demonstrated successful applications on a wide range of toy models, but the gap to "real models" has not yet been bridged. In this work, we extend Stochastic Parameter Decomposition (SPD) to Transformer models, proposing an updated causal importance function suited for sequential data and a new loss function. We demonstrate that SPD can successfully decompose a toy induction-head model and recover the expected 2-step circuit. We also show that applying SPD to GPT-2-small can successfully locate subcomponents corresponding to interpretable concepts like "golf" and "basketball". These results take the first step in the direction of extending SPD to modern models, and show that we can use the method to surface interpretable parameter-space mechanisms.
Weaver: Kronecker Product Approximations of Spatiotemporal Attention for Traffic Network Forecasting
Venue: arXiv cs.LG 2025
Year: 2025

Spatiotemporal forecasting on transportation networks is a complex task that requires understanding how traffic nodes interact within a dynamic, evolving system dictated by traffic flow dynamics and social behavioral patterns. The importance of transportation networks and ITS for modern mobility and commerce necessitates forecasting models that are not only accurate but also interpretable, efficient, and robust under structural or temporal perturbations. Recent approaches, particularly Transformer-based architectures, have improved predictive performance but often at the cost of high computational overhead and diminished architectural interpretability. In this work, we introduce Weaver, a novel attention-based model that applies Kronecker product approximations (KPA) to decompose the PN X PN spatiotemporal attention of O(P^2N^2) complexity into local P X P temporal and N X N spatial attention maps. This Kronecker attention map enables our Parallel-Kronecker Matrix-Vector product (P2-KMV) for efficient spatiotemporal message passing with O(P^2N + N^2P) complexity. To capture real-world traffic dynamics, we address the importance of negative edges in modeling traffic behavior by introducing Valence Attention using the continuous Tanimoto coefficient (CTC), which provides properties conducive to precise latent graph generation and training stability. To fully utilize the model's learning capacity, we introduce the Traffic Phase Dictionary for self-conditioning. Evaluations on PEMS-BAY and METR-LA show that Weaver achieves competitive performance across model categories while training more efficiently.
Consistency Change Detection Framework for Unsupervised Remote Sensing Change Detection
Venue: arXiv cs.CV 2025
Year: 2025

Unsupervised remote sensing change detection aims to monitor and analyze changes from multi-temporal remote sensing images in the same geometric region at different times, without the need for labeled training data. Previous unsupervised methods attempt to achieve style transfer across multi-temporal remote sensing images through reconstruction by a generator network, and then capture the unreconstructable areas as the changed regions. However, it often leads to poor performance due to generator overfitting. In this paper, we propose a novel Consistency Change Detection Framework (CCDF) to address this challenge. Specifically, we introduce a Cycle Consistency (CC) module to reduce the overfitting issues in the generator-based reconstruction. Additionally, we propose a Semantic Consistency (SC) module to enable detail reconstruction. Extensive experiments demonstrate that our method outperforms other state-of-the-art approaches.
iSeal: Encrypted Fingerprinting for Reliable LLM Ownership Verification
Venue: arXiv cs.CR 2025
Year: 2025

Given the high cost of large language model (LLM) training from scratch, safeguarding LLM intellectual property (IP) has become increasingly crucial. As the standard paradigm for IP ownership verification, LLM fingerprinting thus plays a vital role in addressing this challenge. Existing LLM fingerprinting methods verify ownership by extracting or injecting model-specific features. However, they overlook potential attacks during the verification process, leaving them ineffective when the model thief fully controls the LLM's inference process. In such settings, attackers may share prompt-response pairs to enable fingerprint unlearning or manipulate outputs to evade exact-match verification. We propose iSeal, the first fingerprinting method designed for reliable verification when the model thief controls the suspected LLM in an end-to-end manner. It injects unique features into both the model and an external module, reinforced by an error-correction mechanism and a similarity-based verification strategy. These components are resistant to verification-time attacks, including collusion-based fingerprint unlearning and response manipulation, backed by both theoretical analysis and empirical results. iSeal achieves 100 percent Fingerprint Success Rate (FSR) on 12 LLMs against more than 10 attacks, while baselines fail under unlearning and response manipulations.
HitoMi-Cam: A Shape-Agnostic Person Detection Method Using the Spectral Characteristics of Clothing
Venue: arXiv cs.CV 2025
Year: 2025

While convolutional neural network (CNN)-based object detection is widely used, it exhibits a shape dependency that degrades performance for postures not included in the training data. Building upon our previous simulation study published in this journal, this study implements and evaluates the spectral-based approach on physical hardware to address this limitation. Specifically, this paper introduces HitoMi-Cam, a lightweight and shape-agnostic person detection method that uses the spectral reflectance properties of clothing. The author implemented the system on a resource-constrained edge device without a GPU to assess its practical viability. The results indicate that a processing speed of 23.2 frames per second (fps) (253x190 pixels) is achievable, suggesting that the method can be used for real-time applications. In a simulated search and rescue scenario where the performance of CNNs declines, HitoMi-Cam achieved an average precision (AP) of 93.5%, surpassing that of the compared CNN models (best AP of 53.8%). Throughout all evaluation scenarios, the occurrence of false positives remained minimal. This study positions the HitoMi-Cam method not as a replacement for CNN-based detectors but as a complementary tool under specific conditions. The results indicate that spectral-based person detection can be a viable option for real-time operation on edge devices in real-world environments where shapes are unpredictable, such as disaster rescue.
HalluClean: A Unified Framework to Combat Hallucinations in LLMs
Venue: arXiv cs.CL 2025
Year: 2025

Large language models (LLMs) have achieved impressive performance across a wide range of natural language processing tasks, yet they often produce hallucinated content that undermines factual reliability. To address this challenge, we introduce HalluClean, a lightweight and task-agnostic framework for detecting and correcting hallucinations in LLM-generated text. HalluClean adopts a reasoning-enhanced paradigm, explicitly decomposing the process into planning, execution, and revision stages to identify and refine unsupported claims. It employs minimal task-routing prompts to enable zero-shot generalization across diverse domains, without relying on external knowledge sources or supervised detectors. We conduct extensive evaluations on five representative tasks-question answering, dialogue, summarization, math word problems, and contradiction detection. Experimental results show that HalluClean significantly improves factual consistency and outperforms competitive baselines, demonstrating its potential to enhance the trustworthiness of LLM outputs in real-world applications.
The Double Contingency Problem: AI Recursion and the Limits of Interspecies Understanding
Venue: arXiv cs.AI 2025
Year: 2025

Current bioacoustic AI systems achieve impressive cross-species performance by processing animal communication through transformer architectures, foundation model paradigms, and other computational approaches. However, these approaches overlook a fundamental question: what happens when one form of recursive cognition--AI systems with their attention mechanisms, iterative processing, and feedback loops--encounters the recursive communicative processes of other species? Drawing on philosopher Yuk Hui's work on recursivity and contingency, I argue that AI systems are not neutral pattern detectors but recursive cognitive agents whose own information processing may systematically obscure or distort other species' communicative structures. This creates a double contingency problem: each species' communication emerges through contingent ecological and evolutionary conditions, while AI systems process these signals through their own contingent architectural and training conditions. I propose that addressing this challenge requires reconceptualizing bioacoustic AI from universal pattern recognition toward diplomatic encounter between different forms of recursive cognition, with implications for model design, evaluation frameworks, and research methodologies.
A Research on Business Process Optimisation Model Integrating AI and Big Data Analytics
Venue: arXiv cs.AI 2025
Year: 2025

With the deepening of digital transformation, business process optimisation has become the key to improve the competitiveness of enterprises. This study constructs a business process optimisation model integrating artificial intelligence and big data to achieve intelligent management of the whole life cycle of processes. The model adopts a three-layer architecture incorporating data processing, AI algorithms, and business logic to enable real-time process monitoring and optimization. Through distributed computing and deep learning techniques, the system can handle complex business scenarios while maintaining high performance and reliability. Experimental validation across multiple enterprise scenarios shows that the model shortens process processing time by 42%, improves resource utilisation by 28%, and reduces operating costs by 35%. The system maintained 99.9% availability under high concurrent loads. The research results have important theoretical and practical value for promoting the digital transformation of enterprises, and provide new ideas for improving the operational efficiency of enterprises.
QIBONN: A Quantum-Inspired Bilevel Optimizer for Neural Networks on Tabular Classification
Venue: arXiv cs.LG 2025
Year: 2025

Hyperparameter optimization (HPO) for neural networks on tabular data is critical to a wide range of applications, yet it remains challenging due to large, non-convex search spaces and the cost of exhaustive tuning. We introduce the Quantum-Inspired Bilevel Optimizer for Neural Networks (QIBONN), a bilevel framework that encodes feature selection, architectural hyperparameters, and regularization in a unified qubit-based representation. By combining deterministic quantum-inspired rotations with stochastic qubit mutations guided by a global attractor, QIBONN balances exploration and exploitation under a fixed evaluation budget. We conduct systematic experiments under single-qubit bit-flip noise (0.1\%--1\%) emulated by an IBM-Q backend. Results on 13 real-world datasets indicate that QIBONN is competitive with established methods, including classical tree-based methods and both classical/quantum-inspired HPO algorithms under the same tuning budget.