OpenRaiser/Intern-Atlas huggingface dataset:
Proof Simplification and Automated Theorem Proving
Venue: arXiv cs.LO 2018
Year: 2018

The proofs first generated by automated theorem provers are far from optimal by any measure of simplicity. In this paper I describe a technique for simplifying automated proofs. Hopefully this discussion will stimulate interest in the larger, still open, question of what reasonable measures of proof simplicity might be.
A molecular communications model for drug delivery
Venue: arXiv cs.ET 2018
Year: 2018

This paper considers the scenario of a targeted drug delivery system, which consists of deploying a number of biological nanomachines close to a biological target (e.g. a tumor), able to deliver drug molecules in the diseased area. Suitably located transmitters are designed to release a continuous flow of drug molecules in the surrounding environment, where they diffuse and reach the target. These molecules are received when they chemically react with compliant receptors deployed on the receiver surface. In these conditions, if the release rate is relatively high and the drug absorption time is significant, congestion may happen, essentially at the receiver site. This phenomenon limits the drug absorption rate and makes the signal transmission ineffective, with an undesired diffusion of drug molecules elsewhere in the body. The original contribution of this paper consists of a theoretical analysis of the causes of congestion in diffusion-based molecular communications. For this purpose, it is proposed a reception model consisting of a set of pure loss queuing systems. The proposed model exhibits an excellent agreement with the results of a simulation campaign made by using the Biological and Nano-Scale communication simulator version 2 (BiNS2), a well-known simulator for molecular communications, whose reliability has been assessed through in-vitro experiments. The obtained results can be used in rate control algorithms to optimally determine the optimal release rate of molecules in drug delivery applications.
Eliminating Unstable Tests in Floating-Point Programs
Venue: arXiv cs.PL 2018
Year: 2018

Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-number computation. This problem, which is called test instability, may result in a significant difference between the computation of a floating-point program and the expected output in real arithmetic. In this paper, a formally proven program transformation is proposed to detect and correct the effects of unstable tests. The output of this transformation is a floating-point program that is guaranteed to return either the result of the original floating-point program when it can be assured that both its real and its floating-point flows agree or a warning when these flows may diverge. The proposed approach is illustrated with the transformation of the core computation of a polygon containment algorithm developed at NASA that is used in a geofencing system for unmanned aircraft systems.
Patrolling on Dynamic Ring Networks
Venue: arXiv cs.DC 2018
Year: 2018

We study the problem of patrolling the nodes of a network collaboratively by a team of mobile agents, such that each node of the network is visited by at least one agent once in every $I(n)$ time units, with the objective of minimizing the idle time $I(n)$. While patrolling has been studied previously for static networks, we investigate the problem on dynamic networks with a fixed set of nodes, but dynamic edges. In particular, we consider 1-interval-connected ring networks and provide various patrolling algorithms for such networks, for $k=2$ or $k>2$ agents. We also show almost matching lower bounds that hold even for the best starting configurations. Thus, our algorithms achieve close to optimal idle time. Further, we show a clear separation in terms of idle time, for agents that have prior knowledge of the dynamic networks compared to agents that do not have such knowledge. This paper provides the first known results for collaborative patrolling on dynamic graphs.
What is wrong with style transfer for texts?
Venue: arXiv cs.CL 2018
Year: 2018

A number of recent machine learning papers work with an automated style transfer for texts and, counter to intuition, demonstrate that there is no consensus formulation of this NLP task. Different researchers propose different algorithms, datasets and target metrics to address it. This short opinion paper aims to discuss possible formalization of this NLP task in anticipation of a further growing interest to it.
Micromechanical model for sintering and damage in viscoelastic porous ice and snow. Part I: Theory
Venue: arXiv cs.CE 2018
Year: 2018

Ice and snow have sometime been classified as a viscoelastic or viscoplastic mate- rial according to temperature, strain rate, pressure and time scale. Throughout experimental studies presented in the literature, it has been observed that at very low temperatures or high strain rate, porous ice and snow exhibit brittle behavior, but experience high viscous and plastic flow at temperatures closed to the melting point and low rates. At the macroscopic level nonlinearity is not necessarily attributed to material level permanent changes or yielding but mainly to micro cracks, porosity collapse and crack propagation. This paper attempts to address this complex behavior with a full microstructure based model.
Image Registration and Predictive Modeling: Learning the Metric on the Space of Diffeomorphisms
Venue: arXiv cs.CV 2018
Year: 2018

