OpenRaiser/Intern-Atlas huggingface dataset:
Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems
Venue: arXiv cs.LO 2018
Year: 2018

Verification of algorithms and data structures utilized in modern autonomous and semi-autonomous vehicles for land, sea, air, and space presents a significant challenge. Autonomy algorithms, e.g., route planning, pattern matching, and inference, are based on complex data structures such as directed graphs and algebraic data types. Proof techniques for these data structures exist, but are oriented to unbounded, functional realizations, which are not typically efficient in either space or time. Autonomous systems designers, on the other hand, generally limit the space and time allocations for any given function, and require that algorithms deliver results within a finite time, or suffer a watchdog timeout. Furthermore, high-assurance design rules frown on dynamic memory allocation, preferring simple array-based data structure implementations. In order to provide efficient implementations of high-level data structures used in autonomous systems with the high assurance needed for accreditation, we have developed a verifying compilation technique that supports the "natural" functional proof style, but yet applies to more efficient data structure implementations. Our toolchain features code generation to mainstream programming languages, as well as GPU-based and hardware-based realizations. We base the Intermediate Verification Language for our toolchain upon higher-order logic; however, we have used ACL2 to develop our efficient yet verifiable data structure design. ACL2 is particularly well-suited for this work, with its sophisticated libraries for reasoning about aggregate data structures of arbitrary size, efficient execution of formal specifications, as well as its support for "single-threaded objects" -- functional datatypes with imperative "under the hood" implementations. In this paper, we detail our high-assurance data structure design approach, including examples in ACL2 of common algebraic data types implemented using this design approach, proofs of correctness for those data types carried out in ACL2, as well as sample ACL2 implementations of relevant algorithms utilizing these efficient, high-assurance data structures.
Hint Orchestration Using ACL2's Simplifier
Venue: arXiv cs.LO 2018
Year: 2018

This paper describes a strategy for providing hints during an ACL2 proof, implemented in a utility called use-termhint. An extra literal is added to the goal clause and simplified along with the rest of the goal until it is stable under simplification, after which the simplified literal is examined and a hint extracted from it. This simple technique supports some commonly desirable yet elusive features. It supports providing different hints to different cases of a case split, as well as binding variables so as to avoid repeating multiply referenced subterms. Since terms used in these hints are simplified in the same way as the rest of the goal, this strategy is also more robust against changes in the rewriting normal form than hints in which terms from the goal are written out explicitly.
Task Runtime Prediction in Scientific Workflows Using an Online Incremental Learning Approach
Venue: arXiv cs.DC 2018
Year: 2018

Many algorithms in workflow scheduling and resource provisioning rely on the performance estimation of tasks to produce a scheduling plan. A profiler that is capable of modeling the execution of tasks and predicting their runtime accurately, therefore, becomes an essential part of any Workflow Management System (WMS). With the emergence of multi-tenant Workflow as a Service (WaaS) platforms that use clouds for deploying scientific workflows, task runtime prediction becomes more challenging because it requires the processing of a significant amount of data in a near real-time scenario while dealing with the performance variability of cloud resources. Hence, relying on methods such as profiling tasks' execution data using basic statistical description (e.g., mean, standard deviation) or batch offline regression techniques to estimate the runtime may not be suitable for such environments. In this paper, we propose an online incremental learning approach to predict the runtime of tasks in scientific workflows in clouds. To improve the performance of the predictions, we harness fine-grained resources monitoring data in the form of time-series records of CPU utilization, memory usage, and I/O activities that are reflecting the unique characteristics of a task's execution. We compare our solution to a state-of-the-art approach that exploits the resources monitoring data based on regression machine learning technique. From our experiments, the proposed strategy improves the performance, in terms of the error, up to 29.89%, compared to the state-of-the-art solutions.
Response to Comment on "All-optical machine learning using diffractive deep neural networks"
Venue: arXiv cs.NE 2018
Year: 2018

In their Comment, Wei et al. (arXiv:1809.08360v1 [cs.LG]) claim that our original interpretation of Diffractive Deep Neural Networks (D2NN) represent a mischaracterization of the system due to linearity and passivity. In this Response, we detail how this mischaracterization claim is unwarranted and oblivious to several sections detailed in our original manuscript (Science, DOI: 10.1126/science.aat8084) that specifically introduced and discussed optical nonlinearities and reconfigurability of D2NNs, as part of our proposed framework to enhance its performance. To further refute the mischaracterization claim of Wei et al., we, once again, demonstrate the depth feature of optical D2NNs by showing that multiple diffractive layers operating collectively within a D2NN present additional degrees-of-freedom compared to a single diffractive layer to achieve better classification accuracy, as well as improved output signal contrast and diffraction efficiency as the number of diffractive layers increase, showing the deepness of a D2NN, and its inherent depth advantage for improved performance. In summary, the Comment by Wei et al. does not provide an amendment to the original teachings of our original manuscript, and all of our results, core conclusions and methodology of research reported in Science (DOI: 10.1126/science.aat8084) remain entirely valid.
Filtration Simplification for Persistent Homology via Edge Contraction
Venue: arXiv cs.CG 2018
Year: 2018

