diff options
Diffstat (limited to 'chapters/core/implementation/04-python-module.tex')
| -rw-r--r-- | chapters/core/implementation/04-python-module.tex | 6 |
1 files changed, 3 insertions, 3 deletions
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} |