OpenRaiser/Intern-Atlas huggingface dataset:
SenseNet: 3D Objects Database and Tactile Simulator
Venue: arXiv cs.AI 2017
Year: 2017

The majority of artificial intelligence research, as it relates from which to biological senses has been focused on vision. The recent explosion of machine learning and in particular, dee p learning, can be partially attributed to the release of high quality data sets for algorithm s from which to model the world on. Thus, most of these datasets are comprised of images. We believe that focusing on sensorimotor systems and tactile feedback will create algorithms that better mimic human intelligence. Here we present SenseNet: a collection of tactile simulators and a large scale dataset of 3D objects for manipulation. SenseNet was created for the purpose of researching and training Artificial Intelligences (AIs) to interact with the environment via sensorimotor neural systems and tactile feedback. We aim to accelerate that same explosion in image processing, but for the domain of tactile feedback and sensorimotor research. We hope that SenseNet can offer researchers in both the machine learning and computational neuroscience communities brand new opportunities and avenues to explore.
ObamaNet: Photo-realistic lip-sync from text
Venue: arXiv cs.CV 2017
Year: 2017

We present ObamaNet, the first architecture that generates both audio and synchronized photo-realistic lip-sync videos from any new text. Contrary to other published lip-sync approaches, ours is only composed of fully trainable neural modules and does not rely on any traditional computer graphics methods. More precisely, we use three main modules: a text-to-speech network based on Char2Wav, a time-delayed LSTM to generate mouth-keypoints synced to the audio, and a network based on Pix2Pix to generate the video frames conditioned on the keypoints.
Formal specification of the FlexRay protocol using FocusST
Venue: arXiv cs.LO 2017
Year: 2017

FlexRay is a communication protocol developed by the FlexRay Consortium. The core members of the Consortium are Freescale Semiconductor, Robert Bosch GmbH, NXP Semiconductors, BMW, Volkswagen, Daimler, and General Motors, and the protocol was respectively oriented towards embedded systems in the automotive domain. This paper presents a formal specification of the FlexRay protocol using the FocusST framework. This work extends our previous research of formal specifications of this protocol using Focus formal language.
Perceived Audiovisual Quality Modelling based on Decison Trees, Genetic Programming and Neural Networks
Venue: arXiv cs.MM 2017
Year: 2017

Our objective is to build machine learning based models that predict audiovisual quality directly from a set of correlated parameters that are extracted from a target quality dataset. We have used the bitstream version of the INRS audiovisual quality dataset that reflects contemporary real-time configurations for video frame rate, video quantization, noise reduction parameters and network packet loss rate. We have utilized this dataset to build bitstream perceived quality estimation models based on the Random Forests, Bagging, Deep Learning and Genetic Programming methods. We have taken an empirical approach and have generated models varying from very simple to the most complex depending on the number of features used from the quality dataset. Random Forests and Bagging models have overall generated the most accurate results in terms of RMSE and Pearson correlation coefficient values. Deep Learning and Genetic Programming based bitstream models have also achieved good results but that high performance was observed only with a limited range of features. We have also obtained the epsilon-insensitive RMSE values for each model and have computed the significance of the difference between the correlation coefficients. Overall we conclude that computing the bitstream information is worth the effort it takes to generate and helps to build more accurate models for real-time communications. However, it is useful only for the deployment of the right algorithms with the carefully selected subset of the features. The dataset and tools that have been developed during this research are publicly available for research and development purposes.
Multi-measures fusion based on multi-objective genetic programming for full-reference image quality assessment
Venue: arXiv cs.MM 2017
Year: 2017

