OpenRaiser/Intern-Atlas huggingface dataset:
Higher Groups in Homotopy Type Theory
Venue: arXiv cs.LO 2018
Year: 2018

We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.
Localization in internets of mobile agents: A linear approach
Venue: arXiv cs.SY 2018
Year: 2018

Fifth generation~(5G) networks providing much higher bandwidth and faster data rates will allow connecting vast number of static and mobile devices, sensors, agents, users, machines, and vehicles, supporting Internet-of-Things (IoT), real-time dynamic networks of mobile things. Positioning and location awareness will become increasingly important, enabling deployment of new services and contributing to significantly improving the overall performance of the 5G~system. Many of the currently talked about solutions to positioning in~5G are centralized, mostly requiring direct line-of-sight (LoS) to deployed access nodes or anchors at the same time, which in turn requires high-density deployments of anchors. But these LoS and centralized positioning solutions may become unwieldy as the number of users and devices continues to grow without limit in sight. As an alternative to the centralized solutions, this paper discusses distributed localization in a 5G enabled IoT environment where many low power devices, users, or agents are to locate themselves without global or LoS access to anchors. Even though positioning is essentially a non-linear problem (solving circle equations by trilateration or triangulation), we discuss a cooperative \textit{linear} distributed iterative solution with only local measurements, communication and computation needed at each agent. Linearity is obtained by reparametrization of the agent location through barycentric coordinate representations based on local neighborhood geometry that may be computed in terms of certain Cayley-Menger determinants involving relative local inter-agent distance measurements.
Certified Roundoff Error Bounds using Bernstein Expansions and Sparse Krivine-Stengle Representations
Venue: arXiv cs.NA 2018
Year: 2018

Floating point error is a drawback of embedded systems implementation that is difficult to avoid. Computing rigorous upper bounds of roundoff errors is absolutely necessary for the validation of critical software. This problem of computing rigorous upper bounds is even more challenging when addressing non-linear programs. In this paper, we propose and compare two new algorithms based on Bernstein expansions and sparse Krivine-Stengle representations, adapted from the field of the global optimization, to compute upper bounds of roundoff errors for programs implementing polynomial and rational functions. We also provide the convergence rate of these two algorithms. We release two related software package FPBern and FPKriSten, and compare them with the state-of-the-art tools. We show that these two methods achieve competitive performance, while providing accurate upper bounds by comparison with the other tools.
Deep Learning Models Delineates Multiple Nuclear Phenotypes in H&E Stained Histology Sections
Venue: arXiv cs.CV 2018
Year: 2018

Nuclear segmentation is an important step for profiling aberrant regions of histology sections. However, segmentation is a complex problem as a result of variations in nuclear geometry (e.g., size, shape), nuclear type (e.g., epithelial, fibroblast), and nuclear phenotypes (e.g., vesicular, aneuploidy). The problem is further complicated as a result of variations in sample preparation. It is shown and validated that fusion of very deep convolutional networks overcomes (i) complexities associated with multiple nuclear phenotypes, and (ii) separation of overlapping nuclei. The fusion relies on integrating of networks that learn region- and boundary-based representations. The system has been validated on a diverse set of nuclear phenotypes that correspond to the breast and brain histology sections.
Blockchain and Artificial Intelligence
Venue: arXiv cs.AI 2018
Year: 2018

It is undeniable that artificial intelligence (AI) and blockchain concepts are spreading at a phenomenal rate. Both technologies have distinct degree of technological complexity and multi-dimensional business implications. However, a common misunderstanding about blockchain concept, in particular, is that blockchain is decentralized and is not controlled by anyone. But the underlying development of a blockchain system is still attributed to a cluster of core developers. Take smart contract as an example, it is essentially a collection of codes (or functions) and data (or states) that are programmed and deployed on a blockchain (say, Ethereum) by different human programmers. It is thus, unfortunately, less likely to be free of loopholes and flaws. In this article, through a brief overview about how artificial intelligence could be used to deliver bug-free smart contract so as to achieve the goal of blockchain 2.0, we to emphasize that the blockchain implementation can be assisted or enhanced via various AI techniques. The alliance of AI and blockchain is expected to create numerous possibilities.
Hardness Results and Approximation Algorithms for the Minimum Dominating Tree Problem
Venue: arXiv cs.CC 2018
Year: 2018

