OpenRaiser/Intern-Atlas huggingface dataset:
Developing a cardiovascular disease risk factor annotated corpus of Chinese electronic medical records
Venue: arXiv cs.CL 2017
Year: 2017

Cardiovascular disease (CVD) has become the leading cause of death in China, and most of the cases can be prevented by controlling risk factors. The goal of this study was to build a corpus of CVD risk factor annotations based on Chinese electronic medical records (CEMRs). This corpus is intended to be used to develop a risk factor information extraction system that, in turn, can be applied as a foundation for the further study of the progress of risk factors and CVD. We designed a light annotation task to capture CVD risk factors with indicators, temporal attributes and assertions that were explicitly or implicitly displayed in the records. The task included: 1) preparing data; 2) creating guidelines for capturing annotations (these were created with the help of clinicians); 3) proposing an annotation method including building the guidelines draft, training the annotators and updating the guidelines, and corpus construction. Then, a risk factor annotated corpus based on de-identified discharge summaries and progress notes from 600 patients was developed. Built with the help of clinicians, this corpus has an inter-annotator agreement (IAA) F1-measure of 0.968, indicating a high reliability. To the best of our knowledge, this is the first annotated corpus concerning CVD risk factors in CEMRs and the guidelines for capturing CVD risk factor annotations from CEMRs were proposed. The obtained document-level annotations can be applied in future studies to monitor risk factors and CVD over the long term.
Dynamic Choreographies: Theory And Implementation
Venue: arXiv cs.PL 2017
Year: 2017

Programming distributed applications free from communication deadlocks and race conditions is complex. Preserving these properties when applications are updated at runtime is even harder. We present a choreographic approach for programming updatable, distributed applications. We define a choreography language, called Dynamic Interaction-Oriented Choreography (AIOC), that allows the programmer to specify, from a global viewpoint, which parts of the application can be updated. At runtime, these parts may be replaced by new AIOC fragments from outside the application. AIOC programs are compiled, generating code for each participant in a process-level language called Dynamic Process-Oriented Choreographies (APOC). We prove that APOC distributed applications generated from AIOC specifications are deadlock free and race free and that these properties hold also after any runtime update. We instantiate the theoretical model above into a programming framework called Adaptable Interaction-Oriented Choreographies in Jolie (AIOCJ) that comprises an integrated development environment, a compiler from an extension of AIOCs to distributed Jolie programs, and a runtime environment to support their execution.
Correctness Attraction: A Study of Stability of Software Behavior Under Runtime Perturbation
Venue: arXiv cs.SE 2017
Year: 2017

Can the execution of a software be perturbed without breaking the correctness of the output? In this paper, we devise a novel protocol to answer this rarely investigated question. In an experimental study, we observe that many perturbations do not break the correctness in ten subject programs. We call this phenomenon ``correctness attraction''. The uniqueness of this protocol is that it considers a systematic exploration of the perturbation space as well as perfect oracles to determine the correctness of the output. To this extent, our findings on the stability of software under execution perturbations have a level of validity that has never been reported before in the scarce related work. A qualitative manual analysis enables us to set up the first taxonomy ever of the reasons behind correctness attraction.
Linear vs Nonlinear MPC for Trajectory Tracking Applied to Rotary Wing Micro Aerial Vehicles
Venue: arXiv cs.RO 2017
Year: 2017

Precise trajectory tracking is a crucial property for \acp{MAV} to operate in cluttered environment or under disturbances. In this paper we present a detailed comparison between two state-of-the-art model-based control techniques for \ac{MAV} trajectory tracking. A classical \ac{LMPC} is presented and compared against a more advanced \ac{NMPC} that considers the full system model. In a careful analysis we show the advantages and disadvantages of the two implementations in terms of speed and tracking performance. This is achieved by evaluating hovering performance, step response, and aggressive trajectory tracking under nominal conditions and under external wind disturbances.
Guarded Cubical Type Theory
Venue: arXiv cs.LO 2017
Year: 2017

This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Löf type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory (GCTT), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that CTT can be given semantics in presheaves on the product of the cube category and a small category with an initial object. We then show that the category of presheaves on the product of the cube category and omega provides semantics for GCTT.
NewsQA: A Machine Comprehension Dataset
Venue: arXiv cs.CL 2017
Year: 2017

We present NewsQA, a challenging machine comprehension dataset of over 100,000 human-generated question-answer pairs. Crowdworkers supply questions and answers based on a set of over 10,000 news articles from CNN, with answers consisting of spans of text from the corresponding articles. We collect this dataset through a four-stage process designed to solicit exploratory questions that require reasoning. A thorough analysis confirms that NewsQA demands abilities beyond simple word matching and recognizing textual entailment. We measure human performance on the dataset and compare it to several strong neural models. The performance gap between humans and machines (0.198 in F1) indicates that significant progress can be made on NewsQA through future research. The dataset is freely available at https://datasets.maluuba.com/NewsQA.
On rank-width of even-hole-free graphs
Venue: arXiv cs.DM 2017
Year: 2017

