Search

This study evaluates the application of artificial intelligence (AI) to the automatic classification of radiolarians and uses as an example eight distinct morphospecies of the Eocene radiolarian genus Podocyrtis, which are part of three different evolutionary lineages and are useful in biostratigraphy. The samples used in this study were recovered from the equatorial Atlantic (ODP Leg 207) and were supplemented with some samples coming from the North Atlantic and Indian Oceans. To create an automatic classification tool, numerous images of the investigated species were needed to train a MobileNet convolutional neural network entirely coded in Python. Three different datasets were obtained. The first one consists of a mixture of broken and complete specimens, some of which sometimes appear blurry. The second and third datasets were leveled down into two further steps, which excludes broken and blurry specimens while increasing the quality. The convolutional neural network randomly selected 85 % of all specimens for training, while the remaining 15 % were used for validation. The MobileNet architecture had an overall accuracy of about 91 % for all datasets. Three predicational models were thereafter created, which had been trained on each dataset and worked well for classification of Podocyrtis coming from the Indian Ocean (Madingley Rise, ODP Leg 115, Hole 711A) and the western North Atlantic Ocean (New Jersey slope, DSDP Leg 95, Hole 612 and Blake Nose, ODP Leg 171B, Hole 1051A). These samples also provided clearer images since they were mounted with Canada balsam rather than Norland epoxy. In spite of some morphological differences encountered in different parts of the world's oceans and differences in image quality, most species could be correctly classified or at least classified with a neighboring species along a lineage. Classification improved slightly for some species by cropping and/or removing background particles of images which did not segment properly in the image processing. However, depending on cropping or background removal, the best result came from the predictive model trained on the normal stacked dataset consisting of a mixture of broken and complete specimens.

International audience; Bio-inspired computing architectures enable ultralow power consumption and massive parallelism using neuromorphic computing, which is apt to implement Spiking Neural Networks (SNN). Such architectures are particularly suitable for energy-constrained applications. A deeper understanding of Spiking Neural Networks (SNN) behavior during training is needed to improve these architectures. This paper presents VS2N, a web-based tool for interactive visualization and analysis of SNN activity over time. This simulator-independent tool offers a way to examine, analyze and validate different hypotheses about SNN activity. We present available analysis modules and use-cases of the tool as an example.

extended paper; International audience; L’architecture des systèmes numériques traditionnels est loin d’être optimale puisqu’un microprocesseur est tout autant une plaque chauffante qu’un calculateur (Intel Cooking [1]). Il devient donc urgent de proposer des architectures de traitement de l’information radicalement différentes, « neuro-inspirées », qui permettent d’apporter des fonctions cogni-tives aux solutions existantes. C’est ainsi que des neurones et synapses artificiels travaillant à faible tension d’alimentation ont été fabriqués, ce qui leur confère une très basse consommation d’énergie et une fabrication aisée. Ce stand montre à des jeunes lycéens et étudiants que l’utilisation de tels neurones et synapses dans un système de vision artificielle (capture et traitement d’images) conduira certainement à une forte amélioration des performances et, parallèlement, à une réduc-tion drastique de la consommation énergétique. Il s’agit d’une expérience pédagogique innovante, riche de nombreux supports variés, afin de transmettre aux jeunes générations les enjeux des activités de recherche qui se construisent dans les laboratoires de l’Université de Lille.

International audience; Abstract Neuromorphic computation using Spiking Neural Networks (SNN) is pro-posed as an alternative solution for future of computation to conquer the memorybottelneck issue in recent computer architecture. Different spike codings have beendiscussed to improve data transferring and data processing in neuro-inspired compu-tation paradigms. Choosing the appropriate neural network topology could result inbetter performance of computation, recognition and classification. The model of theneuron is another important factor to design and implement SNN systems. The speedof simulation and implementation, ability of integration to the other elements of thenetwork, and suitability for scalable networks are the factors to select a neuron model.The learning algorithms are significant consideration to train the neural network forweight modification. Improving learning in neuromorphic architecture is feasibleby improving the quality of artificial synapse as well as learning algorithm such asSTDP. In this chapter we proposed a new synapse box that can remember and forget.Furthermore, as the most frequent used unsupervised method for network training inSNN is STDP, we analyze and review the various methods of STDP. The sequentialorder of pre- or postsynaptic spikes occurring across a synapse in an interval of timeleads to defining different STDP methods. Based on the importance of stability aswell as Hebbian competition or anti-Hebbian competition the method will be usedin weight modification. We survey the most significant projects that cause makingneuromorphic platform. The advantages and disadvantages of each neuromorphicplatform are introduced in this chapter.

Spiking neural networks (SNNs) equipped with latency coding and spike-timing dependent plasticity rules offer an alternative to solve the data and energy bottlenecks of standard computer vision approaches: they can learn visual features without supervision and can be implemented by ultra-low power hardware architectures. However, their performance in image classification has never been evaluated on recent image datasets. In this paper, we compare SNNs to auto-encoders on three visual recognition datasets, and extend the use of SNNs to color images. The analysis of the results helps us identify some bottlenecks of SNNs: the limits of on-center/off-center coding, especially for color images, and the ineffectiveness of current inhibition mechanisms. These issues should be addressed to build effective SNNs for image recognition.

