Expanding the horizons of finite-precision analysis

Abstract

Numerical programs are ubiquitous across many domains, including embedded systems, scientific computing, and machine learning. These programs utilize finite precision computations that inevitably introduce numerical uncertainties. These uncertainties are usually a combination of input uncertainties arising from, e.g., the noisy sensors of the underlying hardware and finite-precision (roundoff) errors that can occur at every arithmetic operation. While these errors are individually small, they can propagate through an application unintuitively and can make the final results meaningless. Thus, it is essential to verify that numerical errors in a program remain acceptably small. In addition to ensuring accuracy, implementing finite-precision programs on real hardware also necessitates efficiency in terms of resource usage. While precise data types can yield accurate results, they often come at the cost of increased resources, such as execution time and chip area. Thus, optimizing the implementations to strike a balance between accuracy and efficiency for specific hardware applications is crucial. Several static and dynamic analyses exist to verify and estimate roundoff errors, to test, and to optimize the precision of finite-precision programs. Static analyses typically perform sound worst-case analysis but are primarily designed for straight-line special syntax code, with limited support for conditionals and loops. These limitations also extend to sound optimization techniques. Similarly, the current dynamic analyses are also limited by their inherent inability to provide soundness guarantees and to detect errors in large-scale programs within a reasonable time, primarily due to the complexities associated with finite precision. In this thesis, we address three limitations of state-of-the-art analysis and optimization techniques, thus expanding the individual capabilities of these analyses for finite-precision programs. First, we introduce probabilistic analysis for finite-precision programs that goes beyond traditional worst-case analyses by capturing the effects of probabilistic inputs. We explore two important issues in this context. Our first contribution is a probabilistic analysis that takes into account the effects of numerical uncertainties on discrete decisions for both floating-point and fixed-point programs. Secondly, we present the first sound probabilistic error analysis for floating-point programs. The error analysis also handles probabilistic error specifications prevalent in today’s approximate hardware. Our evaluation shows that these two analyses can analyze small but exciting embedded and neural network programs from the literature with arithmetic and elementary operations. Next, we propose a two-phase framework that combines static and dynamic analyses to address their scalability issues for numerical programs. By integrating these approaches, we are able to (conditionally) verify the absence of special floating-point values (NaN and Infinities) and large roundoff errors in more extensive programs with more than 2K lines of C and C++ code. This framework handles complex programming structures and intricate data representations, thus broadening the scope of numerical program verification. Finally, we present the first sound mixed-precision fixed-point quantization technique tailored specifically for neural networks. This technique efficiently optimizes the number of bits needed to implement a network while guaranteeing a provided error bound. An extensive evaluation on existing embedded neural controller benchmarks shows that our technique outperforms generic static fixed-point precision tuners. Our technique enables scalable and efficient optimization in terms of machine cycles when compiled to an FPGA, particularly for large-scale neural networks with thousands of parameters.

