The analogy theorem in Hoare logic for formal verification of knowledge transfer in machine learning

The introduction of machine learning methods has led to significant advances in automation, optimization, and new discoveries in various fields of science and engineering. However, their widespread application faces a fundamental limitation: the models are inapplicable to different data types, and they typically lack rigorous mathematical justification. A key problem is the lack of formal criteria to ensure that a model trained on one data type will retain its properties on another. This paper proposes a solution to this problem by formalizing the concept of "analogy" between datasets and models using first-order logic and Hoare logic. We formulate and prove theorems that establish necessary and sufficient conditions for analogy in the problem of knowledge transfer between machine learning models. A practical test of the analogy theorem on simulated data obtained using the Monte Carlo method, as well as on MNIST and USPS data, showed that the MLP + MDM model demonstrates a classification accuracy of 0.874 on Source MLP MNIST, while it achieves 0.915 on Target and Hybrid.