International audience; Spiking neural networks (SNNs) are good candidates to produce ultra-energy-efficient hardware. However, the performance of these models is currently behind traditional methods. Introducing multi-layered SNNs is a promising way to reduce this gap. We propose in this paper a new threshold adaptation system which uses a timestamp objective at which neurons should fire. We show that our method leads to state-of-the-art classification rates on the MNIST dataset (98.60%) and the Faces/Motorbikes dataset (99.46%) with an unsupervised SNN followed by a linear SVM. We also investigate the sparsity level of the network by testing different inhibition policies and STDP rules.

International audience; Neural networks are one of the most well-known artificial intelligence technique. These networks have known a huge evolution since their first proposal, represented by the three known generations. On the other hand, neuromorphic architectures are a very promising way to overcome the limitation of the Von Neumann architecture and the end of Moore's law. Neuromorphic architectures can lead to a huge energy consumption decrease mostly due to the colocation of computation and storage. These architectures implement spiking neural networks (SNNs), the third generation of artificial neural networks that model very finely biological neural networks. One of the main problematics that prevents us from optimizing and getting the best performance of SNNs and as a result the neuromorphic architectures development and production, is the lack of a clear and complete understanding of their behavior, especially what makes learning efficient. One of the approaches to answer that is analyzing by visualization of simulation traces of such networks and architectures. In this paper, we propose a comparison of the visualization techniques proposed by SNN simulators for analysis purposes.

The memory wall or Von Neumann memory bottleneck decreases the speed of computation in conventional digital platforms. It is due to disharmony of communication speed as well as physical distance between the CPU and memory. In Spiking Neural Network (SNN), both memory and computational elements are integrated into the body of each neuron which provides the possibility of cognitive computing with learning ability in a platform without memory bottleneck. The way of updating the synaptic weights is one of the significant challenges in implementing machine learning methods using spiking model of neurons. Deep Belief learning method recently is used in several state-of-the-art studies due to its potential in robustness computation, pattern recognition, and data classification. In this paper, we use a rate based version of Contrastive Divergence (CD) updating weight rule. Respecting the rate aspect of neural coding, we develop a Spike-Based Deep Belief Network (S-DBN) using Leaky Integrate-and-Fire (LIF) neurons. In experimental evaluations, a two stacked RBMs model is validated using MNIST hand-written digit dataset. The learning accuracy of this architecture is 94.9% yet less than state-of-the-art of Artificial Neural Network (ANN) accuracy, however, quite promising with SNN architecture suitable for hardware implementation. To enhance the accuracy of the network recognition rate, we studied the impacts of notable network parameters for both learning as well as neuron models. Based on the experimental results in this work, choosing optimized parameters for learning rate between 0.008 and 0.01, a frequency of input spikes 18 Hz, the sizes of mini-batches between 25 and 50, and two different membrane voltage thresholds for hidden and visible layers leads to the optimum results in the accuracy rate of the network recognition.

International audience; Understanding brain mechanisms and its problem solving techniques is the motivation of many emerging brain inspired computation methods. In this paper, respecting deep architecture of the brain and spiking model of biological neural networks, we propose a spiking deep belief network to evaluate ability of the deep spiking neural networks in face recognition application on ORL dataset. To overcome the change of using spiking neural networks in a deep learning algorithm, Siegert model is utilized as an abstract neuron model. Although there are state of the art classic machine learning algorithms for face detection, this work is mainly focused on demonstrating capabilities of brain inspired models in this era, which can be serious candidate for future hardware oriented deep learning implementations. Accordingly, the proposed model, because of using leaky integrate-and-fire neuron model, is compatible to be used in efficient neuromorphic platforms for accelerators and hardware implementation.

International audience; Memristor is a two-terminal nanodevice that has recently attracted the attention of many researchers. Its simple structure, non-volatility behavior, high-density integra-tion, and low-power consumption make the memristor a promising candidate to act as a switch in digital gates for future high-performance and low-power nanocom-puting applications. In this paper, we model the behavior of memristor by using Verilog-A. To investigate its char-acteristics in a circuit, we use the HSPICE simulator. Furthermore, a library of digital gates are provided by using two approaches to make digital gates: the first one is based on material implication (IMP) and the second one is based on crossbar arrays. Finally, we perform a comparison and evaluation between the two methods.

