Human-machine collaborative deductive program synthesis
Аннотация
СОВМЕСТНЫЙ ДЕДУКТИВНЫЙ ПРОГРАММНЫЙ СИНТЕЗ ЧЕЛОВЕКА И МАШИНЫ
Аббаси М. М., Джудакизаде М., Бельтюков А. П.
Традиционные подходы, используемые для дедуктивного синтеза программ, обеспечивают высокую точность анализа проблем и выработки решений. Однако для понимания и интерпретации решений требуются обширные знания и глубокое понимание формальной логики. Это создает значительный барьер между человеческой логикой и ее реализацией в программах синтеза с использованием дедуктивного подхода. В этой статье предлагается новый совместный подход человека и машины к дедуктивному синтезу программ, который использует взаимные преимущества человеческой интуиции и продвинутых логических вычислений. Наша методология объединяет постановку задачи человеком, ее автоматизированную формализацию с помощью больших языковых моделей, проверку проблемы человеком, машинный синтез программ на основе конструктивных выводов, их выполнение и итеративные обратные связи в процессе синтеза программы. Мы демонстрируем практическую применимость этого подхода на примере конкретного случая, который заключается в выводе технологий производства продукции из базы данных, которая одновременно генерирует и обрабатывает информацию. Эта структура позволяет людям демократизировать доступ к мощным формальным методам и ускорить разработку сложных, логически обоснованных программных решений.
Ключевые слова
Полный текст:
PDF (English)Литература
Abbasi M. M., Beltiukov A. Summarizing emotions from text using Plutchik’s Wheel of Emotions // 7th Scient. Conf. Information Technologies for Intelligent Decision Making Support (ITIDS 2019). Atlantis Press, 2019. (Advances in Intelligent Systems ResearchVol. 166). P. 291-294. 10.2991/itids-19.2019.52.
Beltyukov A. P., Abbasi M. M. Logical analysis of emotions in text from natural language // Bulletin of Udmurt University. Mathematics. Mechanics. Computer Science.. 2019. Vol. 29, issue 1. P. 106-116. ZFAVBB.
Bratko I. Prolog programming for artificial intelligence. Pearson education, 2001.
Chen M., Tworek J., et al. Evaluating large language models trained on code, 2021. arXiv preprint arXiv:2107.03374. 10.48550/arXiv.2107.03374.
Coda-Forno J., Binz M., et al. CogBench: a large language model walks into a psychology lab. arXiv preprint arXiv:2402.18225. 2024. 10.48550/arXiv.2402.18225.
Colmerauer A., Roussel P. The birth of Prolog. History of programming languages—II, 1996. P. 331-367. https://doi.org/10.1145/234286.105782014.
Covington M. A., Nute D., Vellino A. Prolog Programming in Depth. Prentice-Hall, 1996.
De Moura L., Kong S., et al. The Lean theorem prover (system description). Automated Deduction-CADE-25: 25th Int. Conf. Automated Deduction, Berlin, Germany, August 1-7, 2015, Proc. 25. P. 378-388. 10.1007/978-3-319-21401-6_26.
De Bruijn, N. G. The mathematical language AUTOMATH, its usage, and some of its extensions // Studies in Logic and the Foundations of Mathematics, 1994. Vol. 133, P. 73-100. 10.1016/S0049-237X(08)70200-3.
Gökbakan Ü. B., Dümbgen F., Caron S. A Data-driven Contact Estimation Method for Wheeled-Biped Robots. 2024. P. 2410.12345. 10.48550/arXiv.2410.12345.
Herman G. Faster general parsing through context-free memorization // Proc. 41st ACM SIGPLAN Conf. on Programming Language Design and Implementation, 2020. P. 1022-1035. 10.1145/3385412.3386032.
Itzhaky S., Peleg H., et al. Deductive synthesis of programs with pointers: techniques, challenges, opportunities // Int. Conf. Computer Aided Verification. 2021. P. 110-134. 10.1007/978-3-030-81685-8_5.
Jain N., Vaidyanath S., et al. Jigsaw: Large language models meet program synthesis // Proc. 44th Int. Conf. Software Engineering. 2022. P. 1219-1231. 10.1145/3510003.3510203.
Jiang M., Jain A., et al. SIMCOPILOT: Evaluating Large Language Models for Copilot-Style Code Generation. 2025. 10.48550/arXiv.2505.21514.
Joudakizadeh M., Bel’tyukov A. P. Two-level realization of logical formulas for deductive program synthesis // Vestn. Udmurtsk. Univ. Mat. Mekh. Komp. Nauki, 2024. Vol. 34, No. 4. P. 469–485. 10.35634/vm240401. JLCQGU.
Joudakizadeh M., Bel’tyukov A. P. Adaptive human–machine theorem proving system // Izv. IMI UdGU, 64. 2024. P. 17-33. 10.35634/2226-3594-2024-64-02. BVQGKJ.
Kupferman O., Leshkowitz O. Synthesis with guided environments // Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems. 2025. P. 198-216. 10.1007/978-3-031-90653-4_10.
Li Y., Parsert J., Polgreen E. Guiding enumerative program synthesis with large language models // Int. Conf. Computer Aided Verification. 2024. P. 280-301. 10.1007/978-3-031-65630-9_15.
Liventsev V., Grishina, A., Härmä A., Moonen L. Fully autonomous programming with large language models. Proceedings of the Genetic and Evolutionary Computation Conference. 2023. P. 1146-1155). 10.1145/3583131.3590481.
Manna Z., Waldinger R. Fundamentals of Deduct Program Synthesis (No. SRITN503), 1992.
Mündler N., He J., et al. Type-constrained code generation with language models // Proc. ACM on Programming Languages, 9 (PLDI). 2025. P. 601-626. 10.1145/372927415.
Polu S., Sutskever I. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393. 2020. 10.48550/arXiv.2009.03393.
Singh P., Lau E. T., et al. Comparison of models for the warm-hot circumgalactic medium around Milky Way-like galaxies // Monthly Notices of the Royal Astron. Society. 2024. Vol. 532. № 3. P. 3222-3235. 10.1093/mnras/stae1695. CYPCAI.
Wang M., Deng J. Learning to prove theorems by learning to generate theorems. Advances in neural information processing systems. 2020. Vol. 33, P. 18146-18157. 10.48550/arXiv.2002.07019.
Wei A., Suresh T., et al. Codearc: Benchmarking reasoning capabilities of LLM agents for inductive program synthesis. 2025. 2503.23145. 10.48550/arXiv.2503.23145.
Wielemaker J., Schrijvers T., et al. Swi-prolog // Theory and Practice of Logic Programming. 2012. Vol. 12. No. 1. P. 67-96. 10.1017/S1471068411000494.
Yang Z., Sergey I. Inductive synthesis of inductive heap predicates // Proc. ACM on Programming Languages, 9(OOPSLA1). 2025. P. 169-195. 10.1145/3720420. IVSWVQ.
Zenkner J., Sesterhenn T., Bartelt C. Transductively Informed Inductive Program Synthesis. 2025. P. 2505. 14744. 10.48550/arXiv.2505.14744.
DOI: https://doi.org/10.54708/SIIT-2026-no3-p22
Ссылки
- На текущий момент ссылки отсутствуют.
(c) 2026 M. M. Abbasi, M. Joudakizadeh, A. P. Beltiukov