OpenRaiser/Intern-Atlas huggingface dataset:
Towards a Certified Proof Checker for Deep Neural Network Verification
Venue: arXiv cs.LO 2024
Year: 2024

Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for guaranteeing their safety. These safety properties of DNNs can be proven using tools developed by the verification community. However, these tools are themselves prone to implementation bugs and numerical stability problems, which make their reliability questionable. To overcome this, some verifiers produce proofs of their results which can be checked by a trusted checker. In this work, we present a novel implementation of a proof checker for DNN verification. It improves on existing implementations by offering numerical stability and greater verifiability. To achieve this, we leverage two key capabilities of Imandra, an industrial theorem prover: its support of infinite precision real arithmetic and its formal verification infrastructure. So far, we have implemented a proof checker in Imandra, specified its correctness properties and started to verify the checker's compliance with them. Our ongoing work focuses on completing the formal verification of the checker and further optimizing its performance.
TPU as Cryptographic Accelerator
Venue: arXiv cs.CR 2024
Year: 2024

Cryptographic schemes like Fully Homomorphic Encryption (FHE) and Zero-Knowledge Proofs (ZKPs), while offering powerful privacy-preserving capabilities, are often hindered by their computational complexity. Polynomial multiplication, a core operation in these schemes, is a major performance bottleneck. While algorithmic advancements and specialized hardware like GPUs and FPGAs have shown promise in accelerating these computations, the recent surge in AI accelerators (TPUs/NPUs) presents a new opportunity. This paper explores the potential of leveraging TPUs/NPUs to accelerate polynomial multiplication, thereby enhancing the performance of FHE and ZKP schemes. We present techniques to adapt polynomial multiplication to these AI-centric architectures and provide a preliminary evaluation of their effectiveness. We also discuss current limitations and outline future directions for further performance improvements, paving the way for wider adoption of advanced cryptographic tools.
Parallelising Glauber dynamics
Venue: arXiv cs.DS 2024
Year: 2024

For distributions over discrete product spaces $\prod_{i=1}^n Ω_i'$, Glauber dynamics is a Markov chain that at each step, resamples a random coordinate conditioned on the other coordinates. We show that $k$-Glauber dynamics, which resamples a random subset of $k$ coordinates, mixes $k$ times faster in $χ^2$-divergence, and assuming approximate tensorization of entropy, mixes $k$ times faster in KL-divergence. We apply this to obtain parallel algorithms in two settings: (1) For the Ising model $μ_{J,h}(x)\propto \exp(\frac1 2\left\langle x,Jx \right\rangle + \langle h,x\rangle)$ with $\|J\|<1-c$ (the regime where fast mixing is known), we show that we can implement each step of $\widetilde Θ(n/\|J\|_F)$-Glauber dynamics efficiently with a parallel algorithm, resulting in a parallel algorithm with running time $\widetilde O(\|J\|_F) = \widetilde O(\sqrt n)$. (2) For the mixed $p$-spin model at high enough temperature, we show that with high probability we can implement each step of $\widetilde Θ(\sqrt n)$-Glauber dynamics efficiently and obtain running time $\widetilde O(\sqrt n)$.
STCSNN: High energy efficiency spike-train level spiking neural networks with spatio-temporal conversion
Venue: arXiv cs.NE 2024
Year: 2024

Brain-inspired spiking neuron networks (SNNs) have attracted widespread research interest due to their low power features, high biological plausibility, and strong spatiotemporal information processing capability. Although adopting a surrogate gradient (SG) makes the non-differentiability SNN trainable, achieving comparable accuracy for ANNs and keeping low-power features simultaneously is still tricky. In this paper, we proposed an energy-efficient spike-train level spiking neural network with spatio-temporal conversion, which has low computational cost and high accuracy. In the STCSNN, spatio-temporal conversion blocks (STCBs) are proposed to keep the low power features of SNNs and improve accuracy. However, STCSNN cannot adopt backpropagation algorithms directly due to the non-differentiability nature of spike trains. We proposed a suitable learning rule for STCSNNs by deducing the equivalent gradient of STCB. We evaluate the proposed STCSNN on static and neuromorphic datasets, including Fashion-Mnist, Cifar10, Cifar100, TinyImageNet, and DVS-Cifar10. The experiment results show that our proposed STCSNN outperforms the state-of-the-art accuracy on nearly all datasets, using fewer time steps and being highly energy-efficient.
Quantity-Aware Coarse-to-Fine Correspondence for Image-to-Point Cloud Registration
Venue: arXiv cs.CV 2024
Year: 2024

