The analogy theorem in Hoare logic

Nikitin Nikita

Home/Archive/arXiv

arXiv · 2510.03685

The analogy theorem in Hoare logic

Nikitin Nikita

View original source ↗Read source document ↗Export metadata ↓

Abstract

The introduction of machine learning methods has led to significant advances in automation, optimization, and discoveries in various fields of science and technology. However, their widespread application faces a fundamental limitation: the transfer of models between data domains generally lacks a rigorous mathematical justification. The key problem is the lack of formal criteria to guarantee that a model trained on one type of data will retain its properties on another.This paper proposes a solution to this problem by formalizing the concept of analogy between data sets and models using first-order logic and Hoare logic.We formulate and rigorously prove a theorem that sets out the necessary and sufficient conditions for analogy in the task of knowledge transfer between machine learning models. Practical verification of the analogy theorem on model data obtained using the Monte Carlo method, as well as on MNIST and USPS data, allows us to achieving F1 scores of 0.84 and 0.88 for convolutional neural networks and random forests, respectively.The proposed approach not only allows us to justify the correctness of transfer between domains but also provides tools for comparing the applicability of models to different types of data.The main contribution of the work is a rigorous formalization of analogy at the level of program logic, providing verifiable guarantees of the correctness of knowledge transfer, which opens new opportunities for both theoretical research and the practical use of machine learning models in previously inaccessible areas.

Explore related subjects

stat.ML cs.LG math.LO stat.CO stat.ME

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Nikitin Nikita. 2025-10-04. The analogy theorem in Hoare logic. https://arxiv.org/abs/2510.03685

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Robust Mixture Models for Algorithmic Fairness Under Latent Heterogeneity

Machine learning models optimized for average performance can perform poorly on vulnerable subpopulations. Existing approaches often rely on groups specified in advance, yet fairness-relevant subgroup structure may be latent, intersectional, and driven by complex interactions among continuous and discrete attributes. We introduce \textbf{ROME} (\textbf{\underline{RO}}bust \textbf{\underline{M}}ixture \textbf{\underline{E}}nsemble), a framework that learns latent group structure while optimizing worst-group predictive performance. ROME connects latent-variable modeling with distributionally robust optimization (DRO) through two complementary approaches: an Expectation-Maximization formulation with robust aggregation for linear models and a neural Mixture-of-Experts formulation for nonlinear settings. Across simulations and three real-world regression datasets, ROME improves worst-group performance while maintaining competitive overall accuracy, including in comparisons with established group-aware and group-label-free robust learning methods. ROME provides a flexible approach to robust prediction when fairness-relevant attributes are available for subgroup discovery but their direct use in group-specific outcome models is restricted.

stat.ML↗

arXiv2026

Boltzmann generators for amorphous particle systems

Sampling configurations in thermodynamic equilibrium is a long-standing challenge in statistical physics. Boltzmann generators address this problem by employing generative models to propose independent configurations, which are then reweighted via importance sampling using exact likelihood evaluations. Recent Boltzmann Generators based on continuous normalizing flows and flow matching have achieved significant success for particle systems and biomolecules. However, these approaches have not been extended to amorphous materials (glasses), for which equilibrium sampling is notoriously slow. Because of their disordered structure, the invariances and geometrical constraints of amorphous materials differ from those of crystals and biomolecules, preventing the direct use of existing generative models. Here, we develop Boltzmann Generators tailored to amorphous materials by building the required equivariances directly into Riemannian stochastic interpolants. Our framework incorporates periodic boundary conditions and particle symmetries using equivariant graph neural networks. Numerical experiments demonstrate that enforcing physical symmetries significantly improves the accuracy of Boltzmann Generators, but also reveal an intrinsic limitation of the continuous-flow formulation: accumulated numerical errors during likelihood integration break time-reversibility, compromising exact thermodynamic reweighting. These results reveal a fundamental challenge for continuous-flow generative models in statistical mechanics and call for alternative approaches that preserve exact thermodynamic consistency.

stat.ML↗

arXiv2026

Diagonalized Attention for Individualized Regression: Latent-Row Localization and Prediction

Modern text and image representations are often matrix-valued, with rows corresponding to tokens, patches, or other local feature vectors. Predictive information is often sparse but sample-specific, making classical sparse regression methods with a common support poorly suited to this heterogeneity. This paper formalizes an individualized sparse regression framework for matrix-valued covariates in which each observation has its own rows of interest, while the associated regression effects are shared across the population. To estimate this model, we introduce a diagonalized attention mechanism that uses query--key scores to localize sample-specific signal rows and a value matrix for downstream regression. The proposed method has a parameter dimension independent of sample size and can identify rows of interest for new observations without their responses. We establish existence theorems showing that, under suitable score-separation and concentration conditions, single-head and multi-head diagonalized attention models recover the latent rows with high probability, yielding prediction risk bounds. Our theory therefore provides a statistical explanation of how attention-based scoring localizes sample-specific signals in heterogeneous matrix-valued data. Simulations demonstrate strong prediction and localization in regression and misspecified classification across varying sample sizes, dimensions, and signal cardinalities. Real sentiment analyses show improved classification accuracy and interpretable token selection.

stat.ML↗