From a8bb7736e2e86963bd5761cc05079447abeeaba6 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Tue, 23 Jun 2026 15:26:01 +0200 Subject: using official template + fixing language errors --- biblio.bib | 229 +++++++++++++++++++++ chapters/01-introduction.tex | 42 ++-- chapters/02-background.tex | 4 +- chapters/03-core.tex | 4 +- chapters/04-related-work.tex | 2 +- chapters/05-conclusion.tex | 15 +- chapters/background/01-neural-networks.tex | 4 +- chapters/background/02-interaction-nets.tex | 12 +- chapters/core/01-implementation.tex | 2 +- chapters/core/02-soundness-proof.tex | 4 +- chapters/core/03-benchmarks.tex | 15 +- chapters/core/implementation/01-inpla.tex | 18 +- .../core/implementation/02-interaction-rules.tex | 56 ++--- chapters/core/implementation/03-translation.tex | 8 +- chapters/core/implementation/04-python-module.tex | 6 +- .../02-soundness-of-translation.tex | 4 +- .../03-soundness-of-interaction-rules.tex | 66 +++--- .../soundness-proof/04-soundness-of-reduction.tex | 10 +- front.tex | 42 ++++ main.tex | 68 ------ ...unitrento_colore_it_202002-eps-converted-to.pdf | Bin 0 -> 183512 bytes marin_eric_Computer_Science_2026.tex | 202 ++++++++++++++++++ references.bib | 229 --------------------- 23 files changed, 611 insertions(+), 431 deletions(-) create mode 100644 biblio.bib create mode 100644 front.tex delete mode 100644 main.tex create mode 100644 marchio_unitrento_colore_it_202002-eps-converted-to.pdf create mode 100644 marin_eric_Computer_Science_2026.tex delete mode 100644 references.bib diff --git a/biblio.bib b/biblio.bib new file mode 100644 index 0000000..e3a73fc --- /dev/null +++ b/biblio.bib @@ -0,0 +1,229 @@ +@inproceedings{lafont1990interactionnets, + author = {Lafont, Yves}, + title = {Interaction nets}, + year = {1989}, + isbn = {0897913434}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/96709.96718}, + doi = {10.1145/96709.96718}, + abstract = {We propose a new kind of programming language, with the following features:Interaction nets generalize Girard's proof nets of linear logic and illustrate the advantage of an integrated logic approach, as opposed to the external one. In other words, we did not try to design a logic describing the behaviour of some given computational system, but a programming language for which the type discipline is already (almost) a logic.In fact, we shall scarcely refer to logic, because we adopt a na\"{\i}ve and pragmatic style. A typical application we have in mind for this language is the design of interactive softwares such as editors or window managers.}, + booktitle = {Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, + pages = {95–108}, + numpages = {14}, + location = {San Francisco, California, USA}, + series = {POPL '90} +} +@inproceedings{demoura2008z3, + author="de Moura, Leonardo + and Bj{\o}rner, Nikolaj", + editor="Ramakrishnan, C. R. + and Rehof, Jakob", + title="Z3: An Efficient SMT Solver", + booktitle="Tools and Algorithms for the Construction and Analysis of Systems", + year="2008", + publisher="Springer Berlin Heidelberg", + address="Berlin, Heidelberg", + pages="337--340", + abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.", + isbn="978-3-540-78800-3" +} +@misc{kumar2019equivalentapproximatetransformationsdeep, + title={Equivalent and Approximate Transformations of Deep Neural Networks}, + author={Abhinav Kumar and Thiago Serra and Srikumar Ramalingam}, + year={2019}, + eprint={1905.11428}, + archivePrefix={arXiv}, + primaryClass={cs.LG}, + url={https://arxiv.org/abs/1905.11428}, +} +@article{JMLR:v24:21-0579, + author = {Fenglei Fan and Rongjie Lai and Ge Wang}, + title = {Quasi-Equivalence between Width and Depth of Neural Networks}, + journal = {Journal of Machine Learning Research}, + year = {2023}, + volume = {24}, + number = {183}, + pages = {1--22}, + url = {http://jmlr.org/papers/v24/21-0579.html} +} +@misc{kaulen20256thinternationalverificationneural, + title={The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results}, + author={Konstantin Kaulen and Tobias Ladner and Stanley Bak and Christopher Brix and Hai Duong and Thomas Flinkow and Taylor T. Johnson and Lukas Koller and Edoardo Manino and ThanhVu H Nguyen and Haoze Wu}, + year={2025}, + eprint={2512.19007}, + archivePrefix={arXiv}, + primaryClass={cs.LG}, + url={https://arxiv.org/abs/2512.19007}, +} +@article{fisher1936iris, + author = {FISHER, R. A.}, + title = {THE USE OF MULTIPLE MEASUREMENTS IN TAXONOMIC PROBLEMS}, + journal = {Annals of Eugenics}, + volume = {7}, + number = {2}, + pages = {179-188}, + doi = {https://doi.org/10.1111/j.1469-1809.1936.tb02137.x}, + url = {https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1469-1809.1936.tb02137.x}, + eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1111/j.1469-1809.1936.tb02137.x}, + abstract = {The articles published by the Annals of Eugenics (1925–1954) have been made available online as an historical archive intended for scholarly use. The work of eugenicists was often pervaded by prejudice against racial, ethnic and disabled groups. The online publication of this material for scholarly research purposes is not an endorsement of those views nor a promotion of eugenics in any way.}, + year = {1936} +} +@article{lecun2010mnist, + title={MNIST handwritten digit database}, + author={LeCun, Yann and Cortes, Corinna and Burges, CJ}, + journal={ATT Labs [Online]. Available: http://yann.lecun.com/exdb/mnist}, + volume={2}, + year={2010} +} +@InProceedings{eleftheriadis2022equivalence, + author="Eleftheriadis, Charis + and Kekatos, Nikolaos + and Katsaros, Panagiotis + and Tripakis, Stavros", + editor="Bogomolov, Sergiy + and Parker, David", + title="On Neural Network Equivalence Checking Using SMT Solvers", + booktitle="Formal Modeling and Analysis of Timed Systems", + year="2022", + publisher="Springer International Publishing", + address="Cham", + pages="237--257", + abstract="Two pretrained neural networks are deemed (approximately) equivalent if they yield similar outputs for the same inputs. Equivalence checking of neural networks is of great importance, due to its utility in replacing learning-enabled components with (approximately) equivalent ones, when there is need to fulfill additional requirements or to address security threats, as is the case when using knowledge distillation, adversarial training, etc. In this paper, we present a method to solve various strict and approximate equivalence checking problems for neural networks, by reducing them to SMT satisfiability checking problems. This work explores the utility and limitations of the neural network equivalence checking framework, and proposes avenues for future research and improvements toward more scalable and practically applicable solutions. We present experimental results, for diverse types of neural network models (classifiers and regression networks) and equivalence criteria, towards a general and application-independent equivalence checking approach.", + isbn="978-3-031-15839-1" +} + +@article{rosenblatt1958perceptron, + added-at = {2017-07-19T15:29:59.000+0200}, + author = {Rosenblatt, F.}, + biburl = {https://www.bibsonomy.org/bibtex/214ee8da21c66cd4d00d7ab6eca2d96a9/andreashdez}, + citeulike-article-id = {13697582}, + citeulike-linkout-0 = {http://dx.doi.org/10.1037/h0042519}, + doi = {10.1037/h0042519}, + interhash = {dc0cef9dc06033a04f525efdcde7a660}, + intrahash = {14ee8da21c66cd4d00d7ab6eca2d96a9}, + issn = {0033-295X}, + journal = {Psychological Review}, + keywords = {imported}, + number = 6, + pages = {386--408}, + posted-at = {2016-05-02 20:23:36}, + priority = {2}, + timestamp = {2017-07-19T15:31:02.000+0200}, + title = {{The perceptron: A probabilistic model for information storage and organization in the brain.}}, + url = {http://dx.doi.org/10.1037/h0042519}, + volume = 65, + year = 1958 +} +@article{rumelhart1986learning, + title={Learning representations by back-propagating errors}, + author={Rumelhart, David E and Hinton, Geoffrey E and Williams, Ronald J}, + journal={Nature}, + volume={323}, + number={6088}, + pages={533--536}, + year={1986}, + publisher={Nature Publishing Group} +} + +@inproceedings{katz2017reluplex, + title={Reluplex: An efficient SMT solver for verifying deep neural networks}, + author={Katz, Guy and Barrett, Clark and Dill, David L and Julian, Kyle and Kochenderfer, Mykel J}, + booktitle={International Conference on Computer Aided Verification}, + pages={97--117}, + year={2017}, + organization={Springer} +} + +@inproceedings{katz2019marabou, + title={The Marabou framework for verification and analysis of deep neural networks}, + author={Katz, Guy and Huang, Derek A and Ibeling, Duligur and Julian, Kyle and Burns, Ryan and Sadigh, Dorsa and Barrett, Clark and Dill, David L and Kochenderfer, Mykel J}, + booktitle={International Conference on Computer Aided Verification}, + pages={443--452}, + year={2019}, + organization={Springer} +} + +@article{barrett2016smtlib, + title={The SMT-LIB standard: Version 2.6}, + author={Barrett, Clark and Stump, Aaron and Tinelli, Cesare}, + journal={Department of Computer Science, The University of Iowa, Tech. Rep}, + year={2016} +} +@misc{wang2018efficientformalsafetyanalysis, + title={Efficient Formal Safety Analysis of Neural Networks}, + author={Shiqi Wang and Kexin Pei and Justin Whitehouse and Junfeng Yang and Suman Jana}, + year={2018}, + eprint={1809.08098}, + archivePrefix={arXiv}, + primaryClass={cs.LG}, + url={https://arxiv.org/abs/1809.08098}, +} +@incollection{dantzig1947simplex, + abstract = {In 1947, George Dantzig created a simplex algorithm to solve linear programs for planning and decision-making in large-scale enterprises. The algorithm's success led to a vast array of specializations and generalizations that have dominated practical operations research for half a century}, + added-at = {2010-02-26T23:23:28.000+0100}, + address = {Piscataway, NJ, USA}, + author = {Nash, John C.}, + biburl = {https://www.bibsonomy.org/bibtex/2b85e2108e8f7cc402a52577323035ad9/ytyoun}, + booktitle = {Computing in Science and Engg.}, + doi = {10.1109/5992.814654}, + interhash = {5fb3b9e4a0e81f7811c917b86d1097cb}, + intrahash = {b85e2108e8f7cc402a52577323035ad9}, + issn = {1521-9615}, + keywords = {algorithm magazine matrix simplex top.ten.algorithms}, + number = 1, + pages = {29--31}, + publisher = {IEEE Educational Activities Department}, + timestamp = {2015-12-13T09:44:24.000+0100}, + title = {The (Dantzig) Simplex Method for Linear Programming}, + volume = 2, + year = 2000 +} +@article{zhang2018efficient, + title={Efficient Neural Network Robustness Certification with General Activation Functions}, + author={Zhang, Huan and Weng, Tsui-Wei and Chen, Pin-Yu and Hsieh, Cho-Jui and Daniel, Luca}, + journal={Advances in Neural Information Processing Systems}, + volume={31}, + pages={4939--4948}, + year={2018}, + url={https://arxiv.org/pdf/1811.00866.pdf} +} +@article{xu2020automatic, + title={Automatic perturbation analysis for scalable certified robustness and beyond}, + author={Xu, Kaidi and Shi, Zhouxing and Zhang, Huan and Wang, Yihan and Chang, Kai-Wei and Huang, Minlie and Kailkhura, Bhavya and Lin, Xue and Hsieh, Cho-Jui}, + journal={Advances in Neural Information Processing Systems}, + volume={33}, + year={2020} +} +@inproceedings{xu2021fast, + title={{Fast and Complete}: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers}, + author={Kaidi Xu and Huan Zhang and Shiqi Wang and Yihan Wang and Suman Jana and Xue Lin and Cho-Jui Hsieh}, + booktitle={International Conference on Learning Representations}, + year={2021}, + url={https://openreview.net/forum?id=nVZtXBI6LNn} +} +@article{wang2021beta, + title={{Beta-CROWN}: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification}, + author={Wang, Shiqi and Zhang, Huan and Xu, Kaidi and Lin, Xue and Jana, Suman and Hsieh, Cho-Jui and Kolter, J Zico}, + journal={Advances in Neural Information Processing Systems}, + volume={34}, + year={2021} +} +@inproceedings{shi2024genbab, + title={Neural Network Verification with Branch-and-Bound for General Nonlinearities}, + author={Shi, Zhouxing and Jin, Qirui and Kolter, Zico and Jana, Suman and Hsieh, Cho-Jui and Zhang, Huan}, + booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, + year={2025} +} +@article{zhang2022general, + title={General Cutting Planes for Bound-Propagation-Based Neural Network Verification}, + author={Zhang, Huan and Wang, Shiqi and Xu, Kaidi and Li, Linyi and Li, Bo and Jana, Suman and Hsieh, Cho-Jui and Kolter, J Zico}, + journal={Advances in Neural Information Processing Systems}, + year={2022} +} +@inproceedings{zhou2024scalable, + title={Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes}, + author={Zhou, Duo and Brix, Christopher and Hanasusanto, Grani A and Zhang, Huan}, + booktitle={The Thirty-eighth Annual Conference on Neural Information Processing Systems}, + year={2024} +} diff --git a/chapters/01-introduction.tex b/chapters/01-introduction.tex index 47b7d57..2139af7 100644 --- a/chapters/01-introduction.tex +++ b/chapters/01-introduction.tex @@ -3,24 +3,24 @@ % Context Artificial Intelligence systems have made significant advancements in the last few years and enabled -us to enter a new age of computing. Most of the credit goes to deep neural networks, and to their -exceptional capacity for representing non-linear functions. However, they do not come without +us to enter a new age of computing. Most of the credit goes to deep neural networks and to their +exceptional capacity for representing nonlinear functions. However, they do not come without drawbacks: neural networks are ``black boxes'' that lack transparency. To take advantage of these powerful tools in critical systems such as medicine and aerospace, we need to provide formal guarantees to ensure their safety and trustworthiness. % Problem -In the field of neural network verification, a verification problem is composed of: a trained neural +In the field of neural network verification, a verification problem is composed of a trained neural network and a set of specifications. Then a verification algorithm checks whether the specifications either hold or are violated. The two kinds of properties that can be verified are: \begin{itemize} - \item \textbf{Single-Network}: we check if a single neural network satisfies a given property. - \item \textbf{Multi-Network}: we check if multiple neural networks satisfy a given relation. + \item \textbf{Single-Network}: We check if a single neural network satisfies a given property. + \item \textbf{Multi-Network}: We check if multiple neural networks satisfy a given relation. \end{itemize} An example of a Multi-Network property is equivalence between different neural networks; this verification is crucial when replacing a neural network with a smaller, equivalent one. Techniques based on specialized \textit{Satisfiability Modulo Theories} (SMT) solvers may be used in the verification -algorithm. However, as networks grow in depth and width, the number of non-linear components, most +algorithm. However, as networks grow in depth and width, the number of nonlinear components, most notably the \textit{Rectified Linear Unit}\footnote{Defined as $f(x)=\max(0, x)$, where $x$ is the input to the neuron.} (ReLU) activation function, creates an exponential search space for the solver. Because of this issue, running a solver against a raw, unoptimized network is often computationally prohibitive. @@ -42,15 +42,17 @@ To model such graphs and these rewriting mechanisms, we leverage \textit{Interac parallel graph rewriting rules. Additionally, IN are \textit{strongly confluent}, meaning that they always reduce to a unique normal form regardless of the order in which simplification rules are applied. Thanks to these properties, the simplification of neural network graphs can be parallelized -while maintaining determinism of the resulting AST. In the context of neural network equivalence, +while maintaining the determinism of the resulting AST. In the context of neural network equivalence, this is useful because comparing two neural networks becomes a comparison of two simplified canonical forms of the same intermediate model. -Building on this capability, we developed \textbf{VEIN} (VErification via Interaction Nets), a -framework for neural network verification focused on equivalence. This tool aims to verify both -Single-Network and Multi-Network properties. The tool is composed of two primary modules: +Building on this capability, we developed +\textbf{VEIN}\footnote{\href{https://github.com/eric-marin/VEIN}{\textbf{VEIN Github repository.}}} +(VErification via Interaction Nets), a framework for neural network verification focused on +equivalence. This tool aims to verify both Single-Network and Multi-Network properties. The tool is +composed of two primary modules: \begin{itemize} - \item \textbf{Reduction engine}: a modified version of \textit{Interaction Nets as a Programming + \item \textbf{Reduction engine}: A modified version of \textit{Interaction Nets as a Programming LAnguage}\footnote{\href{https://github.com/inpla/inpla}{\textbf{INPLA Github repository}}.} (INPLA), a multi-threaded parallel interpreter of IN, to simplify the neural network graph; @@ -58,20 +60,20 @@ Single-Network and Multi-Network properties. The tool is composed of two primary \end{itemize} The tool runtime follows three steps: \begin{itemize} - \item \textbf{Translation}: the system translates a neural network in \textit{Open Neural Network + \item \textbf{Translation}: The system translates a neural network in \textit{Open Neural Network Exchange}\footnote{\href{https://onnx.ai/}{\textbf{ONNX Website}}.} (ONNX) file format, an open format built to represent machine learning models, into an IN; - \item \textbf{Reduction}: the INPLA engine reduces the IN to its normal form using the graph + \item \textbf{Reduction}: The INPLA engine reduces the IN to its normal form using the graph rewriting rules that implement symbolic constant folding and identity elimination; - \item \textbf{Evaluation}: then we parse the resulting normal form into Z3 representation and run the + \item \textbf{Evaluation}: Then we parse the resulting normal form into Z3 representation and run the solver to evaluate it along with the provided specification. \end{itemize} % Validation We prove the soundness of our IN pipeline by induction on the number of interaction steps, demonstrating that the ONNX translation and each interaction rule preserve the semantic meaning of -the original neural network. In addition to this formal analysis, we conducted several benchmarks on -checking equivalence between a neural network trained on a dataset and a transformation. +the original neural network. In addition to this formal analysis, we conducted several benchmarks to +check the equivalence between a neural network trained on a dataset and a transformation. % Contributions The development of the \textbf{VEIN} framework and the design of its underlying simplification layer @@ -79,14 +81,14 @@ constitute the primary work of this thesis. To address the challenges of verific and the need for a formal model of representation (B), this thesis introduces several key contributions: \begin{itemize} - \item \textbf{Interaction Rules (Solves A)}: we designed a set of interaction rules to enable graph + \item \textbf{Interaction Rules (Solves A)}: We designed a set of interaction rules to enable graph rewriting for symbolic constant folding while producing an AST ready to be parsed for the SMT solver; - \item \textbf{ONNX-Interaction Net Translation (Solves B)}: we developed a translation procedure for ONNX + \item \textbf{ONNX-Interaction Net Translation (Solves B)}: We developed a translation procedure for ONNX models to IN; - \item \textbf{Soundness Analysis (Validates A/B)}: we provide a formal proof that the IN reduction + \item \textbf{Soundness Analysis (Validates A/B)}: We provide a formal proof that the IN reduction preserves the mathematical properties of the neural network; - \item \textbf{Experimental Evaluation (Validates A/B Empirically)}: we conducted an extensive benchmarking + \item \textbf{Experimental Evaluation (Validates A/B Empirically)}: We conducted an extensive benchmarking on widely known datasets and common \textit{International Verification of Neural Networks Competition}\footnote{The premier international competition dedicated to evaluating and advancing the state-of-the-art in neural network verification, see the diff --git a/chapters/02-background.tex b/chapters/02-background.tex index ca6160e..c306e2e 100644 --- a/chapters/02-background.tex +++ b/chapters/02-background.tex @@ -1,9 +1,9 @@ \chapter{Background} \label{ch:background} -This chapter contains the background theory necessary to understand the rest of the thesis such as: +This chapter contains the background theory necessary to understand the rest of the thesis, such as neural networks (\textbf{\Cref{sec:neural-networks}}), interaction nets -(\textbf{\Cref{sec:interaction-nets}}) and SMT solvers (\textbf{\Cref{sec:satisfiability-modulo-theories}}). +(\textbf{\Cref{sec:interaction-nets}}), and SMT solvers (\textbf{\Cref{sec:satisfiability-modulo-theories}}). \input{chapters/background/01-neural-networks} diff --git a/chapters/03-core.tex b/chapters/03-core.tex index c222f0d..96cd0f1 100644 --- a/chapters/03-core.tex +++ b/chapters/03-core.tex @@ -1,8 +1,8 @@ -\chapter{VEIN} +\chapter{VEIN: VErification via Interaction Nets} \label{ch:core} This chapter contains details on framework implementation (\textbf{\Cref{sec:implementation}}), the -proof of soundness of the pipeline (\textbf{\Cref{sec:soundness-proof}}) and a collection of data +proof of soundness of the pipeline (\textbf{\Cref{sec:soundness-proof}}), and a collection of data gathered from benchmarks (\textbf{\Cref{sec:benchmarks}}). \input{chapters/core/01-implementation} diff --git a/chapters/04-related-work.tex b/chapters/04-related-work.tex index d43cb0e..8e0c760 100644 --- a/chapters/04-related-work.tex +++ b/chapters/04-related-work.tex @@ -36,5 +36,5 @@ the problem of neural network equivalence checking using SMT solvers, and define strict, epsilon, and argmax equivalence adopted in \textbf{\Cref{sec:benchmarks}}. They approach the equivalence problem by directly encoding an SMT formula and relying on internal heuristics of the solver to handle the search space. Instead, \textbf{VEIN} introduces an explicit, formally verified -preprocessing stage that reduces the networks to a normal form before encoding it into an SMT +preprocessing stage that reduces the networks to a normal form before encoding them into an SMT formula. diff --git a/chapters/05-conclusion.tex b/chapters/05-conclusion.tex index b178b7f..089acfb 100644 --- a/chapters/05-conclusion.tex +++ b/chapters/05-conclusion.tex @@ -2,10 +2,11 @@ \label{ch:conclusion} In this thesis, we introduced \textbf{VEIN}, a novel framework for neural network verification with -a particular focus on network equivalence checking. The key achievements of this work include: +a particular focus on neural network equivalence checking. The key achievements of this work +include: \begin{itemize} \item The formalization and implementation of an ONNX-to-IN translation pipeline. - \item The design of interaction rules implementing symbolic constant folding, constant + \item The design of interaction rules implements symbolic constant folding, constant propagation, and identity elimination. \item A soundness proof of the reduction engine, demonstrating that each graph rewriting step preserves the semantics of the original neural network. @@ -15,25 +16,25 @@ a particular focus on network equivalence checking. The key achievements of this While the current version of \textbf{VEIN} establishes a solid foundation for IN-based verification, several limitations remain to be addressed in future research. The future roadmap focuses on performance -optimizations, modeling expressiveness and advanced interaction rules. +optimizations, modeling expressiveness, and advanced interaction rules. \paragraph{Custom Reduction Engine} The current reduction engine relies on a modified version of the INPLA interpreter. While practical, it is prone to high memory overhead. A core objective of future work is to replace INPLA with a custom reduction engine written in Rust. Implementing the engine in Rust will provide: -memory safety without garbage collection, high-performance concurrency and flexibility. +memory safety without garbage collection, high-performance concurrency, and flexibility. \paragraph{Complex Agent Attributes} Currently, interaction net agents in \textbf{VEIN} are limited to simple scalar attributes. This restriction prevents the direct translation of complex operations into single agents. Future work will extend -the framework to support complex attributes, such as tensors, boundary intervals and real numbers. +the framework to support complex attributes, such as tensors, boundary intervals, and real numbers. \paragraph{Advanced Interaction Rules and Symbolic ReLU Pruning} The interaction rules implemented in \textbf{VEIN} are currently limited to constant folding of linear operations. Non-linear activation functions, specifically ReLUs, are passed through without modification unless their inputs are concrete constants. To improve simplification efficiency, we -plan to implement range analysis and interval arithmetic directly within the IN, substantially -reducing the number of split constraints faced by the SMT solver. +plan to implement range analysis and interval arithmetic directly within the IN to determine prunable +ReLUs, substantially reducing the number of split constraints faced by the SMT solver. \paragraph{Integration with Specialized Solvers} The current evaluation of \textbf{VEIN} targets the Z3 solver. However, the intermediate SMT-LIB diff --git a/chapters/background/01-neural-networks.tex b/chapters/background/01-neural-networks.tex index dc3e2d4..5eed7bd 100644 --- a/chapters/background/01-neural-networks.tex +++ b/chapters/background/01-neural-networks.tex @@ -3,7 +3,7 @@ A neural network is a computational model inspired by biological neural networks. It consists of connected nodes called neurons, introduced in its early form by Rosenblatt~\cite{rosenblatt1958perceptron}. -The \textit{Multi-Layer Perceptrons} is an architecture composed of sequential layers, trained using +The \textit{Multi-Layer Perceptron} is an architecture composed of sequential layers, trained using backpropagation as popularized by Rumelhart et al.~\cite{rumelhart1986learning}. \subsection{Neuron} @@ -57,7 +57,7 @@ The output $y$ is defined as: \subsection{Multi-Layer Perceptron} A \textit{Multi-Layer Perceptron} (MLP), illustrated in \textbf{\Cref{fig:mlp}}, is a type of neural network organized -in fully connected layers of neurons: an input layer, one or more hidden layers and an output layer. +in fully connected layers of neurons: an input layer, one or more hidden layers, and an output layer. An MLP is \textit{feedforward}, meaning that the flow of information is strictly propagated from the input to the outputs. \begin{figure}[H] diff --git a/chapters/background/02-interaction-nets.tex b/chapters/background/02-interaction-nets.tex index 874110e..41488f1 100644 --- a/chapters/background/02-interaction-nets.tex +++ b/chapters/background/02-interaction-nets.tex @@ -5,7 +5,7 @@ graphical model of computation based on graph rewriting. \subsection{Basic Concepts} -An IN is an undirected graph with labelled vertices, called \textit{agents}. Each agent +An IN is an undirected graph with labeled vertices, called \textit{agents}. Each agent is an instance of a \textit{symbol}, which has a principal port and a fixed number of auxiliary ports: \begin{figure}[H] \centering @@ -21,7 +21,7 @@ is an instance of a \textit{symbol}, which has a principal port and a fixed numb \end{figure} Each port can be wired to at most one other port. When two different agents are wired to their -respective principal ports they are called an \textit{active pair}: +respective principal ports, they are called an \textit{active pair}: \begin{figure}[H] \centering @@ -34,13 +34,13 @@ respective principal ports they are called an \textit{active pair}: \node[left] at (A.above pax 2) {$\mathit{y}$}; \node[right] at (S.above pax) {$\mathit{x}$}; \end{tikzpicture} - \caption{Example of an active pair, where a $\mathit{Add}$ agent and an $\mathit{S}$ agent are connected via their principal ports.} + \caption{Example of an active pair, where an $\mathit{Add}$ agent and an $\mathit{S}$ agent are connected via their principal ports.} \label{fig:active-pair} \end{figure} \subsection{Interaction Rules} Computation in IN proceeds by rewriting the net using local \emph{interaction rules}. A rule -is defined only for an active pair and for any pair of symbols there is at most one +is defined only for an active pair, and for any pair of symbols, there is at most one interaction rule. \begin{figure}[H] @@ -62,12 +62,12 @@ interaction rule. \node[left] at (A.above pax 2) {$\mathit{y}$}; \node[left] at (S.above pal) {$\mathit{z}$}; } - \caption{Interaction rule for $\mathit{S}$ and $\mathit{Add}$ that emulates Peano addition rule.} + \caption{Interaction rule for $\mathit{S}$ and $\mathit{Add}$ that emulates the Peano addition rule.} \label{fig:rule-concrete-zero} \end{figure} \subsection{Properties} -IN possess the following properties: +IN possesses the following properties: \begin{itemize} \item \textbf{Locality}: only active pairs can be rewritten. \item \textbf{Linearity}: each interaction rule rewrites a constant-size subgraph, independent of diff --git a/chapters/core/01-implementation.tex b/chapters/core/01-implementation.tex index 32154ef..9c25bef 100644 --- a/chapters/core/01-implementation.tex +++ b/chapters/core/01-implementation.tex @@ -3,7 +3,7 @@ This section contains details on the implementation of the reduction engine (\textbf{\Cref{sec:inpla}}), the interaction rules designed (\textbf{\Cref{sec:interaction-rules}}), the algorithm used in the -ONNX-to-IN translation (\textbf{\Cref{sec:translation}}) and the Python module (\textbf{\Cref{sec:python-module}}). +ONNX-to-IN translation (\textbf{\Cref{sec:translation}}), and the Python module (\textbf{\Cref{sec:python-module}}). \input{chapters/core/implementation/01-inpla} diff --git a/chapters/core/02-soundness-proof.tex b/chapters/core/02-soundness-proof.tex index 6b014da..fef6bec 100644 --- a/chapters/core/02-soundness-proof.tex +++ b/chapters/core/02-soundness-proof.tex @@ -1,9 +1,9 @@ \section{Soundness Proof} \label{sec:soundness-proof} -This section contains proof of soundness of the VEIN framework, which is organized in mathematical +This section contains proof of the soundness of the VEIN framework, which is organized in mathematical definitions (\textbf{\Cref{sec:mathematical-definitions}}), proof of the translation layer (\textbf{\Cref{sec:soundness-of-translation}}), -proof of the interaction rules (\textbf{\Cref{sec:soundness-of-interaction-rules}}) and the final +proof of the interaction rules (\textbf{\Cref{sec:soundness-of-interaction-rules}}), and the final induction proof (\textbf{\Cref{sec:soundness-of-reduction}}). \input{chapters/core/soundness-proof/01-mathematical-definitions} diff --git a/chapters/core/03-benchmarks.tex b/chapters/core/03-benchmarks.tex index 31b61a7..25cc0ab 100644 --- a/chapters/core/03-benchmarks.tex +++ b/chapters/core/03-benchmarks.tex @@ -9,12 +9,13 @@ This section contains the benchmark data, illustrated in \textbf{\Cref{tab:bench \item \textbf{RAM}: 16GiB \end{itemize} using the Hyperfine\footnote{\href{https://github.com/sharkdp/hyperfine}{\textbf{Hyperfine Github repository}}.} -benchmarking tool. Hyperfine runs the test ten times, then reports the mean and standard deviation -of execution time. For longer runs, only execution is reported. We defined the following benchmarks: +benchmarking tool. Hyperfine runs the test ten times, then reports the mean and the standard deviation +of execution time. For longer runs, only one execution is reported. We defined the following +benchmarks: \begin{itemize} \item \textbf{Iris}: Network trained on the Iris flowers dataset presented by Fisher~\cite{fisher1936iris}. - It consists of three species of flower (\textit{Iris setosa}, \textit{Iris virginica} and \textit{Iris versicolor}) with - fifty samples each. Each sample has four features: width and length of sepals and petals. + It consists of three species of flower (\textit{Iris setosa}, \textit{Iris virginica}, and \textit{Iris versicolor}) with + fifty samples each. Each sample has four features: the width and length of the sepals and petals. \item \textbf{Pendulum}: A neural safety certificate for stabilizing a pendulum to its upright position under a bound on its angle $\theta$, with state $x=[\theta,\dot\theta]\in\mathbb{R}^2$. \item \textbf{Double Integrator}: A neural safety certificate for stabilizing a second-order linear system @@ -25,13 +26,13 @@ of execution time. For longer runs, only execution is reported. We defined the f \end{itemize} Pendulum and Double Integrator are taken from \textit{cersyve}, a benchmark presented by Kaulen et -al.~\cite{kaulen20256thinternationalverificationneural}. We check equivalence between a pre-trained +al.~\cite{kaulen20256thinternationalverificationneural}. We check the equivalence between a pre-trained and a fine-tuned network for each task. In the Iris and MNIST datasets, we tested equivalence between a neural network and its ad-hoc transformation, such as pruning always positive or negative ReLUs, as presented by Kumar et al.~\cite{kumar2019equivalentapproximatetransformationsdeep}, or changing the architecture from wide -to deep and viceversa, as presented by Fan et al.~\cite{JMLR:v24:21-0579}. +to deep and vice versa, as presented by Fan et al.~\cite{JMLR:v24:21-0579}. For two neural networks $F: \mathbb{R}^n \to \mathbb{R}^m$ and $F': \mathbb{R}^n \to \mathbb{R}^m$, Eleftheriadis et al.~\cite{eleftheriadis2022equivalence} define three kinds of equivalence: @@ -100,4 +101,4 @@ We make three observations: preprocessing. \end{itemize} Additionally, we identify two false SAT results (Stably Active transformation). These are caused -by floating-point error introduced by the INPLA float attributes instead of using real numbers. +by floating-point errors introduced by the INPLA float attributes instead of using real numbers. diff --git a/chapters/core/implementation/01-inpla.tex b/chapters/core/implementation/01-inpla.tex index 57d3195..ff6ef16 100644 --- a/chapters/core/implementation/01-inpla.tex +++ b/chapters/core/implementation/01-inpla.tex @@ -8,17 +8,17 @@ to hold numerical values at their ports. Several modifications adapt INPLA to the pipeline of the framework: \begin{itemize} - \item \textbf{Floating-Point arithmetic}: attributes were limited to integer values. To correctly + \item \textbf{Floating-Point arithmetic}: Attributes were limited to integer values. To correctly represent the computation performed by neural networks, the fork replaces the internal numerical representation by floating-point types. \item \textbf{Pipeline integration}: INPLA was designed for interactive use through the command line, so - various debugging and informational messages are printed along the actual output. To integrate - INPLA in our automated framework, the fork introduces a suppression flag to prevent unnecessary - printing from disrupting its execution. + various debugging and informational messages are printed along with the actual output. To + integrate INPLA in our automated framework, the fork introduces a suppression flag to prevent + unnecessary printing from disrupting its execution. \end{itemize} \paragraph{INPLA syntax} -INPLA evaluates nets which consist of connections between terms. Terms are built on names and agents: +INPLA evaluates nets composed of connections between terms. Terms are built on names and agents: \begin{small} \begin{verbatim} ::= | @@ -28,10 +28,10 @@ INPLA evaluates nets which consist of connections between terms. Terms are built \end{verbatim} \end{small} \begin{itemize} - \item \textbf{Name}: it works as a buffer between terms. - \item \textbf{Agent}: it works as a constructor and de-constructor (defined functions). + \item \textbf{Name}: It works as a buffer between terms. + \item \textbf{Agent}: It works as a constructor and a de-constructor. \end{itemize} -A connection is a relation between two terms and the symbol \texttt{\~} expresses this relation. +A connection is a relation between two terms, and the symbol \texttt{\~} expresses this relation. Interaction rules rewrite connections between agents: \begin{small} \begin{verbatim} @@ -50,7 +50,7 @@ increment operation ``inc'' such that: inc(n) = S(n). \end{verbatim} \end{small} -This is written as the following rules: +This is written according to the following rules: \begin{small} \begin{verbatim} inc(r) >< Z => r ~ S(Z); diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex index 8b02c3c..433989d 100644 --- a/chapters/core/implementation/02-interaction-rules.tex +++ b/chapters/core/implementation/02-interaction-rules.tex @@ -17,7 +17,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \item \textbf{ReLU}: Unary operator for rectified linear unit. \end{itemize} \item - \textbf{Structural Operators}: Agents that perform some kind of operation on net structure. + \textbf{Structural Operators}: Agents that perform some kind of operation on the net structure. \begin{itemize} \item \textbf{Eraser}: Built-in INPLA unary operator to delete other agents. \item \textbf{Dup}: Built-in INPLA unary operator to duplicate other agents. @@ -34,9 +34,9 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \item \textbf{Terminals}: Agents that compose the normal form. \begin{itemize} - \item \textbf{TermAdd}: This agent is parsed as addition for the SMT solver. - \item \textbf{TermMul}: This agent is parsed as multiplication for the SMT solver. - \item \textbf{TermReLU}: This agent is parsed as rectified linear unit for the SMT solver. + \item \textbf{TermAdd}: This agent is parsed as an addition for the SMT solver. + \item \textbf{TermMul}: This agent is parsed as a multiplication for the SMT solver. + \item \textbf{TermReLU}: This agent is parsed as a rectified linear unit for the SMT solver. \item \textbf{TermSymbolic}: This agent is parsed as a specific variable for the SMT solver. \item \textbf{TermConcrete}: This agent is parsed as a real value for the SMT solver. \end{itemize} @@ -184,10 +184,10 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \end{figure} \paragraph{Linear with Add/Mul} -The \textit{Linear} carrier agent interacts directly with the \textit{Add} and \textit{Mul} operators agents as illustrated in +The \textit{Linear} carrier agent interacts directly with the \textit{Add} and \textit{Mul} operators agents, as illustrated in \textbf{\Cref{fig:rule-linear-add}} and \textbf{\Cref{fig:rule-linear-mul}}. Because interactions are local, the binary -operators need to check one operand a time. For this reason \textit{Add} and \textit{Mul} agents are replaced by -\textit{AddCheckLinear} and \textit{MulCheckLinear} intermediate agents that carry the attributes $q$ and $r$ and their +operators need to check one operand at a time. For this reason, \textit{Add} and \textit{Mul} agents are replaced by +\textit{AddCheckLinear} and \textit{MulCheckLinear} intermediate agents that carry the attributes $q$ and $r$, and their principal port faces the other operand. % Linear >< Add @@ -235,11 +235,11 @@ principal port faces the other operand. \end{figure} \paragraph{Concrete with Add/Mul} -The same logic is applied to the \textit{Concrete} carrier agent, but here analyzing the attribute $k$ -enables short-circuiting. In \textbf{\Cref{fig:rule-concrete-add}} we can see that when summing a \textit{Concrete} -with $k=0$ we do not need to check the other operand and we simply wire it to the output. +The same logic is applied to the \textit{Concrete} carrier agent, but here, analyzing the attribute $k$ +enables short-circuiting. In \textbf{\Cref{fig:rule-concrete-add}}, we can see that when summing a \textit{Concrete} +with $k=0$, we do not need to check the other operand, and we simply wire it to the output. This rewiring is also implemented when multiplying a \textit{Concrete} with $k=1$, as shown in -\textbf{\Cref{fig:rule-concrete-mul}}, with the addition that when $k=0$ the other operand is deleted +\textbf{\Cref{fig:rule-concrete-mul}}, with the addition that when $k=0$, the other operand is deleted before it is even invoked. % Concrete >< Add @@ -339,14 +339,14 @@ before it is even invoked. \end{figure} \paragraph{Linear with AddCheckLinear/MulCheckLinear} -If both operands are \textit{Linear} agents they need to be materialized before being wrapped in another +If both operands are \textit{Linear} agents, they need to be materialized before being wrapped in another \textit{Linear} to allow further simplification. This is done because multiplying two linear packets gives a non-linear result. -While adding two linear packets gives a linear result, it depends on two free variables and the +While adding two linear packets gives a linear result, it depends on two free variables, and the \textit{Linear} agent only supports keeping track of one; consequently, the addition of two linear packets results in their materialization. This is illustrated in \textbf{\Cref{fig:rule-linear-addchecklinear}} -and \textbf{\Cref{fig:rule-linear-mulchecklinear}} where the result of the materialization is passed +and \textbf{\Cref{fig:rule-linear-mulchecklinear}}, where the result of the materialization is passed to a TermAdd or TermMul, for Add and Mul respectively, and then to a \textit{Linear} with attributes $q=1,r=0$. @@ -491,11 +491,11 @@ $q=1,r=0$. \end{figure} \paragraph{Concrete with AddCheckLinear/MulCheckLinear} -If, instead, the first operand is a \textit{Linear} agents and the second is a \textit{Concrete} agent different rules -are applied. In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}) the system adds the +If, instead, the first operand is a \textit{Linear} agents and the second is a \textit{Concrete} agent, different rules +are applied. In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}), the system adds the attribute of the \textit{Concrete} agent to the attribute that represents the constant of the \textit{Linear} agent. -For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}) the system multiplies the attribute of -the \textit{Concrete} agent to both the attributes of the \textit{Linear}. +For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}), the system multiplies the attribute of +the \textit{Concrete} agent by both the attributes of the \textit{Linear}. % Concrete >< AddCheckLinear \begin{figure}[H] @@ -538,8 +538,8 @@ the \textit{Concrete} agent to both the attributes of the \textit{Linear}. \end{figure} \paragraph{Linear with AddCheckConcrete/MulCheckConcrete} -In the rules shown in \textbf{\Cref{fig:rule-linear-addcheckconcrete}} and \textbf{\Cref{fig:rule-linear-mulcheckconcrete}} -we follow the exact same logic except the first operand is a \textit{Concrete} and the second is a \textit{Linear}. +In the rules shown in \textbf{\Cref{fig:rule-linear-addcheckconcrete}} and \textbf{\Cref{fig:rule-linear-mulcheckconcrete}}, +we follow the exact same logic, except the first operand is a \textit{Concrete} and the second is a \textit{Linear}. % Linear >< AddCheckConcrete \begin{figure}[H] @@ -582,9 +582,9 @@ we follow the exact same logic except the first operand is a \textit{Concrete} a \end{figure} \paragraph{Concrete with AddCheckConcrete/MulCheckConcrete} -Finally if both operands are \textit{Concrete} agents they are either merged into a single \textit{Concrete} +Finally, if both operands are \textit{Concrete} agents, they are either merged into a single \textit{Concrete} or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckconcrete}} and -\textbf{\Cref{fig:rule-concrete-mulcheckconcrete}} following a similar logic to the previous rules. +\textbf{\Cref{fig:rule-concrete-mulcheckconcrete}}, following a similar logic to the previous rules. % Concrete >< AddCheckConcrete \begin{figure}[H] @@ -672,10 +672,10 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \end{figure} \paragraph{Linear/Concrete with ReLU} -When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is not -enough information to perform any simplification so, as shown in \textbf{\Cref{fig:rule-linear-relu}}, -the agent is just materialized, passed to a \textit{TermReLU} and then wrapped in a \textit{Linear}. -In \textbf{\Cref{fig:rule-concrete-relu}} is illustrated that when the \textit{Concrete} carrier agent +When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents, there is not +enough information to perform any simplification, so, as shown in \textbf{\Cref{fig:rule-linear-relu}}, +the agent is just materialized, passed to a \textit{TermReLU}, and then wrapped in a \textit{Linear}. +In \textbf{\Cref{fig:rule-concrete-relu}}, it is illustrated that when the \textit{Concrete} carrier agent meets the \textit{ReLU} agent, a \textit{Concrete} is wired to the output either with attribute $k$ if $k>0$ or with attribute equal $0$ otherwise. @@ -742,9 +742,9 @@ if $k>0$ or with attribute equal $0$ otherwise. \end{figure} \paragraph{Linear/Concrete with Materialize} -When a \textit{Linear} is materialized it explicitly build an AST using \textit{TermAdd}, \textit{TermMul} and \textit{TermConcrete} +When a \textit{Linear} is materialized, it explicitly builds an AST using \textit{TermAdd}, \textit{TermMul}, and \textit{TermConcrete} to recreate $q*x+r$ as shown in \textbf{\Cref{fig:rule-linear-materialize}}. -When a \textit{Concrete} needs to be materialized it is converted into \textit{TermConcrete} as illustrated in +When a \textit{Concrete} needs to be materialized, it is converted into \textit{TermConcrete} as illustrated in \textbf{\Cref{fig:rule-concrete-materialize}}. % Linear >< Materialize diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex index b86e060..92f47e5 100644 --- a/chapters/core/implementation/03-translation.tex +++ b/chapters/core/implementation/03-translation.tex @@ -8,8 +8,8 @@ at most one connection. This limitation is solved by utilizing the \textit{Dup} necessary copies of a value required by the next operations. Since nodes do not know how successor nodes will utilize their outputs, the translation layer traverses the DAG in reverse order to be able to instantiate the correct number of \textit{Dup} agents. The main algorithm, illustrated -in \textbf{\Cref{alg:onnx-to-in}}, maintains an \textit{interactions} dictionary data-structure, that maps each tensor -name to a list of ports, to keep track of the graph traversal. The ONNX operators supported are Gemm +in \textbf{\Cref{alg:onnx-to-in}}, maintains an \textit{interaction} dictionary data structure that maps each tensor +name to a list of ports to keep track of the graph traversal. The ONNX operators supported are Gemm (General matrix multiplication) and ReLU. \begin{algorithm}[H] @@ -81,8 +81,8 @@ chains of agents, opting instead for balanced binary trees for signal distributi multiple output) and signal reduction (multiple input to single output). As \textbf{\Cref{alg:balanced-fan-in}} and \textbf{\Cref{alg:balanced-fan-out}} illustrate, the depth of agent chains (especially \textit{Dup} chains) is limited to $O(\log N)$. The two algorithms are very similar; the difference is in how they wire the -agents together: in the \textit{Fan-In} the principal port of the agents are facing the leaves, while in the -\textit{Fan-Out} they face the root. +agents together: in the \textit{Fan-In}, the principal ports of the agents are facing the leaves, while in the +\textit{Fan-Out}, they face the root. \begin{algorithm}[H] \caption{Balanced Fan-In} diff --git a/chapters/core/implementation/04-python-module.tex b/chapters/core/implementation/04-python-module.tex index 6023c2e..ab817c4 100644 --- a/chapters/core/implementation/04-python-module.tex +++ b/chapters/core/implementation/04-python-module.tex @@ -15,14 +15,14 @@ The methods offered by \texttt{vein.Solver} are: \end{itemize} The framework uses a \textit{lazy evaluation} strategy: when loading a neural network, it is placed -into a pending queue and it is reduced to normal form only after the \texttt{check} method is +into a pending queue, and it is reduced to normal form only after the \texttt{check} method is called. The specification follows the SMT-LIB\footnote{\href{https://smt-lib.org}{\textbf{SMT-LIB Website}}} format. It should contain the input and output symbolic variables declarations, optional range -constraints on the input variables and the properties to be verified. For Multi-Network (relational) +constraints on the input variables, and the properties to be verified. For Multi-Network (relational) verification, the system ensures that multiple networks share the same input symbolic variables. -This approach allows Z3 to compare their outputs directly given the same inputs. +This approach allows Z3 to compare the outputs directly, given the same inputs. The execution pipeline is implemented within the \texttt{check} method: \begin{itemize} diff --git a/chapters/core/soundness-proof/02-soundness-of-translation.tex b/chapters/core/soundness-proof/02-soundness-of-translation.tex index 4477581..83c0f26 100644 --- a/chapters/core/soundness-proof/02-soundness-of-translation.tex +++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex @@ -1,7 +1,7 @@ \subsection{Soundness of Translation} \label{sec:soundness-of-translation} -We need to prove that for each ONNX operator a semantically equivalent IN is produced. +We need to prove that for each ONNX operator, a semantically equivalent IN is produced. \begin{lemma} The ONNX ReLU operator for an input tensor X and output tensor Y is defined as: @@ -20,7 +20,7 @@ Which is identical to the ONNX definition. \end{lemma} \begin{lemma} -The ONNX Gemm operator for input tensors A, B, C, input $\alpha$ and $\beta$ and output tensor Y is defined as: +The ONNX Gemm operator for input tensors A, B, C, input $\alpha$ and $\beta$, and output tensor Y is defined as: $$ Y = \alpha \cdot A \cdot B + \beta \cdot C $$ diff --git a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex index 6957c3c..02005e3 100644 --- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex +++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex @@ -4,7 +4,7 @@ We need to prove that each interaction rule does not alter the semantics of the IN. \begin{lemma} - For the \textit{Linear} and \textit{Add} agents we have the interaction rule: + For the \textit{Linear} and \textit{Add} agents, we have the interaction rule: $$ \mathit{Linear}(x, q, r) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \\ $$ @@ -26,7 +26,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{Mul} agents we have the interaction rule: + For the \textit{Linear} and \textit{Mul} agents, we have the interaction rule: $$ \mathit{Linear}(x, q, r) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \\ $$ @@ -48,7 +48,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{Add} agents we have the interaction rule: + For the \textit{Concrete} and \textit{Add} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow \begin{cases} @@ -84,7 +84,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{Mul} agents we have the interaction rule: + For the \textit{Concrete} and \textit{Mul} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow \begin{cases} @@ -123,7 +123,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{AddCheckLinear} agents we have the interaction rule: + For the \textit{Linear} and \textit{AddCheckLinear} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\ @@ -178,7 +178,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{MulCheckLinear} agents we have the interaction rule: + For the \textit{Linear} and \textit{MulCheckLinear} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\ @@ -229,7 +229,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{AddCheckLinear} agents we have the interaction rule: + For the \textit{Concrete} and \textit{AddCheckLinear} agents, we have the interaction rule: $$ \mathit{Concrete}(j) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q, r + j) \sim \mathit{out} \\ $$ @@ -251,7 +251,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{MulCheckLinear} agents we have the interaction rule: + For the \textit{Concrete} and \textit{MulCheckLinear} agents, we have the interaction rule: $$ \mathit{Concrete}(j) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q \cdot j, r \cdot j) \sim \mathit{out} \\ $$ @@ -273,7 +273,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{AddCheckConcrete} agents we have the interaction rule: + For the \textit{Linear} and \textit{AddCheckConcrete} agents, we have the interaction rule: $$ \mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s, t + k) \sim \mathit{out} \\ $$ @@ -295,7 +295,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{MulCheckConcrete} agents we have the interaction rule: + For the \textit{Linear} and \textit{MulCheckConcrete} agents, we have the interaction rule: $$ \mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s \cdot k, t \cdot k) \sim \mathit{out} \\ $$ @@ -317,7 +317,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{AddCheckConcrete} agents we have the interaction rule: + For the \textit{Concrete} and \textit{AddCheckConcrete} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \\ @@ -355,7 +355,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{MulCheckConcrete} agents we have the interaction rule: + For the \textit{Concrete} and \textit{MulCheckConcrete} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \\ @@ -396,7 +396,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{ReLU} agents we have the interaction rule: + For the \textit{Linear} and \textit{ReLU} agents, we have the interaction rule: $$ \begin{aligned} \mathit{Linear}(x, q, r) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow @@ -424,7 +424,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{ReLU} agents we have the interaction rule: + For the \textit{Concrete} and \textit{ReLU} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow \begin{cases} @@ -460,7 +460,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{Materialize} agents we have the interaction rule: + For the \textit{Linear} and \textit{Materialize} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Linear}(x, q, r) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \\ @@ -510,7 +510,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{Materialize} agents we have the interaction rule: + For the \textit{Concrete} and \textit{Materialize} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \mathit{TermConcrete}(k) \sim \mathit{out} \\ $$ @@ -532,7 +532,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{Dup} agents we have the interaction rule: + For the \textit{Linear} and \textit{Dup} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ @@ -561,7 +561,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{Eraser} agents we have the interaction rule: + For the \textit{Linear} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{Linear}(x, q, r) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim x \\ $$ @@ -583,7 +583,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{Dup} agents we have the interaction rule: + For the \textit{Concrete} and \textit{Dup} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{Concrete}(k) \sim x; \mathit{Concrete}(k) \sim y \\ $$ @@ -606,7 +606,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{Eraser} agents we have the interaction rule: + For the \textit{Concrete} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{Eraser} \Rightarrow \\ $$ @@ -623,11 +623,11 @@ We need to prove that each interaction rule does not alter the semantics of the \end{aligned} \end{aligned} $$ - Since $k \in \mathbb{R}$ is not violated by RHS, the rule is sound. + Since $k \in \mathbb{R}$ is not violated by the RHS, the rule is sound. \end{lemma} \begin{lemma} - For the \textit{TermAdd} and \textit{Dup} agents we have the interaction rule: + For the \textit{TermAdd} and \textit{Dup} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{TermAdd}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ @@ -658,7 +658,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermAdd} and \textit{Eraser} agents we have the interaction rule: + For the \textit{TermAdd} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{TermAdd}(a, b) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim a; \mathit{Eraser} \sim b \\ $$ @@ -681,7 +681,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermMul} and \textit{Dup} agents we have the interaction rule: + For the \textit{TermMul} and \textit{Dup} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{TermMul}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ @@ -712,7 +712,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermMul} and \textit{Eraser} agents we have the interaction rule: + For the \textit{TermMul} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{TermMul}(a, b) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim a; \mathit{Eraser} \sim b \\ $$ @@ -735,7 +735,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermReLU} and \textit{Dup} agents we have the interaction rule: + For the \textit{TermReLU} and \textit{Dup} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ @@ -764,7 +764,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermReLU} and \textit{Eraser} agents we have the interaction rule: + For the \textit{TermReLU} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{TermReLU}(x) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim x \\ $$ @@ -786,7 +786,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermConcrete} and \textit{Dup} agents we have the interaction rule: + For the \textit{TermConcrete} and \textit{Dup} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ @@ -813,7 +813,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermConcrete} and \textit{Eraser} agents we have the interaction rule: + For the \textit{TermConcrete} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{TermConcrete}(k) \bowtie \mathit{Eraser} \Rightarrow \\ $$ @@ -830,11 +830,11 @@ We need to prove that each interaction rule does not alter the semantics of the \end{aligned} \end{aligned} $$ - Since $k \in \mathbb{R}$ is not violated by RHS, the rule is sound. + Since $k \in \mathbb{R}$ is not violated by the RHS, the rule is sound. \end{lemma} \begin{lemma} - For the \textit{TermSymbolic} and \textit{Dup} agents we have the interaction rule: + For the \textit{TermSymbolic} and \textit{Dup} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ @@ -861,7 +861,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermSymbolic} and \textit{Eraser} agents we have the interaction rule: + For the \textit{TermSymbolic} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{TermSymbolic}(id) \bowtie \mathit{Eraser} \Rightarrow \\ $$ @@ -878,5 +878,5 @@ We need to prove that each interaction rule does not alter the semantics of the \end{aligned} \end{aligned} $$ - Since $x_{id} \in \mathbb{R}$ is not violated by RHS, the rule is sound. + Since $x_{id} \in \mathbb{R}$ is not violated by the RHS, the rule is sound. \end{lemma} diff --git a/chapters/core/soundness-proof/04-soundness-of-reduction.tex b/chapters/core/soundness-proof/04-soundness-of-reduction.tex index 15cc4f4..c373657 100644 --- a/chapters/core/soundness-proof/04-soundness-of-reduction.tex +++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex @@ -4,8 +4,8 @@ \begin{property} A valid IN satisfies the following properties: \begin{itemize} - \item \textbf{DAG}: the net forms a DAG where the roots are the free wires representing the network - outputs. + \item \textbf{Acyclic}: the net forms a forest where the roots are the free wires representing + the network outputs. \item \textbf{Orientation}: carrier agents always have their principal ports oriented toward the outputs, while operator and intermediate agents always have their principal ports oriented toward the inputs. No interaction rule introduces carriers facing the input nor operators or @@ -29,7 +29,7 @@ We will proceed by induction on the number $n$ of reduction steps: \paragraph{Base case: $n = 0$} By \textbf{\Cref{sec:soundness-of-translation}}, the initial $\text{IN}_0$ is constructed such that its semantics $\llbracket \text{IN}_0 \rrbracket$ exactly - match the mathematical definition of the ONNX operators in $\text{NN}$, it follows that: + match the mathematical definition of the ONNX operators in $\text{NN}$; it follows that: \begin{equation} \llbracket \text{IN}_{0} \rrbracket = \llbracket \text{NN} \rrbracket \end{equation} @@ -37,7 +37,7 @@ \paragraph{Induction step: $n \to n + 1$} Assume $\llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket$. If $\text{IN}_n$ is in normal form, the proof is complete. Otherwise, there exists an active pair $A \bowtie B$ that reduces $\text{IN}_n$ to $\text{IN}_{n+1}$. By \textbf{\Cref{sec:soundness-of-interaction-rules}}, - the mathematical definition is preserved after any reduction step, it follows that: + the mathematical definition is preserved after any reduction step; it follows that: \begin{equation} \llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{IN}_{n} \rrbracket \end{equation} @@ -122,7 +122,7 @@ \Phi(\text{IN}_n) = 3^{D-d(a)} > 0 = \Phi(\text{IN}_{n+1}) \end{equation} \end{itemize} - Since $\Phi$ is a non-negative strictly decreasing function, the reduction + Since $\Phi$ is a non-negative, strictly decreasing function, the reduction process must terminate in a finite number of steps $n$. Additionally, since each active pair has exactly one applicable rule, the reduction is diff --git a/front.tex b/front.tex new file mode 100644 index 0000000..f2207e6 --- /dev/null +++ b/front.tex @@ -0,0 +1,42 @@ +\pagestyle{plain} + +\thispagestyle{empty} + +\begin{center} + \begin{figure}[h!] + \centerline{\psfig{file=marchio_unitrento_colore_it_202002.eps,width=0.6\textwidth}} + \end{figure} + + \vspace{2 cm} + + \LARGE{Department of Information Engineering and Computer Science\\} + + \vspace{1 cm} + \Large{Bachelor’s Degree in\\ + Computer Science + %Informatica + %Ingegneria dell'Informazione e delle Comunicazioni + %Ingegneria dell'Informazione e Organizzazione d'Impresa + %Ingegneria Elettronica e delle Telecomunicazioni + } + + \vspace{2 cm} + \Large\textsc{Final Dissertation\\} + \vspace{1 cm} + \Huge\textsc{Verification via Interaction Nets for Neural Networks\\} + % \Large{\it{Sottotitolo (alcune volte lungo - opzionale)}} + + + \vspace{2 cm} + \begin{tabular*}{\textwidth}{ c @{\extracolsep{\fill}} c } + \Large{Supervisors} & \Large{Student}\\ + \Large{Patrignani Marco}& \Large{Marin Eric}\\ + \Large{Vella Flavio}&\\ + \end{tabular*} + + \vspace{2 cm} + + \Large{Academic year 2025/2026} + +\end{center} + diff --git a/main.tex b/main.tex deleted file mode 100644 index 1fce155..0000000 --- a/main.tex +++ /dev/null @@ -1,68 +0,0 @@ -\documentclass[12pt,a4paper,twoside]{report} -\usepackage[utf8]{inputenc} -\usepackage[T1]{fontenc} -\usepackage[english]{babel} -\usepackage{graphicx} -\usepackage{amsmath, amssymb, amsthm} -\usepackage{cite} -\usepackage[colorlinks=true, linkcolor=black, citecolor=black, urlcolor=black]{hyperref} -\usepackage[linesnumbered,ruled,vlined]{algorithm2e} -\usepackage[nameinlink]{cleveref} -\usepackage{xspace} -\usepackage[colorinlistoftodos]{todonotes} -\usepackage[scaled=.83]{beramono} -\usepackage{lineno} -\usepackage{tikz-inet} -\usepackage{stmaryrd} -\usepackage{float} -\usepackage{tablefootnote} - -\usetikzlibrary{calc} -\linenumbers -\crefname{algocf}{alg.}{algs.} -\Crefname{algocf}{Algorithm}{Algorithms} -\crefformat{footnote}{#2\footnotemark[#1]#3} - -\input{macros} -\input{cmds} - -\title{VEIN: VErification via Interaction Nets for Neural Networks} -\author{Eric Marin} -\date{\today} - -\begin{document} - -\maketitle - -\begin{abstract} - This thesis introduces \textbf{VEIN} (VErification via Interaction Nets), a framework for neural network - verification with a focus on neural network equivalence. It acts as a formally verified - preprocessor that reduces neural networks to a normal form before they can be compared by a solver. - To enable this reduction, \textbf{VEIN} translates neural networks into Interaction Nets, a graph rewriting - computational model, and applies a set of graph rewriting rules to reduce the network into an - Abstract Syntax Tree. We present the complete framework and provide in detail: the translation - process, the graph rewriting rules and rigorous proofs of both soundness and termination for the - reduction process. -\end{abstract} - -\tableofcontents - -% Introduction: Context -> Problem -> Solution -> Validation -> Outline -\input{chapters/01-introduction} - -% Background -\input{chapters/02-background} - -% Core -\input{chapters/03-core} - -% Related Work -\input{chapters/04-related-work} - -% Conclusion -\input{chapters/05-conclusion} - -\bibliographystyle{plain} -\bibliography{references} - -\end{document} diff --git a/marchio_unitrento_colore_it_202002-eps-converted-to.pdf b/marchio_unitrento_colore_it_202002-eps-converted-to.pdf new file mode 100644 index 0000000..1954a4f Binary files /dev/null and b/marchio_unitrento_colore_it_202002-eps-converted-to.pdf differ diff --git a/marin_eric_Computer_Science_2026.tex b/marin_eric_Computer_Science_2026.tex new file mode 100644 index 0000000..327bb8d --- /dev/null +++ b/marin_eric_Computer_Science_2026.tex @@ -0,0 +1,202 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Template per Elaborato di Laurea +% DISI - Dipartimento di Ingegneria e Scienza dell’Informazione +% +% update 2015-09-10 +% +% Per la generazione corretta del +% pdflatex nome_file.tex +% bibtex nome_file.aux +% pdflatex nome_file.tex +% pdflatex nome_file.tex +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% formato FRONTE RETRO +\documentclass[epsfig,a4paper,11pt,titlepage,twoside,openany]{book} +\usepackage{epsfig} +\usepackage{plain} +\usepackage{setspace} +\usepackage[paperheight=29.7cm,paperwidth=21cm,outer=1.5cm,inner=2.5cm,top=2cm,bottom=2cm]{geometry} % per definizione layout +\usepackage{titlesec} % per formato custom dei titoli dei capitoli +\usepackage[T1]{fontenc} +\usepackage[english]{babel} +\usepackage{graphicx} +\usepackage{amsmath, amssymb, amsthm} +\usepackage{cite} +\usepackage[colorlinks=true, linkcolor=black, citecolor=black, urlcolor=black]{hyperref} +\usepackage[linesnumbered,ruled,vlined]{algorithm2e} +\usepackage[nameinlink]{cleveref} +\usepackage{xspace} +\usepackage[colorinlistoftodos]{todonotes} +\usepackage[scaled=.83]{beramono} +\usepackage{lineno} +\usepackage{tikz-inet} +\usepackage{stmaryrd} +\usepackage{float} +\usepackage{tablefootnote} + +%%%%%%%%%%%%%% +% supporto lettere accentate +% +%\usepackage[latin1]{inputenc} % per Windows; +\usepackage[utf8x]{inputenc} % per Linux (richiede il pacchetto unicode); +%\usepackage[applemac]{inputenc} % per Mac. + +\singlespacing + +\usepackage[english]{babel} + +\usetikzlibrary{calc} +% \linenumbers +\crefname{algocf}{alg.}{algs.} +\Crefname{algocf}{Algorithm}{Algorithms} +\crefformat{footnote}{#2\footnotemark[#1]#3} + +\input{macros} +\input{cmds} + +\begin{document} + + % nessuna numerazione + \pagenumbering{gobble} + \input{front} + + \clearpage + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Nota +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Sezione Ringraziamenti opzionale +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + % \input{ringraziamenti} + % \clearpage + % \pagestyle{plain} % nessuna intestazione e pie pagina con numero al centro + + + % inizio numerazione pagine in numeri arabi + \mainmatter + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Nota +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Si ricorda che il numero massimo di facciate e' 30. +%% Nel conteggio delle facciate sono incluse +%% indice +%% sommario +%% capitoli +%% Dal conteggio delle facciate sono escluse +%% frontespizio +%% ringraziamenti +%% allegati +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + % indice + \tableofcontents + \clearpage + + + + % gruppo per definizone di successione capitoli senza interruzione di pagina + \begingroup + % nessuna interruzione di pagina tra capitoli + % ridefinizione dei comandi di clear page + \renewcommand{\cleardoublepage}{} + \renewcommand{\clearpage}{} + % redefinizione del formato del titolo del capitolo + % da formato + % Capitolo X + % Titolo capitolo + % a formato + % X Titolo capitolo + + \titleformat{\chapter} + {\normalfont\Huge\bfseries}{\thechapter}{1em}{} + + \titlespacing*{\chapter}{0pt}{0.59in}{0.02in} + \titlespacing*{\section}{0pt}{0.20in}{0.02in} + \titlespacing*{\subsection}{0pt}{0.10in}{0.02in} + + % sommario + \input{chapters/01-introduction} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Nota +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Sommario e' un breve riassunto del lavoro svolto dove si descrive +%% l’obiettivo, l’oggetto della tesi, le metodologie e +%% le tecniche usate, i dati elaborati e la spiegazione delle conclusioni +%% alle quali siete arrivati. +%% Il sommario dell’elaborato consiste al massimo di 3 pagine e deve contenere le seguenti informazioni: +%% contesto e motivazioni +%% breve riassunto del problema affrontato +%% tecniche utilizzate e/o sviluppate +%% risultati raggiunti, sottolineando il contributo personale del laureando/a +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + % lista dei capitoli + % + % \input oppure \include + % + \input{chapters/02-background} + + \input{chapters/03-core} + + \input{chapters/04-related-work} + + \input{chapters/05-conclusion} + + + \endgroup + + + % bibliografia in formato bibtex + % + % aggiunta del capitolo nell'indice + \addcontentsline{toc}{chapter}{Bibliography} + % stile con ordinamento alfabetico in funzione degli autori + \bibliographystyle{plain} + \bibliography{biblio} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Nota +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Nella bibliografia devono essere riportati tutte le fonti consultate +%% per lo svolgimento della tesi. La bibliografia deve essere redatta +%% in ordine alfabetico sul cognome del primo autore. +%% +%% La forma della citazione bibliografica va inserita secondo la fonte utilizzata: +%% +%% LIBRI +%% Cognome e iniziale del nome autore/autori, la data di edizione, titolo, casa editrice, eventuale numero dell’edizione. +%% +%% ARTICOLI DI RIVISTA +%% Cognome e iniziale del nome autore/autori, titolo articolo, titolo rivista, volume, numero, numero di pagine. +%% +%% ARTICOLI DI CONFERENZA +%% Cognome e iniziale del nome autore/autori (anno), titolo articolo, titolo conferenza, luogo della conferenza (città e paese), date della conferenza, numero di pagine. +%% +%% SITOGRAFIA +%% La sitografia contiene un elenco di indirizzi Web consultati e disposti in ordine alfabetico. +%% E’ necessario: +%% Copiare la URL (l’indirizzo web) specifica della pagina consultata +%% Se disponibile, indicare il cognome e nome dell’autore, il titolo ed eventuale sottotitolo del testo +%% Se disponibile, inserire la data di ultima consultazione della risorsa (gg/mm/aaaa). +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + % \titleformat{\chapter} + % {\normalfont\Huge\bfseries}{Allegato \thechapter}{1em}{} + % sezione Allegati - opzionale + % \appendix + % \input{allegati} + +\end{document} diff --git a/references.bib b/references.bib deleted file mode 100644 index e3a73fc..0000000 --- a/references.bib +++ /dev/null @@ -1,229 +0,0 @@ -@inproceedings{lafont1990interactionnets, - author = {Lafont, Yves}, - title = {Interaction nets}, - year = {1989}, - isbn = {0897913434}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - url = {https://doi.org/10.1145/96709.96718}, - doi = {10.1145/96709.96718}, - abstract = {We propose a new kind of programming language, with the following features:Interaction nets generalize Girard's proof nets of linear logic and illustrate the advantage of an integrated logic approach, as opposed to the external one. In other words, we did not try to design a logic describing the behaviour of some given computational system, but a programming language for which the type discipline is already (almost) a logic.In fact, we shall scarcely refer to logic, because we adopt a na\"{\i}ve and pragmatic style. A typical application we have in mind for this language is the design of interactive softwares such as editors or window managers.}, - booktitle = {Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, - pages = {95–108}, - numpages = {14}, - location = {San Francisco, California, USA}, - series = {POPL '90} -} -@inproceedings{demoura2008z3, - author="de Moura, Leonardo - and Bj{\o}rner, Nikolaj", - editor="Ramakrishnan, C. R. - and Rehof, Jakob", - title="Z3: An Efficient SMT Solver", - booktitle="Tools and Algorithms for the Construction and Analysis of Systems", - year="2008", - publisher="Springer Berlin Heidelberg", - address="Berlin, Heidelberg", - pages="337--340", - abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.", - isbn="978-3-540-78800-3" -} -@misc{kumar2019equivalentapproximatetransformationsdeep, - title={Equivalent and Approximate Transformations of Deep Neural Networks}, - author={Abhinav Kumar and Thiago Serra and Srikumar Ramalingam}, - year={2019}, - eprint={1905.11428}, - archivePrefix={arXiv}, - primaryClass={cs.LG}, - url={https://arxiv.org/abs/1905.11428}, -} -@article{JMLR:v24:21-0579, - author = {Fenglei Fan and Rongjie Lai and Ge Wang}, - title = {Quasi-Equivalence between Width and Depth of Neural Networks}, - journal = {Journal of Machine Learning Research}, - year = {2023}, - volume = {24}, - number = {183}, - pages = {1--22}, - url = {http://jmlr.org/papers/v24/21-0579.html} -} -@misc{kaulen20256thinternationalverificationneural, - title={The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results}, - author={Konstantin Kaulen and Tobias Ladner and Stanley Bak and Christopher Brix and Hai Duong and Thomas Flinkow and Taylor T. Johnson and Lukas Koller and Edoardo Manino and ThanhVu H Nguyen and Haoze Wu}, - year={2025}, - eprint={2512.19007}, - archivePrefix={arXiv}, - primaryClass={cs.LG}, - url={https://arxiv.org/abs/2512.19007}, -} -@article{fisher1936iris, - author = {FISHER, R. A.}, - title = {THE USE OF MULTIPLE MEASUREMENTS IN TAXONOMIC PROBLEMS}, - journal = {Annals of Eugenics}, - volume = {7}, - number = {2}, - pages = {179-188}, - doi = {https://doi.org/10.1111/j.1469-1809.1936.tb02137.x}, - url = {https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1469-1809.1936.tb02137.x}, - eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1111/j.1469-1809.1936.tb02137.x}, - abstract = {The articles published by the Annals of Eugenics (1925–1954) have been made available online as an historical archive intended for scholarly use. The work of eugenicists was often pervaded by prejudice against racial, ethnic and disabled groups. The online publication of this material for scholarly research purposes is not an endorsement of those views nor a promotion of eugenics in any way.}, - year = {1936} -} -@article{lecun2010mnist, - title={MNIST handwritten digit database}, - author={LeCun, Yann and Cortes, Corinna and Burges, CJ}, - journal={ATT Labs [Online]. Available: http://yann.lecun.com/exdb/mnist}, - volume={2}, - year={2010} -} -@InProceedings{eleftheriadis2022equivalence, - author="Eleftheriadis, Charis - and Kekatos, Nikolaos - and Katsaros, Panagiotis - and Tripakis, Stavros", - editor="Bogomolov, Sergiy - and Parker, David", - title="On Neural Network Equivalence Checking Using SMT Solvers", - booktitle="Formal Modeling and Analysis of Timed Systems", - year="2022", - publisher="Springer International Publishing", - address="Cham", - pages="237--257", - abstract="Two pretrained neural networks are deemed (approximately) equivalent if they yield similar outputs for the same inputs. Equivalence checking of neural networks is of great importance, due to its utility in replacing learning-enabled components with (approximately) equivalent ones, when there is need to fulfill additional requirements or to address security threats, as is the case when using knowledge distillation, adversarial training, etc. In this paper, we present a method to solve various strict and approximate equivalence checking problems for neural networks, by reducing them to SMT satisfiability checking problems. This work explores the utility and limitations of the neural network equivalence checking framework, and proposes avenues for future research and improvements toward more scalable and practically applicable solutions. We present experimental results, for diverse types of neural network models (classifiers and regression networks) and equivalence criteria, towards a general and application-independent equivalence checking approach.", - isbn="978-3-031-15839-1" -} - -@article{rosenblatt1958perceptron, - added-at = {2017-07-19T15:29:59.000+0200}, - author = {Rosenblatt, F.}, - biburl = {https://www.bibsonomy.org/bibtex/214ee8da21c66cd4d00d7ab6eca2d96a9/andreashdez}, - citeulike-article-id = {13697582}, - citeulike-linkout-0 = {http://dx.doi.org/10.1037/h0042519}, - doi = {10.1037/h0042519}, - interhash = {dc0cef9dc06033a04f525efdcde7a660}, - intrahash = {14ee8da21c66cd4d00d7ab6eca2d96a9}, - issn = {0033-295X}, - journal = {Psychological Review}, - keywords = {imported}, - number = 6, - pages = {386--408}, - posted-at = {2016-05-02 20:23:36}, - priority = {2}, - timestamp = {2017-07-19T15:31:02.000+0200}, - title = {{The perceptron: A probabilistic model for information storage and organization in the brain.}}, - url = {http://dx.doi.org/10.1037/h0042519}, - volume = 65, - year = 1958 -} -@article{rumelhart1986learning, - title={Learning representations by back-propagating errors}, - author={Rumelhart, David E and Hinton, Geoffrey E and Williams, Ronald J}, - journal={Nature}, - volume={323}, - number={6088}, - pages={533--536}, - year={1986}, - publisher={Nature Publishing Group} -} - -@inproceedings{katz2017reluplex, - title={Reluplex: An efficient SMT solver for verifying deep neural networks}, - author={Katz, Guy and Barrett, Clark and Dill, David L and Julian, Kyle and Kochenderfer, Mykel J}, - booktitle={International Conference on Computer Aided Verification}, - pages={97--117}, - year={2017}, - organization={Springer} -} - -@inproceedings{katz2019marabou, - title={The Marabou framework for verification and analysis of deep neural networks}, - author={Katz, Guy and Huang, Derek A and Ibeling, Duligur and Julian, Kyle and Burns, Ryan and Sadigh, Dorsa and Barrett, Clark and Dill, David L and Kochenderfer, Mykel J}, - booktitle={International Conference on Computer Aided Verification}, - pages={443--452}, - year={2019}, - organization={Springer} -} - -@article{barrett2016smtlib, - title={The SMT-LIB standard: Version 2.6}, - author={Barrett, Clark and Stump, Aaron and Tinelli, Cesare}, - journal={Department of Computer Science, The University of Iowa, Tech. Rep}, - year={2016} -} -@misc{wang2018efficientformalsafetyanalysis, - title={Efficient Formal Safety Analysis of Neural Networks}, - author={Shiqi Wang and Kexin Pei and Justin Whitehouse and Junfeng Yang and Suman Jana}, - year={2018}, - eprint={1809.08098}, - archivePrefix={arXiv}, - primaryClass={cs.LG}, - url={https://arxiv.org/abs/1809.08098}, -} -@incollection{dantzig1947simplex, - abstract = {In 1947, George Dantzig created a simplex algorithm to solve linear programs for planning and decision-making in large-scale enterprises. The algorithm's success led to a vast array of specializations and generalizations that have dominated practical operations research for half a century}, - added-at = {2010-02-26T23:23:28.000+0100}, - address = {Piscataway, NJ, USA}, - author = {Nash, John C.}, - biburl = {https://www.bibsonomy.org/bibtex/2b85e2108e8f7cc402a52577323035ad9/ytyoun}, - booktitle = {Computing in Science and Engg.}, - doi = {10.1109/5992.814654}, - interhash = {5fb3b9e4a0e81f7811c917b86d1097cb}, - intrahash = {b85e2108e8f7cc402a52577323035ad9}, - issn = {1521-9615}, - keywords = {algorithm magazine matrix simplex top.ten.algorithms}, - number = 1, - pages = {29--31}, - publisher = {IEEE Educational Activities Department}, - timestamp = {2015-12-13T09:44:24.000+0100}, - title = {The (Dantzig) Simplex Method for Linear Programming}, - volume = 2, - year = 2000 -} -@article{zhang2018efficient, - title={Efficient Neural Network Robustness Certification with General Activation Functions}, - author={Zhang, Huan and Weng, Tsui-Wei and Chen, Pin-Yu and Hsieh, Cho-Jui and Daniel, Luca}, - journal={Advances in Neural Information Processing Systems}, - volume={31}, - pages={4939--4948}, - year={2018}, - url={https://arxiv.org/pdf/1811.00866.pdf} -} -@article{xu2020automatic, - title={Automatic perturbation analysis for scalable certified robustness and beyond}, - author={Xu, Kaidi and Shi, Zhouxing and Zhang, Huan and Wang, Yihan and Chang, Kai-Wei and Huang, Minlie and Kailkhura, Bhavya and Lin, Xue and Hsieh, Cho-Jui}, - journal={Advances in Neural Information Processing Systems}, - volume={33}, - year={2020} -} -@inproceedings{xu2021fast, - title={{Fast and Complete}: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers}, - author={Kaidi Xu and Huan Zhang and Shiqi Wang and Yihan Wang and Suman Jana and Xue Lin and Cho-Jui Hsieh}, - booktitle={International Conference on Learning Representations}, - year={2021}, - url={https://openreview.net/forum?id=nVZtXBI6LNn} -} -@article{wang2021beta, - title={{Beta-CROWN}: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification}, - author={Wang, Shiqi and Zhang, Huan and Xu, Kaidi and Lin, Xue and Jana, Suman and Hsieh, Cho-Jui and Kolter, J Zico}, - journal={Advances in Neural Information Processing Systems}, - volume={34}, - year={2021} -} -@inproceedings{shi2024genbab, - title={Neural Network Verification with Branch-and-Bound for General Nonlinearities}, - author={Shi, Zhouxing and Jin, Qirui and Kolter, Zico and Jana, Suman and Hsieh, Cho-Jui and Zhang, Huan}, - booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, - year={2025} -} -@article{zhang2022general, - title={General Cutting Planes for Bound-Propagation-Based Neural Network Verification}, - author={Zhang, Huan and Wang, Shiqi and Xu, Kaidi and Li, Linyi and Li, Bo and Jana, Suman and Hsieh, Cho-Jui and Kolter, J Zico}, - journal={Advances in Neural Information Processing Systems}, - year={2022} -} -@inproceedings{zhou2024scalable, - title={Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes}, - author={Zhou, Duo and Brix, Christopher and Hanasusanto, Grani A and Zhang, Huan}, - booktitle={The Thirty-eighth Annual Conference on Neural Information Processing Systems}, - year={2024} -} -- cgit v1.2.3