Persistent homology is a popular data analysis technique that is used to capture the changing topology of a filtration associated with some simplicial complex $K$. These topological changes are summarized in persistence diagrams. We propose two contraction operators which when applied to $K$ and its associated filtration, bound the perturbation in the persistence diagrams. The first assumes that the underlying space of $K$ is a $2$-manifold and ensures that simplices are paired with the same simplices in the contracted complex as they are in the original. The second is for arbitrary $d$-complexes, and bounds the bottleneck distance between the initial and contracted $p$-dimensional persistence diagrams. This is accomplished by defining interleaving maps between persistence modules which arise from chain maps defined over the filtrations. In addition, we show how the second operator can efficiently compose across multiple contractions. We conclude with experiments demonstrating the second operator's utility on manifolds.
V3C - a Research Video Collection
Venue: arXiv cs.MM 2018
Year: 2018

With the widespread use of smartphones as recording devices and the massive growth in bandwidth, the number and volume of video collections has increased significantly in the last years. This poses novel challenges to the management of these large-scale video data and especially to the analysis of and retrieval from such video collections. At the same time, existing video datasets used for research and experimentation are either not large enough to represent current collections or do not reflect the properties of video commonly found on the Internet in terms of content, length, or resolution. In this paper, we introduce the Vimeo Creative Commons Collection, in short V3C, a collection of 28'450 videos (with overall length of about 3'800 hours) published under creative commons license on Vimeo. V3C comes with a shot segmentation for each video, together with the resulting keyframes in original as well as reduced resolution and additional metadata. It is intended to be used from 2019 at the International large-scale TREC Video Retrieval Evaluation campaign (TRECVid).
AI Learns to Recognize Bengali Handwritten Digits: Bengali.AI Computer Vision Challenge 2018
Venue: arXiv cs.CV 2018
Year: 2018

Solving problems with Artificial intelligence in a competitive manner has long been absent in Bangladesh and Bengali-speaking community. On the other hand, there has not been a well structured database for Bengali Handwritten digits for mass public use. To bring out the best minds working in machine learning and use their expertise to create a model which can easily recognize Bengali Handwritten digits, we organized Bengali.AI Computer Vision Challenge.The challenge saw both local and international teams participating with unprecedented efforts.
Investigating Enactive Learning for Autonomous Intelligent Agents
Venue: arXiv cs.LG 2018
Year: 2018

The enactive approach to cognition is typically proposed as a viable alternative to traditional cognitive science. Enactive cognition displaces the explanatory focus from the internal representations of the agent to the direct sensorimotor interaction with its environment. In this paper, we investigate enactive learning through means of artificial agent simulations. We compare the performances of the enactive agent to an agent operating on classical reinforcement learning in foraging tasks within maze environments. The characteristics of the agents are analysed in terms of the accessibility of the environmental states, goals, and exploration/exploitation tradeoffs. We confirm that the enactive agent can successfully interact with its environment and learn to avoid unfavourable interactions using intrinsically defined goals. The performance of the enactive agent is shown to be limited by the number of affordable actions.
On the Complexity of Solution Extension of Optimization Problems
Venue: arXiv cs.CC 2018
Year: 2018

The question if a given partial solution to a problem can be extended reasonably occurs in many algorithmic approaches for optimization problems. For instance, when enumerating minimal dominating sets of a graph $G=(V,E)$, one usually arrives at the problem to decide for a vertex set $U \subseteq V$, if there exists a \textit{minimal} dominating set $S$ with $U\subseteq S$. We propose a general, partial-order based formulation of such extension problems and study a number of specific problems which can be expressed in this framework. Possibly contradicting intuition, these problems tend to be NP-hard, even for problems where the underlying optimisation problem can be solved in polynomial time. This raises the question of how fixing a partial solution causes this increase in difficulty. In this regard, we study the parameterised complexity of extension problems with respect to parameters related to the partial solution, as well as the optimality of simple exact algorithms under the Exponential-Time Hypothesis. All complexity considerations are also carried out in very restricted scenarios, be it degree restrictions or topological restrictions (planarity) for graph problems or the size of the given partition for the considered extension variant of Bin Packing.
Interpreting Winograd Schemas Via the SP Theory of Intelligence and Its Realisation in the SP Computer Model
Venue: arXiv cs.AI 2018
Year: 2018