Set constraints (SC) are logical formul\ae in which atoms are inclusions between set expressions. Those set expressions are built over a signature \Sigma, variables and various set operators. On a semantical point of view, the set constraints are interpreted over sets of trees built from \Sigma and the inclusion symbol is interpreted as the subset relation over those sets. By restricting the syntax of those formul\ae and/or the set of operators that can occur in set expressions, different classes of set constraints are obtained. Several classes have been proposed and studied for some problems such as satisfiability and entailment. Among those classes, we focus in this article on the class of definite SC‘s introduced by Heintze and Jaffar, and the class of co-definite SC‘s studied by Charatonik and Podelski. In spite of their name, those two classes are not dual from each other, neither through inclusion inversion nor through complementation. In this article, we propose an extension for each of those two classes by means of an intentional set construction, so called membership expression. A membership expression is an expression \{x\mid \Phi(x)\}. The formula \Phi(x) is a positive first-order formula built from membership atoms t \in S in which S is a set expression. We name those two classes respectively generalized definite and generalized co-definite set constraints. One of the main point concerning those so-extended classes is that the two generalized classes turn out to be dual through complementation. First, we prove in this article that generalized definite set constraints is a proper extension of the definite class, as it is more expressive in terms of sets of solutions. But we show also that those extensions preserve some main properties of the definite and co-definite class. Hence for instance, as definite set constraints, generalized definite SC‘s have a least solution whereas the generalized co-definite SC‘s have a greatest solution, just as co-definite ones. Furthermore, we devise an algorithm based on tree automata that solves the satisfiability problem for generalized definite set constraints. Due to the dualization, the algorithm solves the satisfiability problem for generalized co-definite set constraints as well. This algorithm proves first that for those generalized classes, the satisfiability problem remains DEXPTIME-complete. It provides also a proof for regularity of the least solution of generalized definite constraints and so, by dualization for the greatest solution for the generalized co-definite SC‘s.

International audience; Model Driven Architecture (MDA) design approach proposes to separate design into two stages: implementation independent stage then an implementation-dependent one. This improves the reusability, the reusability, the standability, the maintainability, etc. Here we show how MDA can be augmented using a formal refinement approach: B method. Doing so enables to gradually refine the development from the abstract specification to the executing implementation; furthermore it permits to prove the coherence between components in low levels even if they are implemented in different technologies.

This paper shows the need of development by refinement: from most abstract specification to the implementation, in order to ensure 1) the traceability of the needs and requirements, 2) a good management of the development and 3) a reliable and fault-tolerant design of systems. We propose a formal architecture of models and methods for critical requirements and fault-tolerance. System complexity increases and the choices of their implementation are numerous. So the architecture verification achieves a prominent role in the system design cycle. Fault detecting at this early level decreases the time and costs of correction. We show how a formal method, B method, may be used to write the abstract specification of a system then to product correct-by-construction architecture through many steps of formal refinement. During these steps, a fault scenario is injected with a suitable introspective reaction by the system. All refinement steps, including the introspective correction, should be proven to be correct and satisfy the initial specification of the system. At the lower levels, design is separated between hardware and software communities. But even at these levels many design traces could be captured to prove not only the consistency of each design unit but the coherence between the different sub-parts: software, digital or other technologies

This paper focuses on entry design of complex systems and step-wise refinement. Indeed, design of embedded systems and digital circuits is moving to higher levels of abstraction and mix different technologies (hardware, software, etc). The entry design represents the highest abstract tier of the global system without implementation choices with respect to such and such technologies. At this level, the use of a formal specification language is more and more considered as the foundation of real verification process. What we would like to emphasize is that the refinement from that model to the point where the system could be implemented could be and should be formal too in order to design systems correct by proven construction. An illustration of this approach is the BHDL tool.

The main goal of this project is to provide a method of correct design of digital circuit. It combines the advantages of VHDL, the well-known language of circuit design, with the power of B method that guarantees the correct design (w.r.t. a formal specification). This allows avoiding the design test since it is "correct by proven construction". Furthermore, this project provides a tool, called BHDL, with a graphical interface for creating, editing, viewing and proving modular hardware architectures.

Set constraints is a suitable formalism for static analysis of programs. However, it is known that the complexity of set constraint problems in the most general cases is very high (NEXPTIME-completeness of the satisfiability test). Lots of works are involved in finding more tractable subclasses. In this paper, we investigate two classes of set constraints shown to be useful for program analysis: the first one is an extension of definite set constraints including the main feature of quantified set expressions. We will show that the satisfiability problem for this class is EXPTIME-complete. The second one concerns constraints of the form Xexp, where exp is built with function symbols, the intersection and union connectives and projection operators. The dual aspects of those two classes allows to find a common approach for solving both of them. This approach uses as basic tool tree automata, which axe suitable both for computation and representing the solution of those solving problems. It leads also to simple algorithms and an easy characterization of complexity. This work was supported in part by the HCM project CONSOLE (CHRXCT940495)

Y a-t-il de la pensee, ou de la conscience, ou de la souffrance, ou de la peur plutot que rien ? Quelque chose serait-il dissimule par ce silence animal comme un secret dans un non-dit de fait ? Il est propose des elements reflexifs permettant de refuter les raisonnements analogiques, inductifs et hypothetiques, pour decouvrir l’usage des mots « conscience », « souffrance », « pensee », « peur », de ces mots qui jouent un role dans notre vie avec les animaux.

This paper proposes an equivalent form of the famous Bohm-Jacopini theorem for declarative languages. C. Bohm and G. Jacopini [1] proved that all programming can be done with at most one single whiledo. That result is cited as a mathematical justification for structured programming. A similar result can be shown for declarative programming. Indeed the simplest class of recursive programs in Horn clause languages can be defined by the following scheme