Model Equivalence using Z3

1 min read
Luis QuintanillaLuis Quintanilla

→ https://www.testingbranch.com/Z3-and-model-equivalence/

  • We can formally prove two models behave identically.
  • Use it to validate pruning / distillation work.
  • Use it to guard model retraining in CI/CD.
  • If models diverge, Z3 gives the input that caused the divergence.

    No brute force, no test dataset guesses.

    Just mathematically guaranteed model equivalence (or a counterexample).

Interesting use of Z3