We present a class of (diamond, even hole)-free graphs with no clique cutset that has unbounded rank-width. In general, even-hole-free graphs have unbounded rank-width, because chordal graphs are even-hole-free. A.A. da Silva, A. Silva and C. Linhares-Sales (2010) showed that planar even-hole-free graphs have bounded rank-width, and N.K. Le (2016) showed that even-hole-free graphs with no star cutset have bounded rank-width. A natural question is to ask, whether even-hole-free graphs with no clique cutsets have bounded rank-width. Our result gives a negative answer. Hence we cannot apply Courcelle and Makowsky's meta-theorem which would provide efficient algorithms for a large number of problems, including the maximum independent set problem, whose complexity remains open for (diamond, even hole)-free graphs.
ADMM-based Fast Algorithm for Multi-group Multicast Beamforming in Large-Scale Wireless Systems
Venue: arXiv cs.IT 2017
Year: 2017

Multi-group multicast beamforming in wireless systems with large antenna arrays and massive audience is investigated in this paper. Multicast beamforming design is a well-known non-convex quadratically constrained quadratic programming (QCQP) problem. A conventional method to tackle this problem is to approximate it as a semi-definite programming problem via semi-definite relaxation, whose performance, however, deteriorates considerably as the number of per-group users goes large. A recent attempt is to apply convex-concave procedure (CCP) to find a stationary solution by treating it as a difference of convex programming problem, whose complexity, however, increases dramatically as the problem size increases. In this paper, we propose a low-complexity high-performance algorithm for multi-group multicast beamforming design in large-scale wireless systems by leveraging the alternating direction method of multipliers (ADMM) together with CCP. In specific, the original non-convex QCQP problem is first approximated as a sequence of convex subproblems via CCP. Each convex subproblem is then reformulated as a novel ADMM form. Our ADMM reformulation enables that each updating step is performed by solving multiple small-size subproblems with closed-form solutions in parallel. Numerical results show that our fast algorithm maintains the same favorable performance as state-of-the-art algorithms but reduces the complexity by orders of magnitude.
Sync-DRAW: Automatic Video Generation using Deep Recurrent Attentive Architectures
Venue: arXiv cs.CV 2017
Year: 2017

This paper introduces a novel approach for generating videos called Synchronized Deep Recurrent Attentive Writer (Sync-DRAW). Sync-DRAW can also perform text-to-video generation which, to the best of our knowledge, makes it the first approach of its kind. It combines a Variational Autoencoder~(VAE) with a Recurrent Attention Mechanism in a novel manner to create a temporally dependent sequence of frames that are gradually formed over time. The recurrent attention mechanism in Sync-DRAW attends to each individual frame of the video in sychronization, while the VAE learns a latent distribution for the entire video at the global level. Our experiments with Bouncing MNIST, KTH and UCF-101 suggest that Sync-DRAW is efficient in learning the spatial and temporal information of the videos and generates frames with high structural integrity, and can generate videos from simple captions on these datasets. (Accepted as oral paper in ACM-Multimedia 2017)
Computer Assisted Composition with Recurrent Neural Networks
Venue: arXiv cs.AI 2017
Year: 2017

Sequence modeling with neural networks has lead to powerful models of symbolic music data. We address the problem of exploiting these models to reach creative musical goals, by combining with human input. To this end we generalise previous work, which sampled Markovian sequence models under the constraint that the sequence belong to the language of a given finite state machine provided by the human. We consider more expressive non-Markov models, thereby requiring approximate sampling which we provide in the form of an efficient sequential Monte Carlo method. In addition we provide and compare with a beam search strategy for conditional probability maximisation. Our algorithms are capable of convincingly re-harmonising famous musical works. To demonstrate this we provide visualisations, quantitative experiments, a human listening test and audio examples. We find both the sampling and optimisation procedures to be effective, yet complementary in character. For the case of highly permissive constraint sets, we find that sampling is to be preferred due to the overly regular nature of the optimisation based results. The generality of our algorithms permits countless other creative applications.
Secure Polar Coding for the Two-Way Wiretap Channel
Venue: arXiv cs.IT 2017
Year: 2017

