OpenRaiser/Intern-Atlas huggingface dataset:
CBMC: The C Bounded Model Checker
Venue: arXiv cs.SE 2023
Year: 2023

The C Bounded Model Checker (CBMC) demonstrates the violation of assertions in C programs, or proves safety of the assertions under a given bound. CBMC implements a bit-precise translation of an input C program, annotated with assertions and with loops unrolled to a given depth, into a formula. If the formula is satisfiable, then an execution leading to a violated assertion exists. CBMC is one of the most successful software verification tools. Its main advantages are its precision, robustness and simplicity. CBMC is shipped as part of several Linux distributions. It has been used by thousands of software developers to verify real-world software, such as the Linux kernel, and powers commercial software analysis and test generation tools. Table 1 gives an overview of CBMC's features. CBMC is also a versatile tool that can be applied to solve many practical program analysis problems such as bug finding, property checking, test input generation, detection of security vulnerabilities, equivalence checking and program synthesis. This chapter will give an introduction into CBMC, including practical examples and pointers to further reading. Moreover, we give insights about the development of CBMC itself, showing how its performance evolved over the last decade.
OAcode: Overall Aesthetic 2D Barcode on Screen
Venue: arXiv cs.MM 2023
Year: 2023

Nowadays, two-dimensional (2D) barcodes have been widely used in various domains. And a series of aesthetic 2D barcode schemes have been proposed to improve the visual quality and readability of 2D barcodes for better integration with marketing materials. Yet we believe that the existing aesthetic 2D barcode schemes are partially aesthetic because they only beautify the data area but retain the position detection patterns with the blackwhite appearance of traditional 2D barcode schemes. Thus, in this paper, we propose the first overall aesthetic 2D barcode scheme, called OAcode, in which the position detection pattern is canceled. Its detection process is based on the pre-designed symmetrical data area of OAcode, whose symmetry could be used as the calibration signal to restore the perspective transformation in the barcode scanning process. Moreover, an enhanced demodulation method is proposed to resist the lens distortion common in the camera-shooting process. The experimental results illustrate that when 5$\times$5 cm OAcode is captured with a resolution of 720$\times$1280 pixels, at the screen-camera distance of 10 cm and the angle less or equal to 25°, OAcode has 100% detection rate and 99.5% demodulation accuracy. For 10$\times$10 cm OAcode, it could be extracted by consumer-grade mobile phones at a distance of 90 cm with around 90% accuracy.
Towards Efficient Subarray Hybrid Beamforming: Attention Network-based Practical Feedback in FDD Massive MU-MIMO Systems
Venue: arXiv cs.IT 2023
Year: 2023

Channel state information (CSI) feedback is necessary for the frequency division duplexing (FDD) multiple input multiple output (MIMO) systems due to the channel non-reciprocity. With the help of deep learning, many works have succeeded in rebuilding the compressed ideal CSI for massive MIMO. However, simple CSI reconstruction is of limited practicality since the channel estimation and the targeted beamforming design are not considered. In this paper, a jointly optimized network is introduced for channel estimation and feedback so that a spectral-efficient beamformer can be learned. Moreover, the deployment-friendly subarray hybrid beamforming architecture is applied and a practical lightweight end-to-end network is specially designed. Experiments show that the proposed network is over 10 times lighter at the resource-sensitive user equipment compared with the previous state-of-the-art method with only a minor performance loss.
Exploiting Partial Common Information Microstructure for Multi-Modal Brain Tumor Segmentation
Venue: arXiv cs.CV 2023
Year: 2023