Image-to-point cloud registration aims to determine the relative camera pose between an RGB image and a reference point cloud, serving as a general solution for locating 3D objects from 2D observations. Matching individual points with pixels can be inherently ambiguous due to modality gaps. To address this challenge, we propose a framework to capture quantity-aware correspondences between local point sets and pixel patches and refine the results at both the point and pixel levels. This framework aligns the high-level semantics of point sets and pixel patches to improve the matching accuracy. On a coarse scale, the set-to-patch correspondence is expected to be influenced by the quantity of 3D points. To achieve this, a novel supervision strategy is proposed to adaptively quantify the degrees of correlation as continuous values. On a finer scale, point-to-pixel correspondences are refined from a smaller search space through a well-designed scheme, which incorporates both resampling and quantity-aware priors. Particularly, a confidence sorting strategy is proposed to proportionally select better correspondences at the final stage. Leveraging the advantages of high-quality correspondences, the problem is successfully resolved using an efficient Perspective-n-Point solver within the framework of random sample consensus (RANSAC). Extensive experiments on the KITTI Odometry and NuScenes datasets demonstrate the superiority of our method over the state-of-the-art methods.
Software Testing with Large Language Models: Survey, Landscape, and Vision
Venue: arXiv cs.SE 2024
Year: 2024

Pre-trained large language models (LLMs) have recently emerged as a breakthrough technology in natural language processing and artificial intelligence, with the ability to handle large-scale datasets and exhibit remarkable performance across a wide range of tasks. Meanwhile, software testing is a crucial undertaking that serves as a cornerstone for ensuring the quality and reliability of software products. As the scope and complexity of software systems continue to grow, the need for more effective software testing techniques becomes increasingly urgent, making it an area ripe for innovative approaches such as the use of LLMs. This paper provides a comprehensive review of the utilization of LLMs in software testing. It analyzes 102 relevant studies that have used LLMs for software testing, from both the software testing and LLMs perspectives. The paper presents a detailed discussion of the software testing tasks for which LLMs are commonly used, among which test case preparation and program repair are the most representative. It also analyzes the commonly used LLMs, the types of prompt engineering that are employed, as well as the accompanied techniques with these LLMs. It also summarizes the key challenges and potential opportunities in this direction. This work can serve as a roadmap for future research in this area, highlighting potential avenues for exploration, and identifying gaps in our current understanding of the use of LLMs in software testing.
Inverse Evolution Layers: Physics-informed Regularizers for Deep Neural Networks
Venue: arXiv cs.LG 2024
Year: 2024

Traditional image processing methods employing partial differential equations (PDEs) offer a multitude of meaningful regularizers, along with valuable theoretical foundations for a wide range of image-related tasks. This makes their integration into neural networks a promising avenue. In this paper, we introduce a novel regularization approach inspired by the reverse process of PDE-based evolution models. Specifically, we propose inverse evolution layers (IELs), which serve as bad property amplifiers to penalize neural networks of which outputs have undesired characteristics. Using IELs, one can achieve specific regularization objectives and endow neural networks' outputs with corresponding properties of the PDE models. Our experiments, focusing on semantic segmentation tasks using heat-diffusion IELs, demonstrate their effectiveness in mitigating noisy label effects. Additionally, we develop curve-motion IELs to enforce convex shape regularization in neural network-based segmentation models for preventing the generation of concave outputs. Theoretical analysis confirms the efficacy of IELs as an effective regularization mechanism, particularly in handling training with label issues.
PG-Triggers: Triggers for Property Graphs
Venue: arXiv cs.DB 2024
Year: 2024