In 'Winograd Schema' (WS) sentences like "The city councilmen refused the demonstrators a permit because they feared violence" and "The city councilmen refused the demonstrators a permit because they advocated revolution", it is easy for adults to understand what "they" refers to but can be difficult for AI systems. This paper describes how the SP System -- outlined in an appendix -- may solve this kind of problem of interpretation. The central idea is that a knowledge of discontinuous associations amongst linguistic features, and an ability to recognise such patterns of associations, provides a robust means of determining what a pronoun like "they" refers to. For any AI system to solve this kind of problem, it needs appropriate knowledge of relevant syntax and semantics which, ideally, it should learn for itself. Although the SP System has some strengths in unsupervised learning, its capabilities in this area are not yet good enough to learn the kind of knowledge needed to interpret WS examples, so it must be supplied with such knowledge at the outset. However, its existing strengths in unsupervised learning suggest that it has potential to learn the kind of knowledge needed for the interpretation of WS examples. In particular, it has potential to learn the kind of discontinuous association of linguistic features mentioned earlier.
ECHO-3DHPC: Advance the performance of astrophysics simulations with code modernization
Venue: arXiv cs.DC 2018
Year: 2018

We present recent developments in the parallelization scheme of ECHO-3DHPC, an efficient astrophysical code used in the modelling of relativistic plasmas. With the help of the Intel Software Development Tools, like Fortran compiler and Profile-Guided Optimization (PGO), Intel MPI library, VTune Amplifier and Inspector we have investigated the performance issues and improved the application scalability and the time to solution. The node-level performance is improved by $2.3 \times$ and, thanks to the improved threading parallelisation, the hybrid MPI-OpenMP version of the code outperforms the MPI-only, thus lowering the MPI communication overhead.
The Lamb-Oseen Vortex and Paint Marbling
Venue: arXiv cs.CG 2018
Year: 2018

The displacement pattern arising from the decay of a two-dimensional Lamb-Oseen vortex in a Newtonian fluid can be closely modeled by the closed-form expression presented here. This formula enables Lamb-Oseen vortex simulation orders of magnitude faster than can be accomplished using finite-element methods, and without the accumulation of errors. "French Curl" marbling patterns look as though they are created by a vortex. Analysis and simulation of a nineteenth century example of French Curl finds that the pattern was created without a vortex. True vortexes are rarely seen in paint marbling because, in order to reach Reynolds numbers larger than 90, viscosity of the fluid bath must be much lower than is customarily used.
Algorithm for $\mathcal{B}$-partitions, parameterized complexity of the matrix determinant and permanent
Venue: arXiv cs.CC 2018
Year: 2018

Every square matrix $A=(a_{uv})\in \mathcal{C}^{n\times n}$ can be represented as a digraph having $n$ vertices. In the digraph, a block (or 2-connected component) is a maximally connected subdigraph that has no cut-vertex. The determinant and the permanent of a matrix can be calculated in terms of the determinant and the permanent of some specific induced subdigraphs of the blocks in the digraph. Interestingly, these induced subdigraphs are vertex-disjoint and they partition the digraph. Such partitions of the digraph are called the $\mathcal{B}$-partitions. In this paper, first, we develop an algorithm to find the $\mathcal{B}$-partitions. Next, we analyze the parameterized complexity of matrix determinant and permanent, where, the parameters are the sizes of blocks and the number of cut-vertices of the digraph. We give a class of combinations of cut-vertices and block sizes for which the parametrized complexities beat the state of art complexities of the determinant and the permanent.
Towards the Targeted Environment-Specific Evolution of Robot Components
Venue: arXiv cs.RO 2018
Year: 2018

This research considers the task of evolving the physical structure of a robot to enhance its performance in various environments, which is a significant problem in the field of Evolutionary Robotics. Inspired by the fields of evolutionary art and sculpture, we evolve only targeted parts of a robot, which simplifies the optimisation problem compared to traditional approaches that must simultaneously evolve both (actuated) body and brain. Exploration fidelity is emphasised in areas of the robot most likely to benefit from shape optimisation, whilst exploiting existing robot structure and control. Our approach uses a Genetic Algorithm to optimise collections of Bezier splines that together define the shape of a legged robot's tibia, and leg performance is evaluated in parallel in a high-fidelity simulator. The leg is represented in the simulator as 3D-printable file, and as such can be readily instantiated in reality. Provisional experiments in three distinct environments show the evolution of environment-specific leg structures that are both high-performing and notably different to those evolved in the other environments. This proof-of-concept represents an important step towards the environment-dependent optimisation of performance-critical components for a range of ubiquitous, standard, and already-capable robots that can carry out a wide variety of tasks.
Deep Recurrent Level Set for Segmenting Brain Tumors
Venue: arXiv cs.CV 2018
Year: 2018

