А.П. Халов1, О.М. Атаева2, Н.П. Тучкова3

1–3 ФИЦ ИУ РАН (Москва, Россия)
1 Московский физико-технический институт (национальный исследовательский университет) (Москва, Россия)
1 khalov.a@phystech.edu, 2 oataeva@frccsc.ru, 3 ntuchkova@frccsc.ru

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

Цель. Реализовать подход к построению формальных математических доказательств, в котором большие языковые модели используют структурированный граф знаний SciLib, построенный на основе формальной математической библиотеки MathLib и обеспечивает прозрачность доставки контента.

Результаты. Показано, что использование явной структуры математического знания, реализованной в графе SciLib, является более интерпретируемым и надёжным примером взаимодействия между системами доказательства и большими языковыми моделями.

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

Халов А.П., Атаева О.М., Тучкова Н.П. Обоснование формальных математических доказательств с использованием больших языковых моделей и графа знаний SciLib // Системы высокой доступности. 2026. Т. 22. № 3. С. 55−70. DOI: https://doi.org/10.18127/j20729472-202603-06

1. de Moura L., Ullrich S. The Lean 4 theorem prover and programming language // Proceedings of the 28th International Conference on Automated Deduction (CADE). Springer. 2021.
2. Howard W.A. The formulae-as-types notion of construction // To H. B. Curry: Essays on Combinatory Logic. Lambda Calculus and Formalism. Academic Press. 1980. P. 479–490.
3. Wadler P. Propositions as types // Communications of the ACM. 2015. V. 58. №12. P. 75–84.
4. Martin-Löf P. Intuitionistic Type Theory. Naples: Bibliopolis. 1984.
5. The mathlib Community. The Lean mathematical library // arXiv preprint arXiv:1910.09336. 2020.
6. Yin Z., Song D., Xiong H., Yu D., Chen J. et al. DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition // arXiv preprint arXiv:2504.21801. 2025.
7. Wang H., Liu Z., Lin X., Liu J., Sung F. et al. Kimina-Prover preview: Towards large formal reasoning models with reinforcement learning // arXiv preprint arXiv:2504.11354. 2025.
8. ByteDance Seed AI4Math. Seed-Prover: Deep and broad reasoning for automated theorem proving // arXiv preprint arXiv:2507.23726. 2025.
9. Ataeva O.M., Khalov A.P., Tuchkova N.P. Multi-Level Knowledge Graph for Formal Mathematics // Lobachevskii Journal of Ma­thematics. 2026. V. 47. № 6. P. 2725–2739 https://doi.org/10.1134/S1995080226618990
10. Атаева О.М., Тучкова Н.П. Материализация онтологии научных данных через семантический граф библиотеки SciLibRu // Программирование. 2026. № 5. С. 17–36. https://doi.org/10.7868/S3034584726050039
11. Zheng K., Han J. M., Polu S. miniF2F: A cross-system benchmark for formal Olympiad-level mathematics // International Conference on Learning Representations (ICLR). 2022.
12. The Harmonic Team. Aristotle: IMO-level automated theorem proving // arXiv preprint arXiv:2510.01346. 2025.
13. Lewis P., Perez E., Piktus A., Petroni F., Karpukhin V., Goyal N., Küttler H., Lewis M., Yih W., Rocktäschel T. et al. Retrieval-augmented generation for knowledge-intensive NLP tasks // Advances in Neural Information Processing Systems. 2020. V. 33. P. 9459–9474.
14. Атаева О.М., Тучкова Н.П. Оркестрация методов анализа научных данных в процессах рецензирования // Электронные библиотеки. 2026. Т. 29. Вып. 3. С. 655–680. https://doi.org/10.26907/1562-5419-2026-29-3-655-680
15. Khalov A.P., Ataeva O.M., Tuchkova N.P. Creating a multimodal dataset for the SciLibRu semantic library using a language model // Pattern Recognition and Image Analysis. 2026. V. 36. № 2. P. 665–677. https://doi.org/10.1134/S1054661826700471
16. frenzymath/jixia: A static analysis tool for Lean 4. https://github.com/frenzymath/jixia. GitHub repository; Apache-2.0 license.
17. Hsiang R., Adkisson W., George R. J., Anandkumar A. LeanDojo-v2: A comprehensive library for AI-assisted theorem proving in Lean // NeurIPS 2025 Workshop on MATH-AI. 2025.
18. Hu L., Qin S., Liao Z., Guo Q., Wan L., Feng W., Liu Y. CoLT: Teaching multi-modal models to think with chain of latent thoughts // arXiv preprint arXiv:2606.31986. 2026. https://doi.org/10.48550/arXiv.2606.31986
19. Chen M. et al. Evaluating Large Language Models Trained on Code // arXiv 2021. https://arxiv.org/pdf/2107.03374.
20. Wilcoxon F. Individual comparisons by ranking methods // Biometrics Bulletin. 1945. V. 1. № 6. P. 80–83.