OpenRaiser/Intern-Atlas huggingface dataset:
Decidability of Graph Neural Networks via Logical Characterizations
Venue: arXiv cs.LO 2025
Year: 2025

We present results concerning the expressiveness and decidability of a popular graph learning formalism, graph neural networks (GNNs), exploiting connections with logic. We use a family of recently-discovered decidable logics involving "Presburger quantifiers". We show how to use these logics to measure the expressiveness of classes of GNNs, in some cases getting exact correspondences between the expressiveness of logics and GNNs. We also employ the logics, and the techniques used to analyze them, to obtain decision procedures for verification problems over GNNs. We complement this with undecidability results for static analysis problems involving the logics, as well as for GNN verification problems.
ShapeMoiré: Channel-Wise Shape-Guided Network for Image Demoiréing
Venue: arXiv cs.CV 2025
Year: 2025

Photographing optoelectronic displays often introduces unwanted moiré patterns due to analog signal interference between the pixel grids of the display and the camera sensor arrays. This work identifies two problems that are largely ignored by existing image demoiréing approaches: 1) moiré patterns vary across different channels (RGB); 2) repetitive patterns are constantly observed. However, employing conventional convolutional (CNN) layers cannot address these problems. Instead, this paper presents the use of our recently proposed \emph{Shape} concept. It was originally employed to model consistent features from fragmented regions, particularly when identical or similar objects coexist in an RGB-D image. Interestingly, we find that the Shape information effectively captures the moiré patterns in artifact images. Motivated by this discovery, we propose a new method, ShapeMoiré, for image demoiréing. Beyond modeling shape features at the patch-level, we further extend this to the global image-level and design a novel Shape-Architecture. Consequently, our proposed method, equipped with both ShapeConv and Shape-Architecture, can be seamlessly integrated into existing approaches without introducing any additional parameters or computation overhead during inference. We conduct extensive experiments on four widely used datasets, and the results demonstrate that our ShapeMoiré achieves state-of-the-art performance, particularly in terms of the PSNR metric.
What Foundation Models can Bring for Robot Learning in Manipulation : A Survey
Venue: arXiv cs.RO 2025
Year: 2025

The realization of universal robots is an ultimate goal of researchers. However, a key hurdle in achieving this goal lies in the robots' ability to manipulate objects in their unstructured surrounding environments according to different tasks. The learning-based approach is considered an effective way to address generalization. The impressive performance of foundation models in the fields of computer vision and natural language suggests the potential of embedding foundation models into manipulation tasks as a viable path toward achieving general manipulation capability. However, we believe achieving general manipulation capability requires an overarching framework akin to auto driving. This framework should encompass multiple functional modules, with different foundation models assuming distinct roles in facilitating general manipulation capability. This survey focuses on the contributions of foundation models to robot learning for manipulation. We propose a comprehensive framework and detail how foundation models can address challenges in each module of the framework. What's more, we examine current approaches, outline challenges, suggest future research directions, and identify potential risks associated with integrating foundation models into this domain.
Bootstrap-GS: Self-Supervised Augmentation for High-Fidelity Gaussian Splatting
Venue: arXiv cs.GR 2025
Year: 2025

Recent advancements in 3D Gaussian Splatting (3D-GS) have established new benchmarks for rendering quality and efficiency in 3D reconstruction. However, 3D-GS faces critical limitations when generating novel views that significantly deviate from those encountered during training. Moreover, issues such as dilation and aliasing arise during zoom operations. These challenges stem from a fundamental issue: training sampling deficiency. In this paper, we introduce a bootstrapping framework to address this problem. Our approach synthesizes pseudo-ground truth from novel views that align with the limited training set and reintegrates these synthesized views into the training pipeline. Experimental results demonstrate that our bootstrapping technique not only reduces artifacts but also improves quantitative metrics. Furthermore, our technique is highly adaptable, allowing various Gaussian-based method to benefit from its integration.
Real Time Multi Organ Classification on Computed Tomography Images
Venue: arXiv cs.CV 2025
Year: 2025

