OpenRaiser/Intern-Atlas huggingface dataset:
Defect Transformer: An Efficient Hybrid Transformer Architecture for Surface Defect Detection
Venue: arXiv cs.CV 2022
Year: 2022

Surface defect detection is an extremely crucial step to ensure the quality of industrial products. Nowadays, convolutional neural networks (CNNs) based on encoder-decoder architecture have achieved tremendous success in various defect detection tasks. However, due to the intrinsic locality of convolution, they commonly exhibit a limitation in explicitly modeling long-range interactions, critical for pixel-wise defect detection in complex cases, e.g., cluttered background and illegible pseudo-defects. Recent transformers are especially skilled at learning global image dependencies but with limited local structural information necessary for detailed defect location. To overcome the above limitations, we propose an efficient hybrid transformer architecture, termed Defect Transformer (DefT), for surface defect detection, which incorporates CNN and transformer into a unified model to capture local and non-local relationships collaboratively. Specifically, in the encoder module, a convolutional stem block is firstly adopted to retain more detailed spatial information. Then, the patch aggregation blocks are used to generate multi-scale representation with four hierarchies, each of them is followed by a series of DefT blocks, which respectively include a locally position-aware block for local position encoding, a lightweight multi-pooling self-attention to model multi-scale global contextual relationships with good computational efficiency, and a convolutional feed-forward network for feature transformation and further location information learning. Finally, a simple but effective decoder module is proposed to gradually recover spatial details from the skip connections in the encoder. Extensive experiments on three datasets demonstrate the superiority and efficiency of our method compared with other CNN- and transformer-based networks.
CausNet : Generational orderings based search for optimal Bayesian networks via dynamic programming with parent set constraints
Venue: arXiv cs.AI 2022
Year: 2022

Finding a globally optimal Bayesian Network using exhaustive search is a problem with super-exponential complexity, which severely restricts the number of variables that it can work for. We implement a dynamic programming based algorithm with built-in dimensionality reduction and parent set identification. This reduces the search space drastically and can be applied to large-dimensional data. We use what we call generational orderings based search for optimal networks, which is a novel way to efficiently search the space of possible networks given the possible parent sets. The algorithm supports both continuous and categorical data, and categorical as well as survival outcomes. We demonstrate the efficacy of our algorithm on both synthetic and real data. In simulations, our algorithm performs better than three state-of-art algorithms that are currently used extensively. We then apply it to an Ovarian Cancer gene expression dataset with 513 genes and a survival outcome. Our algorithm is able to find an optimal network describing the disease pathway consisting of 6 genes leading to the outcome node in a few minutes on a basic computer. Our generational orderings based search for optimal networks, is both efficient and highly scalable approach to finding optimal Bayesian Networks, that can be applied to 1000s of variables. Using specifiable parameters - correlation, FDR cutoffs, and in-degree - one can increase or decrease the number of nodes and density of the networks. Availability of two scoring option-BIC and Bge-and implementation of survival outcomes and mixed data types makes our algorithm very suitable for many types of high dimensional biomedical data to find disease pathways.
Revisiting PatchMatch Multi-View Stereo for Urban 3D Reconstruction
Venue: arXiv cs.CV 2022
Year: 2022

In this paper, a complete pipeline for image-based 3D reconstruction of urban scenarios is proposed, based on PatchMatch Multi-View Stereo (MVS). Input images are firstly fed into an off-the-shelf visual SLAM system to extract camera poses and sparse keypoints, which are used to initialize PatchMatch optimization. Then, pixelwise depths and normals are iteratively computed in a multi-scale framework with a novel depth-normal consistency loss term and a global refinement algorithm to balance the inherently local nature of PatchMatch. Finally, a large-scale point cloud is generated by back-projecting multi-view consistent estimates in 3D. The proposed approach is carefully evaluated against both classical MVS algorithms and monocular depth networks on the KITTI dataset, showing state of the art performances.
Multiplicative linear logic from a resolution-based tile system
Venue: arXiv cs.LO 2022
Year: 2022

We present the stellar resolution, a "flexible" tile system based on Robinson's first-order resolution. After establishing formal definitions and basic properties of the stellar resolution, we show its Turing-completeness and to illustrate the model, we exhibit how it naturally represents computation with Horn clauses and automata as well as nondeterministic tiling constructions used in DNA computing. In the second and main part, by using the stellar resolution, we formalise and extend ideas of a new alternative to proof-net theory sketched by Girard in his transcendental syntax programme. In particular, we encode both cut-elimination and logical correctness for the multiplicative fragment of linear logic (MLL). We finally obtain completeness results for both MLL and MLL extended with the so-called MIX rule. By extending the ideas of Girard's geometry of interaction, this suggests a first step towards a new understanding of the interplay between logic and computation where linear logic is seen as a (constructed) way to format computation.
Angular Gap: Reducing the Uncertainty of Image Difficulty through Model Calibration
Venue: arXiv cs.CV 2022
Year: 2022

