My post:
I used the Z3 SMT solver to test if two models are logically equivalent across the entire input space (not just in the sample data).
It either finds a counterexample or proves none exists.
To be considered when simplifying complex models or when retraining routines in mlops.
Post includes code and discussion.