Graph databases are emerging as the leading data management technology for storing large knowledge graphs; significant efforts are ongoing to produce new standards (such as the Graph Query Language, GQL), as well as enrich them with properties, types, schemas, and keys. In this article, we introduce PG-Triggers, a complete proposal for adding triggers to Property Graphs, along the direction marked by the SQL3 Standard. We define the syntax and semantics of PG-Triggers and then illustrate how they can be implemented on top of Neo4j, one of the most popular graph databases. In particular, we introduce a syntax-directed translation from PG-Triggers into Neo4j, which makes use of the so-called {\it APOC triggers}; APOC is a community-contributed library for augmenting the Cypher query language supported by Neo4j. We also cover Memgraph, and show that our approach applies to this system in a similar way. We illustrate the use of PG-Triggers through a life science application inspired by the COVID-19 pandemic. The main objective of this article is to introduce an active database standard for graph databases as a first-class citizen at a time when reactive graph management is in its infancy, so as to minimize the conversion efforts towards a full-fledged standard proposal.
TALL: Thumbnail Layout for Deepfake Video Detection
Venue: arXiv cs.CV 2024
Year: 2024

The growing threats of deepfakes to society and cybersecurity have raised enormous public concerns, and increasing efforts have been devoted to this critical topic of deepfake video detection. Existing video methods achieve good performance but are computationally intensive. This paper introduces a simple yet effective strategy named Thumbnail Layout (TALL), which transforms a video clip into a pre-defined layout to realize the preservation of spatial and temporal dependencies. Specifically, consecutive frames are masked in a fixed position in each frame to improve generalization, then resized to sub-images and rearranged into a pre-defined layout as the thumbnail. TALL is model-agnostic and extremely simple by only modifying a few lines of code. Inspired by the success of vision transformers, we incorporate TALL into Swin Transformer, forming an efficient and effective method TALL-Swin. Extensive experiments on intra-dataset and cross-dataset validate the validity and superiority of TALL and SOTA TALL-Swin. TALL-Swin achieves 90.79$\%$ AUC on the challenging cross-dataset task, FaceForensics++ $\to$ Celeb-DF. The code is available at https://github.com/rainy-xu/TALL4Deepfake.
Attention-Enhanced Co-Interactive Fusion Network (AECIF-Net) for Automated Structural Condition Assessment in Visual Inspection
Venue: arXiv cs.CV 2024
Year: 2024

Efficiently monitoring the condition of civil infrastructure requires automating the structural condition assessment in visual inspection. This paper proposes an Attention-Enhanced Co-Interactive Fusion Network (AECIF-Net) for automatic structural condition assessment in visual bridge inspection. AECIF-Net can simultaneously parse structural elements and segment surface defects on the elements in inspection images. It integrates two task-specific relearning subnets to extract task-specific features from an overall feature embedding. A co-interactive feature fusion module further captures the spatial correlation and facilitates information sharing between tasks. Experimental results demonstrate that the proposed AECIF-Net outperforms the current state-of-the-art approaches, achieving promising performance with 92.11% mIoU for element segmentation and 87.16% mIoU for corrosion segmentation on the test set of the new benchmark dataset Steel Bridge Condition Inspection Visual (SBCIV). An ablation study verifies the merits of the designs for AECIF-Net, and a case study demonstrates its capability to automate structural condition assessment.
CA-LoRA: Adapting Existing LoRA for Compressed LLMs to Enable Efficient Multi-Tasking on Personal Devices
Venue: arXiv cs.CL 2024
Year: 2024