Learning with multiple modalities is crucial for automated brain tumor segmentation from magnetic resonance imaging data. Explicitly optimizing the common information shared among all modalities (e.g., by maximizing the total correlation) has been shown to achieve better feature representations and thus enhance the segmentation performance. However, existing approaches are oblivious to partial common information shared by subsets of the modalities. In this paper, we show that identifying such partial common information can significantly boost the discriminative power of image segmentation models. In particular, we introduce a novel concept of partial common information mask (PCI-mask) to provide a fine-grained characterization of what partial common information is shared by which subsets of the modalities. By solving a masked correlation maximization and simultaneously learning an optimal PCI-mask, we identify the latent microstructure of partial common information and leverage it in a self-attention module to selectively weight different feature representations in multi-modal data. We implement our proposed framework on the standard U-Net. Our experimental results on the Multi-modal Brain Tumor Segmentation Challenge (BraTS) datasets outperform those of state-of-the-art segmentation baselines, with validation Dice similarity coefficients of 0.920, 0.897, 0.837 for the whole tumor, tumor core, and enhancing tumor on BraTS-2020.
Variable Stiffness Improves Safety and Performance in Soft Robotics
Venue: arXiv cs.RO 2023
Year: 2023

This paper proposes a new variable stiffness soft gripper that enables high-performance grasping tasks in industrial applications. The design of the proposed monolithic soft gripper includes a middle bellow and two side bellows (i.e., fingers). The positions of the fingers are regulated by adjusting the negative pressure in the middle bellow actuator via an on-off controller. The stiffness of the soft gripper is modulated by controlling the positive pressure in the fingers through the use of a proportional air-pressure regulator. It is experimentally shown that the proposed soft gripper can modulate its stiffness by 125% within 250ms. It is also shown that the variable stiffness soft gripper can help improve the safety and performance of grasping tasks in industrial applications.
Mobile Cell-Free Massive MIMO: Challenges, Solutions, and Future Directions
Venue: arXiv cs.IT 2023
Year: 2023

Cell-free (CF) massive multiple-input multiple-output (MIMO) systems, which exploit many geographically distributed access points to coherently serve user equipments via spatial multiplexing on the same time-frequency resource, has become a vital component of the next-generation mobile communication networks. Theoretically, CF massive MIMO systems have many advantages, such as large capacity, great coverage, and high reliability, but several obstacles must be overcome. In this article, we study the paradigm of CF massive MIMO-aided mobile communications, including the main application scenarios and associated deployment architectures. Furthermore, we thoroughly investigate the challenges of CF massive MIMO-aided mobile communications. We then exploit a novel predictor antenna, hierarchical cancellation, rate-splitting and dynamic clustering system for CF massive MIMO. Finally, several important research directions regarding CF massive MIMO for mobile communications are presented to facilitate further investigation.
Stochastic Minimum Vertex Cover in General Graphs: a $3/2$-Approximation
Venue: arXiv cs.DS 2023
Year: 2023

Our main result is designing an algorithm that returns a vertex cover of $\mathcal{G}^\star$ with size at most $(3/2+ε)$ times the expected size of the minimum vertex cover, using only $O(n/εp)$ non-adaptive queries. This improves over the best-known 2-approximation algorithm by Behnezhad, Blum, and Derakhshan [SODA'22], who also show that $Ω(n/p)$ queries are necessary to achieve any constant approximation. Our guarantees also extend to instances where edge realizations are not fully independent. We complement this upper bound with a tight $3/2$-approximation lower bound for stochastic graphs whose edges realizations demonstrate mild correlations.
Ten Lessons We Have Learned in the New "Sparseland": A Short Handbook for Sparse Neural Network Researchers
Venue: arXiv cs.LG 2023
Year: 2023

This article does not propose any novel algorithm or new hardware for sparsity. Instead, it aims to serve the "common good" for the increasingly prosperous Sparse Neural Network (SNN) research community. We attempt to summarize some most common confusions in SNNs, that one may come across in various scenarios such as paper review/rebuttal and talks - many drawn from the authors' own bittersweet experiences! We feel that doing so is meaningful and timely, since the focus of SNN research is notably shifting from traditional pruning to more diverse and profound forms of sparsity before, during, and after training. The intricate relationships between their scopes, assumptions, and approaches lead to misunderstandings, for non-experts or even experts in SNNs. In response, we summarize ten Q\&As of SNNs from many key aspects, including dense vs. sparse, unstructured sparse vs. structured sparse, pruning vs. sparse training, dense-to-sparse training vs. sparse-to-sparse training, static sparsity vs. dynamic sparsity, before-training/during-training vs. post-training sparsity, and many more. We strive to provide proper and generically applicable answers to clarify those confusions to the best extent possible. We hope our summary provides useful general knowledge for people who want to enter and engage with this exciting community; and also provides some "mind of ease" convenience for SNN researchers to explain their work in the right contexts. At the very least (and perhaps as this article's most insignificant target functionality), if you are writing/planning to write a paper or rebuttal in the field of SNNs, we hope some of our answers could help you!
Trust, but Verify: Using Self-Supervised Probing to Improve Trustworthiness
Venue: arXiv cs.LG 2023
Year: 2023