In this paper, we exploit the flexibility of multi-objective fitness functions, and the efficiency of the model structure selection ability of a standard genetic programming (GP) with the parameter estimation power of classical regression via multi-gene genetic programming (MGGP), to propose a new fusion technique for image quality assessment (IQA) that is called Multi-measures Fusion based on Multi-Objective Genetic Programming (MFMOGP). This technique can automatically select the most significant suitable measures, from 16 full-reference IQA measures, used in aggregation and finds weights in a weighted sum of their outputs while simultaneously optimizing for both accuracy and complexity. The obtained well-performing fusion of IQA measures are evaluated on four largest publicly available image databases and compared against state-of-the-art full-reference IQA approaches. Results of comparison reveal that the proposed approach outperforms other state-of-the-art recently developed fusion approaches.
Analyzing Design Process and Experiments on the AnITA Generic Tutoring System
Venue: arXiv cs.CY 2018
Year: 2018

In the field of tutoring systems, investigations have shown that there are many tutoring systems specific to a specific domain that, because of their static architecture, cannot be adapted to other domains. As consequence, often neither methods nor knowledge can be reused. In addition, the knowledge engineer must have programming skills in order to enhance and evaluate the system. One particular challenge is to tackle these problems with the development of a generic tutoring system. AnITA, as a stand-alone application, has been developed and implemented particularly for this purpose. However, in the testing phase, we discovered that this architecture did not fully match the user's intuitive understanding of the use of a learning tool. Therefore, AnITA has been redesigned to exclusively work as a client/server application and renamed to AnITA2. This paper discusses the evolvements made on the AnITA tutoring system, the goal of which is to use generic principles for system re-use in any domain. Two experiments were conducted, and the results are presented in this paper.
MAC Layer Hurdles in BSNs
Venue: arXiv cs.NI 2018
Year: 2018

The last few decades have seen considerable research progress in microelectronics and integrated circuits, system-on-chip design, wireless communication, and sensor technology. This progress has enabled the seamless integration of autonomous wireless sensor nodes around a human body to create a Body Sensor Network (BSN). The development of a proactive and ambulatory BSN induces a number of enormous issues and challenges. This paper presents the technical hurdles during the design and implementation of a low-power Medium Access Control (MAC) protocol for in-body and on-body sensor networks. We analyze the performance of IEEE 802.15.4 protocol for the on-body sensor network. We also provide a comprehensive insight into the heterogeneous characteristics of the in-body sensor network. A low-power technique called Pattern-Based Wake-up Table is proposed to handle the normal traffic in a BSN. The proposed technique provides a reliable solution towards low-power communication in the in-body sensor network.
A Complete Dichotomy Rises from the Capture of Vanishing Signatures
Venue: arXiv cs.CC 2018
Year: 2018

We prove a complexity dichotomy theorem for Holant problems over an arbitrary set of complex-valued symmetric constraint functions F on Boolean variables. This extends and unifies all previous dichotomies for Holant problems on symmetric constraint functions (taking values without a finite modulus). We define and characterize all symmetric vanishing signatures. They turned out to be essential to the complete classification of Holant problems. The dichotomy theorem has an explicit tractability criterion expressible in terms of holographic transformations. A Holant problem defined by a set of constraint functions F is solvable in polynomial time if it satisfies this tractability criterion, and is #P-hard otherwise. The tractability criterion can be intuitively stated as follows: A set F is tractable if (1) every function in F has arity at most two, or (2) F is transformable to an affine type, or (3) F is transformable to a product type, or (4) F is vanishing, combined with the right type of binary functions, or (5) F belongs to a special category of vanishing type Fibonacci gates. The proof of this theorem utilizes many previous dichotomy theorems on Holant problems and Boolean #CSP. Holographic transformations play an indispensable role as both a proof technique and in the statement of the tractability criterion.
Programming Languages for Scientific Computing
Venue: arXiv cs.PL 2018
Year: 2018

Scientific computation is a discipline that combines numerical analysis, physical understanding, algorithm development, and structured programming. Several yottacycles per year on the world's largest computers are spent simulating problems as diverse as weather prediction, the properties of material composites, the behavior of biomolecules in solution, and the quantum nature of chemical compounds. This article is intended to review specfic languages features and their use in computational science. We will review the strengths and weaknesses of different programming styles, with examples taken from widely used scientific codes.
A Simple Algorithm for Computing BOCP
Venue: arXiv cs.DS 2018
Year: 2018

