-
Can LLMs Enable Verification in Mainstream Programming?
Authors:
Aleksandr Shefer,
Igor Engel,
Stanislav Alekseev,
Daniil Berezun,
Ekaterina Verbitskaia,
Anton Podkopaev
Abstract:
Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models is becoming increasingly widespread, but it rarely considers producing strong correctness guarantees. In this study, we explore the ability of LLMs to produce verified code in three verification languages (Dafny, Nagini,…
▽ More
Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models is becoming increasingly widespread, but it rarely considers producing strong correctness guarantees. In this study, we explore the ability of LLMs to produce verified code in three verification languages (Dafny, Nagini, and Verus). To do so, we use manually curated datasets derived from the state-ofthe-art Python benchmark, HumanEval. We also assess what types of information are sufficient to achieve good-quality results.
△ Less
Submitted 18 March, 2025;
originally announced March 2025.
-
Support Vector Machine for Determining Euler Angles in an Inertial Navigation System
Authors:
Aleksandr N. Grekov,
Aleksei A. Kabanov,
Sergei Yu. Alekseev
Abstract:
The paper discusses the improvement of the accuracy of an inertial navigation system created on the basis of MEMS sensors using machine learning (ML) methods. As input data for the classifier, we used infor-mation obtained from a developed laboratory setup with MEMS sensors on a sealed platform with the ability to adjust its tilt angles. To assess the effectiveness of the models, test curves were…
▽ More
The paper discusses the improvement of the accuracy of an inertial navigation system created on the basis of MEMS sensors using machine learning (ML) methods. As input data for the classifier, we used infor-mation obtained from a developed laboratory setup with MEMS sensors on a sealed platform with the ability to adjust its tilt angles. To assess the effectiveness of the models, test curves were constructed with different values of the parameters of these models for each core in the case of a linear, polynomial radial basis function. The inverse regularization parameter was used as a parameter. The proposed algorithm based on MO has demonstrated its ability to correctly classify in the presence of noise typical for MEMS sensors, where good classification results were obtained when choosing the optimal values of hyperpa-rameters.
△ Less
Submitted 7 December, 2022;
originally announced December 2022.
-
Problems of representation of electrocardiograms in convolutional neural networks
Authors:
Iana Sereda,
Sergey Alekseev,
Aleksandra Koneva,
Alexey Khorkin,
Grigory Osipov
Abstract:
Using electrocardiograms as an example, we demonstrate the characteristic problems that arise when modeling one-dimensional signals containing inaccurate repeating pattern by means of standard convolutional networks. We show that these problems are systemic in nature. They are due to how convolutional networks work with composite objects, parts of which are not fixed rigidly, but have significant…
▽ More
Using electrocardiograms as an example, we demonstrate the characteristic problems that arise when modeling one-dimensional signals containing inaccurate repeating pattern by means of standard convolutional networks. We show that these problems are systemic in nature. They are due to how convolutional networks work with composite objects, parts of which are not fixed rigidly, but have significant mobility. We also demonstrate some counterintuitive effects related to generalization in deep networks.
△ Less
Submitted 1 December, 2020;
originally announced December 2020.
-
ECG Segmentation by Neural Networks: Errors and Correction
Authors:
Iana Sereda,
Sergey Alekseev,
Aleksandra Koneva,
Roman Kataev,
Grigory Osipov
Abstract:
In this study we examined the question of how error correction occurs in an ensemble of deep convolutional networks, trained for an important applied problem: segmentation of Electrocardiograms(ECG). We also explore the possibility of using the information about ensemble errors to evaluate a quality of data representation, built by the network. This possibility arises from the effect of distillati…
▽ More
In this study we examined the question of how error correction occurs in an ensemble of deep convolutional networks, trained for an important applied problem: segmentation of Electrocardiograms(ECG). We also explore the possibility of using the information about ensemble errors to evaluate a quality of data representation, built by the network. This possibility arises from the effect of distillation of outliers, which was demonstarted for the ensemble, described in this paper.
△ Less
Submitted 26 December, 2018;
originally announced December 2018.
