OpenRaiser/Intern-Atlas huggingface dataset:
Continual Learning as Computationally Constrained Reinforcement Learning
Venue: arXiv cs.LG 2025
Year: 2025

An agent that efficiently accumulates knowledge to develop increasingly sophisticated skills over a long lifetime could advance the frontier of artificial intelligence capabilities. The design of such agents, which remains a long-standing challenge of artificial intelligence, is addressed by the subject of continual learning. This monograph clarifies and formalizes concepts of continual learning, introducing a framework and set of tools to stimulate further research.
Synthetic Dataset for Evaluating Complex Compositional Knowledge for Natural Language Inference
Venue: arXiv cs.CL 2025
Year: 2025

We introduce a synthetic dataset called Sentences Involving Complex Compositional Knowledge (SICCK) and a novel analysis that investigates the performance of Natural Language Inference (NLI) models to understand compositionality in logic. We produce 1,304 sentence pairs by modifying 15 examples from the SICK dataset (Marelli et al., 2014). To this end, we modify the original texts using a set of phrases - modifiers that correspond to universal quantifiers, existential quantifiers, negation, and other concept modifiers in Natural Logic (NL) (MacCartney, 2009). We use these phrases to modify the subject, verb, and object parts of the premise and hypothesis. Lastly, we annotate these modified texts with the corresponding entailment labels following NL rules. We conduct a preliminary verification of how well the change in the structural and semantic composition is captured by neural NLI models, in both zero-shot and fine-tuned scenarios. We found that the performance of NLI models under the zero-shot setting is poor, especially for modified sentences with negation and existential quantifiers. After fine-tuning this dataset, we observe that models continue to perform poorly over negation, existential and universal modifiers.
Rethinking Distribution Shifts: Empirical Analysis and Inductive Modeling for Tabular Data
Venue: arXiv cs.LG 2025
Year: 2025

Different distribution shifts require different interventions, and algorithms must be grounded in the specific shifts they address. However, methodological development for robust algorithms typically relies on structural assumptions that lack empirical validation. Advocating for an empirically grounded data-driven approach to algorithm development, we build an empirical testbed comprising natural shifts across 8 tabular datasets, 172 distribution pairs over 45 methods and 90,000 method configurations encompassing empirical risk minimization and distributionally robust optimization (DRO) methods. We find $Y|X$-shifts are most prevalent in our testbed, in stark contrast to the heavy focus on $X$ (covariate)-shifts in the ML literature, and that the performance of robust algorithms is no better than that of vanilla methods. To understand why, we conduct an in-depth empirical analysis of DRO methods and find that underlooked implementation details -- such as the choice of underlying model class (e.g., LightGBM) and hyperparameter selection -- have a bigger impact on performance than the ambiguity set or its radius. We illustrate via case studies how a data-driven, inductive understanding of distribution shifts can provide a new approach to algorithm development.
Evidence of social learning across symbolic cultural barriers in sperm whales
Venue: arXiv cs.SI 2025
Year: 2025

We provide quantitative evidence suggesting social learning in sperm whales across socio-cultural boundaries, using acoustic data from the Pacific and Atlantic Oceans. Traditionally, sperm whale populations are categorized into clans based on their vocal repertoire: the rhythmically patterned click sequences (codas) that they use. Among these codas, identity codas function as symbolic markers for each clan, accounting for 35-60% of codas they produce. We introduce a computational method to model whale speech, which encodes rhythmic micro-variations within codas, capturing their vocal style. We find that vocal style-clans closely align with repertoire-clans. However, contrary to vocal repertoire, we show that sympatry increases vocal style similarity between clans for non-identity codas, i.e. most codas, suggesting social learning across cultural boundaries. More broadly, this subcoda structure model offers a framework for comparing communication systems in other species, with potential implications for deeper understanding of vocal and cultural transmission within animal societies.
Linear Alignment of Vision-language Models for Image Captioning
Venue: arXiv cs.CV 2025
Year: 2025

