Projects funded by the NCN


Information on the principal investigator and host institution

Information of the project and the call

Keywords

Equipment

Delete all

Deep Neural Architectures for Automated Theorem Proving

2018/29/N/ST6/02903

Keywords:

deep learning neural networks automated theorem proving automated reasoning artificial intelligence

Descriptors:

  • ST6_7: Artificial intelligence, intelligent systems, multi-agent systems
  • ST6_11: Machine learning, statistical data processing and applications using signal processing (e.g. speech, image, video)
  • ST6_4: Formal methods, foundations of computer science, including theoretical computer science, quantum algorithms

Panel:

ST6 - Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems

Host institution :

Uniwersytet Warszawski, Wydział Matematyki, Informatyki i Mechaniki

woj. mazowieckie

Other projects carried out by the institution 

Principal investigator (from the host institution):

Bartosz Piotrowski 

Number of co-investigators in the project: 2

Call: PRELUDIUM 15 - announced on 2018-03-15

Amount awarded: 119 100 PLN

Project start date (Y-m-d): 2019-01-24

Project end date (Y-m-d): 2023-01-23

Project duration:: 48 months (the same as in the proposal)

Project status: Project settled

Project description

Download the project description in a pdf file

Note - project descriptions were prepared by the authors of the applications themselves and placed in the system in an unchanged form.

Equipment purchased [PL]

  1. Stacja robocza (8 000 PLN)
  2. Karta graficzna NVIDIA GeForce GTX 1080 Ti (lub podobna) (4 000 PLN)

Information in the final report

  • Articles in post-conference publications (5)
  1. ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine
    Authors:
    Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
    Conference:
    Automated Reasoning - 10th International Joint Conference (rok: 2020, ), Wydawca: Springer
    Data:
    konferencja 44013
    Status:
    Published
  2. Guiding Inferences in Connection Tableau by Recurrent Neural Networks
    Authors:
    Bartosz Piotrowski, Josef Urban
    Conference:
    13th Conference on Intelligent Computer Mathematics (rok: 2020, ), Wydawca: Springer LNCS
    Data:
    konferencja 44038
    Status:
    Published
  3. ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
    Authors:
    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward Ayers, Dragomir Radev, Jeremy Avigad
    Conference:
    Thirty-seventh Conference on Neural Information Processing Systems , Wydawca: OpenReview.net
    Data:
    konferencja 10-16.12.2023
    Status:
    Submitted
  4. Stateful Premise Selection by Recurrent Neural Networks
    Authors:
    Bartosz Piotrowski, Josef Urban
    Conference:
    23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (rok: 2020, ), Wydawca: EPiC Series in Computing
    Data:
    konferencja 43973
    Status:
    Published
  5. MizAR 60 for Mizar 50
    Authors:
    Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
    Conference:
    Fourteenth Conference on Interactive Theorem Proving (rok: 2023, ), Wydawca: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
    Data:
    konferencja 31.07.2023-04.08.2023
    Status:
    Accepted for publication