Geodesic
Adaptive human–machine theorem proving system
Izvestiya Instituta Matematiki i Informatiki Udmurtskogo Gosudarstvennogo Universiteta, Tome 64 (2024), pp. 17-33.

Voir la notice de l'article provenant de la source Math-Net.Ru

This paper presents a novel approach to constructing human–machine theorem proving systems. These systems integrate machine learning capabilities, human expert knowledge, and rigorous logical control for the effective construction and verification of proofs. The innovation of this approach lies in its openness: the user is given a tool for building such systems. Users can create theorem proving systems by selecting existing logical inference strategies or adding new ones in accordance with the provided interfaces or relationship agreements. The systems being built have a significant human–machine adaptive nature. During their operation, a meta-strategy is developed and trained based on the foundational elements of the existing strategies. The system is designed as a universal framework for managing various strategies, with the provision of a basic architecture and a library of strategies with the possibility of adding new ones. During the learning process, a system of structural characteristics is also accumulated and trained, on the basis of which a decision is made on the use of specific strategy elements at the next step. The presentation is conducted for the sequential calculus of minimal positive predicate logic as the most suitable for the deductive synthesis of programs and algorithms, for which it is proposed to use this approach.
Keywords: automated theorem proving, minimal predicate logic, machine learning, human–machine interaction, artificial intelligence, sequential calculus, deep learning, proof verification 
@article{IIMI_2024_64_a1,
     author = {M. Joudakizadeh and A. P. Bel'tyukov},
     title = {Adaptive human{\textendash}machine theorem proving system},
     journal = {Izvestiya Instituta Matematiki i Informatiki Udmurtskogo Gosudarstvennogo Universiteta},
     pages = {17--33},
     publisher = {mathdoc},
     volume = {64},
     year = {2024},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/IIMI_2024_64_a1/}
}
TY  - JOUR
AU  - M. Joudakizadeh
AU  - A. P. Bel'tyukov
TI  - Adaptive human–machine theorem proving system
JO  - Izvestiya Instituta Matematiki i Informatiki Udmurtskogo Gosudarstvennogo Universiteta
PY  - 2024
SP  - 17
EP  - 33
VL  - 64
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/IIMI_2024_64_a1/
LA  - en
ID  - IIMI_2024_64_a1
ER  - 
%0 Journal Article
%A M. Joudakizadeh
%A A. P. Bel'tyukov
%T Adaptive human–machine theorem proving system
%J Izvestiya Instituta Matematiki i Informatiki Udmurtskogo Gosudarstvennogo Universiteta
%D 2024
%P 17-33
%V 64
%I mathdoc
%U http://geodesic.mathdoc.fr/item/IIMI_2024_64_a1/
%G en
%F IIMI_2024_64_a1
M. Joudakizadeh; A. P. Bel'tyukov. Adaptive human–machine theorem proving system. Izvestiya Instituta Matematiki i Informatiki Udmurtskogo Gosudarstvennogo Universiteta, Tome 64 (2024), pp. 17-33. http://geodesic.mathdoc.fr/item/IIMI_2024_64_a1/

[1] Novikov P.S., Constructive mathematical logic from the point of view of classical one, Nauka, Moscow, 1977

[2] Kolmogoroff A., “On the principle tertium non datur”, Matematicheskii Sbornik, 32:4 (1925), 646–667 (in Russian)

[3] Shanin N.A., “Constructive real numbers and constructive functional spaces”, Trudy Matematicheskogo Instituta imeni V.A. Steklova, 67 (1962), 15–294 (in Russian) | Zbl

[4] Robinson J.A., “A machine-oriented logic based on the resolution principle”, Journal of the ACM (JACM), 12:1 (1965), 23–41 | DOI | MR | Zbl

[5] Dragalin A.G., Constructive proof theory and non-standard analysis, URSS, Moscow, 2003 | MR

[6] Isabelle: A generic theorem prover, ed. Paulson L.C., Springer, Berlin–Heidelberg, 1994 | DOI | MR | Zbl

[7] Harrison J., “HOL Light: A tutorial introduction”, Formal Methods in Computer-Aided Design, Springer, Berlin–Heidelberg, 1996, 265–269 | DOI

[8] Wiedijk F., The seventeen provers of the world, Springer, Berlin–Heidelberg, 2006 | DOI

[9] Lenat D.B., “Eurisko: a program that learns new heuristics and domain concepts: the nature of heuristics III: program design and results”, Artificial Intelligence, 21:1–2 (1983), 61–98 | DOI

[10] Urban J., “MaLARea: a metasystem for automated reasoning in large theories”, ESARLT, 257 (2007) https://ceur-ws.org/Vol-257/05_Urban.pdf

[11] Bansal K., Loos S.M., Rabe M.N., Szegedy C., Wilcox S., “HOList: An environment for machine learning of higher-order theorem proving”, 2019, arXiv: 1904.03241 [cs.LO] | DOI

[12] Piotrowski B., Urban J., “ATPboost: Learning premise selection in binary setting with ATP feedback”, Automated Reasoning, Springer, Cham, 2018, 566–574 | DOI | MR | Zbl

[13] Kaliszyk C., Urban J., Michalewski H., Olšák M., “Reinforcement learning of theorem proving”, 2018, arXiv: 1805.07563 [cs.AI] | DOI

[14] Huang D., Dhariwal P., Song D., Sutskever I., “Gamepad: A learning environment for theorem proving”, 2018, arXiv: 1806.00608 [cs.LG] | DOI

[15] Polu S., Sutskever I., “Generative language modeling for automated theorem proving”, 2020, arXiv: 2009.03393 [cs.LG] | DOI

[16] Wu Y., Jiang A.Q., Li W., Rabe M.N., Staats C., Jamnik M., Szegedy C., “Autoformalization with large language models”, 2022, arXiv: 2205.12615 [cs.LG] | DOI

[17] Polu S., Han J.M., Zheng K., Baksys M., Babuschkin I., Sutskever I., “Formal mathematics statement curriculum learning”, 2022, arXiv: 2202.01344 [cs.LG] | DOI

[18] Chen W., Yin M., Ku M., Lu P., Wan Y., Ma X., Xu J., Wang X., Xia T., “TheoremQA: A theorem-driven question answering dataset”, Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, 2023, 7889–7901 | DOI

[19] Gauthier T., Kaliszyk C., Urban J., Kumar R., Norrish M., “TacticToe: learning to prove with tactics”, Journal of Automated Reasoning, 65:2 (2021), 257–286 | DOI | MR | Zbl

[20] Li W., Yu L., Wu Y., Paulson L.C., “Isarstep: a benchmark for high-level mathematical reasoning”, 2020, arXiv: 2006.09265 [cs.LO] | DOI

[21] Yang K., Swope A.M., Gu A., Chalamala R., Song P., Yu S., Godil S., Prenger R., Anandkumar A., “Leandojo: Theorem proving with retrieval-augmented language models”, 2023, arXiv: 2306.15626 [cs.LG] | DOI