OpenRaiser/Intern-Atlas huggingface dataset:
The Boolean Solution Problem from the Perspective of Predicate Logic -- Extended Version
Venue: arXiv cs.LO 2025
Year: 2025

Finding solution values for unknowns in Boolean equations was a principal reasoning mode in the Algebra of Logic of the 19th century. Schröder investigated it as Auflösungsproblem (solution problem). It is closely related to the modern notion of Boolean unification. Today it is commonly presented in an algebraic setting, but seems potentially useful also in knowledge representation based on predicate logic. We show that it can be modeled on the basis of first-order logic extended by second-order quantification. A wealth of classical results transfers, foundations for algorithms unfold, and connections with second-order quantifier elimination and Craig interpolation become apparent. Although for first-order inputs the set of solutions is recursively enumerable, the development of constructive methods remains a challenge. We identify some cases that allow constructions, most of them based on Craig interpolation.
Simple Compact Monotone Tree Drawings
Venue: arXiv cs.DS 2025
Year: 2025

A monotone drawing of a graph G is a straight-line drawing of G such that every pair of vertices is connected by a path that is monotone with respect to some direction. Trees, as a special class of graphs, have been the focus of several papers and, recently, He and He~\cite{mt:4} showed how to produce a monotone drawing of an arbitrary $n$-vertex tree that is contained in a $12n \times 12n$ grid. All monotone tree drawing algorithms that have appeared in the literature consider rooted ordered trees and they draw them so that (i) the root of the tree is drawn at the origin of the drawing, (ii) the drawing is confined in the first quadrant, and (iii) the ordering/embedding of the tree is respected. In this paper, we provide a simple algorithm that has the exact same characteristics and, given an $n$-vertex rooted tree $T$, it outputs a monotone drawing of $T$ that fits on a $n \times n$ grid. For unrooted ordered trees, we present an algorithms that produces monotone drawings that respect the ordering and fit in an $(n+1) \times (\frac{n}{2} +1)$ grid, while, for unrooted non-ordered trees we produce monotone drawings of good aspect ratio which fit on a grid of size at most $\left\lfloor \frac{3}{4} \left(n+2\right)\right\rfloor \times \left\lfloor \frac{3}{4} \left(n+2\right)\right\rfloor$.
Mission Aware Cyber-physical Security
Venue: arXiv cs.CR 2025
Year: 2025

Perimeter cybersecurity, while essential, has proven insufficient against sophisticated, coordinated, and cyber-physical attacks. In contrast, mission-centric cybersecurity emphasizes finding evidence of attack impact on mission success, allowing for targeted resource allocation to mitigate vulnerabilities and protect critical assets. Mission Aware is a systems-theoretic cybersecurity analysis that identifies components which, if compromised, destabilize the overall mission. It generates evidence by finding potential attack vectors relevant to mission-linked elements and traces this evidence to mission requirements, prioritizing high-impact vulnerabilities relative to mission objectives. Mission Aware is an informational tool for system resilience by unifying cybersecurity analysis with core systems engineering goals.
Minimal Algorithmic Information Loss Methods for Dimension Reduction, Feature Selection and Network Sparsification
Venue: arXiv cs.DS 2025
Year: 2025

We present a novel, domain-agnostic, model-independent, unsupervised, and universally applicable Machine Learning approach for dimensionality reduction based on the principles of algorithmic complexity. Specifically, but without loss of generality, we focus on addressing the challenge of reducing certain dimensionality aspects, such as the number of edges in a network, while retaining essential features of interest. These features include preserving crucial network properties like degree distribution, clustering coefficient, edge betweenness, and degree and eigenvector centralities but can also go beyond edges to nodes and weights for network pruning and trimming. Our approach outperforms classical statistical Machine Learning techniques and state-of-the-art dimensionality reduction algorithms by preserving a greater number of data features that statistical algorithms would miss, particularly nonlinear patterns stemming from deterministic recursive processes that may look statistically random but are not. Moreover, previous approaches heavily rely on a priori feature selection, which requires constant supervision. Our findings demonstrate the effectiveness of the algorithms in overcoming some of these limitations while maintaining a time-efficient computational profile. Our approach not only matches, but also exceeds, the performance of established and state-of-the-art dimensionality reduction algorithms. We extend the applicability of our method to lossy compression tasks involving images and any multi-dimensional data. This highlights the versatility and broad utility of the approach in multiple domains.
Distributed Treewidth Computation and Courcelle's Theorem in the CONGEST Model
Venue: arXiv cs.DS 2025
Year: 2025

