OpenRaiser/Intern-Atlas huggingface dataset:
Branch and Bound for Piecewise Linear Neural Network Verification
Venue: arXiv cs.LG 2025
Year: 2025

The success of Deep Learning and its potential use in many safety-critical applications has motivated research on formal verification of Neural Network (NN) models. In this context, verification involves proving or disproving that an NN model satisfies certain input-output properties. Despite the reputation of learned NN models as black boxes, and the theoretical hardness of proving useful properties about them, researchers have been successful in verifying some classes of models by exploiting their piecewise linear structure and taking insights from formal methods such as Satisifiability Modulo Theory. However, these methods are still far from scaling to realistic neural networks. To facilitate progress on this crucial area, we exploit the Mixed Integer Linear Programming (MIP) formulation of verification to propose a family of algorithms based on Branch-and-Bound (BaB). We show that our family contains previous verification methods as special cases. With the help of the BaB framework, we make three key contributions. Firstly, we identify new methods that combine the strengths of multiple existing approaches, accomplishing significant performance improvements over previous state of the art. Secondly, we introduce an effective branching strategy on ReLU non-linearities. This branching strategy allows us to efficiently and successfully deal with high input dimensional problems with convolutional network architecture, on which previous methods fail frequently. Finally, we propose comprehensive test data sets and benchmarks which includes a collection of previously released testcases. We use the data sets to conduct a thorough experimental comparison of existing and new algorithms and to provide an inclusive analysis of the factors impacting the hardness of verification problems.
Towards a Coq-verified Chain of Esterel Semantics
Venue: arXiv cs.FL 2025
Year: 2025

This paper focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel's circuit semantics used by compilers to generate software code and hardware designs. Excluding the loop construct from Esterel, the paper also provides formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics.
Algorithmic Randomness in Continuous-Time Markov Chains
Venue: arXiv cs.IT 2025
Year: 2025

In this paper we develop the elements of the theory of algorithmic randomness in continuous-time Markov chains (CTMCs). Our main contribution is a rigorous, useful notion of what it means for an individual trajectory of a CTMC to be random. CTMCs have discrete state spaces and operate in continuous time. This, together with the fact that trajectories may or may not halt, presents challenges not encountered in more conventional developments of algorithmic randomness. Although we formulate algorithmic randomness in the general context of CTMCs, we are primarily interested in the computational} power of stochastic chemical reaction networks, which are special cases of CTMCs. This leads us to embrace situations in which the long-term behavior of a network depends essentially on its initial state and hence to eschew assumptions that are frequently made in Markov chain theory to avoid such dependencies. After defining the randomness of trajectories in terms of martingales (algorithmic betting strategies), we prove equivalent characterizations in terms of algorithmic measure theory and Kolmogorov complexity. As a preliminary application we prove that, in any stochastic chemical reaction network, every random trajectory with bounded molecular counts has the non-Zeno property that infinitely many reactions do not occur in any finite interval of time.
Defective Convolutional Networks
Venue: arXiv cs.CV 2025
Year: 2025

Robustness of convolutional neural networks (CNNs) has gained in importance on account of adversarial examples, i.e., inputs added as well-designed perturbations that are imperceptible to humans but can cause the model to predict incorrectly. Recent research suggests that the noises in adversarial examples break the textural structure, which eventually leads to wrong predictions. To mitigate the threat of such adversarial attacks, we propose defective convolutional networks that make predictions relying less on textural information but more on shape information by properly integrating defective convolutional layers into standard CNNs. The defective convolutional layers contain defective neurons whose activations are set to be a constant function. As defective neurons contain no information and are far different from standard neurons in its spatial neighborhood, the textural features cannot be accurately extracted, and so the model has to seek other features for classification, such as the shape. We show extensive evidence to justify our proposal and demonstrate that defective CNNs can defense against black-box attacks better than standard CNNs. In particular, they achieve state-of-the-art performance against transfer-based attacks without any adversarial training being applied.
A Unified View of Graph Regularity via Matrix Decompositions
Venue: arXiv cs.DS 2025
Year: 2025

