П.А. Шапкин1, А.Д. Сидоров2

1,2 Национальный исследовательский ядерный университет «МИФИ» (Москва, Россия)

1 pashapkin@mephi.ru, 2 adsidoroff@gmail.com

Постановка проблемы. Значительный объем трудозатрат при разработке программных систем часто состоит в подборе и интеграции существующих компонентов. При этом средства поиска компонентов сводятся к текстовому поиску по их описаниям. Это требует человеческого труда по проверке найденного кода, так как он может не соответствовать заданному описанию. Инструменты формального доказательства дают возможность описывать спецификации программ в виде типов, а также проводить поиск по этим спецификациям, но требуют от пользователя знания синтаксиса формального языка типов. Данная работа предлагает подход к поиску программных компонентов на естественном языке, основанный в то же время на верифицированных ти́повых спецификациях программ, формализованных в системе Coq.

Цель. Разработать систему текстового поиска типизированных программных компонентов с поддержкой структуры формул Coq по естественно-языковым запросам.

Результаты. Реализован прототип системы, предназначенной для естественно-языкового поиска программных компонентов по верифицированным спецификациям. В качестве спецификаций применены типовые определения на языке Coq. Для перевода выражений с естественного языка использована нейросетевая модель на основе подхода кодировщик-декодировщик.

Практическая значимость. Реализованный прототип дает пример архитектуры для организации репозиториев программных компонентов с целью упрощения поиска и подбора хранимых в них программ по естественно-языковым запросам.

1. Annenkov D. и др. Extracting functional programs from Coq, in Coq // arXiv:2108.02995 [cs]. 2021.
2. Вольфенгаген В.Э. Комбинаторная логика в программировании. Вычисления с объектами в примерах и задачах. Изд. 3-е, дополн. и перераб. М.: Институт «ЮрИнфоР МГУ». 2008.
3. Coq documentation. Introduction and contents // Introduction and Contents - Coq 8.15.0 documentation.
4. Woods W.A. Progress in Natural Language Understanding: An Application to Lunar Geology // Proceedings of the June 4−8 1973. National Computer Conference and Exposition. New York. NY. USA: Association for Computing Machinery. 1973. С. 441−450.
5. Martinez-Gomez P. et al. ccg2lambda: A Compositional Semantics System. 2016. С. 85−90.
6. Vaswani A. и др. Attention Is All You Need. 2017.
7. Cho K. et al. On the Properties of Neural Machine Translation: Encoder-Decoder Approaches // arXiv. 2014.
8. Levkovskyi O., Li W. Generating Predicate Logic Expressions from Natural Language // SoutheastCon. 2021. С. 1−8.
9. Hochreiter S., Schmidhuber J. Long Short-Term Memory // Neural Computation. 1997. Т. 9. № 8. С 1735−1780.
10. Chung J. и др. Empirical Evaluation of Gated Recurrent Neural Networks on Sequence Modeling // CoRR. 2014. Т. abs/1412.3555.
11. ANTLR. ANTLR (ANother Tool for Language Recognition). 2023.
12. Bahdanau D., Cho K., Bengio Y. Neural Machine Translation by Jointly Learning to Align and Translate // arXiv. 2014.
13. OpenAI. GPT-4 Technical Report. 2023.