Curriculum learning needs example difficulty to proceed from easy to hard. However, the credibility of image difficulty is rarely investigated, which can seriously affect the effectiveness of curricula. In this work, we propose Angular Gap, a measure of difficulty based on the difference in angular distance between feature embeddings and class-weight embeddings built by hyperspherical learning. To ascertain difficulty estimation, we introduce class-wise model calibration, as a post-training technique, to the learnt hyperbolic space. This bridges the gap between probabilistic model calibration and angular distance estimation of hyperspherical learning. We show the superiority of our calibrated Angular Gap over recent difficulty metrics on CIFAR10-H and ImageNetV2. We further propose Angular Gap based curriculum learning for unsupervised domain adaptation that can translate from learning easy samples to mining hard samples. We combine this curriculum with a state-of-the-art self-training method, Cycle Self Training (CST). The proposed Curricular CST learns robust representations and outperforms recent baselines on Office31 and VisDA 2017.
Online Total Completion Time Scheduling on Parallel Identical Machines
Venue: arXiv cs.DS 2022
Year: 2022

We investigate deterministic non-preemptive online scheduling with delayed commitment for total completion time minimization on parallel identical machines. In this problem, jobs arrive one-by-one and their processing times are revealed upon arrival. An online algorithm can assign a job to a machine at any time after its arrival. We neither allow preemption nor a restart of the job, that is, once started, the job occupies the assigned machine until its completion. Our objective is the minimization of the sum of the completion times of all jobs. In the more general weighted version of the problem, we multiply the completion time of a job by the individual weight of the job. We apply competitive analysis to evaluate our algorithms. We improve 25-year-old lower bounds for the competitive ratio of this problem by optimizing a simple job pattern. These lower bounds decrease with growing numbers of machines. Based on the job pattern, we develop an online algorithm which is an extension of the delayed-SPT (Shortest Processing Time first) approach to the parallel machine environment. We show that the competitive ratio is at most 1.546 for any even machine number which is a significant improvement over the best previously known competitive ratio of 1.791. For the two-machine environment, this algorithm achieves a tight competitive ratio. This is the first algorithm which optimally solves an online total completion time problem in a parallel machine environment. Finally, we give the first separation between the weighted and unweighted versions of the problem by showing that in the two-machine environment, the competitive ratio of the weighted completion time objective is strictly larger than 1.546.
Conjunctive Queries, Existentially Quantified Systems of Equations and Finite Substitutions
Venue: arXiv cs.LO 2022
Year: 2022

This report presents an elementary theory of unification for positive conjunctive queries. A positive conjunctive query is a formula constructed from propositional constants, equations and atoms using the conjunction $\wedge$ and the existential quantifier $\exists$. In particular, empty queries correspond to existentially quantified systems of equations -- called $\cal E$-formulas. We provide an algorithm which transforms any conjunctive query into a solved form. We prove some lattice-theoretic properties of queries. In particular, the quotient set of $\cal E$-formulas under an equivalence relation forms a complete lattice. Then we present another lattice -- a lattice of finite substitutions. We prove that the both lattices are isomorphic. Finally, we introduce the notion of application of substitutions to formulas and clarify its relationship to $\cal E$-formulas. This theory can be regarded as a basis for alternative presentation of logic programming.
Boolean Decision Rules for Reinforcement Learning Policy Summarisation
Venue: arXiv cs.LG 2022
Year: 2022

Explainability of Reinforcement Learning (RL) policies remains a challenging research problem, particularly when considering RL in a safety context. Understanding the decisions and intentions of an RL policy offer avenues to incorporate safety into the policy by limiting undesirable actions. We propose the use of a Boolean Decision Rules model to create a post-hoc rule-based summary of an agent's policy. We evaluate our proposed approach using a DQN agent trained on an implementation of a lava gridworld and show that, given a hand-crafted feature representation of this gridworld, simple generalised rules can be created, giving a post-hoc explainable summary of the agent's policy. We discuss possible avenues to introduce safety into a RL agent's policy by using rules generated by this rule-based model as constraints imposed on the agent's policy, as well as discuss how creating simple rule summaries of an agent's policy may help in the debugging process of RL agents.
The Theory of Call-by-Value Solvability (long version)
Venue: arXiv cs.LO 2022
Year: 2022