We prove algorithmic weak and \Szemeredi{} regularity lemmas for several classes of sparse graphs in the literature, for which only weak regularity lemmas were previously known. These include core-dense graphs, low threshold rank graphs, and (a version of) $L^p$ upper regular graphs. More precisely, we define \emph{cut pseudorandom graphs}, we prove our regularity lemmas for these graphs, and then we show that cut pseudorandomness captures all of the above graph classes as special cases. The core of our approach is an abstracted matrix decomposition, roughly following Frieze and Kannan [Combinatorica '99] and \Lovasz{} and Szegedy [Geom.\ Func.\ Anal.\ '07], which can be computed by a simple algorithm by Charikar [AAC0 '00]. This gives rise to the class of cut pseudorandom graphs, and using work of Oveis Gharan and Trevisan [TOC '15], it also implies new PTASes for MAX-CUT, MAX-BISECTION, MIN-BISECTION for a significantly expanded class of input graphs. (It is NP Hard to get PTASes for these graphs in general.)
Variable feature weighted fuzzy k-means algorithm for high dimensional data
Venue: arXiv cs.LG 2025
Year: 2025

This paper presents a new fuzzy k-means algorithm for the clustering of high-dimensional data in various subspaces. Since high-dimensional data, some features might be irrelevant and relevant but may have different significance in the clustering process. For better clustering, it is crucial to incorporate the contribution of these features in the clustering process. To combine these features, in this paper, we have proposed a novel fuzzy k-means clustering algorithm by modifying the objective function of the fuzzy k-means using two different entropy terms. The first entropy term helps to minimize the within-cluster dispersion and maximize the negative entropy to determine clusters to contribute to the association of data points. The second entropy term helps control the weight of the features because different features have different contributing weights during the clustering to obtain a better partition. The proposed approach performance is presented in various clustering measures (AR, RI and NMI) on multiple datasets and compared with six other state-of-the-art methods. Impact Statement- In real-world applications, cluster-dependent feature weights help in partitioning the data set into more meaningful clusters. These features may be relevant, irrelevant, or redundant, but they each have different contributions during the clustering process. In this paper, a cluster-dependent feature weights approach is presented using fuzzy k-means to assign higher weights to relevant features and lower weights to irrelevant features during clustering. The method is validated using both supervised and unsupervised performance measures on real-world and synthetic datasets to demonstrate its effectiveness compared to state-of-the-art methods.
Towards Regulated Deep Learning
Venue: arXiv cs.AI 2025
Year: 2025

Regulation of Multi-Agent Systems (MAS) and Declarative Electronic Institutions (DEIs) was a multidisciplinary research topic of the past decade involving (Physical and Software) Agents and Law since the beginning, but recently evolved towards News-claimed Robot Lawyer since 2016. One of these first proposals of restricting the behaviour of Software Agents was Electronic Institutions. However, with the recent reformulation of Artificial Neural Networks (ANNs) as Deep Learning (DL), Security, Privacy,Ethical and Legal issues regarding the use of DL has raised concerns in the Artificial Intelligence (AI) Community. Now that the Regulation of MAS is almost correctly addressed, we propose the Regulation of Artificial Neural Networks as Agent-based Training of a special type of regulated Artificial Neural Network that we call Institutional Neural Network (INN).The main purpose of this paper is to bring attention to Artificial Teaching (AT) and to give a tentative answer showing a proof-of-concept implementation of Regulated Deep Learning (RDL). This paper introduces the former concept and provide $I^*$, a language previously used to model declaratively and extend Electronic Institutions, as a means to regulate the execution of Artificial Neural Networks and their interactions with Artificial Teachers (ATs)
Reducing the Representation Error of GAN Image Priors Using the Deep Decoder
Venue: arXiv cs.LG 2025
Year: 2025