We present a method for metric optimization in the Large Deformation Diffeomorphic Metric Mapping (LDDMM) framework, by treating the induced Riemannian metric on the space of diffeomorphisms as a kernel in a machine learning context. For simplicity, we choose the kernel Fischer Linear Discriminant Analysis (KLDA) as the framework. Optimizing the kernel parameters in an Expectation-Maximization framework, we define model fidelity via the hinge loss of the decision function. The resulting algorithm optimizes the parameters of the LDDMM norm-inducing differential operator as a solution to a group-wise registration and classification problem. In practice, this may lead to a biology-aware registration, focusing its attention on the predictive task at hand such as identifying the effects of disease. We first tested our algorithm on a synthetic dataset, showing that our parameter selection improves registration quality and classification accuracy. We then tested the algorithm on 3D subcortical shapes from the Schizophrenia cohort Schizconnect. Our Schizpohrenia-Control predictive model showed significant improvement in ROC AUC compared to baseline parameters.
FaceOff: Anonymizing Videos in the Operating Rooms
Venue: arXiv cs.CV 2018
Year: 2018

Video capture in the surgical operating room (OR) is increasingly possible and has potential for use with computer assisted interventions (CAI), surgical data science and within smart OR integration. Captured video innately carries sensitive information that should not be completely visible in order to preserve the patient's and the clinical teams' identities. When surgical video streams are stored on a server, the videos must be anonymized prior to storage if taken outside of the hospital. In this article, we describe how a deep learning model, Faster R-CNN, can be used for this purpose and help to anonymize video data captured in the OR. The model detects and blurs faces in an effort to preserve anonymity. After testing an existing face detection trained model, a new dataset tailored to the surgical environment, with faces obstructed by surgical masks and caps, was collected for fine-tuning to achieve higher face-detection rates in the OR. We also propose a temporal regularisation kernel to improve recall rates. The fine-tuned model achieves a face detection recall of 88.05 % and 93.45 % before and after applying temporal-smoothing respectively.
Risk-Sensitive Generative Adversarial Imitation Learning
Venue: arXiv cs.LG 2018
Year: 2018

We study risk-sensitive imitation learning where the agent's goal is to perform at least as well as the expert in terms of a risk profile. We first formulate our risk-sensitive imitation learning setting. We consider the generative adversarial approach to imitation learning (GAIL) and derive an optimization problem for our formulation, which we call it risk-sensitive GAIL (RS-GAIL). We then derive two different versions of our RS-GAIL optimization problem that aim at matching the risk profiles of the agent and the expert w.r.t. Jensen-Shannon (JS) divergence and Wasserstein distance, and develop risk-sensitive generative adversarial imitation learning algorithms based on these optimization problems. We evaluate the performance of our algorithms and compare them with GAIL and the risk-averse imitation learning (RAIL) algorithms in two MuJoCo and two OpenAI classical control tasks.
Generative Invertible Networks (GIN): Pathophysiology-Interpretable Feature Mapping and Virtual Patient Generation
Venue: arXiv cs.CV 2018
Year: 2018

Machine learning methods play increasingly important roles in pre-procedural planning for complex surgeries and interventions. Very often, however, researchers find the historical records of emerging surgical techniques, such as the transcatheter aortic valve replacement (TAVR), are highly scarce in quantity. In this paper, we address this challenge by proposing novel generative invertible networks (GIN) to select features and generate high-quality virtual patients that may potentially serve as an additional data source for machine learning. Combining a convolutional neural network (CNN) and generative adversarial networks (GAN), GIN discovers the pathophysiologic meaning of the feature space. Moreover, a test of predicting the surgical outcome directly using the selected features results in a high accuracy of 81.55%, which suggests little pathophysiologic information has been lost while conducting the feature selection. This demonstrates GIN can generate virtual patients not only visually authentic but also pathophysiologically interpretable.
ScarGAN: Chained Generative Adversarial Networks to Simulate Pathological Tissue on Cardiovascular MR Scans
Venue: arXiv cs.CV 2018
Year: 2018

Medical images with specific pathologies are scarce, but a large amount of data is usually required for a deep convolutional neural network (DCNN) to achieve good accuracy. We consider the problem of segmenting the left ventricular (LV) myocardium on late gadolinium enhancement (LGE) cardiovascular magnetic resonance (CMR) scans of which only some of the scans have scar tissue. We propose ScarGAN to simulate scar tissue on healthy myocardium using chained generative adversarial networks (GAN). Our novel approach factorizes the simulation process into 3 steps: 1) a mask generator to simulate the shape of the scar tissue; 2) a domain-specific heuristic to produce the initial simulated scar tissue from the simulated shape; 3) a refining generator to add details to the simulated scar tissue. Unlike other approaches that generate samples from scratch, we simulate scar tissue on normal scans resulting in highly realistic samples. We show that experienced radiologists are unable to distinguish between real and simulated scar tissue. Training a U-Net with additional scans with scar tissue simulated by ScarGAN increases the percentage of scar pixels correctly included in LV myocardium prediction from 75.9% to 80.5%.
Adaptive Sampling for Convex Regression
Venue: arXiv cs.LG 2018
Year: 2018