We consider the problem of polar coding for secure communications over the two-way wiretap channel, where two legitimate users communicate with each other simultaneously while a passive eavesdropper overhears a combination of their exchanged signals. The legitimate users wish to design a cooperative jamming code such that the interference between their codewords can jam the eavesdropper. In this paper, we design a polar coded cooperative jamming scheme that achieves the whole secrecy rate region of the general two-way wiretap channel under the strong secrecy criterion. The chaining method is used to make proper alignment of polar indices. The randomness required to be shared between two legitimate users is treated as a limited resource and we show that its rate can be made negligible by increasing the blocklength and the number of chained blocks. For the special case when the eavesdropper channel is degraded with respect to the legitimate ones, a simplified scheme is proposed which can simultaneously ensure reliability and weak secrecy within a single transmission block. An example of the binary erasure channel case is given to demonstrate the performance of our scheme.
CDVAE: Co-embedding Deep Variational Auto Encoder for Conditional Variational Generation
Venue: arXiv cs.CV 2017
Year: 2017

Problems such as predicting a new shading field (Y) for an image (X) are ambiguous: many very distinct solutions are good. Representing this ambiguity requires building a conditional model P(Y|X) of the prediction, conditioned on the image. Such a model is difficult to train, because we do not usually have training data containing many different shadings for the same image. As a result, we need different training examples to share data to produce good models. This presents a danger we call "code space collapse" - the training procedure produces a model that has a very good loss score, but which represents the conditional distribution poorly. We demonstrate an improved method for building conditional models by exploiting a metric constraint on training data that prevents code space collapse. We demonstrate our model on two example tasks using real data: image saturation adjustment, image relighting. We describe quantitative metrics to evaluate ambiguous generation results. Our results quantitatively and qualitatively outperform different strong baselines.
Fully Convolutional Crowd Counting On Highly Congested Scenes
Venue: arXiv cs.CV 2017
Year: 2017

In this paper we advance the state-of-the-art for crowd counting in high density scenes by further exploring the idea of a fully convolutional crowd counting model introduced by (Zhang et al., 2016). Producing an accurate and robust crowd count estimator using computer vision techniques has attracted significant research interest in recent years. Applications for crowd counting systems exist in many diverse areas including city planning, retail, and of course general public safety. Developing a highly generalised counting model that can be deployed in any surveillance scenario with any camera perspective is the key objective for research in this area. Techniques developed in the past have generally performed poorly in highly congested scenes with several thousands of people in frame (Rodriguez et al., 2011). Our approach, influenced by the work of (Zhang et al., 2016), consists of the following contributions: (1) A training set augmentation scheme that minimises redundancy among training samples to improve model generalisation and overall counting performance; (2) a deep, single column, fully convolutional network (FCN) architecture; (3) a multi-scale averaging step during inference. The developed technique can analyse images of any resolution or aspect ratio and achieves state-of-the-art counting performance on the Shanghaitech Part B and UCF CC 50 datasets as well as competitive performance on Shanghaitech Part A.
Software-Defined Silicon Photonics based Metro Node for Spatial and Wavelength Superchannel Switching
Venue: arXiv cs.NI 2017
Year: 2017

Due to the growing popularity of optical superchannels and software defined networking, reconfigurable optical add-drop multiplexer (ROADM) architectures for superchannel switching have recently attracted significant attention. ROADMs based on micro electro-mechanical system (MEMS) and liquid crystal-on-silicon (LCoS) technologies are predominantly used. Motivated by requirements for low power, high-speed, small area footprint and compact switching solutions, we propose and demonstrate spatial and wavelength flexible superchannel switching using monolithically integrated silicon photonics (SiP) micro-ring resonators (MRR). We demonstrate the MRRs capabilities and potential to be used as a fundamental building block in ROADMs. Unicast and multicast switching operation of an entire superchannel is demonstrated after transmission over 50 km of standard single mode fiber. The performance of each sub-channel from the 120 Gb/s QPSK Nyquist superchannel is analyzed and degradation in error vector magnitude performance was observed for outer sub-channels due to the 3-dB bandwidth of the MRRs, which is comparable with the superchannel bandwidth. However, all sub-channels for all switching cases (unicast, multicast and bi-directional operation) exhibit performance far below the 7% FEC limit. The switching time of the SiP MRR chip is such that high capacity superchannel interconnects between users can be setup and reconfigured on the microsecond timescale.
A Theoretical Framework for Robustness of (Deep) Classifiers against Adversarial Examples
Venue: arXiv cs.LG 2017
Year: 2017

