[question] ReLU support in Z3 linear arithmetics #5847
-
|
Does Z3 support this, similar (or better) as described in https://link.springer.com/chapter/10.1007/978-3-319-63387-9_5? |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment
-
|
It isn't suitable because the main engine uses infinite precision arithmetic, so far mainly suitable for standard program verification but not best for optimization and areas where you have decimal points and can tolerate FP errors to some bounds. To get an overview of verification techniques for the area check out the tutorial session at https://cpaior2021.dbai.tuwien.ac.at/ on techniques up to summer 2021 in this domain. There are many more recent techniques, also using MIP solvers that use FP and other heuristics for conditional inequalities. |
Beta Was this translation helpful? Give feedback.
It isn't suitable because the main engine uses infinite precision arithmetic, so far mainly suitable for standard program verification but not best for optimization and areas where you have decimal points and can tolerate FP errors to some bounds. To get an overview of verification techniques for the area check out the tutorial session at https://cpaior2021.dbai.tuwien.ac.at/ on techniques up to summer 2021 in this domain. There are many more recent techniques, also using MIP solvers that use FP and other heuristics for conditional inequalities.