Trustworthy machine learning is of primary importance to the practical deployment of deep learning models. While state-of-the-art models achieve astonishingly good performance in terms of accuracy, recent literature reveals that their predictive confidence scores unfortunately cannot be trusted: e.g., they are often overconfident when wrong predictions are made, or so even for obvious outliers. In this paper, we introduce a new approach of self-supervised probing, which enables us to check and mitigate the overconfidence issue for a trained model, thereby improving its trustworthiness. We provide a simple yet effective framework, which can be flexibly applied to existing trustworthiness-related methods in a plug-and-play manner. Extensive experiments on three trustworthiness-related tasks (misclassification detection, calibration and out-of-distribution detection) across various benchmarks verify the effectiveness of our proposed probing framework.
FastCat Catalogues: Interactive Entity-based Exploratory Analysis of Archival Documents
Venue: arXiv cs.DL 2023
Year: 2023

We describe FastCat Catalogues, a Web application that supports researchers studying archival material, such as historians, in exploring and quantitatively analysing the data (transcripts) of archival documents. The application was designed based on real information needs provided by a large group of researchers, makes use of JSON technology, and is configurable for use over any type of archival documents whose contents have been transcribed and exported in JSON format. The supported functionalities include a) source- or record-specific entity browsing, b) source-independent entity browsing, c) data filtering, d) inspection of provenance information, e) data aggregation and visualisation in charts, f) table and chart data export for further (external) analysis. The application is provided as open source and is currently used by historians in maritime history research.
First steps towards quantum machine learning applied to the classification of event-related potentials
Venue: arXiv cs.HC 2023
Year: 2023

Low information transfer rate is a major bottleneck for brain-computer interfaces based on non-invasive electroencephalography (EEG) for clinical applications. This led to the development of more robust and accurate classifiers. In this study, we investigate the performance of quantum-enhanced support vector classifier (QSVC). Training (predicting) balanced accuracy of QSVC was 83.17 (50.25) %. This result shows that the classifier was able to learn from EEG data, but that more research is required to obtain higher predicting accuracy. This could be achieved by a better configuration of the classifier, such as increasing the number of shots.
PAseos Simulates the Environment for Operating multiple Spacecraft
Venue: arXiv cs.DC 2023
Year: 2023

