-
Stochastic rounding and reduced-precision fixed-point arithmetic for solving neural ordinary differential equations
Authors:
Michael Hopkins,
Mantas Mikaitis,
Dave R. Lester,
Steve Furber
Abstract:
Although double-precision floating-point arithmetic currently dominates high-performance computing, there is increasing interest in smaller and simpler arithmetic types. The main reasons are potential improvements in energy efficiency and memory footprint and bandwidth. However, simply switching to lower-precision types typically results in increased numerical errors. We investigate approaches to…
▽ More
Although double-precision floating-point arithmetic currently dominates high-performance computing, there is increasing interest in smaller and simpler arithmetic types. The main reasons are potential improvements in energy efficiency and memory footprint and bandwidth. However, simply switching to lower-precision types typically results in increased numerical errors. We investigate approaches to improving the accuracy of reduced-precision fixed-point arithmetic types, using examples in an important domain for numerical computation in neuroscience: the solution of Ordinary Differential Equations (ODEs). The Izhikevich neuron model is used to demonstrate that rounding has an important role in producing accurate spike timings from explicit ODE solution algorithms. In particular, fixed-point arithmetic with stochastic rounding consistently results in smaller errors compared to single precision floating-point and fixed-point arithmetic with round-to-nearest across a range of neuron behaviours and ODE solvers. A computationally much cheaper alternative is also investigated, inspired by the concept of dither that is a widely understood mechanism for providing resolution below the least significant bit (LSB) in digital signal processing. These results will have implications for the solution of ODEs in other subject areas, and should also be directly relevant to the huge range of practical problems that are represented by Partial Differential Equations (PDEs).
△ Less
Submitted 22 January, 2020; v1 submitted 25 April, 2019;
originally announced April 2019.
-
SpiNNTools: The Execution Engine for the SpiNNaker Platform
Authors:
Andrew G. D. Rowley,
Christian Brenninkmeijer,
Simon Davidson,
Donal Fellows,
Andrew Gait,
David R. Lester,
Luis A. Plana,
Oliver Rhodes,
Alan B. Stokes,
Steve B. Furber
Abstract:
Distributed systems are becoming more common place, as computers typically contain multiple computation processors. The SpiNNaker architecture is such a distributed architecture, containing millions of cores connected with a unique communication network, making it one of the largest neuromorphic computing platforms in the world. Utilising these processors efficiently usually requires expert knowle…
▽ More
Distributed systems are becoming more common place, as computers typically contain multiple computation processors. The SpiNNaker architecture is such a distributed architecture, containing millions of cores connected with a unique communication network, making it one of the largest neuromorphic computing platforms in the world. Utilising these processors efficiently usually requires expert knowledge of the architecture to generate executable code. This work introduces a set of tools (SpiNNTools) that can map computational work described as a graph in to executable code that runs on this novel machine. The SpiNNaker architecture is highly scalable which in turn produces unique challenges in loading data, executing the mapped problem and the retrieval of data. In this paper we describe these challenges in detail and the solutions implemented.
△ Less
Submitted 16 October, 2018;
originally announced October 2018.
-
Verified Real Number Calculations: A Library for Interval Arithmetic
Authors:
Marc Daumas,
David Lester,
César Muñoz
Abstract:
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a r…
▽ More
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations take place in an algebraic setting. In order to reduce the dependency effect of interval arithmetic, we integrate two techniques: interval splitting and taylor series expansions. This pragmatic approach has been developed, and formally verified, in a theorem prover. The formal development also includes a set of customizable strategies to automate proofs involving explicit calculations over real numbers. Our ultimate goal is to provide guaranteed proofs of numerical properties with minimal human theorem-prover interaction.
△ Less
Submitted 28 August, 2007;
originally announced August 2007.
-
Stochastic Formal Methods for Hybrid Systems
Authors:
Marc Daumas,
David Lester,
Erik Martin-Dorel,
Annick Truffert
Abstract:
We provide a framework to bound the probability that accumulated errors were never above a given threshold on hybrid systems. Such systems are used for example to model an aircraft or a nuclear power plant on one side and its software on the other side. This report contains simple formulas based on Lévy's and Markov's inequalities and it presents a formal theory of random variables with a specia…
▽ More
We provide a framework to bound the probability that accumulated errors were never above a given threshold on hybrid systems. Such systems are used for example to model an aircraft or a nuclear power plant on one side and its software on the other side. This report contains simple formulas based on Lévy's and Markov's inequalities and it presents a formal theory of random variables with a special focus on producing concrete results. We selected four very common applications that fit in our framework and cover the common practices of hybrid systems that evolve for a long time. We compute the number of bits that remain continuously significant in the first two applications with a probability of failure around one against a billion, where worst case analysis considers that no significant bit remains. We are using PVS as such formal tools force explicit statement of all hypotheses and prevent incorrect uses of theorems.
△ Less
Submitted 24 February, 2009; v1 submitted 18 October, 2006;
originally announced October 2006.
-
Stochastic Formal Methods: An application to accuracy of numeric software
Authors:
Marc Daumas,
David Lester
Abstract:
This paper provides a bound on the number of numeric operations (fixed or floating point) that can safely be performed before accuracy is lost. This work has important implications for control systems with safety-critical software, as these systems are now running fast enough and long enough for their errors to impact on their functionality. Furthermore, worst-case analysis would blindly advise…
▽ More
This paper provides a bound on the number of numeric operations (fixed or floating point) that can safely be performed before accuracy is lost. This work has important implications for control systems with safety-critical software, as these systems are now running fast enough and long enough for their errors to impact on their functionality. Furthermore, worst-case analysis would blindly advise the replacement of existing systems that have been successfully running for years. We present here a set of formal theorems validated by the PVS proof assistant. These theorems will allow code analyzing tools to produce formal certificates of accurate behavior. For example, FAA regulations for aircraft require that the probability of an error be below $10^{-9}$ for a 10 hour flight.
△ Less
Submitted 19 December, 2006; v1 submitted 23 June, 2006;
originally announced June 2006.
