Unsupervised Learning (UL) implementations are widely used, but prone to issues such as nondeterminism and inconsistency, which makes them unreliable and exploitable. Moreover, the lack of a specification (or ground truth) makes UL implementations hard to verify or test: when they produce diverging results on a dataset, they do so subtly and silently, which gives users a false sense of security, and complicates developers’ job of tracing the error to its root cause. We introduce an approach, Ocelot, that reduces nondeterminism/inconsistency checking to satisfiability checking in Z3. Given the Python code of an UL implementation, Ocelot automatically isolates a nondeterministic “kernel” (variables and code), which forms the basis for a Z3 specification. A Z3-found solution acts as a “witness” dataset – a typically small dataset that can be used to reliably reproduce the error. Ocelot has exposed sources of nondeterminism and inconsistency in popular implementations (Scikit-learn, MATLAB, and R) of well-known Clustering algorithms (Affinity Propagation, DBSCAN, HAC, and K-means) and Anomaly Detection algorithms (Isolation Forest, Local Outlier Factor). Moreover, Ocelot has exposed regressions (changes in semantics) in the evolution of these implementations.

@inproceedings{paperbot11626,
  title = {Checking Unsupervised Learning for Nondeterminism and Inconsistency via SMT Solving},
  author = {Muyeed Ahmed and Iulian Neamtiu},
  booktitle = {ICSE},
  year = {2026},
  doi = {10.1145/3744916.3787844}
}