Variational Level Set (VLS) has been a widely used method in medical segmentation. However, segmentation accuracy in the VLS method dramatically decreases when dealing with intervening factors such as lighting, shadows, colors, etc. Additionally, results are quite sensitive to initial settings and are highly dependent on the number of iterations. In order to address these limitations, the proposed method incorporates VLS into deep learning by defining a novel end-to-end trainable model called as Deep Recurrent Level Set (DRLS). The proposed DRLS consists of three layers, i.e, Convolutional layers, Deconvolutional layers with skip connections and LevelSet layers. Brain tumor segmentation is taken as an instant to illustrate the performance of the proposed DRLS. Convolutional layer learns visual representation of brain tumor at different scales. Since brain tumors occupy a small portion of the image, deconvolutional layers are designed with skip connections to obtain a high quality feature map. Level-Set Layer drives the contour towards the brain tumor. In each step, the Convolutional Layer is fed with the LevelSet map to obtain a brain tumor feature map. This in turn serves as input for the LevelSet layer in the next step. The experimental results have been obtained on BRATS2013, BRATS2015 and BRATS2017 datasets. The proposed DRLS model improves both computational time and segmentation accuracy when compared to the the classic VLS-based method. Additionally, a fully end-to-end system DRLS achieves state-of-the-art segmentation on brain tumors.
Stochastic Synthesis for Stochastic Computing
Venue: arXiv cs.ET 2018
Year: 2018

Stochastic computing (SC) is an emerging computing technique which offers higher computational density, and lower power over binary-encoded (BE) computation. Unlike BE computation, SC encodes values as probabilistic bitstreams which makes designing new circuits unintuitive. Existing techniques for synthesizing SC circuits are limited to specific classes of functions such as polynomial evaluation or constant scaling. In this paper, we propose using stochastic synthesis, which is originally a program synthesis technique, to automate the task of synthesizing new SC circuits. Our results show stochastic synthesis is more general than past techniques and can synthesize manually designed SC circuits as well as new ones such as an approximate square root unit.
Stability, convergence, and limit cycles in some human physiological processes
Venue: arXiv cs.SY 2018
Year: 2018

Mathematical models for physiological processes aid qualitative understanding of the impact of various parameters on the underlying process. We analyse two such models for human physiological processes: the Mackey-Glass and the Lasota equations, which model the change in the concentration of blood cells in the human body. We first study the local stability of these models, and derive bounds on various model parameters and the feedback delay for the concentration to equilibrate. We then deduce conditions for non-oscillatory convergence of the solutions, which could ensure that the blood cell concentration does not oscillate. Further, we define the convergence characteristics of the solutions which govern the rate at which the concentration equilibrates when the system is stable. Owing to the possibility that physiological parameters can seldom be estimated precisely, we also derive bounds for robust stability\textemdash which enable one to ensure that the blood cell concentration equilibrates despite parametric uncertainty. We also highlight that when the necessary and sufficient condition for local stability is violated, the system transits into instability via a Hopf bifurcation, leading to limit cycles in the blood cell concentration. We then outline a framework to characterise the type of the Hopf bifurcation and determine the asymptotic orbital stability of limit cycles. The analysis is complemented with numerical examples, stability charts and bifurcation diagrams. The insights into the dynamical properties of the mathematical models may serve to guide the study of dynamical diseases.
Distributed Nonlinear Control Design using Separable Control Contraction Metrics
Venue: arXiv cs.SY 2018
Year: 2018

This paper gives convex conditions for synthesis of a distributed control system for large-scale networked nonlinear dynamic systems. It is shown that the technique of control contraction metrics (CCMs) can be extended to this problem by utilizing separable metric structures, resulting in controllers that only depend on information from local sensors and communications from immediate neighbours. The conditions given are pointwise linear matrix inequalities, and are necessary and sufficient for linear positive systems and certain monotone nonlinear systems. Distributed synthesis methods for systems on chordal graphs are also proposed based on SDP decompositions. The results are illustrated on a problem of vehicle platooning with heterogeneous vehicles, and a network of nonlinear dynamic systems with over 1000 states that is not feedback linearizable and has an uncontrollable linearization
Optimal Impulse Control of SIR Epidemics over Scale-Free Networks
Venue: arXiv cs.SY 2018
Year: 2018

Recent wide spreading of Ransomware has created new challenges for cybersecurity over large-scale networks. The densely connected networks can exacerbate the spreading and makes the containment and control of the malware more challenging. In this work, we propose an impulse optimal control framework for epidemics over networks. The hybrid nature of discrete-time control policy of continuous-time epidemic dynamics together with the network structure poses a challenging optimal control problem. We leverage the Pontryagin's minimum principle for impulsive systems to obtain an optimal structure of the controller and use numerical experiments to corroborate our results.