OpenRaiser/Intern-Atlas huggingface dataset:
Generating Discriminative Object Proposals via Submodular Ranking
Venue: arXiv cs.CV 2016
Year: 2016

A multi-scale greedy-based object proposal generation approach is presented. Based on the multi-scale nature of objects in images, our approach is built on top of a hierarchical segmentation. We first identify the representative and diverse exemplar clusters within each scale by using a diversity ranking algorithm. Object proposals are obtained by selecting a subset from the multi-scale segment pool via maximizing a submodular objective function, which consists of a weighted coverage term, a single-scale diversity term and a multi-scale reward term. The weighted coverage term forces the selected set of object proposals to be representative and compact; the single-scale diversity term encourages choosing segments from different exemplar clusters so that they will cover as many object patterns as possible; the multi-scale reward term encourages the selected proposals to be discriminative and selected from multiple layers generated by the hierarchical image segmentation. The experimental results on the Berkeley Segmentation Dataset and PASCAL VOC2012 segmentation dataset demonstrate the accuracy and efficiency of our object proposal model. Additionally, we validate our object proposals in simultaneous segmentation and detection and outperform the state-of-art performance.
Reversible Communicating Processes
Venue: arXiv cs.PL 2016
Year: 2016

Reversible distributed programs have the ability to abort unproductive computation paths and backtrack, while unwinding communication that occurred in the aborted paths. While it is natural to assume that reversibility implies full state recovery (as with traditional roll-back recovery protocols), an interesting alternative is to separate backtracking from local state recovery. For example, such a model could be used to create complex transactions out of nested compensable transactions where a programmer-supplied compensation defines the work required to "unwind" a transaction. Reversible distributed computing has received considerable theoretical attention, but little reduction to practice; the few published implementations of languages supporting reversibility depend upon a high degree of central control. The objective of this paper is to demonstrate that a practical reversible distributed language can be efficiently implemented in a fully distributed manner. We discuss such a language, supporting CSP-style synchronous communication, embedded in Scala. While this language provided the motivation for the work described in this paper, our focus is upon the distributed implementation. In particular, we demonstrate that a "high-level" semantic model can be implemented using a simple point-to-point protocol.
Communicating machines as a dynamic binding mechanism of services
Venue: arXiv cs.LO 2016
Year: 2016

Distributed software is becoming more and more dynamic to support applications able to respond and adapt to the changes of their execution environment. For instance, service-oriented computing (SOC) envisages applications as services running over globally available computational resources where discovery and binding between them is transparently performed by a middleware. Asynchronous Relational Networks (ARNs) is a well-known formal orchestration model, based on hypergraphs, for the description of service-oriented software artefacts. Choreography and orchestration are the two main design principles for the development of distributed software. In this work, we propose Communicating Relational Networks (CRNs), which is a variant of ARNs, but relies on choreographies for the characterisation of the communicational aspects of a software artefact, and for making their automated analysis more efficient.
Wireless Communications with Unmanned Aerial Vehicles: Opportunities and Challenges
Venue: arXiv cs.IT 2016
Year: 2016

Wireless communication systems that include unmanned aerial vehicles (UAVs) promise to provide cost-effective wireless connectivity for devices without infrastructure coverage. Compared to terrestrial communications or those based on high-altitude platforms (HAPs), on-demand wireless systems with low-altitude UAVs are in general faster to deploy, more flexibly re-configured, and are likely to have better communication channels due to the presence of short-range line-of-sight (LoS) links. However, the utilization of highly mobile and energy-constrained UAVs for wireless communications also introduces many new challenges. In this article, we provide an overview of UAV-aided wireless communications, by introducing the basic networking architecture and main channel characteristics, highlighting the key design considerations as well as the new opportunities to be exploited.
Impact of LOS/NLOS Propagation and Path Loss in Ultra-Dense Cellular Networks
Venue: arXiv cs.IT 2016
Year: 2016

Most prior work on performance analysis of ultra-dense cellular networks (UDNs) has considered standard power-law path loss models and non-line-of-sight (NLOS) propagation modeled by Rayleigh fading. The effect of line-of-sight (LOS) on coverage and throughput and its implication on network densification are still not fully understood. In this paper, we investigate the performance of UDNs when the signal propagation includes both LOS and NLOS components. Using a stochastic geometry based cellular network model, we derive expressions for the coverage probability, as well as tight approximations and upper bounds for both closest and strongest base station (BS) association. Our results show that under standard singular path loss model, LOS propagation increases the coverage, especially with nearest BS association. On the contrary, using dual slope path loss, LOS propagation is beneficial with closest BS association and detrimental for strongest BS association.
Analytic Methods to Calculate Fault Trees with Loops - Restrictions of Application and Solution Uniqueness
Venue: arXiv cs.SE 2016
Year: 2016