The next generation of spacecraft is anticipated to enable various new applications involving onboard processing, machine learning and decentralised operational scenarios. Even though many of these have been previously proposed and evaluated, the operational constraints of real mission scenarios are often either not considered or only rudimentary. Here, we present an open-source Python module called PASEOS that is capable of modelling operational scenarios involving one or multiple spacecraft. It considers several physical phenomena including thermal, power, bandwidth and communications constraints as well as the impact of radiation on spacecraft. PASEOS can be run both as a high-performance-oriented numerical simulation and/or in a real-time mode directly on edge hardware. We demonstrate these capabilities in three scenarios, one in real-time simulation on a Unibap iX-10 100 satellite processor, another in a simulation modelling an entire constellation performing tasks over several hours and one training a machine learning model in a decentralised setting. While we demonstrate tasks in Earth orbit, PASEOS is conceptually designed to allow deep space scenarios too. Our results show that PASEOS can model the described scenarios efficiently and thus provide insight into operational considerations. We show this in terms of runtime and overhead as well as by investigating the modelled temperature, battery status and communication windows of a constellation. By running PASEOS on an actual satellite processor, we showcase how PASEOS can be directly included in hardware demonstrators for future missions. Overall, we provide the first solution to holistically model the physical constraints spacecraft encounter in Earth orbit and beyond. The PASEOS module is available open-source online together with an extensive documentation to enable researchers to quickly incorporate it in their studies.
Codes for Correcting $t$ Limited-Magnitude Sticky Deletions
Venue: arXiv cs.IT 2023
Year: 2023

Codes for correcting sticky insertions/deletions and limited-magnitude errors have attracted significant attention due to their applications of flash memories, racetrack memories, and DNA data storage systems. In this paper, we first consider the error type of $t$-sticky deletions with $\ell$-limited-magnitude and propose a non-systematic code for correcting this type of error with redundancy $2t(1-1/p)\cdot\log(n+1)+O(1)$, where $p$ is the smallest prime larger than $\ell+1$. Next, we present a systematic code construction with an efficient encoding and decoding algorithm with redundancy $\frac{\lceil2t(1-1/p)\rceil\cdot\lceil\log p\rceil}{\log p} \log(n+1)+O(\log\log n)$, where $p$ is the smallest prime larger than $\ell+1$.
Diagnosis of Constant Faults in Switching Networks
Venue: arXiv cs.CC 2023
Year: 2023

In this paper, we study decision trees for diagnosis of constant faults in switching networks. Each constant fault consists in assigning Boolean constants to some edges of the network instead of literals. The problem of diagnosis is to recognize the function implemented by the switching network with a constant fault from a given set of faults. For this problem solving, we use decision trees. Each query (attribute) of a decision tree consists of observing the value of function implemented by the faulty switching network on a given tuple of variable values. We study the depth of decision trees for diagnosis of arbitrary and specially constructed switching networks and the complexity of diagnostic decision tree construction.
Coherence and Diversity through Noise: Self-Supervised Paraphrase Generation via Structure-Aware Denoising
Venue: arXiv cs.CL 2023
Year: 2023

In this paper, we propose SCANING, an unsupervised framework for paraphrasing via controlled noise injection. We focus on the novel task of paraphrasing algebraic word problems having practical applications in online pedagogy as a means to reduce plagiarism as well as ensure understanding on the part of the student instead of rote memorization. This task is more complex than paraphrasing general-domain corpora due to the difficulty in preserving critical information for solution consistency of the paraphrased word problem, managing the increased length of the text and ensuring diversity in the generated paraphrase. Existing approaches fail to demonstrate adequate performance on at least one, if not all, of these facets, necessitating the need for a more comprehensive solution. To this end, we model the noising search space as a composition of contextual and syntactic aspects and sample noising functions consisting of either one or both aspects. This allows for learning a denoising function that operates over both aspects and produces semantically equivalent and syntactically diverse outputs through grounded noise injection. The denoising function serves as a foundation for learning a paraphrasing function which operates solely in the input-paraphrase space without carrying any direct dependency on noise. We demonstrate SCANING considerably improves performance in terms of both semantic preservation and producing diverse paraphrases through extensive automated and manual evaluation across 4 datasets.
Perception Datasets for Anomaly Detection in Autonomous Driving: A Survey
Venue: arXiv cs.RO 2023
Year: 2023