In this paper, we introduce the first principled adaptive-sampling procedure for learning a convex function in the $L_\infty$ norm, a problem that arises often in the behavioral and social sciences. We present a function-specific measure of complexity and use it to prove that, for each convex function $f_{\star}$, our algorithm nearly attains the information-theoretically optimal, function-specific error rate. We also corroborate our theoretical contributions with numerical experiments, finding that our method substantially outperforms passive, uniform sampling for favorable synthetic and data-derived functions in low-noise settings with large sampling budgets. Our results also suggest an idealized "oracle strategy", which we use to gauge the potential advance of any adaptive-sampling strategy over passive sampling, for any given convex function.
Constructions of maximally recoverable local reconstruction codes via function fields
Venue: arXiv cs.IT 2018
Year: 2018

Local Reconstruction Codes (LRCs) allow for recovery from a small number of erasures in a local manner based on just a few other codeword symbols. A maximally recoverable (MR) LRC offers the best possible blend of such local and global fault tolerance, guaranteeing recovery from all erasure patterns which are information-theoretically correctable given the presence of local recovery groups. In an $(n,r,h,a)$-LRC, the $n$ codeword symbols are partitioned into $r$ disjoint groups each of which include $a$ local parity checks capable of locally correcting $a$ erasures. MR LRCs have received much attention recently, with many explicit constructions covering different regimes of parameters. Unfortunately, all known constructions require a large field size that exponential in $h$ or $a$, and it is of interest to obtain MR LRCs of minimal possible field size. In this work, we develop an approach based on function fields to construct MR LRCs. Our method recovers, and in most parameter regimes improves, the field size of previous approaches. For instance, for the case of small $r \ll ε\log n$ and large $h \ge Ω(n^{1-ε})$, we improve the field size from roughly $n^h$ to $n^{εh}$. For the case of $a=1$ (one local parity check), we improve the field size quadratically from $r^{h(h+1)}$ to $r^{h \lfloor (h+1)/2 \rfloor}$ for some range of $r$. The improvements are modest, but more importantly are obtained in a unified manner via a promising new idea.
Moving Object Segmentation in Jittery Videos by Stabilizing Trajectories Modeled in Kendall's Shape Space
Venue: arXiv cs.CV 2018
Year: 2018