The denotational semantics of the untyped lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped call-by-value lambda-calculus (CbV) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory.
Model Checking for Rectangular Hybrid Systems: A Quantified Encoding Approach
Venue: arXiv cs.LO 2022
Year: 2022

Satisfiability Modulo Theories (SMT) solvers have been successfully applied to solve many problems in formal verification such as bounded model checking (BMC) for many classes of systems from integrated circuits to cyber-physical systems. Typically, BMC is performed by checking satisfiability of a possibly long, but quantifier-free formula. However, BMC problems can naturally be encoded as quantified formulas over the number of BMC steps. In this approach, we then use decision procedures supporting quantifiers to check satisfiability of these quantified formulas. This approach has previously been applied to perform BMC using a Quantified Boolean Formula (QBF) encoding for purely discrete systems, and then discharges the QBF checks using QBF solvers. In this paper, we present a new quantified encoding of BMC for rectangular hybrid automata (RHA), which requires using more general logics due to the real (dense) time and real-valued state variables modeling continuous states. We have implemented a preliminary experimental prototype of the method using the HyST model transformation tool to generate the quantified BMC (QBMC) queries for the Z3 SMT solver. We describe experimental results on several timed and hybrid automata benchmarks, such as the Fischer and Lynch-Shavit mutual exclusion algorithms. We compare our approach to quantifier-free BMC approaches, such as those in the dReach tool that uses the dReal SMT solver, and the HyComp tool built on top of nuXmv that uses the MathSAT SMT solver. Based on our promising experimental results, QBMC may in the future be an effective and scalable analysis approach for RHA and other classes of hybrid automata as further improvements are made in quantifier handling in SMT solvers such as Z3.
Fusion of Physiological and Behavioural Signals on SPD Manifolds with Application to Stress and Pain Detection
Venue: arXiv cs.LG 2022
Year: 2022

Existing multimodal stress/pain recognition approaches generally extract features from different modalities independently and thus ignore cross-modality correlations. This paper proposes a novel geometric framework for multimodal stress/pain detection utilizing Symmetric Positive Definite (SPD) matrices as a representation that incorporates the correlation relationship of physiological and behavioural signals from covariance and cross-covariance. Considering the non-linearity of the Riemannian manifold of SPD matrices, well-known machine learning techniques are not suited to classify these matrices. Therefore, a tangent space mapping method is adopted to map the derived SPD matrix sequences to the vector sequences in the tangent space where the LSTM-based network can be applied for classification. The proposed framework has been evaluated on two public multimodal datasets, achieving both the state-of-the-art results for stress and pain detection tasks.
PBRE: A Rule Extraction Method from Trained Neural Networks Designed for Smart Home Services
Venue: arXiv cs.AI 2022
Year: 2022

Designing smart home services is a complex task when multiple services with a large number of sensors and actuators are deployed simultaneously. It may rely on knowledge-based or data-driven approaches. The former can use rule-based methods to design services statically, and the latter can use learning methods to discover inhabitants' preferences dynamically. However, neither of these approaches is entirely satisfactory because rules cannot cover all possible situations that may change, and learning methods may make decisions that are sometimes incomprehensible to the inhabitant. In this paper, PBRE (Pedagogic Based Rule Extractor) is proposed to extract rules from learning methods to realize dynamic rule generation for smart home systems. The expected advantage is that both the explainability of rule-based methods and the dynamicity of learning methods are adopted. We compare PBRE with an existing rule extraction method, and the results show better performance of PBRE. We also apply PBRE to extract rules from a smart home service represented by an NRL (Neural Network-based Reinforcement Learning). The results show that PBRE can help the NRL-simulated service to make understandable suggestions to the inhabitant.
Accelerating Deep Learning Model Inference on Arm CPUs with Ultra-Low Bit Quantization and Runtime
Venue: arXiv cs.LG 2022
Year: 2022