Organ segmentation is a fundamental task in medical imaging since it is useful for many clinical automation pipelines. However, some tasks do not require full segmentation. Instead, a classifier can identify the selected organ without segmenting the entire volume. In this study, we demonstrate a classifier based method to obtain organ labels in real time by using a large context size with a sparse data sampling strategy. Although our method operates as an independent classifier at query locations, it can generate full segmentations by querying grid locations at any resolution, offering faster performance than segmentation algorithms. We compared our method with existing segmentation techniques, demonstrating its superior runtime potential for practical applications in medical imaging.
Useful Evaluation: Syntax and Semantics (Technical Report)
Venue: arXiv cs.LO 2025
Year: 2025

This work provides the first inductive definition of useful CBV evaluation. For that, we first restrict the substitution operation in the Value Substitution Calculus to be linear, yielding the LCBV strategy. We then further restrict substitution in LCBV, so that substitution contributes to the progress of the computation. This optimisation is the UCBV strategy, and its notion of substitution is sensitive to the surrounding evaluation context, so it is non-trivial to capture it inductively. Moreover, we show that UCBV is a sound and complete implementation of LCBV, optimised to implement useful evaluation. As a further contribution, we show that an existing notion of usefulness in the literature, namely the GLAMoUr abstract machine, implements the UCBV strategy with polynomial overhead in time. This establishes that UCBV is time-invariant, i.e., that the number of reduction steps to normal form in UCBV can be used as a measure of time complexity. Defining UCBV leads us to the first semantic model of useful CBV evaluation through system U, a non-idempotent intersection type system. Our main result is a characterisation of termination for useful CBV evaluation via system U: a term is typable in system U if and only if it terminates in UCBV. Additionally, system U provides a quantitative interpretation for UCBV, offering exact step-count information for program evaluation. Even though the specification of the operational semantics of UCBV is highly complex, system U is notably simple. As far as we know, system U is one of the scarce quantitative type systems capturing exactly the substitution step-count for a call-by-value strategy.
Replicating Human Anatomy with Vision Controlled Jetting -- A Pneumatic Musculoskeletal Hand and Forearm
Venue: arXiv cs.RO 2025
Year: 2025

The functional replication and actuation of complex structures inspired by nature is a longstanding goal for humanity. Creating such complex structures combining soft and rigid features and actuating them with artificial muscles would further our understanding of natural kinematic structures. We printed a biomimetic hand in a single print process comprised of a rigid skeleton, soft joint capsules, tendons, and printed touch sensors. We showed it's actuation using electric motors. In this work, we expand on this work by adding a forearm that is also closely modeled after the human anatomy and replacing the hand's motors with 22 independently controlled pneumatic artificial muscles (PAMs). Our thin, high-strain (up to 30.1%) PAMs match the performance of state-of-the-art artificial muscles at a lower cost. The system showcases human-like dexterity with independent finger movements, demonstrating successful grasping of various objects, ranging from a small, lightweight coin to a large can of 272g in weight. The performance evaluation, based on fingertip and grasping forces along with finger joint range of motion, highlights the system's potential.
Real-Time Convolutional Neural Network-Based Star Detection and Centroiding Method for CubeSat Star Tracker
Venue: arXiv cs.CV 2025
Year: 2025

