OpenRaiser/Intern-Atlas huggingface dataset:
Encodings of Bounded Synthesis
Venue: arXiv cs.LO 2018
Year: 2018

The reactive synthesis problem is to compute a system satisfying a given specification in temporal logic. Bounded synthesis is the approach to bound the maximum size of the system that we accept as a solution to the reactive synthesis problem. As a result, bounded synthesis is decidable whenever the corresponding verification problem is decidable, and can be applied in settings where classic synthesis fails, such as in the synthesis of distributed systems. In this paper, we study the constraint solving problem behind bounded synthesis. We consider different reductions of the bounded synthesis problem of linear-time temporal logic (LTL) to constraint systems given as boolean formulas (SAT), quantified boolean formulas (QBF), and dependency quantified boolean formulas (DQBF). The reductions represent different trade-offs between conciseness and algorithmic efficiency. In the SAT encoding, both inputs and states of the system are represented explicitly; in QBF, inputs are symbolic and states are explicit; in DQBF, both inputs and states are symbolic. We evaluate the encodings systematically using benchmarks from the reactive synthesis competition (SYNTCOMP) and state-of-the-art solvers. Our key, and perhaps surprising, empirical finding is that QBF clearly dominates both SAT and DQBF.
Evaluation of Session-based Recommendation Algorithms
Venue: arXiv cs.IR 2018
Year: 2018

Recommender systems help users find relevant items of interest, for example on e-commerce or media streaming sites. Most academic research is concerned with approaches that personalize the recommendations according to long-term user profiles. In many real-world applications, however, such long-term profiles often do not exist and recommendations therefore have to be made solely based on the observed behavior of a user during an ongoing session. Given the high practical relevance of the problem, an increased interest in this problem can be observed in recent years, leading to a number of proposals for session-based recommendation algorithms that typically aim to predict the user's immediate next actions. In this work, we present the results of an in-depth performance comparison of a number of such algorithms, using a variety of datasets and evaluation measures. Our comparison includes the most recent approaches based on recurrent neural networks like GRU4REC, factorized Markov model approaches such as FISM or FOSSIL, as well as simpler methods based, e.g., on nearest neighbor schemes. Our experiments reveal that algorithms of this latter class, despite their sometimes almost trivial nature, often perform equally well or significantly better than today's more complex approaches based on deep neural networks. Our results therefore suggest that there is substantial room for improvement regarding the development of more sophisticated session-based recommendation algorithms.
Path loss model modification for various gains and directions of antennas
Venue: arXiv cs.IT 2018
Year: 2018

Emerging telecommunication technologies like 5G, green communications, and massive MIMO contribute to the use of directional antennas and beamforming. For this reason, modern propagation models should consider directional antennas with different beam widths, gains and radiation pattern directions. Most of the available propagation models are based on omnidirectional or isotropic antennas. A proposition to solve this problem is an empirical path loss model that considers the different types of antennas. This model assumes that the transmitting and receiving antenna beams are directing each other. In this paper, we propose modifying this model by determining attenuation for any direction of the antenna patterns. For this aim, the multi-elliptic channel model is used.
On the Limitation of Local Intrinsic Dimensionality for Characterizing the Subspaces of Adversarial Examples
Venue: arXiv cs.LG 2018
Year: 2018

Understanding and characterizing the subspaces of adversarial examples aid in studying the robustness of deep neural networks (DNNs) to adversarial perturbations. Very recently, Ma et al. (ICLR 2018) proposed to use local intrinsic dimensionality (LID) in layer-wise hidden representations of DNNs to study adversarial subspaces. It was demonstrated that LID can be used to characterize the adversarial subspaces associated with different attack methods, e.g., the Carlini and Wagner's (C&W) attack and the fast gradient sign attack. In this paper, we use MNIST and CIFAR-10 to conduct two new sets of experiments that are absent in existing LID analysis and report the limitation of LID in characterizing the corresponding adversarial subspaces, which are (i) oblivious attacks and LID analysis using adversarial examples with different confidence levels; and (ii) black-box transfer attacks. For (i), we find that the performance of LID is very sensitive to the confidence parameter deployed by an attack, and the LID learned from ensembles of adversarial examples with varying confidence levels surprisingly gives poor performance. For (ii), we find that when adversarial examples are crafted from another DNN model, LID is ineffective in characterizing their adversarial subspaces. These two findings together suggest the limited capability of LID in characterizing the subspaces of adversarial examples.
Flow From Motion: A Deep Learning Approach
Venue: arXiv cs.LG 2018
Year: 2018