Deep Learning has been one of the most disruptive technological advancements in recent times. The high performance of deep learning models comes at the expense of high computational, storage and power requirements. Sensing the immediate need for accelerating and compressing these models to improve on-device performance, we introduce Deeplite Neutrino for production-ready optimization of the models and Deeplite Runtime for deployment of ultra-low bit quantized models on Arm-based platforms. We implement low-level quantization kernels for Armv7 and Armv8 architectures enabling deployment on the vast array of 32-bit and 64-bit Arm-based devices. With efficient implementations using vectorization, parallelization, and tiling, we realize speedups of up to 2x and 2.2x compared to TensorFlow Lite with XNNPACK backend on classification and detection models, respectively. We also achieve significant speedups of up to 5x and 3.2x compared to ONNX Runtime for classification and detection models, respectively.
The Multiple Subnetwork Hypothesis: Enabling Multidomain Learning by Isolating Task-Specific Subnetworks in Feedforward Neural Networks
Venue: arXiv cs.LG 2022
Year: 2022

Neural networks have seen an explosion of usage and research in the past decade, particularly within the domains of computer vision and natural language processing. However, only recently have advancements in neural networks yielded performance improvements beyond narrow applications and translated to expanded multitask models capable of generalizing across multiple data types and modalities. Simultaneously, it has been shown that neural networks are overparameterized to a high degree, and pruning techniques have proved capable of significantly reducing the number of active weights within the network while largely preserving performance. In this work, we identify a methodology and network representational structure which allows a pruned network to employ previously unused weights to learn subsequent tasks. We employ these methodologies on well-known benchmarking datasets for testing purposes and show that networks trained using our approaches are able to learn multiple tasks, which may be related or unrelated, in parallel or in sequence without sacrificing performance on any task or exhibiting catastrophic forgetting.
Using attention methods to predict judicial outcomes
Venue: arXiv cs.LG 2022
Year: 2022

Legal Judgment Prediction is one of the most acclaimed fields for the combined area of NLP, AI, and Law. By legal prediction we mean an intelligent systems capable to predict specific judicial characteristics, such as judicial outcome, a judicial class, predict an specific case. In this research, we have used AI classifiers to predict judicial outcomes in the Brazilian legal system. For this purpose, we developed a text crawler to extract data from the official Brazilian electronic legal systems. These texts formed a dataset of second-degree murder and active corruption cases. We applied different classifiers, such as Support Vector Machines and Neural Networks, to predict judicial outcomes by analyzing textual features from the dataset. Our research showed that Regression Trees, Gated Recurring Units and Hierarchical Attention Networks presented higher metrics for different subsets. As a final goal, we explored the weights of one of the algorithms, the Hierarchical Attention Networks, to find a sample of the most important words used to absolve or convict defendants.
A Pattern-based deadlock-freedom analysis strategy for concurrent systems
Venue: arXiv cs.SE 2022
Year: 2022

Local analysis has long been recognised as an effective tool to combat the state-space explosion problem. In this work, we propose a method that systematises the use of local analysis in the verification of deadlock freedom for concurrent and distributed systems. It combines a strategy for system decomposition with the verification of the decomposed subsystems via adherence to behavioural patterns. At the core of our work, we have a number of CSP refinement expressions that allows the user of our method to automatically verify all the behavioural restrictions that we impose. We also propose a prototype tool to support our method. Finally, we demonstrate the practical impact our method can have by analysing how it fares when applied to some examples.
Recognizing Hand Use and Hand Role at Home After Stroke from Egocentric Video
Venue: arXiv cs.CV 2022
Year: 2022

Introduction: Hand function is a central determinant of independence after stroke. Measuring hand use in the home environment is necessary to evaluate the impact of new interventions, and calls for novel wearable technologies. Egocentric video can capture hand-object interactions in context, as well as show how more-affected hands are used during bilateral tasks (for stabilization or manipulation). Automated methods are required to extract this information. Objective: To use artificial intelligence-based computer vision to classify hand use and hand role from egocentric videos recorded at home after stroke. Methods: Twenty-one stroke survivors participated in the study. A random forest classifier, a SlowFast neural network, and the Hand Object Detector neural network were applied to identify hand use and hand role at home. Leave-One-Subject-Out-Cross-Validation (LOSOCV) was used to evaluate the performance of the three models. Between-group differences of the models were calculated based on the Mathews correlation coefficient (MCC). Results: For hand use detection, the Hand Object Detector had significantly higher performance than the other models. The macro average MCCs using this model in the LOSOCV were 0.50 +- 0.23 for the more-affected hands and 0.58 +- 0.18 for the less-affected hands. Hand role classification had macro average MCCs in the LOSOCV that were close to zero for all models. Conclusion: Using egocentric video to capture the hand use of stroke survivors at home is feasible. Pose estimation to track finger movements may be beneficial to classifying hand roles in the future.