验证 Tsetlin 机器的性质

Tsetlin 机器（TsMs）是一种有前景且可解释的机器学习方法，可应用于多种分类任务。我们提出了将 TsMs 精确编码为命题逻辑的方法，并使用 SAT 求解器形式化验证 TsMs 的性质。特别地，我们在本工作中引入了机器学习模型相似性的概念，并将该概念应用于检查 TsMs 的相似性。我们还考虑了文献中的鲁棒性与等价性概念，并针对 TsMs 进行了适配。随后，我们展示了编码的正确性，并给出了关于以下性质的结果：TsMs 的对抗鲁棒性、等价性与相似性。在我们的实验中，我们分别采用 MNIST 和 IMDB 数据集进行图像与情感分类。我们将使用 TsMs 获得的鲁棒性验证结果与文献中使用二值神经网络在 MNIST 上获得的结果进行了讨论。