Wearable devices have the potential to enhance sports performance, yet they are not fulfilling this promise. Our previous studies with 6 professional tennis coaches and 20 players indicate that this could be due the lack of psychological or mental state feedback, which the coaches claim to provide. Towards this end, we propose to detect the flow state, mental state of optimal performance, using wearables data to be later used in training. We performed a study with a professional tennis coach and two players. The coach provided labels about the players' flow state while each player had a wearable device on their racket holding wrist. We trained multiple models using the wearables data and the coach labels. Our deep neural network models achieved around 98% testing accuracy for a variety of conditions. This suggests that the flow state or what coaches recognize as flow, can be detected using wearables data in tennis which is a novel result. The implication for the HCI community is that having access to such information would allow for design of novel hardware and interaction paradigms that would be helpful in professional athlete training.
HAMLET: Interpretable Human And Machine co-LEarning Technique
Venue: arXiv cs.AI 2018
Year: 2018

Efficient label acquisition processes are key to obtaining robust classifiers. However, data labeling is often challenging and subject to high levels of label noise. This can arise even when classification targets are well defined, if instances to be labeled are more difficult than the prototypes used to define the class, leading to disagreements among the expert community. Here, we enable efficient training of deep neural networks. From low-confidence labels, we iteratively improve their quality by simultaneous learning of machines and experts. We call it Human And Machine co-LEarning Technique (HAMLET). Throughout the process, experts become more consistent, while the algorithm provides them with explainable feedback for confirmation. HAMLET uses a neural embedding function and a memory module filled with diverse reference embeddings from different classes. Its output includes classification labels and highly relevant reference embeddings as explanation. We took the study of brain monitoring at intensive care unit (ICU) as an application of HAMLET on continuous electroencephalography (cEEG) data. Although cEEG monitoring yields large volumes of data, labeling costs and difficulty make it hard to build a classifier. Additionally, while experts agree on the labels of clear-cut examples of cEEG patterns, labeling many real-world cEEG data can be extremely challenging. Thus, a large minority of sequences might be mislabeled. HAMLET has shown significant performance gain against deep learning and other baselines, increasing accuracy from 7.03% to 68.75% on challenging inputs. Besides improved performance, clinical experts confirmed the interpretability of those reference embeddings in helping explaining the classification results by HAMLET.
On the Runtime Analysis of the Clearing Diversity-Preserving Mechanism
Venue: arXiv cs.NE 2018
Year: 2018

Clearing is a niching method inspired by the principle of assigning the available resources among a niche to a single individual. The clearing procedure supplies these resources only to the best individual of each niche: the winner. So far, its analysis has been focused on experimental approaches that have shown that clearing is a powerful diversity-preserving mechanism. Using rigorous runtime analysis to explain how and why it is a powerful method, we prove that a mutation-based evolutionary algorithm with a large enough population size, and a phenotypic distance function always succeeds in optimising all functions of unitation for small niches in polynomial time, while a genotypic distance function requires exponential time. Finally, we prove that with phenotypic and genotypic distances clearing is able to find both optima for Twomax and several general classes of bimodal functions in polynomial expected time. We use empirical analysis to highlight some of the characteristics that makes it a useful mechanism and to support the theoretical results.
DJAM: distributed Jacobi asynchronous method for learning personal models
Venue: arXiv cs.LG 2018
Year: 2018

Processing data collected by a network of agents often boils down to solving an optimization problem. The distributed nature of these problems calls for methods that are, themselves, distributed. While most collaborative learning problems require agents to reach a common (or consensus) model, there are situations in which the consensus solution may not be optimal. For instance, agents may want to reach a compromise between agreeing with their neighbors and minimizing a personal loss function. We present DJAM, a Jacobi-like distributed algorithm for learning personalized models. This method is implementation-friendly: it has no hyperparameters that need tuning, it is asynchronous, and its updates only require single-neighbor interactions. We prove that DJAM converges with probability one to the solution, provided that the personal loss functions are strongly convex and have Lipschitz gradient. We then give evidence that DJAM is on par with state-of-the-art methods: our method reaches a solution with error similar to the error of a carefully tuned ADMM in about the same number of single-neighbor interactions.
Generating Talking Face Landmarks from Speech
Venue: arXiv cs.CV 2018
Year: 2018