Generative models, such as GANs, learn an explicit low-dimensional representation of a particular class of images, and so they may be used as natural image priors for solving inverse problems such as image restoration and compressive sensing. GAN priors have demonstrated impressive performance on these tasks, but they can exhibit substantial representation error for both in-distribution and out-of-distribution images, because of the mismatch between the learned, approximate image distribution and the data generating distribution. In this paper, we demonstrate a method for reducing the representation error of GAN priors by modeling images as the linear combination of a GAN prior with a Deep Decoder. The deep decoder is an underparameterized and most importantly unlearned natural signal model similar to the Deep Image Prior. No knowledge of the specific inverse problem is needed in the training of the GAN underlying our method. For compressive sensing and image superresolution, our hybrid model exhibits consistently higher PSNRs than both the GAN priors and Deep Decoder separately, both on in-distribution and out-of-distribution images. This model provides a method for extensibly and cheaply leveraging both the benefits of learned and unlearned image recovery priors in inverse problems.
Last iterate convergence in no-regret learning: constrained min-max optimization for convex-concave landscapes
Venue: arXiv cs.LG 2025
Year: 2025

In a recent series of papers it has been established that variants of Gradient Descent/Ascent and Mirror Descent exhibit last iterate convergence in convex-concave zero-sum games. Specifically, \cite{DISZ17, LiangS18} show last iterate convergence of the so called "Optimistic Gradient Descent/Ascent" for the case of \textit{unconstrained} min-max optimization. Moreover, in \cite{Metal} the authors show that Mirror Descent with an extra gradient step displays last iterate convergence for convex-concave problems (both constrained and unconstrained), though their algorithm does not follow the online learning framework; it uses extra information rather than \textit{only} the history to compute the next iteration. In this work, we show that "Optimistic Multiplicative-Weights Update (OMWU)" which follows the no-regret online learning framework, exhibits last iterate convergence locally for convex-concave games, generalizing the results of \cite{DP19} where last iterate convergence of OMWU was shown only for the \textit{bilinear case}. We complement our results with experiments that indicate fast convergence of the method.
Hedonic Seat Arrangement Problems
Venue: arXiv cs.GT 2025
Year: 2025

In this paper, we study a variant of hedonic games, called \textsc{Seat Arrangement}. The model is defined by a bijection from agents with preferences for each other to vertices in a graph $G$. The utility of an agent depends on the neighbors assigned in the graph. More precisely, it is the sum over all neighbors of the preferences that the agent has towards the agent assigned to the neighbor. We first consider the price of stability and fairness for different classes of preferences. In particular, we show that there is an instance such that the price of fairness ({\sf PoF}) is unbounded in general. Moreover, we show an upper bound $\tilde{d}(G)$ and an almost tight lower bound $\tilde{d}(G)-1/4$ of {\sf PoF}, where $\tilde{d}(G)$ is the average degree of an input graph. Then we investigate the computational complexity of problems to find certain ``good'' seat arrangements, say \textsc{Utilitarian Arrangement}, \textsc{Egalitarian Arrangement}, \textsc{Stable Arrangement}, and \textsc{Envy-free Arrangement}. We give dichotomies of computational complexity of four \textsc{Seat Arrangement} problems from the perspective of the maximum order of connected components in an input graph. For the parameterized complexity, \textsc{Utilitarian Arrangement} can be solved in time $n^{O(γ)}$, while it cannot be solved in time $f(γ)n^{o(γ)}$ under ETH, where $n$ is the number of agents and $γ$ is the vertex cover number of an input graph. Moreover, we show that \textsc{Egalitarian Arrangement} and \textsc{Envy-free Arrangement} are weakly NP-hard even on graphs of bounded vertex cover number. Finally, we prove that determining whether a stable arrangement can be obtained from a given arrangement by $k$ swaps is W[1]-hard when parameterized by $k+γ$, whereas it can be solved in time $n^{O(k)}$.
Cumulative Games: Who is the current player?
Venue: arXiv cs.GT 2025
Year: 2025

