OpenRaiser/Intern-Atlas huggingface dataset:
Deciding Hyperproperties Combined with Functional Specifications
Venue: arXiv cs.LO 2022
Year: 2022

We study satisfiability for HyperLTL with a $\forall^*\exists^*$ quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate multiple traces (so-called hyperproperties), which are often combined with trace properties that specify functional behavior on single traces. Following this conceptual split, we first define several safety and liveness fragments of $\forall^*\exists^*$ HyperLTL, and characterize the complexity of their (often much easier) satisfiability problem. We then add LTL trace properties as functional specifications. Though (highly) undecidable in many cases, this way of combining "simple" HyperLTL and arbitrary LTL also leads to interesting new decidable fragments. This systematic study of $\forall^*\exists^*$ fragments is complemented by a new (incomplete) algorithm for $\forall\exists^*$-HyperLTL satisfiability.
A practical optimal control approach for two-speed actuators
Venue: arXiv cs.RO 2022
Year: 2022

This paper addresses the closed-loop control of an actuator with both a continuous input variable (motor torque) and a discrete input variable (mode selection). In many applications, robots have to bear large loads while moving slowly and also have to move quickly through the air with almost no load, leading to conflicting requirements for their actuators. An actuator with multiple gear ratios, like in a powertrain, can address this issue by allowing an effective use of power over a wide range of output speed. However, having discrete modes of operation adds complexity to the high-level control and planning. Here a controller for two-speed actuators that automatically select both the best gear ratio and the motor torque is developed. The approach is to: first derive a low-dimensional model, then use dynamic programming to find the best actions for all possible situations, and last use regression analysis to extract simplified global feedback laws. This approach produces simple practical nearly-optimal feedback laws. A controller that globally minimizes a quadratic cost function is derived for a two-speed actuator prototype, global stability is proven and performance is demonstrated experimentally.
Self-Supervised Pre-training of Vision Transformers for Dense Prediction Tasks
Venue: arXiv cs.CV 2022
Year: 2022

We present a new self-supervised pre-training of Vision Transformers for dense prediction tasks. It is based on a contrastive loss across views that compares pixel-level representations to global image representations. This strategy produces better local features suitable for dense prediction tasks as opposed to contrastive pre-training based on global image representation only. Furthermore, our approach does not suffer from a reduced batch size since the number of negative examples needed in the contrastive loss is in the order of the number of local features. We demonstrate the effectiveness of our pre-training strategy on two dense prediction tasks: semantic segmentation and monocular depth estimation.
Type Systems in Resource-Aware Programming: Opportunities and Challenges
Venue: arXiv cs.PL 2022
Year: 2022

Type systems provide software developers immediate feedback about a subset of correctness properties of their programs. IDE integrations often take advantage of type systems to present errors, suggest completions and even improve navigation. On the other hand, understanding the time and energy consumption of the execution of a program requires manual testing. In this paper, we identify existing work on using type systems for energy awareness, and define the requirements for a practical approach, which the existing approaches do not address fully. Furthermore, we also discuss how existing type systems can help generalize refactors for energy-efficiency.
Transparency, Governance and Regulation of Algorithmic Tools Deployed in the Criminal Justice System: a UK Case Study
Venue: arXiv cs.CY 2022
Year: 2022

We present a survey of tools used in the criminal justice system in the UK in three categories: data infrastructure, data analysis, and risk prediction. Many tools are currently in deployment, offering potential benefits, including improved efficiency and consistency. However, there are also important concerns. Transparent information about these tools, their purpose, how they are used, and by whom is difficult to obtain. Even when information is available, it is often insufficient to enable a satisfactory evaluation. More work is needed to establish governance mechanisms to ensure that tools are deployed in a transparent, safe and ethical way. We call for more engagement with stakeholders and greater documentation of the intended goal of a tool, how it will achieve this goal compared to other options, and how it will be monitored in deployment. We highlight additional points to consider when evaluating the trustworthiness of deployed tools and make concrete proposals for policy.
bsnsing: A decision tree induction method based on recursive optimal boolean rule composition
Venue: arXiv cs.LG 2022
Year: 2022

This paper proposes a new mixed-integer programming (MIP) formulation to optimize split rule selection in the decision tree induction process, and develops an efficient search algorithm that is able to solve practical instances of the MIP model faster than commercial solvers. The formulation is novel for it directly maximizes the Gini reduction, an effective split selection criterion which has never been modeled in a mathematical program for its nonconvexity. The proposed approach differs from other optimal classification tree models in that it does not attempt to optimize the whole tree, therefore the flexibility of the recursive partitioning scheme is retained and the optimization model is more amenable. The approach is implemented in an open-source R package named bsnsing. Benchmarking experiments on 75 open data sets suggest that bsnsing trees are the most capable of discriminating new cases compared to trees trained by other decision tree codes including the rpart, C50, party and tree packages in R. Compared to other optimal decision tree packages, including DL8.5, OSDT, GOSDT and indirectly more, bsnsing stands out in its training speed, ease of use and broader applicability without losing in prediction accuracy.
Robust and accelerated single-spike spiking neural network training with applicability to challenging temporal tasks
Venue: arXiv cs.NE 2022
Year: 2022