Star trackers are one of the most accurate celestial sensors used for absolute attitude determination. The devices detect stars in captured images and accurately compute their projected centroids on an imaging focal plane with subpixel precision. Traditional algorithms for star detection and centroiding often rely on threshold adjustments for star pixel detection and pixel brightness weighting for centroid computation. However, challenges like high sensor noise and stray light can compromise algorithm performance. This article introduces a Convolutional Neural Network (CNN)-based approach for star detection and centroiding, tailored to address the issues posed by noisy star tracker images in the presence of stray light and other artifacts. Trained using simulated star images overlayed with real sensor noise and stray light, the CNN produces both a binary segmentation map distinguishing star pixels from the background and a distance map indicating each pixel's proximity to the nearest star centroid. Leveraging this distance information alongside pixel coordinates transforms centroid calculations into a set of trilateration problems solvable via the least squares method. Our method employs efficient UNet variants for the underlying CNN architectures, and the variants' performances are evaluated. Comprehensive testing has been undertaken with synthetic image evaluations, hardware-in-the-loop assessments, and night sky tests. The tests consistently demonstrated that our method outperforms several existing algorithms in centroiding accuracy and exhibits superior resilience to high sensor noise and stray light interference. An additional benefit of our algorithms is that they can be executed in real-time on low-power edge AI processors.
Coexistence of eMBB+ and mMTC+ in Uplink Cell-Free Massive MIMO Networks
Venue: arXiv cs.IT 2025
Year: 2025

This paper tackles the problem of designing proper uplink multiple access schemes for coexistence between enhanced mobile broadband+ (eMBB+) users and massive machine-type communications+ (mMTC+) devices in a terminal-centric cell-free massive MIMO system. Specifically, the use of a time-frequency spreading technique for the mMTC+ devices has been proposed. Coupled with the assumption of imperfect channel knowledge, closed-form bounds of the achievable (ergodic) rate for the two data services are derived. Using suitable power control mechanisms, we show it is possible to efficiently multiplex eMBB+ and mMTC+ traffic in the same time-frequency resource grid. Numerical experiments reveal interesting trade-offs in the selection of the spreading gain and the number of serving access points within the system. Results also demonstrate that the performance of the mMTC+ devices is slightly affected by the presence of the eMBB+ users. Overall, our approach can endow good quality of service to both 6G cornerstones at once.
ViTHSD: Exploiting Hatred by Targets for Hate Speech Detection on Vietnamese Social Media Texts
Venue: arXiv cs.CL 2025
Year: 2025

The growth of social networks makes toxic content spread rapidly. Hate speech detection is a task to help decrease the number of harmful comments. With the diversity in the hate speech created by users, it is necessary to interpret the hate speech besides detecting it. Hence, we propose a methodology to construct a system for targeted hate speech detection from online streaming texts from social media. We first introduce the ViTHSD - a targeted hate speech detection dataset for Vietnamese Social Media Texts. The dataset contains 10K comments, each comment is labeled to specific targets with three levels: clean, offensive, and hate. There are 5 targets in the dataset, and each target is labeled with the corresponding level manually by humans with strict annotation guidelines. The inter-annotator agreement obtained from the dataset is 0.45 by Cohen's Kappa index, which is indicated as a moderate level. Then, we construct a baseline for this task by combining the Bi-GRU-LSTM-CNN with the pre-trained language model to leverage the power of text representation of BERTology. Finally, we suggest a methodology to integrate the baseline model for targeted hate speech detection into the online streaming system for practical application in preventing hateful and offensive content on social media.
Integrated Sensing and Communications for Unsourced Random Access: Fundamental Limits and Practical Model
Venue: arXiv cs.IT 2025
Year: 2025

This work addresses the problem of integrated sensing and communications (ISAC) involving a massive number of unsourced and uncoordinated users. In the proposed model, known as the unsourced ISAC system (UNISAC), all active communication and sensing users simultaneously share a short frame to transmit their signals without requiring scheduling by the base station or the need to announce their identities. Consequently, the received signal from each user is heavily affected by interference from numerous other users, making it challenging to extract individual transmissions. UNISAC is designed to decode the message sequences from communication users while simultaneously detecting active sensing users and estimating their angles of arrival, regardless of the senders' identities. \textcolor{black}{We establish a second-order achievable bound for UNISAC that explicitly quantifies performance deviations due to finite resources, and we show that it outperforms ISAC approaches built on traditional multiple access methods, including ALOHA, time-division multiple access (TDMA), treating interference as noise (TIN), and a TDMA-based scheme combined with multiple signal classification for sensing.} Additionally, we propose a practical model that validates the feasibility of the achievable result, showing comparable or even superior performance in scenarios with a small number of users. Through numerical simulations, we demonstrate the effectiveness of both the practical UNISAC model and the achievable result.
Kuroda's Translation for Higher-Order Logic
Venue: arXiv cs.LO 2025
Year: 2025

