Exploring Approximations for Floating-Point Arithmetic using UppSAT
We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT --- a new implementation of a systematic approximation refinement framework [ZWR17] as an abstract SMT solver. Provided with an approximation and a decision procedure (implemented in an off-the-shelf SMT solver), UppSAT yields an approximating SMT solver. Additionally, UppSAT includes a library of predefined approximation components which can be combined and extended to define new encodings, orderings and solving strategies. We propose that UppSAT can be used as a sandbox for easy and flexible exploration of new approximations. To substantiate this, we explore several approximations of floating-point arithmetic. Approximations can be viewed as a composition of an encoding into a target theory, a precision ordering, and a number of strategies for model reconstruction and precision (or approximation) refinement. We present encodings of floating-point arithmetic into reduced precision floating-point arithmetic, real-arithmetic, and fixed-point arithmetic (encoded in the theory of bit-vectors). In an experimental evaluation, we compare the advantages and disadvantages of approximating solvers obtained by combining various encodings and decision procedures (based on existing state-of-the-art SMT solvers for floating-point, real, and bit-vector arithmetic).
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Bitwidth-Specific Logarithmic Arithmetic for Future Hardware-Accelerated Training
While advancements in quantization have significantly reduced the computational costs of inference in deep learning, training still predominantly relies on complex floating-point arithmetic. Low-precision fixed-point tra…
K-TanH: Efficient TanH For Deep Learning
We propose K-TanH, a novel, highly accurate, hardware efficient approximation of popular activation function TanH for Deep Learning. K-TanH consists of parameterized low-precision integer operations, such as, shift and a…
CPUDeep LearningTranslationLow-Precision Floating-Point Schemes for Neural Network Training
The use of low-precision fixed-point arithmetic along with stochastic rounding has been proposed as a promising alternative to the commonly used 32-bit floating point arithmetic to enhance training neural networks traini…
On the Constructing Bifurcation Diagram of the Quadratic Map With Floating-Point Arithmetic
This paper presents an analysis on the effects of floating-point arithmetic on the constructing bifurcation diagram of the quadratic map. More precisely, we are interested in showing the dependence of initial conditions …
Low-complexity Three-dimensional Discrete Hartley Transform Approximations for Medical Image Compression
The discrete Hartley transform (DHT) is a useful tool for medical image coding. The three-dimensional DHT (3D DHT) can be employed to compress medical image data, such as magnetic resonance and X-ray angiography. However…
Image CompressionPICOSSIM