The presence of a corresponding talking face has been shown to significantly improve speech intelligibility in noisy conditions and for hearing impaired population. In this paper, we present a system that can generate landmark points of a talking face from an acoustic speech in real time. The system uses a long short-term memory (LSTM) network and is trained on frontal videos of 27 different speakers with automatically extracted face landmarks. After training, it can produce talking face landmarks from the acoustic speech of unseen speakers and utterances. The training phase contains three key steps. We first transform landmarks of the first video frame to pin the two eye points into two predefined locations and apply the same transformation on all of the following video frames. We then remove the identity information by transforming the landmarks into a mean face shape across the entire training dataset. Finally, we train an LSTM network that takes the first- and second-order temporal differences of the log-mel spectrogram as input to predict face landmarks in each frame. We evaluate our system using the mean-squared error (MSE) loss of landmarks of lips between predicted and ground-truth landmarks as well as their first- and second-order temporal differences. We further evaluate our system by conducting subjective tests, where the subjects try to distinguish the real and fake videos of talking face landmarks. Both tests show promising results.
Crowd-based Multi-Predicate Screening of Papers in Literature Reviews
Venue: arXiv cs.HC 2018
Year: 2018

Systematic literature reviews (SLRs) are one of the most common and useful form of scientific research and publication. Tens of thousands of SLRs are published each year, and this rate is growing across all fields of science. Performing an accurate, complete and unbiased SLR is however a difficult and expensive endeavor. This is true in general for all phases of a literature review, and in particular for the paper screening phase, where authors lter a set of potentially in-scope papers based on a number of exclusion criteria. To address the problem, in recent years the research community has began to explore the use of the crowd to allow for a faster, accurate, cheaper and unbiased screening of papers. Initial results show that crowdsourcing can be effective, even for relatively complex reviews. In this paper we derive and analyze a set of strategies for crowd-based screening, and show that an adaptive strategy, that continuously re-assesses the statistical properties of the problem to minimize the number of votes needed to take decisions for each paper, significantly outperforms a number of non-adaptive approaches in terms of cost and accuracy. We validate both applicability and results of the approach through a set of crowdsourcing experiments, and discuss properties of the problem and algorithms that we believe to be generally of interest for classification problems where items are classified via a series of successive tests (as it often happens in medicine).
Locality-Sensitive Hashing for Earthquake Detection: A Case Study of Scaling Data-Driven Science
Venue: arXiv cs.DB 2018
Year: 2018

In this work, we report on a novel application of Locality Sensitive Hashing (LSH) to seismic data at scale. Based on the high waveform similarity between reoccurring earthquakes, our application identifies potential earthquakes by searching for similar time series segments via LSH. However, a straightforward implementation of this LSH-enabled application has difficulty scaling beyond 3 months of continuous time series data measured at a single seismic station. As a case study of a data-driven science workflow, we illustrate how domain knowledge can be incorporated into the workload to improve both the efficiency and result quality. We describe several end-to-end optimizations of the analysis pipeline from pre-processing to post-processing, which allow the application to scale to time series data measured at multiple seismic stations. Our optimizations enable an over 100$\times$ speedup in the end-to-end analysis pipeline. This improved scalability enabled seismologists to perform seismic analysis on more than ten years of continuous time series data from over ten seismic stations, and has directly enabled the discovery of 597 new earthquakes near the Diablo Canyon nuclear power plant in California and 6123 new earthquakes in New Zealand.
A Conversational Interface to Improve Medication Adherence: Towards AI Support in Patient's Treatment
Venue: arXiv cs.CY 2018
Year: 2018

Medication adherence is of utmost importance for many chronic conditions, regardless of the disease type. Engaging patients in self-tracking their medication is a big challenge. One way to potentially reduce this burden is to use reminders to promote wellness throughout all stages of life and improve medication adherence. Chatbots have proven effectiveness in triggering users to engage in certain activity, such as medication adherence. In this paper, we discuss "Roborto", a chatbot to create an engaging interactive and intelligent environment for patients and assist in positive lifestyle modification. We introduce a way for healthcare providers to track patients adherence and intervene whenever necessary. We describe the health, technical and behavioural approaches to the problem of medication non-adherence and propose a diagnostic and decision support tool. The proposed study will be implemented and validated through a pilot experiment with users to measure the efficacy of the proposed approach.
Directional Modulation: A Secure Solution to 5G and Beyond Mobile Networks
Venue: arXiv cs.IT 2018
Year: 2018