Given an undirected graph $G = (V, E)$ and a weight function $w:E \to \mathbb{R}$, the \textsc{Minimum Dominating Tree} problem asks to find a minimum weight sub-tree of $G$, $T = (U, F)$, such that every $v \in V \setminus U$ is adjacent to at least one vertex in $U$. The special case when the weight function is uniform is known as the \textsc{Minimum Connected Dominating Set} problem. Given an undirected graph $G = (V, E)$ with some subsets of vertices called groups, and a weight function $w:E \to \mathbb{R}$, the \textsc{Group Steiner Tree} problem is to find a minimum weight sub-tree of $G$ which contains at least one vertex from each group. In this paper we show that the two problems are equivalents from approximability perspective. This improves upon both the best known approximation algorithm and the best inapproximability result for the \textsc{Minimum Dominating Tree} problem. We also consider two extrema variants of the \textsc{Minimum Dominating Tree} problem, namely, the \textsc{Minimum Dominating Star} and the \textsc{Minimum Dominating Path} problems which ask to find a minimum dominating star and path respectively.
DyPerm: Maximizing Permanence for Dynamic Community Detection
Venue: arXiv cs.SI 2018
Year: 2018

In this paper, we propose DyPerm, the first dynamic community detection method which optimizes a novel community scoring metric, called permanence. DyPerm incrementally modifies the community structure by updating those communities where the editing of nodes and edges has been performed, keeping the rest of the network unchanged. We present strong theoretical guarantees to show how/why mere updates on the existing community structure leads to permanence maximization in dynamic networks, which in turn decreases the computational complexity drastically. Experiments on both synthetic and six real-world networks with given ground-truth community structure show that DyPerm achieves (on average) 35% gain in accuracy (based on NMI) compared to the best method among four baseline methods. DyPerm also turns out to be 15 times faster than its static counterpart.
Single-Perspective Warps in Natural Image Stitching
Venue: arXiv cs.CV 2018
Year: 2018

Results of image stitching can be perceptually divided into single-perspective and multiple-perspective. Compared to the multiple-perspective result, the single-perspective result excels in perspective consistency but suffers from projective distortion. In this paper, we propose two single-perspective warps for natural image stitching. The first one is a parametric warp, which is a combination of the as-projective-as-possible warp and the quasi-homography warp via dual-feature. The second one is a mesh-based warp, which is determined by optimizing a total energy function that simultaneously emphasizes different characteristics of the single-perspective warp, including alignment, naturalness, distortion and saliency. A comprehensive evaluation demonstrates that the proposed warp outperforms some state-of-the-art warps, including homography, APAP, AutoStitch, SPHP and GSP.
Tensor Comprehensions: Framework-Agnostic High-Performance Machine Learning Abstractions
Venue: arXiv cs.PL 2018
Year: 2018

Deep learning models with convolutional and recurrent networks are now ubiquitous and analyze massive amounts of audio, image, video, text and graph data, with applications in automatic translation, speech-to-text, scene understanding, ranking user preferences, ad placement, etc. Competing frameworks for building these networks such as TensorFlow, Chainer, CNTK, Torch/PyTorch, Caffe1/2, MXNet and Theano, explore different tradeoffs between usability and expressiveness, research or production orientation and supported hardware. They operate on a DAG of computational operators, wrapping high-performance libraries such as CUDNN (for NVIDIA GPUs) or NNPACK (for various CPUs), and automate memory allocation, synchronization, distribution. Custom operators are needed where the computation does not fit existing high-performance library calls, usually at a high engineering cost. This is frequently required when new operators are invented by researchers: such operators suffer a severe performance penalty, which limits the pace of innovation. Furthermore, even if there is an existing runtime call these frameworks can use, it often doesn't offer optimal performance for a user's particular network architecture and dataset, missing optimizations between operators as well as optimizations that can be done knowing the size and shape of data. Our contributions include (1) a language close to the mathematics of deep learning called Tensor Comprehensions, (2) a polyhedral Just-In-Time compiler to convert a mathematical description of a deep learning DAG into a CUDA kernel with delegated memory management and synchronization, also providing optimizations such as operator fusion and specialization for specific sizes, (3) a compilation cache populated by an autotuner. [Abstract cutoff]
SNC: A Cloud Service Platform for Symbolic-Numeric Computation using Just-In-Time Compilation
Venue: arXiv cs.DC 2018
Year: 2018