Spiking neural networks (SNNs), particularly the single-spike variant in which neurons spike at most once, are considerably more energy efficient than standard artificial neural networks (ANNs). However, single-spike SSNs are difficult to train due to their dynamic and non-differentiable nature, where current solutions are either slow or suffer from training instabilities. These networks have also been critiqued for their limited computational applicability such as being unsuitable for time-series datasets. We propose a new model for training single-spike SNNs which mitigates the aforementioned training issues and obtains competitive results across various image and neuromorphic datasets, with up to a $13.98\times$ training speedup and up to an $81\%$ reduction in spikes compared to the multi-spike SNN. Notably, our model performs on par with multi-spike SNNs in challenging tasks involving neuromorphic time-series datasets, demonstrating a broader computational role for single-spike SNNs than previously believed.
Zero-Shot and Few-Shot Learning for Lung Cancer Multi-Label Classification using Vision Transformer
Venue: arXiv cs.CV 2022
Year: 2022

Lung cancer is the leading cause of cancer-related death worldwide. Lung adenocarcinoma (LUAD) and lung squamous cell carcinoma (LUSC) are the most common histologic subtypes of non-small-cell lung cancer (NSCLC). Histology is an essential tool for lung cancer diagnosis. Pathologists make classifications according to the dominant subtypes. Although morphology remains the standard for diagnosis, significant tool needs to be developed to elucidate the diagnosis. In our study, we utilize the pre-trained Vision Transformer (ViT) model to classify multiple label lung cancer on histologic slices (from dataset LC25000), in both Zero-Shot and Few-Shot settings. Then we compare the performance of Zero-Shot and Few-Shot ViT on accuracy, precision, recall, sensitivity and specificity. Our study show that the pre-trained ViT model has a good performance in Zero-Shot setting, a competitive accuracy ($99.87\%$) in Few-Shot setting ({epoch = 1}) and an optimal result ($100.00\%$ on both validation set and test set) in Few-Shot seeting ({epoch = 5}).
On the solvability of weakly linear systems of fuzzy relation equations
Venue: arXiv cs.AI 2022
Year: 2022

Systems of fuzzy relation equations and inequalities in which an unknown fuzzy relation is on the one side of the equation or inequality are linear systems. They are the most studied ones, and a vast literature on linear systems focuses on finding solutions and solvability criteria for such systems. The situation is quite different with the so-called weakly linear systems, in which an unknown fuzzy relation is on both sides of the equation or inequality. Precisely, the scholars have only given the characterization of the set of exact solutions to such systems. This paper describes the set of fuzzy relations that solve weakly linear systems to a certain degree and provides ways to compute them. We pay special attention to developing the algorithms for computing fuzzy preorders and fuzzy equivalences that are solutions to some extent to weakly linear systems. We establish additional properties for the set of such approximate solutions over some particular types of complete residuated lattices. We demonstrate the advantage of this approach via many examples that arise from the problem of aggregation of fuzzy networks.
A Design Space for Explainable Ranking and Ranking Models
Venue: arXiv cs.LG 2022
Year: 2022

Item ranking systems support users in multi-criteria decision-making tasks. Users need to trust rankings and ranking algorithms to reflect user preferences nicely while avoiding systematic errors and biases. However, today only few approaches help end users, model developers, and analysts to explain rankings. We report on the study of explanation approaches from the perspectives of recommender systems, explainable AI, and visualization research and propose the first cross-domain design space for explainers of item rankings. In addition, we leverage the descriptive power of the design space to characterize a) existing explainers and b) three main user groups involved in ranking explanation tasks. The generative power of the design space is a means for future designers and developers to create more target-oriented solutions in this only weakly exploited space.
How to Compose Shortest Paths
Venue: arXiv cs.DM 2022
Year: 2022

The composition problem for shortest paths asks the following: given shortest paths on weighted graphs M and N which share a common boundary, find the shortest paths on their union. This problem is a crucial step in any algorithm which uses the divide and conquer method to find shortest paths. This extended abstract details how this problem may be understood categorically. Finding shortest paths is represented by a functor and the composition problem asks to find the value of this functor on a pushout using the values of the functor on the components. Furthermore, we present an algorithm which solves the composition problem for shortest paths. When implemented in Python, this algorithm reduces the computation time for finding shortest paths by relying on precompilation.
Dictionary Learning with Accumulator Neurons
Venue: arXiv cs.CV 2022
Year: 2022