Combinatorial Game Theory(CGT)is a branch of Game Theory that has developed largely independently of Economic Game Theory (EGT), and is concerned with deep mathematical properties of two-player zero-sum games recursively defined over various combinatorial structures. The aim of this work is to lay the foundations for bridging the conceptual and technical gaps between CGT and EGT, here interpreted as multiplayer Extensive Form Games, so that they can be treated within a unified framework. More specifically, we introduce a class of $n$-player, general-sum games, called {\sc Cumulative Games}, which can be analyzed using tools from both CGT and EGT. We show how two of the most fundamental definitions of CGT, the outcome function and the disjunctive sum operator, naturally extend to the class of {\sc Cumulative Games}. The outcome function allows for efficient equilibrium computation under certain restrictions, while the disjunctive sum operator lets us define a partial order over games according to the advantage that a given player has. Finally, we show that any Extensive Form Game can be written as a {\sc Cumulative Game}.
Vector TSP: A Traveling Salesperson Problem with Racetrack-like Acceleration Constraints
Venue: arXiv cs.DS 2025
Year: 2025

We study a new version of the Traveling Salesperson Problem, called \VectorTSP, where the traveler is subject to discrete acceleration constraints, as defined in the paper-and-pencil game Racetrack (also known as Vector Racer). In this model, the degrees of freedom at a certain point in time depends on the current velocity, and the speed is not limited. The paper introduces this problem and initiates its study, discussing also the main differences with existing versions of TSP. Not surprisingly, the problem turns out to be NP-hard. A key feature of \VectorTSP is that it deals with acceleration in a discrete, combinatorial way, making the problem more amenable to algorithmic investigation. The problem involves two layers of trajectory planning: (1) the order in which cities are visited, and (2) the physical trajectory realizing such a visit, both interacting with each other. This interaction is formalized as an interactive protocol between a high-level tour algorithm and a trajectory oracle, the former calling the latter repeatedly. We present an exact implementation of the trajectory oracle, adapting the A* algorithm for paths over multiple checkpoints whose ordering is \emph{given} (this algorithm being possibly of independent interest). To motivate the problem further, we perform experiments showing that the naive approach consisting of solving the instance as an \EuclideanTSP first, then optimizing the trajectory of the resulting tour, is typically suboptimal and outperformed by simple (but dedicated) heuristics.
ShieldNN: A Provably Safe NN Filter for Unsafe NN Controllers
Venue: arXiv cs.RO 2025
Year: 2025

In this paper, we develop a novel closed-form Control Barrier Function (CBF) and associated controller shield for the Kinematic Bicycle Model (KBM) with respect to obstacle avoidance. The proposed CBF and shield -- designed by an algorithm we call ShieldNN -- provide two crucial advantages over existing methodologies. First, ShieldNN considers steering and velocity constraints directly with the non-affine KBM dynamics; this is in contrast to more general methods, which typically consider only affine dynamics and do not guarantee invariance properties under control constraints. Second, ShieldNN provides a closed-form set of safe controls for each state unlike more general methods, which typically rely on optimization algorithms to generate a single instantaneous for each state. Together, these advantages make ShieldNN uniquely suited as an efficient Multi-Obstacle Safe Actions (i.e. multiple-barrier-function shielding) during training time of a Reinforcement Learning (RL) enabled Neural Network controller. We show via experiments that ShieldNN dramatically increases the completion rate of RL training episodes in the presence of multiple obstacles, thus establishing the value of ShieldNN in training RL-based controllers.
Local structure of idempotent algebras II
Venue: arXiv cs.LO 2025
Year: 2025

In this paper we continue the study of edge-colored graphs associated with finite idempotent algebras initiated in arXiv:2006.09599. We prove stronger connectivity properties of such graphs that will allows us to demonstrate several useful structural features of subdirect products of idempotent algebras such as rectangularity and 2-decomposition.
Adaptive Discretization against an Adversary: Lipschitz bandits, Dynamic Pricing, and Auction Tuning
Venue: arXiv cs.LG 2025
Year: 2025

