Campus Event Calendar
Event Entry
What and Who
Expanding the Horizons of Finite-Precision Analysis
Debasmita Lohar
MMCI
SWS Student Defense Talks - Thesis Proposal
SWS
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 27 June 2022
11:00
60 Minutes
E1 5
029
Saarbrücken
Abstract
Finite-precision programs inevitably introduce numerical uncertainties,
which are usually a combination of input uncertainties due to noisy
sensors of the underlying hardware and finite-precision errors that can
potentially occur at every operation. While these errors are
individually small, they propagate through an application and can make
its final results meaningless. Furthermore, an implementation on actual
hardware necessitates a trade-off between accuracy and efficiency. It
is thus essential to verify that the numerical uncertainties remain
acceptably small and to optimize the implementations such that the
results are accurate enough for the applications.
There exist several static (or dynamic) analyses for finite-precision
programs. The static analyses generally perform sound worst-case
analysis and primarily focus on straight-line special syntax code, with
limited support for conditionals and loops. In contrast, dynamic
analyses usually scale well for real-world programs. However, the
current dynamic analyses of finite-precision are limited to relatively
small programs. Moreover, they do not provide any correctness guarantee
that is crucial for critical applications.
In this thesis, we propose analysis and optimization techniques to
expand the horizons of the current finite-precision analysis. Our
approach captures the probability distributions of inputs and performs
probabilistic analysis for small but exciting embedded and neural
network examples. Using our analysis, it is possible to (conditionally)
verify larger programs (with more than 2K lines of code, including complex
programming and data structures). Furthermore, we enable program optimization by
soundly generating quantized neural network classifiers with millions of
parameters and fewer bits significantly faster than (generic) static fixed-point
arithmetic tuners. Finally, we aim to scale the analysis for larger programs with
probabilistic inputs.
which are usually a combination of input uncertainties due to noisy
sensors of the underlying hardware and finite-precision errors that can
potentially occur at every operation. While these errors are
individually small, they propagate through an application and can make
its final results meaningless. Furthermore, an implementation on actual
hardware necessitates a trade-off between accuracy and efficiency. It
is thus essential to verify that the numerical uncertainties remain
acceptably small and to optimize the implementations such that the
results are accurate enough for the applications.
There exist several static (or dynamic) analyses for finite-precision
programs. The static analyses generally perform sound worst-case
analysis and primarily focus on straight-line special syntax code, with
limited support for conditionals and loops. In contrast, dynamic
analyses usually scale well for real-world programs. However, the
current dynamic analyses of finite-precision are limited to relatively
small programs. Moreover, they do not provide any correctness guarantee
that is crucial for critical applications.
In this thesis, we propose analysis and optimization techniques to
expand the horizons of the current finite-precision analysis. Our
approach captures the probability distributions of inputs and performs
probabilistic analysis for small but exciting embedded and neural
network examples. Using our analysis, it is possible to (conditionally)
verify larger programs (with more than 2K lines of code, including complex
programming and data structures). Furthermore, we enable program optimization by
soundly generating quantized neural network classifiers with millions of
parameters and fewer bits significantly faster than (generic) static fixed-point
arithmetic tuners. Finally, we aim to scale the analysis for larger programs with
probabilistic inputs.
Contact
--email hidden
Virtual Meeting Details
Zoom
921 9616 1367
passcode not visible
logged in users only
Maria-Louise Albrecht, 06/14/2022 13:26 -- Created document.