One of the important tasks of the Reliability Estimation is Analysis of the Fault Tree. A problem of Fault Trees analysis is considered one of the most complex ones, since structure of such trees is characterized by a considerable number of interconnections. Usually analytical methods are used and most applicable method is Minimal Cut Sets building and calculation. Classical Fault Tree Analysis methods are applicable only for Fault Trees without loops. Loops can appear in Fault Tree, when a TOP or some intermediate gates appear as input to another gate at a lower level of the model. An occurrence of a Loop has been a problematic issue in a Fault Tree calculation. The article relates to the uniqueness of the solution for the Fault Trees with arbitrary Loops. There are assumed, that failures of the Basic Events are non-repairable and Fault Tree gates may be expressed by two main logic gates.
A Versatile Scene Model with Differentiable Visibility Applied to Generative Pose Estimation
Venue: arXiv cs.CV 2016
Year: 2016

Generative reconstruction methods compute the 3D configuration (such as pose and/or geometry) of a shape by optimizing the overlap of the projected 3D shape model with images. Proper handling of occlusions is a big challenge, since the visibility function that indicates if a surface point is seen from a camera can often not be formulated in closed form, and is in general discrete and non-differentiable at occlusion boundaries. We present a new scene representation that enables an analytically differentiable closed-form formulation of surface visibility. In contrast to previous methods, this yields smooth, analytically differentiable, and efficient to optimize pose similarity energies with rigorous occlusion handling, fewer local minima, and experimentally verified improved convergence of numerical optimization. The underlying idea is a new image formation model that represents opaque objects by a translucent medium with a smooth Gaussian density distribution which turns visibility into a smooth phenomenon. We demonstrate the advantages of our versatile scene model in several generative pose estimation problems, namely marker-less multi-object pose estimation, marker-less human motion capture with few cameras, and image-based 3D geometry estimation.
Human Machine Epistemology Survey
Venue: arXiv cs.HC 2016
Year: 2016

Pluridisciplinar convergence is a major problem that had emerged with Human-Artefact Systems and so-called " Augmented Humanity " as academical fields and even more as technical fields. Problems come mainly from the juxtaposition of two very different types of system, a biological one and an artificial one. Thus, conceiving and designing the multiple couplings between them has become a major difficulty. Some came with reductionnist solutions to answer these problems but since we know that a biological system and a technical system are different, this approach is limited from its beginning. Using a specifically designed questionnaire and statistical analysis we determined how specialists (medical practitioners, ergonomists and engineers) in the domain conceive themselves what is a Human-Artifact System and how they relate to existent traditions and showed that some of them relate to the integrativist views.
Enabling Basic Normative HRI in a Cognitive Robotic Architecture
Venue: arXiv cs.RO 2016
Year: 2016

Collaborative human activities are grounded in social and moral norms, which humans consciously and subconsciously use to guide and constrain their decision-making and behavior, thereby strengthening their interactions and preventing emotional and physical harm. This type of norm-based processing is also critical for robots in many human-robot interaction scenarios (e.g., when helping elderly and disabled persons in assisted living facilities, or assisting humans in assembly tasks in factories or even the space station). In this position paper, we will briefly describe how several components in an integrated cognitive architecture can be used to implement processes that are required for normative human-robot interactions, especially in collaborative tasks where actions and situations could potentially be perceived as threatening and thus need a change in course of action to mitigate the perceived threats.
Climate Change Research in View of Bibliometrics
Venue: arXiv cs.DL 2016
Year: 2016

This bibliometric study of a large publication set dealing with research on climate change aims at mapping the relevant literature from a bibliometric perspective and presents a multitude of quantitative data: (1) The growth of the overall publication output as well as (2) of some major subfields, (3) the contributing journals and countries as well as their citation impact, and (4) a title word analysis aiming to illustrate the time evolution and relative importance of specific research topics. The study is based on 222,060 papers published between 1980 and 2014. The total number of papers shows a strong increase with a doubling every 5-6 years. Continental biomass related research is the major subfield, closely followed by climate modeling. Research dealing with adaptation, mitigation, risks, and vulnerability of global warming is comparatively small, but their share of papers increased exponentially since 2005. Research on vulnerability and on adaptation published the largest proportion of very important papers. Research on climate change is quantitatively dominated by the USA, followed by the UK, Germany, and Canada. The citation-based indicators exhibit consistently that the UK has produced the largest proportion of high impact papers compared to the other countries (having published more than 10,000 papers). The title word analysis shows that the term climate change comes forward with time. Furthermore, the term impact arises and points to research dealing with the various effects of climate change. Finally, the term model and related terms prominently appear independent of time, indicating the high relevance of climate modeling.
Face Attribute Prediction Using Off-the-Shelf CNN Features
Venue: arXiv cs.CV 2016
Year: 2016

