-
A fast plastic scintillator for low intensity proton beam monitoring
Authors:
Adélie André,
Christophe Hoarau,
Yannick Boursier,
Afef Cherni,
Mathieu Dupont,
Laurent Gallin Martel,
Marie-Laure Gallin Martel,
Alicia Garnier,
Joel Hérault,
Johan-Petter Hofverberg,
Pavel Kavrigin,
Christian Morel,
Jean-François Muraz,
Maxime Pinson,
Giovanni Tripodo,
Daniel Maneval,
Sara Marcatili
Abstract:
In the context of particle therapy monitoring, we are developing a gamma-ray detector to determine the ion range in vivo from the measurement of particle time-of-flight. For this application, a beam monitor capable to tag in time the incident ion with a time resolution below 235 ps FWHM (100 ps rms) is required to provide a start signal for the acquisition. We have therefore developed a dedicated…
▽ More
In the context of particle therapy monitoring, we are developing a gamma-ray detector to determine the ion range in vivo from the measurement of particle time-of-flight. For this application, a beam monitor capable to tag in time the incident ion with a time resolution below 235 ps FWHM (100 ps rms) is required to provide a start signal for the acquisition. We have therefore developed a dedicated detector based on a fast organic scintillator (EJ-204) of 25x25x1 mm3 coupled to four SiPM strips that allow measuring the particle incident position by scintillation light sharing. The prototype was characterised with single protons of energies between 63 and 225 MeV at the MEDICYC and ProteusONE facilities of the Antoine Lacassagne proton therapy centre in Nice. We obtained a time resolution of 120 ps FWHM at 63 MeV, and a spatial resolution of ~2 mm rms for single particles. Two identical detectors also allowed to measure the MEDICYC proton energy with 0.3% accuracy.
△ Less
Submitted 12 November, 2024;
originally announced November 2024.
-
What Operations can be Performed Directly on Compressed Arrays, and with What Error?
Authors:
Tripti Agarwal,
Harvey Dam,
Dorra Ben Khalifa,
Matthieu Martel,
P. Sadayappan,
Ganesh Gopalakrishnan
Abstract:
In response to the rapidly escalating costs of computing with large matrices and tensors caused by data movement, several lossy compression methods have been developed to significantly reduce data volumes. Unfortunately, all these methods require the data to be decompressed before further computations are done. In this work, we develop a lossy compressor that allows a dozen fairly fundamental oper…
▽ More
In response to the rapidly escalating costs of computing with large matrices and tensors caused by data movement, several lossy compression methods have been developed to significantly reduce data volumes. Unfortunately, all these methods require the data to be decompressed before further computations are done. In this work, we develop a lossy compressor that allows a dozen fairly fundamental operations directly on compressed data while offering good compression ratios and modest errors. We implement a new compressor PyBlaz based on the familiar GPU-powered PyTorch framework, and evaluate it on three non-trivial applications, choosing different number systems for internal representation. Our results demonstrate that the compressed-domain operations achieve good scalability with problem sizes while incurring errors well within acceptable limits. To our best knowledge, this is the first such lossy compressor that supports compressed-domain operations while achieving acceptable performance as well as error.
△ Less
Submitted 17 June, 2024;
originally announced June 2024.
-
Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers
Authors:
Céline Bellanger,
Pierre-Loïc Garoche,
Matthieu Martel,
Célia Picard
Abstract:
Signal Temporal Logic (STL) is a convenient formalism to express bounded horizon properties of autonomous critical systems. STL extends LTL to real-valued signals and associates a non-singleton bound interval to each temporal operators. In this work we provide a rigorous encoding of non-nested discrete-time STL formulas into Lustre synchronous observers.
Our encoding provides a three-valued onl…
▽ More
Signal Temporal Logic (STL) is a convenient formalism to express bounded horizon properties of autonomous critical systems. STL extends LTL to real-valued signals and associates a non-singleton bound interval to each temporal operators. In this work we provide a rigorous encoding of non-nested discrete-time STL formulas into Lustre synchronous observers.
Our encoding provides a three-valued online semantics for the observers and therefore enables both the verification of the property and the search of counter-examples. A key contribution of this work is an instrumented proof of the validity of the implementation. Each node is proved correct with respect to the original STL semantics. All the experiments are automated with the Kind2 model-checker and the Z3 SMT solver.
△ Less
Submitted 16 November, 2023;
originally announced November 2023.
-
An Initial Exploration: Learning to Generate Realistic Audio for Silent Video
Authors:
Matthew Martel,
Jackson Wagner
Abstract:
Generating realistic audio effects for movies and other media is a challenging task that is accomplished today primarily through physical techniques known as Foley art. Foley artists create sounds with common objects (e.g., boxing gloves, broken glass) in time with video as it is playing to generate captivating audio tracks. In this work, we aim to develop a deep-learning based framework that does…
▽ More
Generating realistic audio effects for movies and other media is a challenging task that is accomplished today primarily through physical techniques known as Foley art. Foley artists create sounds with common objects (e.g., boxing gloves, broken glass) in time with video as it is playing to generate captivating audio tracks. In this work, we aim to develop a deep-learning based framework that does much the same - observes video in it's natural sequence and generates realistic audio to accompany it. Notably, we have reason to believe this is achievable due to advancements in realistic audio generation techniques conditioned on other inputs (e.g., Wavenet conditioned on text). We explore several different model architectures to accomplish this task that process both previously-generated audio and video context. These include deep-fusion CNN, dilated Wavenet CNN with visual context, and transformer-based architectures. We find that the transformer-based architecture yields the most promising results, matching low-frequencies to visual patterns effectively, but failing to generate more nuanced waveforms.
△ Less
Submitted 23 August, 2023;
originally announced August 2023.
-
Optimizing Bilingual Neural Transducer with Synthetic Code-switching Text Generation
Authors:
Thien Nguyen,
Nathalie Tran,
Liuhui Deng,
Thiago Fraga da Silva,
Matthew Radzihovsky,
Roger Hsiao,
Henry Mason,
Stefan Braun,
Erik McDermott,
Dogan Can,
Pawel Swietojanski,
Lyan Verwimp,
Sibel Oyman,
Tresi Arvizo,
Honza Silovsky,
Arnab Ghoshal,
Mathieu Martel,
Bharat Ram Ambati,
Mohamed Ali
Abstract:
Code-switching describes the practice of using more than one language in the same sentence. In this study, we investigate how to optimize a neural transducer based bilingual automatic speech recognition (ASR) model for code-switching speech. Focusing on the scenario where the ASR model is trained without supervised code-switching data, we found that semi-supervised training and synthetic code-swit…
▽ More
Code-switching describes the practice of using more than one language in the same sentence. In this study, we investigate how to optimize a neural transducer based bilingual automatic speech recognition (ASR) model for code-switching speech. Focusing on the scenario where the ASR model is trained without supervised code-switching data, we found that semi-supervised training and synthetic code-switched data can improve the bilingual ASR system on code-switching speech. We analyze how each of the neural transducer's encoders contributes towards code-switching performance by measuring encoder-specific recall values, and evaluate our English/Mandarin system on the ASCEND data set. Our final system achieves 25% mixed error rate (MER) on the ASCEND English/Mandarin code-switching test set -- reducing the MER by 2.1% absolute compared to the previous literature -- while maintaining good accuracy on the monolingual test sets.
△ Less
Submitted 21 October, 2022;
originally announced October 2022.
-
An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods
Authors:
Farah Benmouhoub,
Pierre-Loïc Garoche,
Matthieu Martel
Abstract:
Nowadays, parallel computing is ubiquitous in several application fields, both in engineering and science. The computations rely on the floating-point arithmetic specified by the IEEE754 Standard. In this context, an elementary brick of computation, used everywhere, is the sum of a sequence of numbers. This sum is subject to many numerical errors in floating-point arithmetic. To alleviate this iss…
▽ More
Nowadays, parallel computing is ubiquitous in several application fields, both in engineering and science. The computations rely on the floating-point arithmetic specified by the IEEE754 Standard. In this context, an elementary brick of computation, used everywhere, is the sum of a sequence of numbers. This sum is subject to many numerical errors in floating-point arithmetic. To alleviate this issue, we have introduced a new parallel algorithm for summing a sequence of floating-point numbers. This algorithm which scales up easily with the number of processors, adds numbers of the same exponents first. In this article, our main contribution is an extensive analysis of its efficiency with respect to several properties: accuracy, convergence and reproducibility. In order to show the usefulness of our algorithm, we have chosen a set of representative numerical methods which are Simpson, Jacobi, LU factorization and the Iterated power method.
△ Less
Submitted 11 May, 2022;
originally announced May 2022.
-
Constrained Precision Tuning
Authors:
Dorra Ben Khalifa,
Matthieu Martel
Abstract:
Precision tuning or customized precision number representations is emerging, in these recent years, as one of the most promising techniques that has a positive impact on the footprint of programs concerning energy consumption, bandwidth usage and computation time of numerical programs. In contrast to the uniform precision, mixed precision tuning assigns different finite-precision types to each var…
▽ More
Precision tuning or customized precision number representations is emerging, in these recent years, as one of the most promising techniques that has a positive impact on the footprint of programs concerning energy consumption, bandwidth usage and computation time of numerical programs. In contrast to the uniform precision, mixed precision tuning assigns different finite-precision types to each variable and arithmetic operation of a program and offers many additional optimization opportunities. However, this technique introduces new challenge related to the cost of operations or type conversions which can overload the program execution after tuning. In this article, we extend our tool POP (Precision OPtimizer), with efficient ways to limit the number of drawbacks of mixed precision and to achieve best compromise between performance and memory consumption. On a popular set of tests from the FPBench suite, we discuss the results obtained by POP.
△ Less
Submitted 14 March, 2022;
originally announced March 2022.
-
Compressed Matrix Computations
Authors:
Matthieu Martel
Abstract:
Frugal computing is becoming an important topic for environmental reasons. In this context, several techniques have been proposed to reduce the storage of scientific data by dedicated compression methods specially tailored for arrays of floating-point numbers. While these techniques are quite efficient to save memory, they introduce additional computations to compress and decompress the data befor…
▽ More
Frugal computing is becoming an important topic for environmental reasons. In this context, several techniques have been proposed to reduce the storage of scientific data by dedicated compression methods specially tailored for arrays of floating-point numbers. While these techniques are quite efficient to save memory, they introduce additional computations to compress and decompress the data before processing them. In this article, we introduce a new lossy, fixed-rate compression technique for 2D-arrays of floating-point numbers which allows one to compute directly on the compressed data, without decompressing them. We obtain important speedups since less operations are needed to compute among the compressed data and since no decompression and re-compression is needed. More precisely, our technique makes it possible to perform basic linear algebra operations such as addition, multiplication by a constant among compressed matrices and dot product and matrix multiplication among partly uncompressed matrices. This work has been implemented into a tool named blaz and a comparison with the well-known compressor zfp in terms of execution-time and accuracy is presented.
△ Less
Submitted 25 February, 2022;
originally announced February 2022.
-
Fixed-Point Code Synthesis For Neural Networks
Authors:
Hanane Benmaghnia,
Matthieu Martel,
Yassamine Seladji
Abstract:
Over the last few years, neural networks have started penetrating safety critical systems to take decisions in robots, rockets, autonomous driving car, etc. A problem is that these critical systems often have limited computing resources. Often, they use the fixed-point arithmetic for its many advantages (rapidity, compatibility with small memory devices.) In this article, a new technique is introd…
▽ More
Over the last few years, neural networks have started penetrating safety critical systems to take decisions in robots, rockets, autonomous driving car, etc. A problem is that these critical systems often have limited computing resources. Often, they use the fixed-point arithmetic for its many advantages (rapidity, compatibility with small memory devices.) In this article, a new technique is introduced to tune the formats (precision) of already trained neural networks using fixed-point arithmetic, which can be implemented using integer operations only. The new optimized neural network computes the output with fixed-point numbers without modifying the accuracy up to a threshold fixed by the user. A fixed-point code is synthesized for the new optimized neural network ensuring the respect of the threshold for any input vector belonging the range [xmin, xmax] determined during the analysis. From a technical point of view, we do a preliminary analysis of our floating neural network to determine the worst cases, then we generate a system of linear constraints among integer variables that we can solve by linear programming. The solution of this system is the new fixed-point format of each neuron. The experimental results obtained show the efficiency of our method which can ensure that the new fixed-point neural network has the same behavior as the initial floating-point neural network.
△ Less
Submitted 4 February, 2022;
originally announced February 2022.
-
A Study of the Floating-Point Tuning Behaviour on the N-body Problem
Authors:
Dorra Ben Khalifa,
Matthieu Martel
Abstract:
In this article, we apply a new methodology for precision tuning to the N-body problem. Our technique, implemented in a tool named POP, makes it possible to optimize the numerical data types of a program performing floating-point computations by taking into account the requested accuracy on the results. POP reduces the problem of finding the minimal number of bits needed for each variable of the p…
▽ More
In this article, we apply a new methodology for precision tuning to the N-body problem. Our technique, implemented in a tool named POP, makes it possible to optimize the numerical data types of a program performing floating-point computations by taking into account the requested accuracy on the results. POP reduces the problem of finding the minimal number of bits needed for each variable of the program to an Integer Linear Problem (ILP) which can be optimally solved in one shot by a classical linear programming solver. The POP tool has been successfully tested on programs implementing several numerical algorithms coming from mathematical libraries and other applicative domains such as IoT. In this work, we demonstrate the efficiency of POP to tune the classical gravitational N-body problem by considering five bodies that interact under gravitational force from one another, subject to Newton's laws of motion. Results on the effect of POP in term of mixed-precision tuning of the N-body example are discussed.
△ Less
Submitted 31 July, 2021;
originally announced August 2021.
-
Interleaving & Reconfigurable Interaction: Separating Choice from Scheduling using Glue
Authors:
Yehia Abd Alrahman,
Mauricio Martel,
Nir Piterman
Abstract:
Reconfigurable interaction induces another dimension of nondeterminism in concurrent systems which makes it hard to reason about the different choices of the system from a global perspective. Namely, (1) choices that correspond to concurrent execution of independent events; and (2) forced interleaving (or scheduling) due to reconfiguration. Unlike linear order semantics of computations, partial or…
▽ More
Reconfigurable interaction induces another dimension of nondeterminism in concurrent systems which makes it hard to reason about the different choices of the system from a global perspective. Namely, (1) choices that correspond to concurrent execution of independent events; and (2) forced interleaving (or scheduling) due to reconfiguration. Unlike linear order semantics of computations, partial order semantics recovers information about the interdependence among the different events for fixed interaction, but still is unable to handle reconfiguration. We introduce glued partial orders as a way to capture reconfiguration. Much like partial orders capture all possible choices for fixed systems, glued partial orders capture all possible choices alongside reconfiguration. We show that a glued partial order is sufficient to correctly capture all partial order computations that differ in forced interleaving due to reconfiguration. Furthermore, we show that computations belonging to different glued partial orders are only different due to non-determinism.
△ Less
Submitted 30 July, 2021;
originally announced July 2021.
-
Fast and Efficient Bit-Level Precision Tuning
Authors:
Assalé Adjé,
Dorra Ben Khalifa,
Matthieu Martel
Abstract:
In this article, we introduce a new technique for precision tuning. This problem consists of finding the least data types for numerical values such that the result of the computation satisfies some accuracy requirement. State of the art techniques for precision tuning use a try and fail approach. They change the data types of some variables of the program and evaluate the accuracy of the result. D…
▽ More
In this article, we introduce a new technique for precision tuning. This problem consists of finding the least data types for numerical values such that the result of the computation satisfies some accuracy requirement. State of the art techniques for precision tuning use a try and fail approach. They change the data types of some variables of the program and evaluate the accuracy of the result. Depending on what is obtained, they change more or less data types and repeat the process. Our technique is radically different. Based on semantic equations, we generate an Integer Linear Problem (ILP) from the program source code. Basically, this is done by reasoning on the most significant bit and the number of significant bits of the values which are integer quantities. The integer solution to this problem, computed in polynomial time by a (real) linear programming solver, gives the optimal data types at the bit level. A finer set of semantic equations is also proposed which does not reduce directly to an ILP problem. So we use policy iteration to find the solution. Both techniques have been implemented and we show that our results encompass the results of state of the art tools.
△ Less
Submitted 9 March, 2021;
originally announced March 2021.
-
Conservative Extensions in Horn Description Logics with Inverse Roles
Authors:
Jean Christoph Jung,
Carsten Lutz,
Mauricio Martel,
Thomas Schneider
Abstract:
We investigate the decidability and computational complexity of conservative extensions and the related notions of inseparability and entailment in Horn description logics (DLs) with inverse roles. We consider both query conservative extensions, defined by requiring that the answers to all conjunctive queries are left unchanged, and deductive conservative extensions, which require that the entaile…
▽ More
We investigate the decidability and computational complexity of conservative extensions and the related notions of inseparability and entailment in Horn description logics (DLs) with inverse roles. We consider both query conservative extensions, defined by requiring that the answers to all conjunctive queries are left unchanged, and deductive conservative extensions, which require that the entailed concept inclusions, role inclusions, and functionality assertions do not change. Upper bounds for query conservative extensions are particularly challenging because characterizations in terms of unbounded homomorphisms between universal models, which are the foundation of the standard approach to establishing decidability, fail in the presence of inverse roles. We resort to a characterization that carefully mixes unbounded and bounded homomorphisms and enables a decision procedure that combines tree automata and a mosaic technique. Our main results are that query conservative extensions are 2ExpTime-complete in all DLs between ELI and Horn-ALCHIF and between Horn-ALC and Horn-ALCHIF, and that deductive conservative extensions are 2ExpTime-complete in all DLs between ELI and ELHIF_\bot. The same results hold for inseparability and entailment.
△ Less
Submitted 19 November, 2020;
originally announced November 2020.
-
Conservative Extensions in Guarded and Two-Variable Fragments
Authors:
Jean Christoph Jung,
Carsten Lutz,
Mauricio Martel,
Thomas Schneider,
Frank Wolter
Abstract:
We investigate the decidability and computational complexity of (deductive) conservative extensions in fragments of first-order logic (FO), with a focus on the two-variable fragment FO$^2$ and the guarded fragment GF. We prove that conservative extensions are undecidable in any FO fragment that contains FO$^2$ or GF (even the three-variable fragment thereof), and that they are decidable and 2\ExpT…
▽ More
We investigate the decidability and computational complexity of (deductive) conservative extensions in fragments of first-order logic (FO), with a focus on the two-variable fragment FO$^2$ and the guarded fragment GF. We prove that conservative extensions are undecidable in any FO fragment that contains FO$^2$ or GF (even the three-variable fragment thereof), and that they are decidable and 2\ExpTime-complete in the intersection GF$^2$ of FO$^2$ and GF.
△ Less
Submitted 29 May, 2017;
originally announced May 2017.
-
Relation-Changing Logics as Fragments of Hybrid Logics
Authors:
Carlos Areces,
Raul Fervari,
Guillaume Hoffmann,
Mauricio Martel
Abstract:
Relation-changing modal logics are extensions of the basic modal logic that allow changes to the accessibility relation of a model during the evaluation of a formula. In particular, they are equipped with dynamic modalities that are able to delete, add, and swap edges in the model, both locally and globally. We provide translations from these logics to hybrid logic along with an implementation. I…
▽ More
Relation-changing modal logics are extensions of the basic modal logic that allow changes to the accessibility relation of a model during the evaluation of a formula. In particular, they are equipped with dynamic modalities that are able to delete, add, and swap edges in the model, both locally and globally. We provide translations from these logics to hybrid logic along with an implementation. In general, these logics are undecidable, but we use our translations to identify decidable fragments. We also compare the expressive power of relation-changing modal logics with hybrid logics.
△ Less
Submitted 13 September, 2016;
originally announced September 2016.
-
Automatic Repair of Overflowing Expressions with Abstract Interpretation
Authors:
Francesco Logozzo,
Matthieu Martel
Abstract:
We consider the problem of synthesizing provably non-overflowing integer arithmetic expressions or Boolean relations among integer arithmetic expressions. First we use a numerical abstract domain to infer numerical properties among program variables. Then we check if those properties guarantee that a given expression does not overflow. If this is not the case, we synthesize an equivalent, yet not-…
▽ More
We consider the problem of synthesizing provably non-overflowing integer arithmetic expressions or Boolean relations among integer arithmetic expressions. First we use a numerical abstract domain to infer numerical properties among program variables. Then we check if those properties guarantee that a given expression does not overflow. If this is not the case, we synthesize an equivalent, yet not-overflowing expression, or we report that such an expression does not exists.
The synthesis of a non-overflowing expression depends on three, orthogonal factors: the input expression (e.g., is it linear, polynomial,... ?), the output expression (e.g., are case splits allowed?), and the underlying numerical abstract domain - the more precise the abstract domain is, the more correct expressions can be synthesized.
We consider three common cases: (i) linear expressions with integer coefficients and intervals; (ii) Boolean expressions of linear expressions; and (iii) linear expressions with templates. In the first case we prove there exists a complete and polynomial algorithm to solve the problem. In the second case, we have an incomplete yet polynomial algorithm, whereas in the third we have a complete yet worst-case exponential algorithm.
△ Less
Submitted 19 September, 2013;
originally announced September 2013.