In this article, we devise a concise algorithm for computing BOCP. Our method is simple, easy-to-implement but without loss of efficiency. Given two circular-arc polygons with $m$ and $n$ edges respectively, our method runs in $O(m+n+(l+k)\log l)$ time, using $O(m+n+k)$ space, where $k$ is the number of intersections, and $l$ is the number of {edge}s. Our algorithm has the power to approximate to linear complexity when $k$ and $l$ are small. The superiority of the proposed algorithm is also validated through empirical study.
A Note on "A polynomial-time algorithm for global value numbering"
Venue: arXiv cs.PL 2018
Year: 2018

Global Value Numbering(GVN) is a popular method for detecting redundant computations. A polynomial time algorithm for GVN is presented by Gulwani and Necula(2006). Here we present two limitations of this GVN algorithm due to which detection of certain kinds of redundancies can not be done using this algorithm. The first one is concerning the use of this algorithm in detecting some instances of the classical global common subexpressions, and the second is concerning its use in the detection of some redundancies that a local value numbering algorithm will detect. We suggest improvements that enable the algorithm to detect these kinds of redundancies as well.
A Note on Topology Preservation in Classification, and the Construction of a Universal Neuron Grid
Venue: arXiv cs.NE 2018
Year: 2018

It will be shown that according to theorems of K. Menger, every neuron grid if identified with a curve is able to preserve the adopted qualitative structure of a data space. Furthermore, if this identification is made, the neuron grid structure can always be mapped to a subset of a universal neuron grid which is constructable in three space dimensions. Conclusions will be drawn for established neuron grid types as well as neural fields.
Some Remarks on Lower Bounds for Queue Machines (Preliminary Report)
Venue: arXiv cs.CC 2018
Year: 2018

We first give an improved lower bound for the deterministic online simulation of tapes or pushdown stores by queues. Then we inspect some proofs in a classical work on queue machines in the area of Formal Languages and outline why a main argument in the proofs is incomplete. Based on descriptional complexity, we show the intuition behind the argument to be correct.
Clustering, Coding, and the Concept of Similarity
Venue: arXiv cs.LG 2018
Year: 2018

This paper develops a theory of clustering and coding which combines a geometric model with a probabilistic model in a principled way. The geometric model is a Riemannian manifold with a Riemannian metric, ${g}_{ij}({\bf x})$, which we interpret as a measure of dissimilarity. The probabilistic model consists of a stochastic process with an invariant probability measure which matches the density of the sample input data. The link between the two models is a potential function, $U({\bf x})$, and its gradient, $\nabla U({\bf x})$. We use the gradient to define the dissimilarity metric, which guarantees that our measure of dissimilarity will depend on the probability measure. Finally, we use the dissimilarity metric to define a coordinate system on the embedded Riemannian manifold, which gives us a low-dimensional encoding of our original data.
Predicate Logic as a Modelling Language: The IDP System
Venue: arXiv cs.LO 2018
Year: 2018

With the technology of the time, Kowalski's seminal 1974 paper {\em Predicate Logic as a Programming Language} was a breakthrough for the use of logic in computer science. It introduced two fundamental ideas: on the declarative side, the use of the Horn clause logic fragment of classical logic, which was soon extended with negation as failure, on the procedural side the procedural interpretation which made it possible to write algorithms in the formalism. Since then, strong progress was made both on the declarative understanding of the logic programming formalism and in automated reasoning technologies, particularly in SAT solving, Constraint Programming and Answer Set Programming. This has paved the way for the development of an extension of logic programming that embodies a more pure view of logic as a modelling language and its role for problem solving. In this paper, we present the \idp language and system. The language is essentially classical logic extended with one of logic programmings most important contributions to knowledge representation: the representation of complex definitions as rule sets under well-founded semantics. The system is a knowledge base system: a system in which complex declarative information is stored in a knowledge base which can be used to solve different computational problems by applying multiple forms of inference. In this view, theories are declarative modellings, bags of information, descriptions of possible states of affairs. They are neither procedures nor descriptions of computational problems. As such, the \idp language and system preserve the fundamental idea of a declarative reading of logic programs, while they break with the fundamental idea of the procedural interpretation of logic programs.
Study of Behaviours via Visitable Paths
Venue: arXiv cs.LO 2018
Year: 2018