In 1951, Kuroda defined an embedding of classical first-order logic into intuitionistic logic, such that a formula and its translation are equivalent in classical logic. Recently, Brown and Rizkallah extended this translation to higher-order logic, but did not prove the classical equivalence, and showed that the embedding fails in the presence of functional extensionality. We prove that functional extensionality and propositional extensionality are sufficient to derive the classical equivalence between a higher-order formula and its translation. We emphasize a condition under which Kuroda's translation works with functional extensionality.
RAG and RAU: A Survey on Retrieval-Augmented Language Model in Natural Language Processing
Venue: arXiv cs.CL 2025
Year: 2025

Large Language Models (LLMs) have catalyzed significant advancements in Natural Language Processing (NLP), yet they encounter challenges such as hallucination and the need for domain-specific knowledge. To mitigate these, recent methodologies have integrated information retrieved from external resources with LLMs, substantially enhancing their performance across NLP tasks. This survey paper addresses the absence of a comprehensive overview on Retrieval-Augmented Language Models (RALMs), both Retrieval-Augmented Generation (RAG) and Retrieval-Augmented Understanding (RAU), providing an in-depth examination of their paradigm, evolution, taxonomy, and applications. The paper discusses the essential components of RALMs, including Retrievers, Language Models, and Augmentations, and how their interactions lead to diverse model structures and applications. RALMs demonstrate utility in a spectrum of tasks, from translation and dialogue systems to knowledge-intensive applications. The survey includes several evaluation methods of RALMs, emphasizing the importance of robustness, accuracy, and relevance in their assessment. It also acknowledges the limitations of RALMs, particularly in retrieval quality and computational efficiency, offering directions for future research. In conclusion, this survey aims to offer a structured insight into RALMs, their potential, and the avenues for their future development in NLP. The paper is supplemented with a Github Repository containing the surveyed works and resources for further study: https://github.com/2471023025/RALM_Survey.
Towards Scenario- and Capability-Driven Dataset Development and Evaluation: An Approach in the Context of Mapless Automated Driving
Venue: arXiv cs.CV 2025
Year: 2025

The foundational role of datasets in defining the capabilities of deep learning models has led to their rapid proliferation. At the same time, published research focusing on the process of dataset development for environment perception in automated driving has been scarce, thereby reducing the applicability of openly available datasets and impeding the development of effective environment perception systems. Sensor-based, mapless automated driving is one of the contexts where this limitation is evident. While leveraging real-time sensor data, instead of pre-defined HD maps promises enhanced adaptability and safety by effectively navigating unexpected environmental changes, it also increases the demands on the scope and complexity of the information provided by the perception system. To address these challenges, we propose a scenario- and capability-based approach to dataset development. Grounded in the principles of ISO 21448 (safety of the intended functionality, SOTIF), extended by ISO/TR 4804, our approach facilitates the structured derivation of dataset requirements. This not only aids in the development of meaningful new datasets but also enables the effective comparison of existing ones. Applying this methodology to a broad range of existing lane detection datasets, we identify significant limitations in current datasets, particularly in terms of real-world applicability, a lack of labeling of critical features, and an absence of comprehensive information for complex driving maneuvers.
SIMPLOT: Enhancing Chart Question Answering by Distilling Essentials
Venue: arXiv cs.CV 2025
Year: 2025

