Solving formalizable mathematical problems using computers remains a relevant challenge with several fundamentally different approaches. A significant contribution to this field was made by A. S. Podkolzin, who proposed an original solver architecture based on logical inference using term rewriting rules. This article describes the architecture of a simplified system that implements the key ideas of this approach: an attention-switching mechanism via levels, organization of a rule base, and context representation with metadata.

The beginning of the 21st century in data science is characterized by the emergence of new interdisciplinary fields as well as an expansion of the general theoretical framework and development of statistical methods for solving novel problems. This article describes known approaches to addressing the problem of statistical identification of unidirectional (causal) relationships between variables using non-experimental data, and highlights distinctive features of statistical models employed for this purpose. It also considers a case study on generating data with nonlinear dependencies among variables through convolutional neural networks, where two different estimation techniques are investigated — Bayesian networks and double machine learning. The results show that both these approaches yield inaccurate estimates of individual effects in the considered scenario, and recommendations are provided regarding aggregated effect evaluation.

We present a formal study of the Istanbul BFT (IBFT) protocol family that connects its vulnerable early design, corrected intermediate variants, and a censorship-resistant modification within a unified verification framework. Using TLA+ specifications and TLC model checking, we (i) obtain counterexample traces demonstrating safety violations in the first IBFT version, (ii) verify safety and liveness for a corrected QBFT variant, and (iii) formalize censorship resistance for leader-based Byzantine consensus as a bounded chain-quality requirement and show that standard leader rotation can violate it. We then introduce and verify the f-skip leader-selection rule, which enforces censorship resistance while preserving the original safety and liveness guarantees.

Word vector representations are widely used in machine translation, recommender systems, and information retrieval. The quality of such representations, measured as the rank correlation with expert assessments of semantic similarity, remains limited. This paper proposes an approach to improving the quality of word vector representations by merging several independent sources of primary representations. The notions of monotone and antimonotone quadruplets of words are introduced, and the hypothesis that the information contained in monotone quadruplets allows one to recover the true order of similarities for antimonotone quadruplets is formulated and verified. A method for selecting word quadruplets, a two-step correction procedure based on a fully connected layer and a quadruplet loss function, as well as a method for evaluating the quality of the resulting representations are proposed. Experimental results on Word2Vec and GloVe models trained on a lemmatised Wikipedia corpus demonstrate the feasibility of improving representation quality when evaluated on the MEN, SimLex-999, and WordSim-353 expert datasets.

The development of deep learning models for classification tasks poses particular challenges when dealing with a large number of classes under conditions of limited data and computational resources. Metric learning offers a promising approach to solving this problem, although its effectiveness is often limited by inherent shortcomings of standard loss functions, such as contrastive and triplet losses, as well as suboptimal training sample selection strategies. This paper presents solutions to these issues: a novel autoprobabilistic mining method for example selection and an improved metric loss function. The proposed autoprobabilistic mining method aids in selecting the most informative example pairs for training Siamese neural networks. In combination with a previously developed autoclustering method, this approach enhances training efficiency by maximizing data utility while minimizing computational costs. Additionally, a new triplet-based metric loss function is introduced, which accounts for cluster-specific characteristics and is designed to overcome specific drawbacks of traditional contrastive and triplet loss functions, thereby improving the process of feature embedding formation. The effectiveness of the proposed methods was validated through experiments on optical character recognition using the PHD08 (Korean alphabet) and Omniglot datasets. For the full Korean alphabet in the PHD08 dataset, the novel loss function with random mining achieved a classification accuracy of \(82.6\%\), establishing a new benchmark. Using a reduced alphabet, a baseline of \(88.6\%\) was set on PHD08. The application of the auto-probabilistic mining method alone improved accuracy to \(90.6\%\) (\(+2.0\%\)), and its combination with auto-clustering further increased it to \(92.3\%\) (\(+3.7\%\)). On the Omniglot dataset, the proposed mining method attained \(92.32\%\), which rose to \(93.17\%\) when coupled with auto-clustering. The results demonstrate that the proposed loss function and mining strategy offer a robust and effective solution for complex pattern recognition tasks, especially in scenarios characterized by a high number of classes and resource limitations.

The problem of the magnitude of the restriction in a \(k\)-digit set on the permissible deviation from the average count of digits having each of the \(k\) values under the condition of a given proportion of such sequences. An approach is proposed that allows monitoring the influence of various parameters on the final result at each stage, and estimates of the accuracy of the approximate solution are provided.

The paper addresses the problem of asymptotic complexity of implementing systems of Boolean functions in the model of cellular circuits composed of functional and switching elements. The main focus is on deriving high-accuracy asymptotic estimates for the area of cellular circuits realizing sufficiently large classes of Boolean functions. Methods for obtaining upper and lower asymptotic bounds applicable to wide classes of functions are formulated. As a consequence of these methods, high-accuracy asymptotic estimates are obtained for the system of all self-dual Boolean functions. Upper bounds are derived using a constructive approach based on reducing the considered classes of functions to universal multipoles of smaller order and subsequent modification of the corresponding cellular circuits. As a result, matching upper and lower asymptotic bounds on the circuit area are established for the class of self-dual Boolean functions, leading to an asymptotic equality for the order of growth of their implementation complexity in the cellular circuit model.

This article provides a survey of circuit complexity bounds for basic boolean transforms exploited in digital circuit design and efficient methods for synthesizing such circuits. The exposition covers structurally simple functions and operators, such as counters, adders, encoders, and multiplexors, and excludes more complex algebraic operations with numbers, polynomials, and matrices. Several applications to implementing more specific operations are also discussed.