P.A. Shapkin1, A.D. Sidorov2

1,2 National Research Nuclear University MEPhI (Moscow, Russia)

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

A significant amount of work in software system development is the selection and integration of existing components. Often the searching for components reduces to text search by their descriptions. This requires human interaction in order to check the found code, since it may not correspond to the specified description. Formal proof tools make it possible to describe program specifications in the form of types, as well as to search by these specifications, but require the user to know the syntax of the formal language of types. This paper proposes an approach to searching for software components in natural language, at the same time based on verified typed specifications formalized in the Coq proof assistant. Development of a text search system for typed software components with support for natural language queries.

A prototype of a system designed for natural language search of software components by verified specifications has been implemented. Type definitions in the Coq language are used as specifications. A neural network model based on the encoder-decoder approach is used to translate expressions from the natural language. The implemented prototype provides an example of an architecture for organizing repositories of software components in order to simplify the search and selection of programs stored in them by natural language queries.

Shapkin P.A., Sidorov A.D. A natural language search system for specified software components. Information-measuring and Control Systems. 2024. V. 22. № 5. P. 80−87. DOI: https://doi.org/10.18127/j20700814-202405-09 (in Russian)

1. Annenkov D. i dr. Extracting functional programs from Coq, in Coq. arXiv:2108.02995 [cs]. 2021.
2. Volfengagen V.E. Kombinatornaya logika v programmirovanii. Vychisleniya s ob'ektami v primerakh i zadachakh. Izd. 3-e, dopoln. i pererab. M.: Institut "YurInfoR MGU". 2008. (in Russian)
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. S. 441−450.
5. Martinez-Gomez P. et al. ccg2lambda: A Compositional Semantics System. 2016. S. 85−90.
6. Vaswani A. i dr. 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. S. 1−8.
9. Hochreiter S., Schmidhuber J. Long Short-Term Memory. Neural Computation. 1997. T. 9. № 8. S 1735−1780.
10. Chung J. i dr. Empirical Evaluation of Gated Recurrent Neural Networks on Sequence Modeling. CoRR. 2014. T. 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.