Recently, interpreting complex charts with logical reasoning has emerged as challenges due to the development of vision-language models. A prior state-of-the-art (SOTA) model has presented an end-to-end method that leverages the vision-language model to convert charts into table format utilizing Large Language Model (LLM) for reasoning. However, unlike natural images, charts contain a mix of essential and irrelevant information required for chart reasoning, and we discover that this characteristic can lower the performance of chart-to-table extraction. In this paper, we introduce SIMPLOT, a method designed to extract only the elements necessary for chart reasoning. The proposed method involves two steps: 1) training to mimic a simple plot that contains only the essential information from a complex chart for table extraction, followed by 2) performing reasoning based on the table. Our model enables accurate chart reasoning without the need for additional annotations or datasets, and its effectiveness is demonstrated through various experiments. Furthermore, we propose a novel prompt mimicking how human interpret charts for more accurate reasoning. Our source code is available at https://github.com/sangwu99/Simplot.
Bypassing Skip-Gram Negative Sampling: Dimension Regularization as a More Efficient Alternative for Graph Embeddings
Venue: arXiv cs.LG 2025
Year: 2025

A wide range of graph embedding objectives decompose into two components: one that enforces similarity, attracting the embeddings of nodes that are perceived as similar, and another that enforces dissimilarity, repelling the embeddings of nodes that are perceived as dissimilar. Without repulsion, the embeddings would collapse into trivial solutions. Skip-Gram Negative Sampling (SGNS) is a popular and efficient repulsion approach that prevents collapse by repelling each node from a sample of dissimilar nodes. In this work, we show that when repulsion is most needed and the embeddings approach collapse, SGNS node-wise repulsion is, in the aggregate, an approximate re-centering of the node embedding dimensions. Such dimension operations are more scalable than node operations and produce a simpler geometric interpretation of the repulsion. Our theoretical result establishes dimension regularization as an effective and more efficient, compared to skip-gram node contrast, approach to enforcing dissimilarity among embeddings of nodes. We use this result to propose a flexible algorithm augmentation framework that improves the scalability of any existing algorithm using SGNS. The framework prioritizes node attraction and replaces SGNS with dimension regularization. We instantiate this generic framework for LINE and node2vec and show that the augmented algorithms preserve downstream link-prediction performance while reducing GPU memory usage by up to 33.3% and training time by 23.4%. Moreover, we show that completely removing repulsion (a special case of our augmentation framework) in LINE reduces training time by 70.9% on average, while increasing link prediction performance, especially for graphs that are globally sparse but locally dense. In general, however, repulsion is needed, and dimension regularization provides an efficient alternative to SGNS.
A Logic for Reasoning About Aggregate-Combine Graph Neural Networks
Venue: arXiv cs.AI 2025
Year: 2025

We propose a modal logic in which counting modalities appear in linear inequalities. We show that each formula can be transformed into an equivalent graph neural network (GNN). We also show that a broad class of GNNs can be transformed efficiently into a formula, thus significantly improving upon the literature about the logical expressiveness of GNNs. We also show that the satisfiability problem is PSPACE-complete. These results bring together the promise of using standard logical methods for reasoning about GNNs and their properties, particularly in applications such as GNN querying, equivalence checking, etc. We prove that such natural problems can be solved in polynomial space.
Proof of Sampling: A Nash Equilibrium-Based Verification Protocol for Decentralized Systems
Venue: arXiv cs.GT 2025
Year: 2025

This paper introduces the Proof of Sampling (PoSP) protocol, a Nash Equilibrium-based verification mechanism, and its application to decentralized machine learning inference through spML. Our protocol has a pure strategy Nash Equilibrium, compelling rational participants to act honestly. It economically disincentivizes dishonest behavior, making it costly for participants to compromise the network's integrity. In our spML protocol, we apply PoSP to decentralized inference for AI applications via a novel cryptographic protocol. The resulting protocol is much more efficient than zero knowledge proof based approaches. Moreover, we anticipate that the PoSP protocol could be effectively utilized for designing verification mechanisms within Actively Validated Services (AVS) in restaking solutions. We further expect that the PoSP protocol could be applied to a variety of other decentralized applications. Our approach enhances the reliability and efficiency of decentralized systems, paving the way for a new generation of decentralized applications.