Deep neural networks (DNN) which are employed in perception systems for autonomous driving require a huge amount of data to train on, as they must reliably achieve high performance in all kinds of situations. However, these DNN are usually restricted to a closed set of semantic classes available in their training data, and are therefore unreliable when confronted with previously unseen instances. Thus, multiple perception datasets have been created for the evaluation of anomaly detection methods, which can be categorized into three groups: real anomalies in real-world, synthetic anomalies augmented into real-world and completely synthetic scenes. This survey provides a structured and, to the best of our knowledge, complete overview and comparison of perception datasets for anomaly detection in autonomous driving. Each chapter provides information about tasks and ground truth, context information, and licenses. Additionally, we discuss current weaknesses and gaps in existing datasets to underline the importance of developing further data.
Federated Survival Forests
Venue: arXiv cs.LG 2023
Year: 2023

Survival analysis is a subfield of statistics concerned with modeling the occurrence time of a particular event of interest for a population. Survival analysis found widespread applications in healthcare, engineering, and social sciences. However, real-world applications involve survival datasets that are distributed, incomplete, censored, and confidential. In this context, federated learning can tremendously improve the performance of survival analysis applications. Federated learning provides a set of privacy-preserving techniques to jointly train machine learning models on multiple datasets without compromising user privacy, leading to a better generalization performance. However, despite the widespread development of federated learning in recent AI research, few studies focus on federated survival analysis. In this work, we present a novel federated algorithm for survival analysis based on one of the most successful survival models, the random survival forest. We call the proposed method Federated Survival Forest (FedSurF). With a single communication round, FedSurF obtains a discriminative power comparable to deep-learning-based federated models trained over hundreds of federated iterations. Moreover, FedSurF retains all the advantages of random forests, namely low computational cost and natural handling of missing values and incomplete datasets. These advantages are especially desirable in real-world federated environments with multiple small datasets stored on devices with low computational capabilities. Numerical experiments compare FedSurF with state-of-the-art survival models in federated networks, showing how FedSurF outperforms deep-learning-based federated algorithms in realistic environments with non-identically distributed data.
Guide the Learner: Controlling Product of Experts Debiasing Method Based on Token Attribution Similarities
Venue: arXiv cs.CL 2023
Year: 2023

Several proposals have been put forward in recent years for improving out-of-distribution (OOD) performance through mitigating dataset biases. A popular workaround is to train a robust model by re-weighting training examples based on a secondary biased model. Here, the underlying assumption is that the biased model resorts to shortcut features. Hence, those training examples that are correctly predicted by the biased model are flagged as being biased and are down-weighted during the training of the main model. However, assessing the importance of an instance merely based on the predictions of the biased model may be too naive. It is possible that the prediction of the main model can be derived from another decision-making process that is distinct from the behavior of the biased model. To circumvent this, we introduce a fine-tuning strategy that incorporates the similarity between the main and biased model attribution scores in a Product of Experts (PoE) loss function to further improve OOD performance. With experiments conducted on natural language inference and fact verification benchmarks, we show that our method improves OOD results while maintaining in-distribution (ID) performance.
Top-Down Beats Bottom-Up in 3D Instance Segmentation
Venue: arXiv cs.CV 2023
Year: 2023

Most 3D instance segmentation methods exploit a bottom-up strategy, typically including resource-exhaustive post-processing. For point grouping, bottom-up methods rely on prior assumptions about the objects in the form of hyperparameters, which are domain-specific and need to be carefully tuned. On the contrary, we address 3D instance segmentation with a TD3D: the pioneering cluster-free, fully-convolutional and entirely data-driven approach trained in an end-to-end manner. This is the first top-down method outperforming bottom-up approaches in 3D domain. With its straightforward pipeline, it demonstrates outstanding accuracy and generalization ability on the standard indoor benchmarks: ScanNet v2, its extension ScanNet200, and S3DIS, as well as on the aerial STPLS3D dataset. Besides, our method is much faster on inference than the current state-of-the-art grouping-based approaches: our flagship modification is 1.9x faster than the most accurate bottom-up method, while being more accurate, and our faster modification shows state-of-the-art accuracy running at 2.6x speed. Code is available at https://github.com/SamsungLabs/td3d .