Recently, there has been a demand to deploy Large Language Models (LLMs) on personal devices such as laptops and smartphones. These LLMs have different model variants when handling different tasks. However, personal devices have limited resources and require reduced storage overhead. To address this, there are two key methods available: the first is model compression, which compresses LLMs into smaller sizes; the second is LoRA, which can transfer an LLM to other tasks with very few parameters, avoiding the storage of multiple model variants in multi-task scenarios by only preserving LoRAs. However, our experiments show that directly combining these two methods yields sub-optimal performance. Considering that the open-source community has already contributed many LoRAs to LLMs, we propose to adapt these existing LoRAs from the LLMs to their compressed version and introduce a Compression-Aware LoRA (CA-LoRA) framework. We incorporate knowledge inheritance and recovery strategies to recover the lost knowledge caused by model compression. Experiment results demonstrate that CA-LoRA outperforms the vanilla LoRA methods applied to a compressed LLM and achieves comparable performance to the non-compressed LLM with existing LoRA modules. The source code of CA-LoRA is available at https://github.com/thunlp/CA-LoRA.
Semi-Elastic LiDAR-Inertial Odometry
Venue: arXiv cs.RO 2024
Year: 2024

Existing LiDAR-inertial state estimation assumes that the state at the beginning of current sweep is identical to the state at the end of last sweep. However, if the state at the end of last sweep is not accurate, the current state cannot satisfy the constraints from LiDAR and IMU consistently, ultimately resulting in local inconsistency of solved state (e.g., zigzag trajectory or high-frequency oscillating velocity). This paper proposes a semi-elastic optimization-based LiDAR-inertial state estimation method, which imparts sufficient elasticity to the state to allow it be optimized to the correct value. This approach can preferably ensure the accuracy, consistency, and robustness of state estimation. We incorporate the proposed LiDAR-inertial state estimation method into an optimization-based LiDAR-inertial odometry (LIO) framework. Experimental results on four public datasets demonstrate that: 1) our method outperforms existing state-of-the-art LiDAR-inertial odometry systems in terms of accuracy; 2) semi-elastic optimization-based LiDAR-inertial state estimation can better ensure consistency and robustness than traditional and elastic optimization-based LiDAR-inertial state estimation. We have released the source code of this work for the development of the community.
AIOptimizer - Software performance optimisation prototype for cost minimisation
Venue: arXiv cs.SE 2024
Year: 2024

This study presents AIOptimizer, a prototype for a cost-reduction-based software performance optimisation tool. The study focuses on the design elements of AIOptimizer, including user-friendliness, scalability, accuracy, and adaptability. To deliver efficient and user-focused performance optimisation solutions, it promotes the use of robust integration, continuous learning, modular design, and data collection methods. The paper also looks into AIOptimizer features including collaboration, efficiency prediction, cost optimisation suggestions, and fault diagnosis. Additionally, it introduces AIOptimizer, a recommendation engine for cost optimisation based on reinforcement learning, and examines several software development life cycle models. The goal of this research study is to showcase AIOptimizer as a prototype that continuously improves software performance and reduces costs by utilising sophisticated optimisation techniques and intelligent recommendation systems. Numerous software development life cycle models, including the Big Bang, V-, Waterfall, Iterative, and Agile models are the subject of the study. Every model has benefits and drawbacks, and the features and requirements of the project will decide how useful each is.
AdvFusion: Adapter-based Knowledge Transfer for Code Summarization on Code Language Models
Venue: arXiv cs.SE 2024
Year: 2024

Programming languages can benefit from one another by utilizing a pre-trained model for software engineering tasks such as code summarization and method name prediction. While full fine-tuning of Code Language Models (Code-LMs) has been explored for multilingual knowledge transfer, research on Parameter Efficient Fine-Tuning (PEFT) for this purpose is limited. AdapterFusion, a PEFT architecture, aims to enhance task performance by leveraging information from multiple languages but primarily focuses on the target language. To address this, we propose AdvFusion, a novel PEFT-based approach that effectively learns from other languages before adapting to the target task. Evaluated on code summarization and method name prediction, AdvFusion outperforms AdapterFusion by up to 1.7 points and surpasses LoRA with gains of 1.99, 1.26, and 2.16 for Ruby, JavaScript, and Go, respectively. We open-source our scripts for replication purposes.
Real-time goal recognition using approximations in Euclidean space
Venue: arXiv cs.AI 2024
Year: 2024