Algorithmic meta-theorems, stating that graph properties expressible in some particular logic can be decided efficiently in graph classes having some specific structural properties, are now standard in sequential graph algorithms. One of the most classic examples is Courcelle's theorem: all properties expressible in Monadic Second-Order logic (MSO) are decidable in linear time in graphs of bounded treewidth. We provide here a distributed version of Courcelle's theorem, in the standard CONGEST model for distributed computing: For any MSO formula $φ$ and any constant $k$, there is a CONGEST algorithm that, given an input communication network $G$ of treewidth at most $k$ and of diameter $D$, decides if $G$ satisfies property $φ$ in $\tilde O(D)$ rounds. Simple examples show that the dependency on $D$ is unavoidable. Also, if we drop the assumption of bounded treewidth, deciding MSO properties such as 3-colorability are known to require $\tildeΩ(n^2)$ rounds in the CONGEST model. Our results extend to optimization problems (e.g., computing a maximum size independent set, or a minimum dominating set) and counting (e.g. triangle counting). As usual, the $\tilde{O}$ notation hides polylogarithmic factors in $n$; here it also hides a constant factor depending on $k$ and on the MSO formula $φ$. We also give a distributed algorithm producing a linear approximation for treewidth: For any $k$, it decides that the treewidth of the input network $G$ is larger than $k$ or computes a tree decomposition of width $O(k)$ and depth $O(\log n)$, in $\tilde O(k^{O(k)} D)$ rounds in CONGEST. Our algorithms make use of the low-congestion shortcuts framework introduced by Ghaffari and Haeupler [SODA 2016], and our main technical tool is an $\tilde O(k^4 D)$ algorithm for computing $(s,t)$-vertex separators of size at most $k+1$ in graphs of treewidth at most $k$.
Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation
Venue: arXiv cs.LO 2025
Year: 2025

In \cite{Craig}, we introduced a syntactically defined and highly general class of calculi known as \emph{semi-analytic}. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must satisfy the Craig interpolation property. In this paper, we show that if the calculus is also terminating in a certain formal sense, then its logic has the Uniform Interpolation Property (UIP). This result has significant applications. On the positive side, it provides a uniform and modular method for proving UIP for various logics, including $\mathsf{FL_e}$, $\mathsf{FL_{ew}}$, $\mathsf{CFL_e}$, $\mathsf{CFL_{ew}}$, and their $K$, $D$, and $T$-type modal extensions, as well as $\mathsf{CPC}$, $\mathsf{K}$, and $\mathsf{KD}$. However, its more striking consequence lies in the negative direction. It extends the negative results of \cite{Craig} to logics with CIP but without UIP. In particular, it shows that the modal logics $\mathsf{K4}$ and $\mathsf{S4}$ do not have a terminating semi-analytic calculus. \textbf{keywords:} Uniform interpolation, Sequent calculi, Substructural logics, Modal logics, Subexponential modalities
Discovering Influential Factors in Variational Autoencoders
Venue: arXiv cs.LG 2025
Year: 2025

In the field of machine learning, it is still a critical issue to identify and supervise the learned representation without manually intervening or intuition assistance to extract useful knowledge or serve for the downstream tasks. In this work, we focus on supervising the influential factors extracted by the variational autoencoder(VAE). The VAE is proposed to learn independent low dimension representation while facing the problem that sometimes pre-set factors are ignored. We argue that the mutual information of the input and each learned factor of the representation plays a necessary indicator of discovering the influential factors. We find the VAE objective inclines to induce mutual information sparsity in factor dimension over the data intrinsic dimension and therefore result in some non-influential factors whose function on data reconstruction could be ignored. We show mutual information also influences the lower bound of the VAE's reconstruction error and downstream classification task. To make such indicator applicable, we design an algorithm for calculating the mutual information for the VAE and prove its consistency. Experimental results on MNIST, CelebA and DEAP datasets show that mutual information can help determine influential factors, of which some are interpretable and can be used to further generation and classification tasks, and help discover the variant that connects with emotion on DEAP dataset.
Semantic and structural image segmentation for prosthetic vision
Venue: arXiv cs.CV 2025
Year: 2025

Prosthetic vision is being applied to partially recover the retinal stimulation of visually impaired people. However, the phosphenic images produced by the implants have very limited information bandwidth due to the poor resolution and lack of color or contrast. The ability of object recognition and scene understanding in real environments is severely restricted for prosthetic users. Computer vision can play a key role to overcome the limitations and to optimize the visual information in the simulated prosthetic vision, improving the amount of information that is presented. We present a new approach to build a schematic representation of indoor environments for phosphene images. The proposed method combines a variety of convolutional neural networks for extracting and conveying relevant information about the scene such as structural informative edges of the environment and silhouettes of segmented objects. Experiments were conducted with normal sighted subjects with a Simulated Prosthetic Vision system. The results show good accuracy for object recognition and room identification tasks for indoor scenes using the proposed approach, compared to other image processing methods.
A Search for Good Pseudo-random Number Generators : Survey and Empirical Studies
Venue: arXiv cs.CR 2025
Year: 2025