Recently, vision-language models like CLIP have advanced the state of the art in a variety of multi-modal tasks including image captioning and caption evaluation. Many approaches leverage CLIP for cross-modal retrieval to condition pre-trained language models on visual input. However, CLIP generally suffers from a mis-alignment of image and text modalities in the joint embedding space. We investigate efficient methods to linearly re-align the joint embedding space for the downstream task of image captioning. This leads to an efficient training protocol that merely requires computing a closed-form solution for a linear mapping in the joint CLIP space. Consequently, we propose a lightweight captioning method called ReCap, which can be trained up to 1000 times faster than existing lightweight methods. Moreover, we propose two new learning-based image-captioning metrics built on CLIP score along with our proposed alignment. We evaluate ReCap on MS-COCO, Flickr30k, VizWiz and MSRVTT. On the former two, ReCap performs comparably to state-of-the-art lightweight methods using rule-based metrics while outperforming them on most of the CLIP-based metrics. On the latter two benchmarks, ReCap consistently outperforms competitors across all metrics and exhibits strong transfer capabilities and resilience to noise. Finally, we demonstrate that our proposed metrics correlate stronger with human judgement than existing metrics on the Flickr8k-Expert, Flickr8k-Crowdflower, and THumB datasets.
Safety and Liveness of Quantitative Properties and Automata
Venue: arXiv cs.FL 2025
Year: 2025

Safety and liveness stand as fundamental concepts in formal languages, playing a key role in verification. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In the quantitative setting, properties are arbitrary functions from infinite words to partially-ordered domains. Extending this paradigm to the quantitative domain, where properties are arbitrary functions mapping infinite words to partially-ordered domains, we introduce and study the notions of quantitative safety and liveness. First, we formally define quantitative safety and liveness, and prove that our definitions induce conservative quantitative generalizations of both the safety-progress hierarchy and the safety-liveness decomposition of boolean properties. Consequently, like their boolean counterparts, quantitative properties can be min-decomposed into safety and liveness parts, or alternatively, max-decomposed into co-safety and co-liveness parts. We further establish a connection between quantitative safety and topological continuity and provide alternative characterizations of quantitative safety and liveness in terms of their boolean analogs. Second, we instantiate our framework with the specific classes of quantitative properties expressed by automata. These quantitative automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totally-ordered domain of real numbers. For all common value functions, we provide a procedure for deciding whether a given automaton is safe or live, we show how to construct its safety closure, and we present a min-decomposition into safe and live automata.
SecureFalcon: Are We There Yet in Automated Software Vulnerability Detection with LLMs?
Venue: arXiv cs.CR 2025
Year: 2025

Software vulnerabilities can cause numerous problems, including crashes, data loss, and security breaches. These issues greatly compromise quality and can negatively impact the market adoption of software applications and systems. Traditional bug-fixing methods, such as static analysis, often produce false positives. While bounded model checking, a form of Formal Verification (FV), can provide more accurate outcomes compared to static analyzers, it demands substantial resources and significantly hinders developer productivity. Can Machine Learning (ML) achieve accuracy comparable to FV methods and be used in popular instant code completion frameworks in near real-time? In this paper, we introduce SecureFalcon, an innovative model architecture with only 121 million parameters derived from the Falcon-40B model and explicitly tailored for classifying software vulnerabilities. To achieve the best performance, we trained our model using two datasets, namely the FormAI dataset and the FalconVulnDB. The FalconVulnDB is a combination of recent public datasets, namely the SySeVR framework, Draper VDISC, Bigvul, Diversevul, SARD Juliet, and ReVeal datasets. These datasets contain the top 25 most dangerous software weaknesses, such as CWE-119, CWE-120, CWE-476, CWE-122, CWE-190, CWE-121, CWE-78, CWE-787, CWE-20, and CWE-762. SecureFalcon achieves 94% accuracy in binary classification and up to 92% in multiclassification, with instant CPU inference times. It outperforms existing models such as BERT, RoBERTa, CodeBERT, and traditional ML algorithms, promising to push the boundaries of software vulnerability detection and instant code completion frameworks.
MaxMin-L2-SVC-NCH: A Novel Approach for Support Vector Classifier Training and Parameter Selection
Venue: arXiv cs.LG 2025
Year: 2025

