Is there any smt theories for tensor manipulations?

Question

I wonder if there is any smt theory for tensor(or multi dimensional arrays) manipulations. For example, such theory might include operators like transpose, insert, reshape, select, etc (as in numpy or in tensorflow)

Answer 1

Assuming by SMT you mean "Satisfiability Modulo Theories."

Perhaps not for arbitrary neural-nets; but ReLU's been "verified" using SMT based techniques in the past. I'm using the word "verified" in quotation marks, because it's not entirely clear what it would mean for a neural-net to be correct to start with, though there are stability inspired criteria.

For a (relatively) recent few papers on this, see:

• http://theory.stanford.edu/~barrett/pubs/KBD+17.pdf
• http://theory.stanford.edu/~barrett/pubs/JBK20.pdf
• http://theory.stanford.edu/~barrett/pubs/LAL+21.pdf