2020 year, volume 24, issue 1 (PDF)

Vtorushin Yu.I. About verification of formalized mathematical proofs

An algorithm for verification of formalized mathematical proofs is considered. Its main part is described in the framework of some production system with metavariables. Theorems of soundness and completeness are proved.

Keywords: automated theorem proving, system for automated deduction, first order language, predicate calculus, production system, artificial intelligence.

Andrew M. Mironov Verification of functional programs by state diagrams

In the paper we introduce graphical objects (called state diagrams) related to functional programs. It is shown that the state diagrams can be used to solve problems of verification of functional programs. The proposed approach is illustrated by an example of verification of a sorting program.

Keywords: program verification, functional programs, state diagrams.

Sukhareva A.V. Completeness, stability and interpretability of probabilistic topic models

Interpretability of the solution, the possibility of unsupervised learning, scalability made topic modeling one of the most popular tools for statistical text analysis. Topic models make it possible to reduce the dimension of the data space, since they describe each document as a probabilistic mixture of abstract topics, each topic as distribution over the vocabulary words of a collection. The transition from the space of words into the space of topics leads to a natural solution of the problems of synonymy and polysemy of terms. However, there are a number of disadvantages caused by the dependence of the solution on the initialization. The instability of topic models is a well-known fact, but the problem of completeness related to it is still not studied in the literature. To solve this problem, the article explores a new algorithm for finding a complete set of topics based on the building of the convex hull. Experimentally confirmed the effectiveness of this algorithm. In practice, a complete set of topics was used as the initialization of the ARTM (additive regularization for topic modeling) model. Compared with the randomized initial approximation, the basis topics allows to increase stability, perplexity by more than 10%, coherence by several times.

Keywords: probabilistic topic modeling, stability of topic models, complete set of topics of topic models, latent Dirichlet allocation, LDA, regularization, ARTM, BigARTM.

Konovalov A.Yu. The non-extensional constructive set theory is sound with respect to the sematics of the arithmetic realizability based on hyperarithmetic sorts

A semantics of the arithmetical realizability based on hyperarithmetical sorts for formulas of the language of set theory is introduced. It is proved that constructive set theory without the extensionality axiom is sound with this semantics.

Keywords: constructive semantics, realizability, arithmetical realizability, axiomatic set theory, hyperarithmetical sorts.

Khapkin A.V. On reducing the nonlinear depth of convolutional neural schemes

The paper considers one-dimensional convolutional schemes in the McCulloch-Pitts basis. It is shown that the considered schemes can be implemented by a scheme from the a priori and dynamic parts, in which the calculations in the a priori part are independent of the input data. In this case, the a priori and dynamic parts have a nonlinear depth equal to 2.

Keywords: convolutional neural network, neural scheme, nonlinear complexity, McCulloch-Pitts model.

Tsaregorodtsev K.D. On the relationship between proper families and edge orientations of Boolean cubes

This paper is devoted to the study of relationship between proper families of Boolean functions and unique sink orientations of cubes. A one-to-one correspondence between these two objects is established, a number of properties are carried over from unique sink orientations to proper families. These results include an upper bound for the number of proper families of given size and coNP-completeness of the problem of recognizing properness.

Keywords: proper families of Boolean functions, unique sink orientations.

Vedernikov I.K. A class of machine sufficient for optimal prediction of general regular super-events

The machine predicts the next character of the input sequence if it outputs that character the moment before. The paper considers the machine class contraction for the task of predicting an arbitrary general regular super-event in the multivalued alphabet. The class of machine sufficient for the predicting problem is obtained in this paper. In addition, the transition from the estimations of simple super-events to the estimations of the complex super-events is proved with the help of the class aforementioned.

Keywords: predicting machine, prediction of superwords by a machine, general regular super-events.

Gremyakov A.O. Estimation of the maximum number of nonzero coefficients of a function polynomial under the action of a permutation group on a table of function values

For coefficients of polynomials of functions over finite fields Fq , we consider the problem of finding a lower bound for the maximum minimum of the number of nonzero coefficients in the polynomial, where the maximum is taken over all functions and the minimum is taken from their transformations corresponding to various field assignments. Moreover, various types of such transformations are considered. The main results of the paper relate to two types of transformations, the description of which is given in the first section of the paper. The paper estimates L(q) ≥ q − 2 for the maximum minimum of the number of nonzero coefficients in the polynomial for the certain type of transformations that leave the zero field element in place.

Keywords: coefficients of polynomials, Boolean functions, polynomial of a Boolean function, table of values of a function, sagemath.

Dergach P.S., Bulgakov L.R. About the dimension difference of periodic subsets of the natural series

This work is devoted to describing the change in the dimension of periodic subsets of the natural series with seemingly insignificant operations like removal/addition to the set of one number. The case is investigated when the dimension of the initial set is equal to 1 or 2. By the dimension of the set is meant the minimum number of disjoint arithmetic progressions that give this set in the union. For sets of dimension 2 the result is obtained only in cases of pairs of general position progressions. In this paper we give the results on how the dimension changes depending on whether the number x is deleted/added to.

Keywords: arithmetic progression, natural series, progressive set.

Popkov K.A. Short single diagnostic tests for contact circuits under breaks and closures of contacts

We prove that almost any Boolean function on n variables can be implemented by an irredundant two-pole contact circuit allowing a single diagnostic test of length 8 regarding breaks and closures of contacts.

Keywords: contact circuit, Boolean function, contact break, contact closure, single diagnostic test.

← Back to archive