Directional modulation (DM), as an efficient secure transmission way, offers security through its directive property and is suitable for line-of-propagation (LoP) channels such as millimeter wave (mmWave) massive multiple-input multiple-output (MIMO), satellite communication, unmanned aerial vehicle (UAV), and smart transportation. If the direction angle of the desired received is known, the desired channel gain vector is obtainable. Thus, in advance, the DM transmitter knows the values of directional angles of desired user and eavesdropper, or their direction of arrival (DOAs) because the beamforming vector of confidential messages and artificial noise (AN) projection matrix is mainly determined by directional angles of desired user and eavesdropper. For a DM transceiver, working as a receiver, the first step is to measure the DOAs of desired user and eavesdropper. Then, in the second step, using the measured DOAs, the beamforming vector of confidential messages and AN projection matrix is designed. In this paper, we describe the DOA measurement methods, power allocation, and beamforming in DM networks. A machine learning-based DOA measurement method is proposed to make a substantial SR performance gain compared to single-snapshot measurement without machine learning for a given null-space projection beamforming scheme. However, for a conventional DM network, there still exists a serious secure issue: the eavesdropper moves inside the main beam of the desired user and may intercept the confidential messages intended to the desired users because the beamforming vector of confidential messages and AN projection matrix are only angle-dependence. To address this problem, we present a new concept of secure and precise transmission, where the transmit waveform has two-dimensional even three-dimensional dependence by using DM, random frequency selection, and phase alignment at DM transmitter.
Manufacturing processes hardware and software development to implement innovative technologies of aircraft manufacturing facilities management
Venue: arXiv cs.CY 2018
Year: 2018

The paper presents approaches to modern aircraft manufacturing facilities' competitiveness growth based on innovative technologies of management decisions implementation. The paper establishes a connection between the aircraft industry and the development of the national economy, along with the dependence of the Russian economy on international manufacturers of civil airplanes. Comparative statistics of civil aircrafts produced by Russian and international manufacturers are given. Comparative analysis of military and civil aviation is done. It is shown that project implementation based on Open Source and OLAP-technologies at a high-technology enterprise is a pre-requisite for the competitive growth of aircraft manufacturing facilities.
Privacy Things: Systematic Approach to Privacy and Personal Identifiable Information
Venue: arXiv cs.CY 2018
Year: 2018

Defining privacy and related notions such as Personal Identifiable Information (PII) is a central notion in computer science and other fields. The theoretical, technological, and application aspects of PII require a framework that provides an overview and systematic structure for the discipline's topics. This paper develops a foundation for representing information privacy. It introduces a coherent conceptualization of the privacy senses built upon diagrammatic representation. A new framework is presented based on a flow-based model that includes generic operations performed on PII.
A Fast Face Detection Method via Convolutional Neural Network
Venue: arXiv cs.CV 2018
Year: 2018

Current face or object detection methods via convolutional neural network (such as OverFeat, R-CNN and DenseNet) explicitly extract multi-scale features based on an image pyramid. However, such a strategy increases the computational burden for face detection. In this paper, we propose a fast face detection method based on discriminative complete features (DCFs) extracted by an elaborately designed convolutional neural network, where face detection is directly performed on the complete feature maps. DCFs have shown the ability of scale invariance, which is beneficial for face detection with high speed and promising performance. Therefore, extracting multi-scale features on an image pyramid employed in the conventional methods is not required in the proposed method, which can greatly improve its efficiency for face detection. Experimental results on several popular face detection datasets show the efficiency and the effectiveness of the proposed method for face detection.
Facets of Software Doping
Venue: arXiv cs.LO 2018
Year: 2018

This paper provides an informal discussion of the formal aspects of software doping.
Guidelines Towards Better Participation of Older Adults in Software Development Processes using a new SPIRAL Method and Participatory Approach
Venue: arXiv cs.SE 2018
Year: 2018

This paper presents a new method of engaging older participants in the process of application and IT solutions development for older adults for emerging IT and tech startups. A new method called SPIRAL (Support for Participant Involvement in Rapid and Agile software development Labs) is proposed which adds both sustainability and flexibility to the development process with older adults. This method is based on the participatory approach and user empowerment of older adults with the aid of a bootstrapped Living Lab concept and it goes beyond well established user-centered and empathic design. SPIRAL provides strategies for direct involvement of older participants in the software development processes from the very early stage to support the agile approach with rapid prototyping, in particular in new and emerging startup environments with limited capabilities, including time, team and resources.