1,721,119 research outputs found

    Reverse Complexity

    No full text
    Reverse Complexity is a long term research program aiming at discovering the abstract, logical principles underlying Complexity Theory, by means of a formal, reverse analysis of its proofs. The final goal is to get a cleaner, machine independent presentation of the foundation of Complexity Theory and a better, synergic integration with logic; in particular, we aim to provide abstract, axiomatic characterizations of Complexity Classes with the purpose to better grasp their essence, identify their distinctive properties, suggest new, possibly non-standard computational models and finally provide new tools for separating them. In this article, we introduce the program and illustrate its methodology through an investigation of the well known Hierarchy Theorems. The analysis is conducted with the assistance of an interactive theorem prover (in our case, Matita), not only used to check the formal correctness of proofs, but as an important driver of the actual research

    About Generative Aspects of Variational Autoencoders

    No full text
    An essential prerequisite for random generation of good quality samples in Variational Autoencoders (VAE) is that the distribution of variables in the latent space has a known distribution, typically a normal distribution N(0, 1). This should be induced by a regularization term in the loss function, minimizing for each data X, the Kullback-Leibler distance between the posterior inference distribution of latent variables Q(z|X) and N(0, 1). In this article, we investigate the marginal inference distribution Q(z) as a Gaussian Mixture Model, proving, under a few reasonable assumptions, that although the first and second moment of Q(z) might indeed be coherent with those of a normal distribution, there is no reason to believe the same for other moments; in particular, its Kurtosis is likely to be different from 3. The actual distribution of Q(z) is possibly very far from a Normal, raising doubts on the effectiveness of generative sampling according to the vanilla VAE framework

    Computational complexity via finite types

    No full text
    We address computational complexity writing polymorphic functions between finite types (i.e., types with a finite number of canonical elements), expressing costs in terms of the cardinality of these types. This allows us to rediscover, in a more syntactical setting, the known result that the different levels in the hierarchy of higher-order primitive recursive functions (Gödel system T), when interpreted over finite structures, precisely capture basic complexity classes: functions of rank 1 characterize LOGSPACE, rank 2 PTIME, rank 3 PSPACE, rank 4 EXPTIME = DTIME(2^poly), and so on

    Comparing the latent space of generative models

    Get PDF
    Different encodings of datapoints in the latent space of latent-vector generative models may result in more or less effective and disentangled characterizations of the different explanatory factors of variation behind the data. Many works have been recently devoted to the explorationof the latent space of specific models, mostly focused on the study of how features are disentangled and of how trajectories producing desired alterations of data in the visible space can be found. In this work we address the more general problem of comparing the latent spaces of different models, looking for transformations between them. We confined the investigation to the familiar and largely investigated case of generative models for the data manifold of human faces. The surprising, preliminary result reported in this article is that (provided models have not been taught or explicitly conceived to act differently) a simple linear mapping is enough to pass from a latent space to another while preserving most of the information

    Balancing Reconstruction Error and Kullback-Leibler Divergence in Variational Autoencoders

    Get PDF
    Likelihood-based generative frameworks are receiving increasing attention in the deep learning community, mostly on account of their strong probabilistic foundation. Among them, Variational Autoencoders (VAEs) are reputed for their fast and tractable sampling and relatively stable training, but if not properly tuned they may easily produce poor generative performances. The loss function of Variational Autoencoders is the sum of two components, with somehow contrasting effects: the reconstruction loss,improving the quality of the resulting images, and the Kullback-Leibler divergence, acting as a regularizer of the latent space. Correctly balancing these two components is a delicate issue, and one of the major problems of VAEs. Recent techniques address the problem by allowing the network to learn the balancing factor during training, according to a suitable loss function. In this article, we show that learning can be replaced by a simple deterministic computation, expressing the balancing factor in terms of a running average of the reconstruction error over the last minibatches. As a result, we keep a constant balance between the two components along training: as reconstruction improves, we proportionally decrease KL-divergence in order to prevent its prevalence, that would forbid further improvements of the quality of reconstructions. Our technique is simple and effective: it clarifies the learning objective for the balancing factor, and it produces faster and more accurate behaviours. On typical datasets such as Cifar10 and CelebA, our technique sensibly outperforms all previous VAE architectures with comparable parameter capacity

    Syllabification of the Divine Comedy

    Get PDF
    We provide a syllabification algorithm for the Divine Comedy using techniques from probabilistic and constraint programming. We particularly focus on the synalephe, addressed in terms of the "propensity" of a word to take part in a synalephe with adjacent words. We jointly provide an online vocabulary containing, for each word, information about its syllabification, the location of the tonic accent, and the aforementioned synalephe propensity, on the left and right sides. The algorithm is intrinsically nondeterministic, producing different possible syllabifications for each verse, with different likelihoods; metric constraints relative to accents on the 10th, 4th, and 6th syllables are used to further reduce the solution space. The most likely syllabification is hence returned as output. We believe that this work could be a major milestone for a lot of different investigations. From the point of view of digital humanities it opens new perspectives on computer-assisted analysis of digital sources, comprising automated detection of anomalous and problematic cases, metric clustering of verses and their categorization, or more foundational investigations addressing, e.g., the phonetic roles of consonants and vowels. From the point of view of text processing and deep learning, information about syllabification and the location of accents opens a wide range of exciting perspectives, from the possibility of automatic learning syllabification of words and verses to the improvement of generative models, aware of metric issues, and more respectful of the expected musicality

    Variance Loss in Variational Autoencoders

    Get PDF
    In this article, we highlight what appears to be major issue of Variational Autoencoders, evinced from an extensive experimentation with different network architectures and datasets: the variance of generated data is significantly lower than that of training data. Since generative models are usually evaluated with metrics such as the Frechet Inception Distance (FID) that compare the distributions of (features of) real versus generated images, the variance loss typically results in degraded scores. This problem is particularly relevant in a two stage setting, where we use a second VAE to sample in the latent space of the first VAE. The minor variance creates a mismatch between the actual distribution of latent variables and those generated by the second VAE, that hinders the beneficial effects of the second stage. Renormalizing the output of the second VAE towards the expected normal spherical distribution, we obtain a sudden burst in the quality of generated samples, as also testified in terms of FID

    A formalization of multi-tape Turing machines

    Get PDF
    We discuss the formalization, in the Matita Theorem Prover, of basic results on multi-tapes Turing machines, up to the existence of a (certified) Universal Machine, and propose it as a natural benchmark for comparing different interactive provers and assessing the state of the art in the mechanization of formal reasoning. The work is meant to be a preliminary step towards the creation of a formal repository in Complexity Theory, and is a small piece in our long-term Reverse Complexity program, aiming to a comfortable, machine independent axiomatization of the field

    The Effectiveness of Data Augmentation for Detection of Gastrointestinal Diseases from Endoscopical Images

    No full text
    The lack, due to privacy concerns, of large public databases of medical pathologies is a well-known and major problem, substantially hindering the application of deep learning techniques in this field. In this article, we investigate the possibility to supply to the deficiency in the number of data by means of data augmentation techniques, working on the recent Kvasir dataset (Pogorelov et al., 2017) of endoscopical images of gastrointestinal diseases. The dataset comprises 4,000 colored images labeled and verified by medical endoscopists, covering a few common pathologies at different anatomical landmarks: Z-line, pylorus and cecum. We show how the application of data augmentation techniques allows to achieve sensible improvements of the classification with respect to previous approaches, both in terms of precision and recall

    MicroRacer: A Didactic Environment for Deep Reinforcement Learning

    Get PDF
    MicroRacer is a simple, open source environment inspired by car racing especially meant for the didactics of Deep Reinforcement Learning. The complexity of the environment has been explicitly calibrated to allow users to experiment with many different methods, networks and hyperparameters settings without requiring sophisticated software or exceedingly long training times. Baseline agents for major learning algorithms such as DDPG, PPO, SAC, TD3 and DSAC are provided too, along with a preliminary comparison in terms of training time and performance
    corecore