The Locally Competitive Algorithm (LCA) uses local competition between non-spiking leaky integrator neurons to infer sparse representations, allowing for potentially real-time execution on massively parallel neuromorphic architectures such as Intel's Loihi processor. Here, we focus on the problem of inferring sparse representations from streaming video using dictionaries of spatiotemporal features optimized in an unsupervised manner for sparse reconstruction. Non-spiking LCA has previously been used to achieve unsupervised learning of spatiotemporal dictionaries composed of convolutional kernels from raw, unlabeled video. We demonstrate how unsupervised dictionary learning with spiking LCA (\hbox{S-LCA}) can be efficiently implemented using accumulator neurons, which combine a conventional leaky-integrate-and-fire (\hbox{LIF}) spike generator with an additional state variable that is used to minimize the difference between the integrated input and the spiking output. We demonstrate dictionary learning across a wide range of dynamical regimes, from graded to intermittent spiking, for inferring sparse representations of both static images drawn from the CIFAR database as well as video frames captured from a DVS camera. On a classification task that requires identification of the suite from a deck of cards being rapidly flipped through as viewed by a DVS camera, we find essentially no degradation in performance as the LCA model used to infer sparse spatiotemporal representations migrates from graded to spiking. We conclude that accumulator neurons are likely to provide a powerful enabling component of future neuromorphic hardware for implementing online unsupervised learning of spatiotemporal dictionaries optimized for sparse reconstruction of streaming video from event based DVS cameras.
Fitting and recognition of geometric primitives in segmented 3D point clouds using a localized voting procedure
Venue: arXiv cs.CV 2022
Year: 2022

The automatic creation of geometric models from point clouds has numerous applications in CAD (e.g., reverse engineering, manufacturing, assembling) and, more in general, in shape modelling and processing. Given a segmented point cloud representing a man-made object, we propose a method for recognizing simple geometric primitives and their interrelationships. Our approach is based on the Hough transform (HT) for its ability to deal with noise, missing parts and outliers. In our method we introduce a novel technique for processing segmented point clouds that, through a voting procedure, is able to provide an initial estimate of the geometric parameters characterizing each primitive type. By using these estimates, we localize the search of the optimal solution in a dimensionally-reduced parameter space thus making it efficient to extend the HT to more primitives than those that are generally found in the literature, i.e. planes and spheres. Then, we extract a number of geometric descriptors that uniquely characterize a segment, and, on the basis of these descriptors, we show how to aggregate parts of primitives (segments). Experiments on both synthetic and industrial scans reveal the robustness of the primitive fitting method and its effectiveness for inferring relations among segments.
Segmentation Consistency Training: Out-of-Distribution Generalization for Medical Image Segmentation
Venue: arXiv cs.CV 2022
Year: 2022

Generalizability is seen as one of the major challenges in deep learning, in particular in the domain of medical imaging, where a change of hospital or in imaging routines can lead to a complete failure of a model. To tackle this, we introduce Consistency Training, a training procedure and alternative to data augmentation based on maximizing models' prediction consistency across augmented and unaugmented data in order to facilitate better out-of-distribution generalization. To this end, we develop a novel region-based segmentation loss function called Segmentation Inconsistency Loss (SIL), which considers the differences between pairs of augmented and unaugmented predictions and labels. We demonstrate that Consistency Training outperforms conventional data augmentation on several out-of-distribution datasets on polyp segmentation, a popular medical task.
MVMO: A Multi-Object Dataset for Wide Baseline Multi-View Semantic Segmentation
Venue: arXiv cs.CV 2022
Year: 2022

We present MVMO (Multi-View, Multi-Object dataset): a synthetic dataset of 116,000 scenes containing randomly placed objects of 10 distinct classes and captured from 25 camera locations in the upper hemisphere. MVMO comprises photorealistic, path-traced image renders, together with semantic segmentation ground truth for every view. Unlike existing multi-view datasets, MVMO features wide baselines between cameras and high density of objects, which lead to large disparities, heavy occlusions and view-dependent object appearance. Single view semantic segmentation is hindered by self and inter-object occlusions that could benefit from additional viewpoints. Therefore, we expect that MVMO will propel research in multi-view semantic segmentation and cross-view semantic transfer. We also provide baselines that show that new research is needed in such fields to exploit the complementary information of multi-view setups.
Introduction of a tree-based technique for efficient and real-time label retrieval in the object tracking system
Venue: arXiv cs.CV 2022
Year: 2022