Predicting attributes from face images in the wild is a challenging computer vision problem. To automatically describe face attributes from face containing images, traditionally one needs to cascade three technical blocks --- face localization, facial descriptor construction, and attribute classification --- in a pipeline. As a typical classification problem, face attribute prediction has been addressed using deep learning. Current state-of-the-art performance was achieved by using two cascaded Convolutional Neural Networks (CNNs), which were specifically trained to learn face localization and attribute description. In this paper, we experiment with an alternative way of employing the power of deep representations from CNNs. Combining with conventional face localization techniques, we use off-the-shelf architectures trained for face recognition to build facial descriptors. Recognizing that the describable face attributes are diverse, our face descriptors are constructed from different levels of the CNNs for different attributes to best facilitate face attribute prediction. Experiments on two large datasets, LFWA and CelebA, show that our approach is entirely comparable to the state-of-the-art. Our findings not only demonstrate an efficient face attribute prediction approach, but also raise an important question: how to leverage the power of off-the-shelf CNN representations for novel tasks.
Opportunistic Detection Rules: Finite and Asymptotic Analysis
Venue: arXiv cs.IT 2016
Year: 2016

Opportunistic detection rules (ODRs) are variants of fixed-sample-size detection rules in which the statistician is allowed to make an early decision on the alternative hypothesis opportunistically based on the sequentially observed samples. From a sequential decision perspective, ODRs are also mixtures of one-sided and truncated sequential detection rules. Several results regarding ODRs are established in this paper. In the finite regime, the maximum sample size is modeled either as a fixed finite number, or a geometric random variable with a fixed finite mean. For both cases, the corresponding Bayesian formulations are investigated. The former case is a slight variation of the well-known finite-length sequential hypothesis testing procedure in the literature, whereas the latter case is new, for which the Bayesian optimal ODR is shown to be a sequence of likelihood ratio threshold tests with two different thresholds: a running threshold, which is determined by solving a stationary state equation, is used when future samples are still available, and a terminal threshold (simply the ratio between the priors scaled by costs) is used when the statistician reaches the final sample and thus has to make a decision immediately. In the asymptotic regime, the tradeoff among the exponents of the (false alarm and miss) error probabilities and the normalized expected stopping time under the alternative hypothesis is completely characterized and proved to be tight, via an information-theoretic argument. Within the tradeoff region, one noteworthy fact is that the performance of the Stein-Chernoff Lemma is attainable by ODRs.
An automatic method for segmentation of fission tracks in epidote crystal photomicrographs
Venue: arXiv cs.CV 2016
Year: 2016

Manual identification of fission tracks has practical problems, such as variation due to observer-observation efficiency. An automatic processing method that could identify fission tracks in a photomicrograph could solve this problem and improve the speed of track counting. However, separation of non-trivial images is one of the most difficult tasks in image processing. Several commercial and free softwares are available, but these softwares are meant to be used in specific images. In this paper, an automatic method based on starlet wavelets is presented in order to separate fission tracks in mineral photomicrographs. Automatization is obtained by Matthews correlation coefficient, and results are evaluated by precision, recall and accuracy. This technique is an improvement of a method aimed at segmentation of scanning electron microscopy images. This method is applied in photomicrographs of epidote phenocrystals, in which accuracy higher than 89% was obtained in fission track segmentation, even for difficult images. Algorithms corresponding to the proposed method are available for download. Using the method presented here, an user could easily determine fission tracks in photomicrographs of mineral samples.
On Scaling Rules for Energy of VLSI Polar Encoders and Decoders
Venue: arXiv cs.IT 2016
Year: 2016

It is shown that all polar encoding schemes of rate $R>\frac{1}{2}$ of block length $N$ implemented according to the Thompson VLSI model must take energy $E\geΩ\left(N^{3/2}\right)$. This lower bound is achievable up to polylogarithmic factors using a mesh network topology defined by Thompson and the encoding algorithm defined by Arikan. A general class of circuits that compute successive cancellation decoding adapted from Arikan's butterfly network algorithm is defined. It is shown that such decoders implemented on a rectangle grid for codes of rate $R>2/3$ must take energy $E\geΩ(N^{3/2})$, and this can also be reached up to polylogarithmic factors using a mesh network. Capacity approaching sequences of energy optimal polar encoders and decoders, as a function of reciprocal gap to capacity $χ= (1-R/C)^{-1}$, have energy that scales as $Ω\left(χ^{5.325}\right)\le E \le O\left(χ^{7.05}\log^{4}\left(χ\right)\right)$.
Game-theoretic Interpretation of Type Theory Part II: Uniqueness of Identity Proofs and Univalence
Venue: arXiv cs.LO 2016
Year: 2016