The selection of Gaussian kernel parameters plays an important role in the applications of support vector classification (SVC). A commonly used method is the k-fold cross validation with grid search (CV), which is extremely time-consuming because it needs to train a large number of SVC models. In this paper, a new approach is proposed to train SVC and optimize the selection of Gaussian kernel parameters. We first formulate the training and the parameter selection of SVC as a minimax optimization problem named as MaxMin-L2-SVC-NCH, in which the minimization problem is an optimization problem of finding the closest points between two normal convex hulls (L2-SVC-NCH) while the maximization problem is an optimization problem of finding the optimal Gaussian kernel parameters. A lower time complexity can be expected in MaxMin-L2-SVC-NCH because CV is not needed. We then propose a projected gradient algorithm (PGA) for the training of L2-SVC-NCH. It is revealed that the famous sequential minimal optimization (SMO) algorithm is a special case of the PGA. Thus, the PGA can provide more flexibility than the SMO. Furthermore, the solution of the maximization problem is done by a gradient ascent algorithm with dynamic learning rate. The comparative experiments between MaxMin-L2-SVC-NCH and the previous best approaches on public datasets show that MaxMin-L2-SVC-NCH greatly reduces the number of models to be trained while maintaining competitive test accuracy. These findings indicate that MaxMin-L2-SVC-NCH is a better choice for SVC tasks.
Deciding One to One property of Boolean maps: Condition and algorithm in terms of implicants
Venue: arXiv cs.SC 2025
Year: 2025

This paper addresses the computational problem of deciding invertibility (or one to one-ness) of a Boolean map $F$ in $n$-Boolean variables. This problem is a special case of deciding invertibilty of a map $F:\mathbb{F}_{q}^n\rightarrow\mathbb{F}_{q}^n$ over the finite field $\mathbb{F}_q$ for $q=2$. Algebraic condition for invertibility of $F$ is well known to be equivalent to invertibility of the Koopman operator of $F$ as shown in \cite{RamSule}. In this paper a condition for invertibility is derived in the special case of Boolean maps $F:B_0^n\rightarrow B_0^n$ where $B_0$ is the two element Boolean algebra in terms of \emph{implicants} of Boolean equations defined by the map. This condition is then extended to the case of general maps in $n$ variables and $m\geq n$ equations. Hence this condition answers the special case of invertibility of maps $F$ defined over the binary field $\mathbb{F}_2$ alternatively, in terms of implicants instead of the Koopman operator. The problem of deciding invertibility of a map $F$ (or that of finding its Garden of Eden (GOE)) over finite fields is distinct from the satisfiability problem (SAT) or the problem of deciding consistency of polynomial equations over finite fields. Hence the well known algorithms for deciding SAT or of solvability using Grobner basis for checking membership in an ideal generated by polynomials is not known to answer the question of invertibility of a map. Similarly it appears that algorithms for satisfiability or polynomial solvability are not useful for computation of GOE of $F$ even for maps over the binary field $\mathbb{F}_2$.
Problems in NP can Admit Double-Exponential Lower Bounds when Parameterized by Treewidth or Vertex Cover
Venue: arXiv cs.CC 2025
Year: 2025