Around 2000, J.-Y. Girard developed a logical theory, called Ludics. This theory was a step in his program of Geometry of Interaction, the aim of which being to account for the dynamics of logical proofs. In Ludics, objects called designs keep only what is relevant for the cut elimination process, hence the dynamics of a proof: a design is an abstraction of a formal proof. The notion of behaviour is the counterpart in Ludics of the notion of type or the logical notion of formula. Formally a behaviour is a closed set of designs. Our aim is to explore the constructions of behaviours and to analyse their properties. In this paper a design is viewed as a set of coherent paths. We recall or give variants of properties concerning visitable paths, where a visitable path is a path in a design or a set of designs that may be traversed by interaction with a design of the orthogonal of the set. We are then able to answer the following question: which properties should satisfy a set of paths for being exactly the set of visitable paths of a behaviour? Such a set and its dual should be prefix-closed, daimon-closed and satisfy two saturation properties. This allows us to have a means for defining the whole set of visitable paths of a given set of designs without closing it explicitly, that is without computing the orthogonal of this set of designs. We finally apply all these results for making explicit the structure of a behaviour generated by constants and multiplicative/additive connectives. We end by proposing an oriented tensor for which we give basic properties.
Mining Attribute-Based Access Control Policies from Logs
Venue: arXiv cs.CR 2018
Year: 2018

Attribute-based access control (ABAC) provides a high level of flexibility that promotes security and information sharing. ABAC policy mining algorithms have potential to significantly reduce the cost of migration to ABAC, by partially automating the development of an ABAC policy from information about the existing access-control policy and attribute data. This paper presents an algorithm for mining ABAC policies from operation logs and attribute data. To the best of our knowledge, it is the first algorithm for this problem.
Duality and Optimality of Auctions for Uniform Distributions
Venue: arXiv cs.GT 2018
Year: 2018

We develop a general duality-theory framework for revenue maximization in additive Bayesian auctions. The framework extends linear programming duality and complementarity to constraints with partial derivatives. The dual system reveals the geometric nature of the problem and highlights its connection with the theory of bipartite graph matchings. We demonstrate the power of the framework by applying it to a multiple-good monopoly setting where the buyer has uniformly distributed valuations for the items, the canonical long-standing open problem in the area. We propose a deterministic selling mechanism called Straight-Jacket Auction (SJA), which we prove to be exactly optimal for up to 6 items, and conjecture its optimality for any number of goods. The duality framework is used not only for proving optimality, but perhaps more importantly for deriving the optimal mechanism itself; as a result, SJA is defined by natural geometric constraints.
Generating Synchronizing Automata with Large Reset Lengths
Venue: arXiv cs.FL 2018
Year: 2018

We study synchronizing automata with the shortest reset words of relatively large length. First, we refine the Frankl-Pin result on the length of the shortest words of rank $m$, and the Béal, Berlinkov, Perrin, and Steinberg results on the length of the shortest reset words in one-cluster automata. The obtained results are useful in computation aimed in extending the class of small automata for which the Černý conjecture is verified and discovering new automata with special properties regarding synchronization.
Unguarded Recursion on Coinductive Resumptions
Venue: arXiv cs.LO 2018
Year: 2018

We study a model of side-effecting processes obtained by starting from a monad modelling base effects and adjoining free operations using a cofree coalgebra construction; one thus arrives at what one may think of as types of non-wellfounded side-effecting trees, generalizing the infinite resumption monad. Correspondingly, the arising monad transformer has been termed the coinductive generalized resumption transformer. Monads of this kind have received some attention in the recent literature; in particular, it has been shown that they admit guarded iteration. Here, we show that they also admit unguarded iteration, i.e. form complete Elgot monads, provided that the underlying base effect supports unguarded iteration. Moreover, we provide a universal characterization of the coinductive resumption monad transformer in terms of coproducts of complete Elgot monads.
Computing Minimum Rainbow and Strong Rainbow Colorings of Block Graphs
Venue: arXiv cs.DM 2018
Year: 2018