Cloud services have been widely employed in IT industry and scientific research. By using Cloud services users can move computing tasks and data away from local computers to remote datacenters. By accessing Internet-based services over lightweight and mobile devices, users deploy diversified Cloud applications on powerful machines. The key drivers towards this paradigm for the scientific computing field include the substantial computing capacity, on-demand provisioning and cross-platform interoperability. To fully harness the Cloud services for scientific computing, however, we need to design an application-specific platform to help the users efficiently migrate their applications. In this, we propose a Cloud service platform for symbolic-numeric computation - SNC. SNC allows the Cloud users to describe tasks as symbolic expressions through C/C++, Python, Java APIs and SNC script. Just-In-Time (JIT) compilation through using LLVM/JVM is used to compile the user code to the machine code. We implemented the SNC design and tested a wide range of symbolic-numeric computation applications (including nonlinear minimization, Monte Carlo integration, finite element assembly and multibody dynamics) on several popular cloud platforms (including the Google Compute Engine, Amazon EC2, Microsoft Azure, Rackspace, HP Helion and VMWare vCloud). These results demonstrate that our approach can work across multiple cloud platforms, support different languages and significantly improve the performance of symbolic-numeric computation using cloud platforms. This offered a way to stimulate the need for using the cloud computing for the symbolic-numeric computation in the field of scientific research.
SLAQ: Quality-Driven Scheduling for Distributed Machine Learning
Venue: arXiv cs.DC 2018
Year: 2018

Training machine learning (ML) models with large datasets can incur significant resource contention on shared clusters. This training typically involves many iterations that continually improve the quality of the model. Yet in exploratory settings, better models can be obtained faster by directing resources to jobs with the most potential for improvement. We describe SLAQ, a cluster scheduling system for approximate ML training jobs that aims to maximize the overall job quality. When allocating cluster resources, SLAQ explores the quality-runtime trade-offs across multiple jobs to maximize system-wide quality improvement. To do so, SLAQ leverages the iterative nature of ML training algorithms, by collecting quality and resource usage information from concurrent jobs, and then generating highly-tailored quality-improvement predictions for future iterations. Experiments show that SLAQ achieves an average quality improvement of up to 73% and an average delay reduction of up to 44% on a large set of ML training jobs, compared to resource fairness schedulers.
Challenging Images For Minds and Machines
Venue: arXiv cs.LG 2018
Year: 2018

There is no denying the tremendous leap in the performance of machine learning methods in the past half-decade. Some might even say that specific sub-fields in pattern recognition, such as machine-vision, are as good as solved, reaching human and super-human levels. Arguably, lack of training data and computation power are all that stand between us and solving the remaining ones. In this position paper we underline cases in vision which are challenging to machines and even to human observers. This is to show limitations of contemporary models that are hard to ameliorate by following the current trend to increase training data, network capacity or computational power. Moreover, we claim that attempting to do so is in principle a suboptimal approach. We provide a taster of such examples in hope to encourage and challenge the machine learning community to develop new directions to solve the said difficulties.
Parameter and Insertion Function Co-synthesis for Opacity Enhancement in Parametric Stochastic Discrete Event Systems
Venue: arXiv cs.CR 2018
Year: 2018

Opacity is a property that characterizes the system's capability to keep its "secret" from being inferred by an intruder that partially observes the system's behavior. In this paper, we are concerned with enhancing the opacity using insertion functions, while at the same time, enforcing the task specification in a parametric stochastic discrete event system. We first obtain the parametric Markov decision process that encodes all the possible insertions. Based on which, we convert this parameter and insertion function co-synthesis problem into a nonlinear program. We prove that if the output of this program satisfies all the constraints, it will be a valid solution to our problem. Therefore, the security and the capability of enforcing the task specification can be simultaneously guaranteed.
Do Citations and Readership Identify Seminal Publications?
Venue: arXiv cs.DL 2018
Year: 2018

In this paper, we show that citation counts work better than a random baseline (by a margin of 10%) in distinguishing excellent research, while Mendeley reader counts don't work better than the baseline. Specifically, we study the potential of these metrics for distinguishing publications that caused a change in a research field from those that have not. The experiment has been conducted on a new dataset for bibliometric research called TrueImpactDataset. TrueImpactDataset is a collection of research publications of two types -- research papers which are considered seminal works in their area and papers which provide a literature review of a research area. We provide overview statistics of the dataset and propose to use it for validating research evaluation metrics. Using the dataset, we conduct a set of experiments to study how citation and reader counts perform in distinguishing these publication types, following the intuition that causing a change in a field signifies research contribution. We show that citation counts help in distinguishing research that strongly influenced later developments from works that predominantly discuss the current state of the art with a degree of accuracy (63%, i.e. 10% over the random baseline). In all setups, Mendeley reader counts perform worse than a random baseline.
Abstract Family-based Model Checking using Modal Featured Transition Systems: Preservation of CTL* (Extended Version)
Venue: arXiv cs.LO 2018
Year: 2018