Treewidth (tw) is an important parameter that, when bounded, yields tractability for many problems. For example, graph problems expressible in Monadic Second Order (MSO) logic and QUANTIFIED SAT or, more generally, QUANTIFIED CSP, are FPT parameterized by the tw of the input's (primal) graph plus the length of the MSO-formula [Courcelle, Information & Computation 1990] and the quantifier rank [Chen, ECAI 2004], resp. The algorithms from these (meta-)results have running times whose dependence on tw is a tower of exponents. A conditional lower bound by Fichte et al. [LICS 2020] shows that, for QUANTIFIED SAT, the height of this tower is equal to the number of quantifier alternations. Lower bounds showing that at least double-exponential factors in the running time are necessary are rare: there are very few (for tw and vertex cover vc parameterizations) and they are for problems that are complete for #NP, $Σ_2^p$, $Π_2^p$, or higher levels of the polynomial hierarchy. We show, for the first time, that it is not necessary to go higher up in the polynomial hierarchy to obtain such lower bounds. We design a novel, yet simple versatile technique based on Sperner families to obtain such lower bounds and apply it to 3 problems: METRIC DIMENSION, STRONG METRIC DIMENSION, and GEODETIC SET. We prove that they do not admit $2^{2^{o(tw)}} \cdot n^{O(1)}$-time algorithms, even on bounded diameter graphs, unless the ETH fails. For STRONG METRIC DIMENSION, the lower bound holds even for vc. We complement our lower bounds with matching upper bounds.
Long-range Meta-path Search on Large-scale Heterogeneous Graphs
Venue: arXiv cs.AI 2025
Year: 2025

Utilizing long-range dependency, a concept extensively studied in homogeneous graphs, remains underexplored in heterogeneous graphs, especially on large ones, posing two significant challenges: Reducing computational costs while maximizing effective information utilization in the presence of heterogeneity, and overcoming the over-smoothing issue in graph neural networks. To address this gap, we investigate the importance of different meta-paths and introduce an automatic framework for utilizing long-range dependency on heterogeneous graphs, denoted as Long-range Meta-path Search through Progressive Sampling (LMSPS). Specifically, we develop a search space with all meta-paths related to the target node type. By employing a progressive sampling algorithm, LMSPS dynamically shrinks the search space with hop-independent time complexity. Through a sampling evaluation strategy, LMSPS conducts a specialized and effective meta-path selection, leading to retraining with only effective meta-paths, thus mitigating costs and over-smoothing. Extensive experiments across diverse heterogeneous datasets validate LMSPS's capability in discovering effective long-range meta-paths, surpassing state-of-the-art methods. Our code is available at https://github.com/JHL-HUST/LMSPS.
Runtime Stealthy Perception Attacks against DNN-based Adaptive Cruise Control Systems
Venue: arXiv cs.CR 2025
Year: 2025

Adaptive Cruise Control (ACC) is a widely used driver assistance technology for maintaining the desired speed and safe distance to the leading vehicle. This paper evaluates the security of the deep neural network (DNN) based ACC systems under runtime stealthy perception attacks that strategically inject perturbations into camera data to cause forward collisions. We present a context-aware strategy for the selection of the most critical times for triggering the attacks and a novel optimization-based method for the adaptive generation of image perturbations at runtime. We evaluate the effectiveness of the proposed attack using an actual vehicle, a publicly available driving dataset, and a realistic simulation platform with the control software from a production ACC system, a physical-world driving simulator, and interventions by the human driver and safety features such as Advanced Emergency Braking System (AEBS). Experimental results show that the proposed attack achieves 142.9 times higher success rate in causing hazards and 82.6% higher evasion rate than baselines, while being stealthy and robust to real-world factors and dynamic changes in the environment. This study highlights the role of human drivers and basic safety mechanisms in preventing attacks.
Higher Catoids, Higher Quantales and their Correspondences
Venue: arXiv cs.LO 2025
Year: 2025

We introduce $ω$-catoids as generalisations of (strict) $ω$-categories and in particular the higher path categories generated by computads or polygraphs in higher-dimensional rewriting. We also introduce $ω$-quantales that generalise the $ω$-Kleene algebras recently proposed for algebraic coherence proofs in higher-dimensional rewriting. We then establish correspondences between $ω$-catoids and convolution $ω$-quantales. These are related to Jónsson-Tarski-style dualities between relational structures and lattices with operators. We extend these correspondences to $(ω,p)$-catoids, catoids with a groupoid structure above some dimension, and convolution $(ω,p)$-quantales, using Dedekind quantales above some dimension to capture homotopic constructions and proofs in higher-dimensional rewriting. We also specialise them to finitely decomposable $(ω, p)$-catoids, an appropriate setting for defining $(ω, p)$-semirings and $(ω, p)$-Kleene algebras. These constructions support the systematic development and justification of $ω$-Kleene algebra and $ω$-quantale axioms, improving on the recent approach mentioned, where axioms for $ω$-Kleene algebras have been introduced in an ad hoc fashion.
SAMConvex: Fast Discrete Optimization for CT Registration using Self-supervised Anatomical Embedding and Correlation Pyramid
Venue: arXiv cs.CV 2025
Year: 2025