Lipschitz bandits is a prominent version of multi-armed bandits that studies large, structured action spaces such as the $[0,1]$ interval, where similar actions are guaranteed to have similar rewards. A central theme here is the adaptive discretization of the action space, which gradually ``zooms in'' on the more promising regions thereof. The goal is to take advantage of ``nicer'' problem instances, while retaining near-optimal worst-case performance. While the stochastic version of the problem is well-understood, the general version with adversarial rewards is not. We provide the first algorithm (\emph{Adversarial Zooming}) for adaptive discretization in the adversarial version, and derive instance-dependent regret bounds. In particular, we recover the worst-case optimal regret bound for the adversarial version, and the instance-dependent regret bound for the stochastic version. We apply our algorithm to several fundamental applications -- including dynamic pricing and auction reserve tuning -- all under adversarial reward models. While these domains often violate Lipschitzness, our analysis only requires a weaker version thereof, allowing for meaningful regret bounds without additional smoothness assumptions. Notably, we extend our results to multi-product dynamic pricing with non-smooth reward structures, a setting which does not even satisfy one-sided Lipschitzness.
KRW Composition Theorems via Lifting
Venue: arXiv cs.CC 2025
Year: 2025

One of the major open problems in complexity theory is proving super-logarithmic lower bounds on the depth of circuits (i.e., $\mathbf{P}\not\subseteq\mathbf{NC}^1$). Karchmer, Raz, and Wigderson (Computational Complexity 5(3/4), 1995) suggested to approach this problem by proving that depth complexity behaves "as expected" with respect to the composition of functions $f\diamond g$. They showed that the validity of this conjecture would imply that $\mathbf{P}\not\subseteq\mathbf{NC}^1$. Several works have made progress toward resolving this conjecture by proving special cases. In particular, these works proved the KRW conjecture for every outer function $f$, but only for few inner functions $g$. Thus, it is an important challenge to prove the KRW conjecture for a wider range of inner functions. In this work, we extend significantly the range of inner functions that can be handled. First, we consider the $\textit{monotone}$ version of the KRW conjecture. We prove it for every monotone inner function $g$ whose depth complexity can be lower bounded via a query-to-communication lifting theorem. This allows us to handle several new and well-studied functions such as the $s\textbf{-}t$-connectivity, clique, and generation functions. In order to carry this progress back to the $\textit{non-monotone}$ setting, we introduce a new notion of $\textit{semi-monotone}$ composition, which combines the non-monotone complexity of the outer function $f$ with the monotone complexity of the inner function $g$. In this setting, we prove the KRW conjecture for a similar selection of inner functions $g$, but only for a specific choice of the outer function $f$.
Optimization of Scoring Rules
Venue: arXiv cs.GT 2025
Year: 2025

We characterize the optimal reward functions (scoring rules) that incentivize an agent to acquire information and report it truthfully to the principal. The optimal scoring rules let the agent make a simple binary bet in single-dimensional problems, and choose the dimension with the most surprising signal to be scored on in symmetric multi-dimensional problems. This scoring rule format remains approximately optimal for asymmetric distributions. These results demonstrate the importance of linking incentives to obtain high-quality information in multi-dimensional problems. In contrast, standard scoring rules like the quadratic scoring rule, or averages of single-dimensional scoring rules can be far from optimal.
On the generalization of Tanimoto-type kernels to real valued functions
Venue: arXiv cs.LG 2025
Year: 2025

The Tanimoto kernel (Jaccard index) is a well known tool to describe the similarity between sets of binary attributes. It has been extended to the case when the attributes are nonnegative real values. This paper introduces a more general Tanimoto kernel formulation which allows to measure the similarity of arbitrary real-valued functions. This extension is constructed by unifying the representation of the attributes via properly chosen sets. After deriving the general form of the kernel, explicit feature representation is extracted from the kernel function, and a simply way of including general kernels into the Tanimoto kernel is shown. Finally, the kernel is also expressed as a quotient of piecewise linear functions, and a smooth approximation is provided.