In the present paper, based on the previous work (Part I), we present a game semantics for the intensional variant of intuitionistic type theory that refutes the principle of uniqueness of identity proofs and validates the univalence axiom, though we do not interpret non-trivial higher propositional equalities. Specifically, following the historic groupoid interpretation by Hofmann and Streicher, we equip predicative games in Part I with a groupoid structure, which gives rise to the notion of (predicative) gamoids. Roughly, gamoids are "games with (computational) equalities specified", which interpret subtleties in Id-types. We then formulate a category with families of predicative gamoids, equipped with dependent product, dependent sum, and Id-types as well as universes, which forms a concrete instance of the groupoid model. We believe that this work is an important stepping-stone towards a complete interpretation of homotopy type theory.
Dark Memory and Accelerator-Rich System Optimization in the Dark Silicon Era
Venue: arXiv cs.AR 2016
Year: 2016

The key challenge to improving performance in the age of Dark Silicon is how to leverage transistors when they cannot all be used at the same time. In modern SOCs, these transistors are often used to create specialized accelerators which improve energy efficiency for some applications by 10-1000X. While this might seem like the magic bullet we need, for most CPU applications more energy is dissipated in the memory system than in the processor: these large gains in efficiency are only possible if the DRAM and memory hierarchy are mostly idle. We refer to this desirable state as Dark Memory, and it only occurs for applications with an extreme form of locality. To show our findings, we introduce Pareto curves in the energy/op and mm$^2$/(ops/s) metric space for compute units, accelerators, and on-chip memory/interconnect. These Pareto curves allow us to solve the power, performance, area constrained optimization problem to determine which accelerators should be used, and how to set their design parameters to optimize the system. This analysis shows that memory accesses create a floor to the achievable energy-per-op. Thus high performance requires Dark Memory, which in turn requires co-design of the algorithm for parallelism and locality, with the hardware.
Fundamental Limits of Cache-Aided Interference Management
Venue: arXiv cs.IT 2016
Year: 2016

We consider a system comprising a library of $N$ files (e.g., movies) and a wireless network with $K_T$ transmitters, each equipped with a local cache of size of $M_T$ files, and $K_R$ receivers, each equipped with a local cache of size of $M_R$ files. Each receiver will ask for one of the $N$ files in the library, which needs to be delivered. The objective is to design the cache placement (without prior knowledge of receivers' future requests) and the communication scheme to maximize the throughput of the delivery. In this setting, we show that the sum degrees-of-freedom (sum-DoF) of $\min\left\{\frac{K_T M_T+K_R M_R}{N},K_R\right\}$ is achievable, and this is within a factor of 2 of the optimum, under one-shot linear schemes. This result shows that (i) the one-shot sum-DoF scales linearly with the aggregate cache size in the network (i.e., the cumulative memory available at all nodes), (ii) the transmitters' and receivers' caches contribute equally in the one-shot sum-DoF, and (iii) caching can offer a throughput gain that scales linearly with the size of the network. To prove the result, we propose an achievable scheme that exploits the redundancy of the content at transmitters' caches to cooperatively zero-force some outgoing interference and availability of the unintended content at receivers' caches to cancel (subtract) some of the incoming interference. We develop a particular pattern for cache placement that maximizes the overall gains of cache-aided transmit and receive interference cancellations. For the converse, we present an integer optimization problem which minimizes the number of communication blocks needed to deliver any set of requested files to the receivers. We then provide a lower bound on the value of this optimization problem, hence leading to an upper bound on the linear one-shot sum-DoF of the network, which is within a factor of 2 of the achievable sum-DoF.
Mathematical Theory Exploration in Theorema: Reduction Rings
Venue: arXiv cs.SC 2016
Year: 2016

In this paper we present the first-ever computer formalization of the theory of Gröbner bases in reduction rings, which is an important theory in computational commutative algebra, in Theorema. Not only the formalization, but also the formal verification of all results has already been fully completed by now; this, in particular, includes the generic implementation and correctness proof of Buchberger's algorithm in reduction rings. Thanks to the seamless integration of proving and computing in Theorema, this implementation can now be used to compute Gröbner bases in various different domains directly within the system. Moreover, a substantial part of our formalization is made up solely by "elementary theories" such as sets, numbers and tuples that are themselves independent of reduction rings and may therefore be used as the foundations of future theory explorations in Theorema. In addition, we also report on two general-purpose Theorema tools we developed for an efficient and convenient exploration of mathematical theories: an interactive proving strategy and a "theory analyzer" that already proved extremely useful when creating large structured knowledge bases.