Estimating displacement vector field via a cost volume computed in the feature space has shown great success in image registration, but it suffers excessive computation burdens. Moreover, existing feature descriptors only extract local features incapable of representing the global semantic information, which is especially important for solving large transformations. To address the discussed issues, we propose SAMConvex, a fast coarse-to-fine discrete optimization method for CT registration that includes a decoupled convex optimization procedure to obtain deformation fields based on a self-supervised anatomical embedding (SAM) feature extractor that captures both local and global information. To be specific, SAMConvex extracts per-voxel features and builds 6D correlation volumes based on SAM features, and iteratively updates a flow field by performing lookups on the correlation volumes with a coarse-to-fine scheme. SAMConvex outperforms the state-of-the-art learning-based methods and optimization-based methods over two inter-patient registration datasets (Abdomen CT and HeadNeck CT) and one intra-patient registration dataset (Lung CT). Moreover, as an optimization-based method, SAMConvex only takes $\sim2$s ($\sim5s$ with instance optimization) for one paired images.
Alignment complete relational Hoare logics for some and all
Venue: arXiv cs.LO 2025
Year: 2025

In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (RHL) provide compositional rules that embody various alignments of executions. Seemingly more flexible alignments can be expressed in terms of product automata based on program transition relations. A single degenerate alignment rule (sequential composition), atop a complete Hoare logic, comprises a RHL for $\forall\forall$ properties that is complete in the sense of Cook. The notion of alignment completeness was previously proposed as an additional measure, and some rules were shown to be alignment complete with respect to a few ad hoc forms of alignment automata. This paper proves alignment completeness with respect to a general class of $\forall\forall$ alignment automata, for a RHL comprised of standard rules together with a rule of semantics-preserving rewrites based on Kleene algebra with tests. A new logic for $\forall\exists$ properties is introduced and shown to be sound and alignment complete for a new general class of automata. The $\forall\forall$ and $\forall\exists$ automata are shown to be semantically complete. Thus both logics are complete in the sense of Cook. The paper includes discussion of why alignment is not the only important principle for relational reasoning and proposes entailment completeness as further means to evaluate RHLs.
FigCaps-HF: A Figure-to-Caption Generative Framework and Benchmark with Human Feedback
Venue: arXiv cs.CL 2025
Year: 2025

Captions are crucial for understanding scientific visualizations and documents. Existing captioning methods for scientific figures rely on figure-caption pairs extracted from documents for training, many of which fall short with respect to metrics like helpfulness, explainability, and visual-descriptiveness [15] leading to generated captions being misaligned with reader preferences. To enable the generation of high-quality figure captions, we introduce FigCaps-HF a new framework for figure-caption generation that can incorporate domain expert feedback in generating captions optimized for reader preferences. Our framework comprises of 1) an automatic method for evaluating quality of figure-caption pairs, 2) a novel reinforcement learning with human feedback (RLHF) method to optimize a generative figure-to-caption model for reader preferences. We demonstrate the effectiveness of our simple learning framework by improving performance over standard fine-tuning across different types of models. In particular, when using BLIP as the base model, our RLHF framework achieves a mean gain of 35.7%, 16.9%, and 9% in ROUGE, BLEU, and Meteor, respectively. Finally, we release a large-scale benchmark dataset with human feedback on figure-caption pairs to enable further evaluation and development of RLHF techniques for this problem.