Most machine learning classifiers, including deep neural networks, are vulnerable to adversarial examples. Such inputs are typically generated by adding small but purposeful modifications that lead to incorrect outputs while imperceptible to human eyes. The goal of this paper is not to introduce a single method, but to make theoretical steps towards fully understanding adversarial examples. By using concepts from topology, our theoretical analysis brings forth the key reasons why an adversarial example can fool a classifier ($f_1$) and adds its oracle ($f_2$, like human eyes) in such analysis. By investigating the topological relationship between two (pseudo)metric spaces corresponding to predictor $f_1$ and oracle $f_2$, we develop necessary and sufficient conditions that can determine if $f_1$ is always robust (strong-robust) against adversarial examples according to $f_2$. Interestingly our theorems indicate that just one unnecessary feature can make $f_1$ not strong-robust, and the right feature representation learning is the key to getting a classifier that is both accurate and strong-robust.
Large-scale Validation of Counterfactual Learning Methods: A Test-Bed
Venue: arXiv cs.LG 2017
Year: 2017

The ability to perform effective off-policy learning would revolutionize the process of building better interactive systems, such as search engines and recommendation systems for e-commerce, computational advertising and news. Recent approaches for off-policy evaluation and learning in these settings appear promising. With this paper, we provide real-world data and a standardized test-bed to systematically investigate these algorithms using data from display advertising. In particular, we consider the problem of filling a banner ad with an aggregate of multiple products the user may want to purchase. This paper presents our test-bed, the sanity checks we ran to ensure its validity, and shows results comparing state-of-the-art off-policy learning methods like doubly robust optimization, POEM, and reductions to supervised learning using regression baselines. Our results show experimental evidence that recent off-policy learning methods can improve upon state-of-the-art supervised learning techniques on a large-scale real-world data set.
Alleviating Overfitting for Polysemous Words for Word Representation Estimation Using Lexicons
Venue: arXiv cs.CL 2017
Year: 2017

Though there are some works on improving distributed word representations using lexicons, the improper overfitting of the words that have multiple meanings is a remaining issue deteriorating the learning when lexicons are used, which needs to be solved. An alternative method is to allocate a vector per sense instead of a vector per word. However, the word representations estimated in the former way are not as easy to use as the latter one. Our previous work uses a probabilistic method to alleviate the overfitting, but it is not robust with a small corpus. In this paper, we propose a new neural network to estimate distributed word representations using a lexicon and a corpus. We add a lexicon layer in the continuous bag-of-words model and a threshold node after the output of the lexicon layer. The threshold rejects the unreliable outputs of the lexicon layer that are less likely to be the same with their inputs. In this way, it alleviates the overfitting of the polysemous words. The proposed neural network can be trained using negative sampling, which maximizing the log probabilities of target words given the context words, by distinguishing the target words from random noises. We compare the proposed neural network with the continuous bag-of-words model, the other works improving it, and the previous works estimating distributed word representations using both a lexicon and a corpus. The experimental results show that the proposed neural network is more efficient and balanced for both semantic tasks and syntactic tasks than the previous works, and robust to the size of the corpus.
A new rule for almost-certain termination of probabilistic- and demonic programs
Venue: arXiv cs.LO 2017
Year: 2017

Extending our own and others' earlier approaches to reasoning about termination of probabilistic programs, we propose and prove a new rule for termination with probability one, also known as "almost-certain termination". The rule uses both (non-strict) super martingales and guarantees of progress, together, and it seems to cover significant cases that earlier methods do not. In particular, it suffices for termination of the unbounded symmetric random walk in both one- and two dimensions: for the first, we give a proof; for the second, we use a theorem of Foster to argue that a proof exists. Non-determinism (i.e. demonic choice) is supported; but we do currently restrict to discrete distributions.
Security Analysis of Encrypted Virtual Machines
Venue: arXiv cs.CR 2017
Year: 2017

Cloud computing has become indispensable in today's computer landscape. The flexibility it offers for customers as well as for providers has become a crucial factor for large parts of the computer industry. Virtualization is the key technology that allows for sharing of hardware resources among different customers. The controlling software component, called hypervisor, provides a virtualized view of the computer resources and ensures separation of different guest virtual machines. However, this important cornerstone of cloud computing is not necessarily trustworthy. To mitigate this threat AMD introduced Secure Encrypted Virtualization, short SEV. SEV is a processor extension that encrypts guest memory in order to prevent a potentially malicious hypervisor from accessing guest data. In this paper we analyse whether the proposed features can resist a malicious hypervisor and discuss the trade-offs imposed by additional protection mechanisms. To do so, we developed a model of SEV's security capabilities based on the available documentation as actual silicon implementations are not yet on the market. We found that the currently proposed version of SEV is not up to the task owing to three design shortcomings. First, as with standard AMD-V, under SEV, the virtual machine control block is not encrypted and handled directly by the hypervisor, allowing him to bypass VM memory encryption by executing conveniently chosen gadgets. Secondly, the general purpose registers are not encrypted upon vmexit, leaking potentially sensitive data. Finally, the control of the nested pagetables allows a malicious hypervisor to closely control the execution of a VM and attack it with memory replay attacks.