Moving Object Segmentation is a challenging task for jittery/wobbly videos. For jittery videos, the non-smooth camera motion makes discrimination between foreground objects and background layers hard to solve. While most recent works for moving video object segmentation fail in this scenario, our method generates an accurate segmentation of a single moving object. The proposed method performs a sparse segmentation, where frame-wise labels are assigned only to trajectory coordinates, followed by the pixel-wise labeling of frames. The sparse segmentation involving stabilization and clustering of trajectories in a 3-stage iterative process. At the 1st stage, the trajectories are clustered using pairwise Procrustes distance as a cue for creating an affinity matrix. The 2nd stage performs a block-wise Procrustes analysis of the trajectories and estimates Frechet means (in Kendall's shape space) of the clusters. The Frechet means represent the average trajectories of the motion clusters. An optimization function has been formulated to stabilize the Frechet means, yielding stabilized trajectories at the 3rd stage. The accuracy of the motion clusters are iteratively refined, producing distinct groups of stabilized trajectories. Next, the labels obtained from the sparse segmentation are propagated for pixel-wise labeling of the frames, using a GraphCut based energy formulation. Use of Procrustes analysis and energy minimization in Kendall's shape space for moving object segmentation in jittery videos, is the novelty of this work. Second contribution comes from experiments performed on a dataset formed of 20 real-world natural jittery videos, with manually annotated ground truth. Experiments are done with controlled levels of artificial jitter on videos of SegTrack2 dataset. Qualitative and quantitative results indicate the superiority of the proposed method.
Unsupervised learning of foreground object detection
Venue: arXiv cs.CV 2018
Year: 2018

Unsupervised learning poses one of the most difficult challenges in computer vision today. The task has an immense practical value with many applications in artificial intelligence and emerging technologies, as large quantities of unlabeled videos can be collected at relatively low cost. In this paper, we address the unsupervised learning problem in the context of detecting the main foreground objects in single images. We train a student deep network to predict the output of a teacher pathway that performs unsupervised object discovery in videos or large image collections. Our approach is different from published methods on unsupervised object discovery. We move the unsupervised learning phase during training time, then at test time we apply the standard feed-forward processing along the student pathway. This strategy has the benefit of allowing increased generalization possibilities during training, while remaining fast at testing. Our unsupervised learning algorithm can run over several generations of student-teacher training. Thus, a group of student networks trained in the first generation collectively create the teacher at the next generation. In experiments our method achieves top results on three current datasets for object discovery in video, unsupervised image segmentation and saliency detection. At test time the proposed system is fast, being one to two orders of magnitude faster than published unsupervised methods.
Reconciling Irrational Human Behavior with AI based Decision Making: A Quantum Probabilistic Approach
Venue: arXiv cs.AI 2018
Year: 2018

There are many examples of human decision making which cannot be modeled by classical probabilistic and logic models, on which the current AI systems are based. Hence the need for a modeling framework which can enable intelligent systems to detect and predict cognitive biases in human decisions to facilitate better human-agent interaction. We give a few examples of irrational behavior and use a generalized probabilistic model inspired by the mathematical framework of Quantum Theory to model and explain such behavior.
Wirelessly Powered Data Aggregation for IoT via Over-the-Air Functional Computation: Beamforming and Power Control
Venue: arXiv cs.IT 2018
Year: 2018

As a revolution in networking, Internet of Things (IoT) aims at automating the operations of our societies by connecting and leveraging an enormous number of distributed devices (e.g., sensors and actuators). One design challenge is efficient wireless data aggregation (WDA) over tremendous IoT devices. This can enable a series of IoT applications ranging from latency-sensitive high-mobility sensing to data-intensive distributed machine learning. Over-the-air (functional) computation (AirComp) has emerged to be a promising solution that merges computing and communication by exploiting analogwave addition in the air. Another IoT design challenge is battery recharging for dense sensors which can be tackled by wireless power transfer (WPT). The coexisting of AirComp and WPT in IoT system calls for their integration to enhance the performance and efficiency of WDA. This motivates the current work on developing the wirelessly powered AirComp (WP-AirComp) framework by jointly optimizing wireless power control, energy and (data) aggregation beamforming to minimize the AirComp error. To derive a practical solution, we recast the non-convex joint optimization problem into the equivalent outer and inner sub-problems for (inner) wireless power control and energy beamforming, and (outer) the efficient aggregation beamforming, respectively. The former is solved in closed form while the latter is efficiently solved using the semidefinite relaxation technique. The results reveal that the optimal energy beams point to the dominant eigen-directions of the WPT channels, and the optimal power allocation tends to equalize the close-loop (down-link WPT and up-link AirComp) effective channels of different sensors. Simulation demonstrates that controlling WPT provides additional design dimensions for substantially reducing the AirComp error.
A Novel Sliding Mode Control for a Class of Affine Dynamic Systems
Venue: arXiv cs.SY 2018
Year: 2018

This paper proposes a novel sliding mode control (SMC) method for a class of affine dynamic systems. In this type of systems, the high-frequency gain matrix (HFGM), which is the matrix multiplying the control vector in the dynamic equation of the sliding variables vector, is neither deterministic nor positive definite. This case has rarely been covered by general SMC methods, which perform well under the condition that the HFGM is certain or uncertain but positive definite. In this study, the control law is determined by solving a nonlinear vector equation instead of the conventional algebraic expression, which is not applicable when the HFGM is uncertain and non-positive definite. Theorems with some relaxed system parametric uncertainty assumptions are proposed to guarantee the existence and uniqueness of the solution, and proofs of them, based on the principle of the convex cone set, are given in the text. The proposed control strategy can be easily applied in practice, and the chattering caused by the discontinuous control can be suppressed, as it can in general SMCs. The proposed controller was used in two affine dynamic systems, and the simulation results demonstrate its effectiveness.
AMoDSim: An Efficient and Modular Simulation Framework for Autonomous Mobility on Demand
Venue: arXiv cs.MA 2018
Year: 2018

Urban transportation of next decade is expected to be disrupted by Autonomous Mobility on Demand (AMoD): AMoD providers will collect ride requests from users and will dispatch a fleet of autonomous vehicles to satisfy requests in the most efficient way. Differently from current ride sharing systems, in which driver behavior has a clear impact on the system, AMoD systems will be exclusively determined by the dispatching logic. As a consequence, a recent interest in the Operations Research and Computer Science communities has focused on this control logic. The new propositions and methodologies are generally evaluated via simulation. Unfortunately, there is no simulation platform that has emerged as reference, with the consequence that each author uses her own custom-made simulator, applicable only in her specific study, with no aim of generalization and without public release. This slows down the progress in the area as researchers cannot build on each other's work and cannot share, reproduce and verify the results. The goal of this paper is to present AMoDSim, an open-source simulation platform aimed to fill this gap and accelerate research in future ride sharing systems.