Hacker News new | ask | show | jobs
by mpcsb 221 days ago
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.