While recent work on online goal recognition efficiently infers goals under low observability, comparatively less work focuses on online goal recognition that works in both discrete and continuous domains. Online goal recognition approaches often rely on repeated calls to the planner at each new observation, incurring high computational costs. Recognizing goals online in continuous space quickly and reliably is critical for any trajectory planning problem since the real physical world is fast-moving, e.g. robot applications. We develop an efficient method for goal recognition that relies either on a single call to the planner for each possible goal in discrete domains or a simplified motion model that reduces the computational burden in continuous ones. The resulting approach performs the online component of recognition orders of magnitude faster than the current state of the art, making it the first online method effectively usable for robotics applications that require sub-second recognition.
Faster Approximation Scheme for Euclidean $k$-TSP
Venue: arXiv cs.CG 2024
Year: 2024

In the Euclidean $k$-traveling salesman problem ($k$-TSP), we are given $n$ points in the $d$-dimensional Euclidean space, for some fixed constant $d\geq 2$, and a positive integer $k$. The goal is to find a shortest tour visiting at least $k$ points. We give an approximation scheme for the Euclidean $k$-TSP in time $n\cdot 2^{O(1/\varepsilon^{d-1})} \cdot(\log n)^{2d^2\cdot 2^d}$. This improves Arora's approximation scheme of running time $n\cdot k\cdot (\log n)^{\left(O\left(\sqrt{d}/\varepsilon\right)\right)^{d-1}}$ [J. ACM 1998]. Our algorithm is Gap-ETH tight and can be derandomized by increasing the running time by a factor $O(n^d)$.
Analyzing Dataset Annotation Quality Management in the Wild
Venue: arXiv cs.CL 2024
Year: 2024

Data quality is crucial for training accurate, unbiased, and trustworthy machine learning models as well as for their correct evaluation. Recent works, however, have shown that even popular datasets used to train and evaluate state-of-the-art models contain a non-negligible amount of erroneous annotations, biases, or artifacts. While practices and guidelines regarding dataset creation projects exist, to our knowledge, large-scale analysis has yet to be performed on how quality management is conducted when creating natural language datasets and whether these recommendations are followed. Therefore, we first survey and summarize recommended quality management practices for dataset creation as described in the literature and provide suggestions for applying them. Then, we compile a corpus of 591 scientific publications introducing text datasets and annotate it for quality-related aspects, such as annotator management, agreement, adjudication, or data validation. Using these annotations, we then analyze how quality management is conducted in practice. A majority of the annotated publications apply good or excellent quality management. However, we deem the effort of 30\% of the works as only subpar. Our analysis also shows common errors, especially when using inter-annotator agreement and computing annotation error rates.
Zero-Shot Image Harmonization with Generative Model Prior
Venue: arXiv cs.CV 2024
Year: 2024

We propose a zero-shot approach to image harmonization, aiming to overcome the reliance on large amounts of synthetic composite images in existing methods. These methods, while showing promising results, involve significant training expenses and often struggle with generalization to unseen images. To this end, we introduce a fully modularized framework inspired by human behavior. Leveraging the reasoning capabilities of recent foundation models in language and vision, our approach comprises three main stages. Initially, we employ a pretrained vision-language model (VLM) to generate descriptions for the composite image. Subsequently, these descriptions guide the foreground harmonization direction of a text-to-image generative model (T2I). We refine text embeddings for enhanced representation of imaging conditions and employ self-attention and edge maps for structure preservation. Following each harmonization iteration, an evaluator determines whether to conclude or modify the harmonization direction. The resulting framework, mirroring human behavior, achieves harmonious results without the need for extensive training. We present compelling visual results across diverse scenes and objects, along with a user study validating the effectiveness of our approach.