This paper addresses the issue of the real-time tracking quality of moving objects in large-scale video surveillance systems. During the tracking process, the system assigns an identifier or label to each tracked object to distinguish it from other objects. In such a mission, it is essential to keep this identifier for the same objects, whatever the area, the time of their appearance, or the detecting camera. This is to conserve as much information about the tracking object as possible, decrease the number of ID switching (ID-Sw), and increase the quality of object tracking. To accomplish object labeling, a massive amount of data collected by the cameras must be searched to retrieve the most similar (nearest neighbor) object identifier. Although this task is simple, it becomes very complex in large-scale video surveillance networks, where the data becomes very large. In this case, the label retrieval time increases significantly with this increase, which negatively affects the performance of the real-time tracking system. To avoid such problems, we propose a new solution to automatically label multiple objects for efficient real-time tracking using the indexing mechanism. This mechanism organizes the metadata of the objects extracted during the detection and tracking phase in an Adaptive BCCF-tree. The main advantage of this structure is: its ability to index massive metadata generated by multi-cameras, its logarithmic search complexity, which implicitly reduces the search response time, and its quality of research results, which ensure coherent labeling of the tracked objects. The system load is distributed through a new Internet of Video Things infrastructure-based architecture to improve data processing and real-time object tracking performance. The experimental evaluation was conducted on a publicly available dataset generated by multi-camera containing different crowd activities.
Computational Reproducibility Within Prognostics and Health Management
Venue: arXiv cs.DL 2022
Year: 2022

Scientific research frequently involves the use of computational tools and methods. Providing thorough documentation, open-source code, and data -- the creation of reproducible computational research -- helps others understand a researcher's work. Here, we explore computational reproducibility, broadly, and from within the field of prognostics and health management (PHM). The adoption of reproducible computational research practices remains low across scientific disciplines and within PHM. Our text mining of more than 300 articles, from publications engaged in PHM research, showed that fewer than 1% of researchers made their code and data available to others. Although challenges remain, there are also clear opportunities, and benefits, for engaging in reproducible computational research. Highlighting an opportunity, we introduce an open-source software tool, called PyPHM, to assist PHM researchers in accessing and preprocessing common industrial datasets.
Dataset Bias in Android Malware Detection
Venue: arXiv cs.SE 2022
Year: 2022

Researchers have proposed kinds of malware detection methods to solve the explosive mobile security threats. We argue that the experiment results are inflated due to the research bias introduced by the variability of malware dataset. We explore the impact of bias in Android malware detection in three aspects, the method used to flag the ground truth, the distribution of malware families in the dataset, and the methods to use the dataset. We implement a set of experiments of different VT thresholds and find that the methods used to flag the malware data affect the malware detection performance directly. We further compare the impact of malware family types and composition on malware detection in detail. The superiority of each approach is different under various combinations of malware families. Through our extensive experiments, we showed that the methods to use the dataset can have a misleading impact on evaluation, and the performance difference can be up to over 40%. We argue that these research biases observed in this paper should be carefully controlled/eliminated to enforce a fair comparison of malware detection techniques. Providing reasonable and explainable results is better than only reporting a high detection accuracy with vague dataset and experimental settings.
MACE: An Efficient Model-Agnostic Framework for Counterfactual Explanation
Venue: arXiv cs.AI 2022
Year: 2022

Counterfactual explanation is an important Explainable AI technique to explain machine learning predictions. Despite being studied actively, existing optimization-based methods often assume that the underlying machine-learning model is differentiable and treat categorical attributes as continuous ones, which restricts their real-world applications when categorical attributes have many different values or the model is non-differentiable. To make counterfactual explanation suitable for real-world applications, we propose a novel framework of Model-Agnostic Counterfactual Explanation (MACE), which adopts a newly designed pipeline that can efficiently handle non-differentiable machine-learning models on a large number of feature values. in our MACE approach, we propose a novel RL-based method for finding good counterfactual examples and a gradient-less descent method for improving proximity. Experiments on public datasets validate the effectiveness with better validity, sparsity and proximity.
Discovery of Keys for Graphs [Extended Version]
Venue: arXiv cs.DB 2022
Year: 2022

Keys for graphs uses the topology and value constraints needed to uniquely identify entities in a graph database. They have been studied to support object identification, knowledge fusion, data deduplication, and social network reconciliation. In this paper, we present our algorithm to mine keys over graphs. Our algorithm discovers keys in a graph via frequent subgraph expansion. We present two properties that define a meaningful key, including minimality and support. Lastly, using real-world graphs, we experimentally verify the efficiency of our algorithm on real world graphs.