Numerische Programme sind in vielen Bereichen allgegenwärtig, darunter in eingebetteten Systemen, wissenschaftlichem Rechnen und maschinellem Lernen. Diese Programme verwenden Berechnungen mit endlicher Präzision, die zwangsläufig numerische Unsicherheiten mit sich bringen. Diese Unsicherheiten sind in der Regel eine Kombination aus Eingabeunsicherheiten, die beispielsweise durch verrauschte Sensoren der zugrunde liegenden Hardware entstehen, und Fehlern durch endliche Genauigkeit (Rundungsfehler), die bei jeder Rechenoperation auftreten können. Auch wenn diese Fehler individuell klein sind, können sie sich unintuitiv durch eine Anwendung ausbreiten und dazu führen, dass die Endergebnisse bedeutungslos werden. Daher ist es wichtig zu überprüfen, ob numerische Fehler in einem Programm akzeptabel klein bleiben. Neben der Sicherstellung der Genauigkeit erfordert die Implementierung von Programmen mit endlicher Präzision auf realer Hardware auch eine effiziente Ressourcennutzung. Während präzise Datentypen genaue Ergebnisse liefern können, gehen sie oft mit höheren Ressourcen wie Ausführungszeit und Chipfläche einher. Daher ist es von entscheidender Bedeutung, die Implementierungen zu optimieren, um ein Gleichgewicht zwischen Genauigkeit und Effizienz für bestimmte Hardwareanwendungen zu finden. Es gibt mehrere statische und dynamische Analysen, um Rundungsfehler zu überprüfen und abzuschätzen, um die Präzision von Programmen mit endlicher Genauigkeit zu testen und zu optimieren. Statische Analysen führen in der Regel eine Worst-Case-Analyse durch, sind jedoch in erster Linie für geradlinigen Code mit spezieller Syntax konzipiert und bieten nur begrenzte Unterstützung für Bedingungen und Schleifen. Diese Einschränkungen erstrecken sich auch auf korrekte Optimierungstechniken. Ebenso sind die aktuellen dynamischen Analysen auch dadurch eingeschränkt, dass sie nicht in der Lage sind, Garantien zu geben und Fehler in umfangreichen Programmen innerhalb einer angemessenen Zeit zu erkennen, was vor allem auf die mit endlicher Präzision verbundenen Komplexitäten zurückzuführen ist. In dieser Arbeit befassen wir uns mit drei Einschränkungen moderner Analyse- und Optimierungstechniken und erweitern die individuellen Möglichkeiten dieser Analysen für Programme mit endlicher Präzision. Zunächst führen wir eine probabilistische Analyse für Programme mit endlicher Genauigkeit ein, die über herkömmliche Worst-Case-Analysen hinausgeht, indem sie die Auswirkungen probabilistischer Eingaben erfasst. Wir untersuchen in diesem Zusammenhang zwei wichtige Themen. Unser erster Beitrag ist eine probabilistische Analyse, die die Auswirkungen nu- merischer Unsicherheiten auf diskrete Entscheidungen sowohl für Gleitkomma- als auch für Festkommaprogramme berücksichtigt. Zweitens präsentieren wir die erste fundierte proba- bilistische Fehleranalyse für Gleitkommaprogramme. Die Fehleranalyse berücksichtigt auch probabilistische Fehlerspezifikationen, die in heutiger Approximate Hardware vorherrschen. Unsere Auswertung zeigt, dass diese beiden Analysen kleine, aber interessante eingebettete und neuronale Netzwerkprogramme aus der Literatur mit arithmetischen und elementaren Operationen analysieren können. Als nächstes schlagen wir ein zweiphasiges Framework vor, das statische und dynamische Analysen kombiniert, um deren Skalierbarkeitsprobleme für numerische Programme anzugehen. Durch die Integration dieser Ansätze können wir (bedingt) das Fehlen spezieller Gleitkommaw- erte (NaN und Unendlichkeiten) und großer Rundungsfehler in umfangreicheren Programmen mit mehr als 2K Zeilen C- und C++-Code überprüfen. Dieses Framework verarbeitet komplexe Programmierstrukturen und komplizierte Datendarstellungen und erweitert so den Umfang der numerischen Programmverifizierung. Abschließend stellen wir die erste korrekte Festkomma-Quantisierungstechnik mit gemischter Präzision vor, die speziell auf neuronale Netze zugeschnitten ist. Diese Technik optimiert effizient die Anzahl der zur Implementierung eines Netzwerks erforderlichen Bits und garantiert gleichzeitig eine gegebene Fehlergrenze. Eine umfassende Auswertung bestehender Benchmarks für eingebettete neuronale Controller zeigt, dass unsere Technik generische statische Festkomma- Präzisionstuner übertrifft. Unsere Technik ermöglicht eine skalierbare und effiziente Optimierung in Bezug auf Maschinenzyklen, wenn sie in einem FPGA kompiliert wird, insbesondere für große neuronale Netze mit Tausenden von Parametern.