This paper targets to search so-called \emph{good} generators by doing a brief survey over the generators developed in the history of pseudo-random number generators (PRNGs), verify their claims and rank them based on strong empirical tests in same platforms. To do this, the genre of PRNGs developed so far are explored and classified into three groups -- linear congruential generator based, linear feedback shift register based and cellular automata based. From each group, the well-known widely used generators which claimed themselves to be `\emph{good}' are chosen. Overall $30$ PRNGs are selected in this way on which two types of empirical testing are done -- blind statistical tests with Diehard battery of tests, battery \emph{rabbit} of TestU01 library and NIST statistical test-suite as well as graphical tests (lattice test and space-time diagram test). Finally, the selected PRNGs are divided into $24$ groups and are ranked according to their overall performance in all empirical tests.
CRAVES: Controlling Robotic Arm with a Vision-based Economic System
Venue: arXiv cs.CV 2025
Year: 2025

Training a robotic arm to accomplish real-world tasks has been attracting increasing attention in both academia and industry. This work discusses the role of computer vision algorithms in this field. We focus on low-cost arms on which no sensors are equipped and thus all decisions are made upon visual recognition, e.g., real-time 3D pose estimation. This requires annotating a lot of training data, which is not only time-consuming but also laborious. In this paper, we present an alternative solution, which uses a 3D model to create a large number of synthetic data, trains a vision model in this virtual domain, and applies it to real-world images after domain adaptation. To this end, we design a semi-supervised approach, which fully leverages the geometric constraints among keypoints. We apply an iterative algorithm for optimization. Without any annotations on real images, our algorithm generalizes well and produces satisfying results on 3D pose estimation, which is evaluated on two real-world datasets. We also construct a vision-based control system for task accomplishment, for which we train a reinforcement learning agent in a virtual environment and apply it to the real-world. Moreover, our approach, with merely a 3D model being required, has the potential to generalize to other types of multi-rigid-body dynamic systems. Website: https://qiuwch.github.io/craves.ai. Code: https://github.com/zuoym15/craves.ai
The Kikuchi Hierarchy and Tensor PCA
Venue: arXiv cs.DS 2025
Year: 2025

For the tensor PCA (principal component analysis) problem, we propose a new hierarchy of increasingly powerful algorithms with increasing runtime. Our hierarchy is analogous to the sum-of-squares (SOS) hierarchy but is instead inspired by statistical physics and related algorithms such as belief propagation and AMP (approximate message passing). Our level-$\ell$ algorithm can be thought of as a linearized message-passing algorithm that keeps track of $\ell$-wise dependencies among the hidden variables. Specifically, our algorithms are spectral methods based on the Kikuchi Hessian, which generalizes the well-studied Bethe Hessian to the higher-order Kikuchi free energies. It is known that AMP, the flagship algorithm of statistical physics, has substantially worse performance than SOS for tensor PCA. In this work we 'redeem' the statistical physics approach by showing that our hierarchy gives a polynomial-time algorithm matching the performance of SOS. Our hierarchy also yields a continuum of subexponential-time algorithms, and we prove that these achieve the same (conjecturally optimal) tradeoff between runtime and statistical power as SOS. Our proofs are much simpler than prior work, and also apply to the related problem of refuting random $k$-XOR formulas. The results we present here apply to tensor PCA for tensors of all orders, and to $k$-XOR when $k$ is even. Our methods suggest a new avenue for systematically obtaining optimal algorithms for Bayesian inference problems, and our results constitute a step toward unifying the statistical physics and sum-of-squares approaches to algorithm design.
Progressive Cross-Stream Cooperation in Spatial and Temporal Domain for Action Localization
Venue: arXiv cs.CV 2025
Year: 2025

Spatio-temporal action localization consists of three levels of tasks: spatial localization, action classification, and temporal localization. In this work, we propose a new progressive cross-stream cooperation (PCSC) framework that improves all three tasks above. The basic idea is to utilize both spatial region (resp., temporal segment proposals) and features from one stream (i.e., the Flow/RGB stream) to help another stream (i.e., the RGB/Flow stream) to iteratively generate better bounding boxes in the spatial domain (resp., temporal segments in the temporal domain). In this way, not only the actions could be more accurately localized both spatially and temporally, but also the action classes could be predicted more precisely. Specifically, we first combine the latest region proposals (for spatial detection) or segment proposals (for temporal localization) from both streams to form a larger set of labelled training samples to help learn better action detection or segment detection models. Second, to learn better representations, we also propose a new message passing approach to pass information from one stream to another stream, which also leads to better action detection and segment detection models. By first using our newly proposed PCSC framework for spatial localization at the frame-level and then applying our temporal PCSC framework for temporal localization at the tube-level, the action localization results are progressively improved at both the frame level and the video level. Comprehensive experiments on two benchmark datasets UCF-101-24 and J-HMDB demonstrate the effectiveness of our newly proposed approaches for spatio-temporal action localization in realistic scenarios.
Equivariant neural networks and equivarification
Venue: arXiv cs.LG 2025
Year: 2025

Equivariant neural networks are a class of neural networks designed to preserve symmetries inherent in the data. In this paper, we introduce a general method for modifying a neural network to enforce equivariance, a process we refer to as equivarification. We further show that group convolutional neural networks (G-CNNs) arise as a special case of our framework.
Steinhaus Filtration and Stable Paths in the Mapper
Venue: arXiv cs.LG 2025
Year: 2025

We define a new filtration called the Steinhaus filtration built from a single cover based on a generalized Steinhaus distance, a generalization of Jaccard distance. The homology persistence module of a Steinhaus filtration with infinitely many cover elements may not be $q$-tame, even when the covers are in a totally bounded space. While this may pose a challenge to derive stability results, we show that the Steinhaus filtration is stable when the cover is finite. We show that while the Čech and Steinhaus filtrations are not isomorphic in general, they are isomorphic for a finite point set in dimension one. Furthermore, the VR filtration completely determines the $1$-skeleton of the Steinhaus filtration in arbitrary dimension. We then develop a language and theory for stable paths within the Steinhaus filtration. We demonstrate how the framework can be applied to several applications where a standard metric may not be defined but a cover is readily available. We introduce a new perspective for modeling recommendation system datasets. As an example, we look at a movies dataset and we find the stable paths identified in our framework represent a sequence of movies constituting a gentle transition and ordering from one genre to another. For explainable machine learning, we apply the Mapper algorithm for model induction by building a filtration from a single Mapper complex, and provide explanations in the form of stable paths between subpopulations. For illustration, we build a Mapper complex from a supervised machine learning model trained on the FashionMNIST dataset. Stable paths in the Steinhaus filtration provide improved explanations of relationships between subpopulations of images.
Key Event Receipt Infrastructure (KERI)
Venue: arXiv cs.CR 2025
Year: 2025

An identity system based secure overlay for the Internet is presented. This includes a primary root-of-trust in self-certifying identifiers. It presents a formalism for Autonomic Identifiers (AIDs) and Autonomic Namespaces (ANs). They are part of an Autonomic Identity System (AIS). This system uses the design principle of minimally sufficient means to provide a candidate trust spanning layer for the internet. Associated with this system is a decentralized key management infrastructure (DKMI). The primary root-of-trust are self-certifying identifiers that are strongly bound at issuance to a cryptographic signing (public, private) key-pair. These are self-contained until/unless control needs to be transferred to a new key-pair. In that event an append only chained key-event log of signed transfer statements provides end verifiable control provenance. This makes intervening operational infrastructure replaceable because the event logs may be therefore be served up by ambient infrastructure. End verifiable logs on ambient infrastructure enables ambient verifiability (verifiable by anyone, anywhere, at anytime). The primary key management operation is key rotation (transference) via a novel key pre-rotation scheme. Two primary trust modalities motivated the design, these are a direct (one-to-one) mode and an indirect (one-to-any) mode. In the direct mode, the identity controller establishes control via verified signatures of the controlling key-pair. The indirect mode extends that trust basis with witnessed key event receipt logs (KERLs) for validating events. The security and accountability guarantees of indirect mode are provided by KERIs Agreement Algorithm for Control Establishment (KACE) among a set of witnesses.
Q-GADMM: Quantized Group ADMM for Communication Efficient Decentralized Machine Learning
Venue: arXiv cs.LG 2025
Year: 2025

In this article, we propose a communication-efficient decentralized machine learning (ML) algorithm, coined quantized group ADMM (Q-GADMM). To reduce the number of communication links, every worker in Q-GADMM communicates only with two neighbors, while updating its model via the group alternating direction method of multipliers (GADMM). Moreover, each worker transmits the quantized difference between its current model and its previously quantized model, thereby decreasing the communication payload size. However, due to the lack of centralized entity in decentralized ML, the spatial sparsity and payload compression may incur error propagation, hindering model training convergence. To overcome this, we develop a novel stochastic quantization method to adaptively adjust model quantization levels and their probabilities, while proving the convergence of Q-GADMM for convex objective functions. Furthermore, to demonstrate the feasibility of Q-GADMM for non-convex and stochastic problems, we propose quantized stochastic GADMM (Q-SGADMM) that incorporates deep neural network architectures and stochastic sampling. Simulation results corroborate that Q-GADMM significantly outperforms GADMM in terms of communication efficiency while achieving the same accuracy and convergence speed for a linear regression task. Similarly, for an image classification task using DNN, Q-SGADMM achieves significantly less total communication cost with identical accuracy and convergence speed compared to its counterpart without quantization, i.e., stochastic GADMM (SGADMM).