A path in an edge-colored graph $G$ is rainbow if no two edges of it are colored the same. The graph $G$ is rainbow-connected if there is a rainbow path between every pair of vertices. If there is a rainbow shortest path between every pair of vertices, the graph $G$ is strongly rainbow-connected. The minimum number of colors needed to make $G$ rainbow-connected is known as the rainbow connection number of $G$, and is denoted by $\text{rc}(G)$. Similarly, the minimum number of colors needed to make $G$ strongly rainbow-connected is known as the strong rainbow connection number of $G$, and is denoted by $\text{src}(G)$. We prove that for every $k \geq 3$, deciding whether $\text{src}(G) \leq k$ is NP-complete for split graphs, which form a subclass of chordal graphs. Furthermore, there exists no polynomial-time algorithm for approximating the strong rainbow connection number of an $n$-vertex split graph with a factor of $n^{1/2-ε}$ for any $ε> 0$ unless P = NP. We then turn our attention to block graphs, which also form a subclass of chordal graphs. We determine the strong rainbow connection number of block graphs, and show it can be computed in linear time. Finally, we provide a polynomial-time characterization of bridgeless block graphs with rainbow connection number at most 4.
The number system hidden inside the Boolean satisfiability problem
Venue: arXiv cs.CC 2018
Year: 2018

This paper gives a novel approach to analyze SAT problem more deeply. First, I define new elements of Boolean formula such as dominant variable, decision chain, and chain coupler. Through the analysis of the SAT problem using the elements, I prove that we can construct a k-SAT (k>2) instance where the coefficients of cutting planes take exponentially large values in the input size. This exponential property is caused by the number system formed from the calculation of coefficients. In addition, I show that 2-SAT does not form the number system and Horn-SAT partially forms the number system according to the feasible value of the dominant variable. Whether or not the coefficients of cutting planes in cutting plane proof are polynomially bounded was open problem. Many researchers believed that cutting plane proofs with large coefficients are highly non-intuitive20. However, we can construct a k-SAT (k>2) instance in which cutting planes take exponentially large coefficients by the number system. In addition, this exponential property is so strong that it gives definite answers for several questions: why Horn-SAT has the intermediate property between 2-SAT and 3-SAT; why random-SAT is so easy; and why k-SAT (k>2) cannot be solved with the linear programming technique. As we know, 2-SAT is NL-complete, Horn-SAT is P-complete, and k-SAT (k>2) is NP-complete. In terms of computational complexity, this paper gives a clear mathematical property by which SAT problems in three different classes are distinguished.
Multiplicative Complexity of Vector Valued Boolean Functions
Venue: arXiv cs.CC 2018
Year: 2018

We consider the multiplicative complexity of Boolean functions with multiple bits of output, studying how large a multiplicative complexity is necessary and sufficient to provide a desired nonlinearity. For so-called $ΣΠΣ$ circuits, we show that there is a tight connection between error correcting codes and circuits computing functions with high nonlinearity. Combining this with known coding theory results, we show that functions with $n$ inputs and $n$ outputs with the highest possible nonlinearity must have at least $2.32n$ AND gates. We further show that one cannot prove stronger lower bounds by only appealing to the nonlinearity of a function; we show a bilinear circuit computing a function with almost optimal nonlinearity with the number of AND gates being exactly the length of such a shortest code. Additionally we provide a function which, for general circuits, has multiplicative complexity at least $2n-3$. Finally we study the multiplicative complexity of "almost all" functions. We show that every function with $n$ bits of input and $m$ bits of output can be computed using at most $2.5(1+o(1))\sqrt{m2^n}$ AND gates.