Variational systems allow effective building of many custom variants by using features (configuration options) to mark the variable functionality. In many of the applications, their quality assurance and formal verification are of paramount importance. Family-based model checking allows simultaneous verification of all variants of a variational system in a single run by exploiting the commonalities between the variants. Yet, its computational cost still greatly depends on the number of variants (often huge). In this work, we show how to achieve efficient family-based model checking of CTL* temporal properties using variability abstractions and off-the-shelf (single-system) tools. We use variability abstractions for deriving abstract family-based model checking, where the variability model of a variational system is replaced with an abstract (smaller) version of it, called modal featured transition system, which preserves the satisfaction of both universal and existential temporal properties, as expressible in CTL*. Modal featured transition systems contain two kinds of transitions, termed may and must transitions, which are defined by the conservative (over-approximating) abstractions and their dual (under-approximating) abstractions, respectively. The variability abstractions can be combined with different partitionings of the set of variants to infer suitable divide-and-conquer verification plans for the variational system. We illustrate the practicality of this approach for several variational systems.
A co-located partitions strategy for parallel CFD-DEM couplings
Venue: arXiv cs.CE 2018
Year: 2018

In this work, a new partition-collocation strategy for the parallel execution of CFD--DEM couplings is investigated. Having a good parallel performance is a key issue for an Eulerian-Lagrangian software that aims to be applied to solve industrially significant problems, as the computational cost of these couplings is one of their main drawback. The approach presented here consists in co-locating the overlapping parts of the simulation domain of each software on the same MPI process, in order to reduce the cost of the data exchanges. It is shown how this strategy allows reducing memory consumption and inter-process communication between CFD and DEM to a minimum and therefore to overcome an important parallelization bottleneck identified in the literature. Three benchmarks are proposed to assess the consistency and scalability of this approach. A coupled execution on 280 cores shows that less than 0.1% of the time is used to perform inter-physics data exchange.
Robust Continuous Co-Clustering
Venue: arXiv cs.LG 2018
Year: 2018

Clustering consists of grouping together samples giving their similar properties. The problem of modeling simultaneously groups of samples and features is known as Co-Clustering. This paper introduces ROCCO - a Robust Continuous Co-Clustering algorithm. ROCCO is a scalable, hyperparameter-free, easy and ready to use algorithm to address Co-Clustering problems in practice over massive cross-domain datasets. It operates by learning a graph-based two-sided representation of the input matrix. The underlying proposed optimization problem is non-convex, which assures a flexible pool of solutions. Moreover, we prove that it can be solved with a near linear time complexity on the input size. An exhaustive large-scale experimental testbed conducted with both synthetic and real-world datasets demonstrates ROCCO's properties in practice: (i) State-of-the-art performance in cross-domain real-world problems including Biomedicine and Text Mining; (ii) very low sensitivity to hyperparameter settings; (iii) robustness to noise and (iv) a linear empirical scalability in practice. These results highlight ROCCO as a powerful general-purpose co-clustering algorithm for cross-domain practitioners, regardless of their technical background.
Do Programmers Work at Night or During the Weekend?
Venue: arXiv cs.SE 2018
Year: 2018

Abnormal working hours can reduce work health, general well-being, and productivity, independent from a profession. To inform future approaches for automatic stress and overload detection, this paper establishes empirically collected measures of the work patterns of software engineers. To this aim, we perform the first large-scale study of software engineers' working hours by investigating the time stamps of commit activities of 86 large open source software projects, both containing hired and volunteer developers. We find that two thirds of software engineers mainly follow typical office hours, empirically established to be from 10h to 18h, and do not usually work during nights and weekends. Large variations between projects and individuals exist. Surprisingly, we found no support that project maturation would decrease abnormal working hours. In the Firefox case study, we found that hired developers work more during office hours while seniority, either in terms of number of commits or job status, did not impact working hours. We conclude that the use of working hours or timestamps of work products for stress detection requires establishing baselines at the level of individuals.
Locomoting robots composed of immobile robots
Venue: arXiv cs.RO 2018
Year: 2018

Robotic materials are multi-robot systems formulated to leverage the low-order computation and actuation of the constituents to manipulate the high-order behavior of the entire material. We study the behaviors of ensembles composed of smart active particles, smarticles. Smarticles are small, low cost robots equipped with basic actuation and sensing abilities that are individually incapable of rotating or displacing. We demonstrate that a "supersmarticle", composed of many smarticles constrained within a bounding membrane, can harness the internal collisions of the robotic material among the constituents and the membrane to achieve diffusive locomotion. The emergent diffusion can be directed by modulating the robotic material properties in response to a light source, analogous to biological phototaxis. The light source introduces asymmetries within the robotic material, resulting in modified populations of interaction modes and dynamics which ultimately result in supersmarticle biased locomotion. We present experimental methods and results for the robotic material which moves with a directed displacement in response to a light source.