| ENIGMA anonymous: Symbol-independent inference guiding machine (system description) J Jakubův, K Chvalovský, M Olšák, B Piotrowski, M Suda, J Urban International Joint Conference on Automated Reasoning, 448-463, 2020 | 75 | 2020 |
| Proofnet: Autoformalizing and formally proving undergraduate-level mathematics Z Azerbayev, B Piotrowski, H Schoelkopf, EW Ayers, D Radev, J Avigad arXiv preprint arXiv:2302.12433, 2023 | 71* | 2023 |
| ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback B Piotrowski, J Urban Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as …, 2018 | 56 | 2018 |
| Magnushammer: A transformer-based approach to premise selection M Mikuła, S Tworkowski, S Antoniak, B Piotrowski, AQ Jiang, JP Zhou, ... arXiv preprint arXiv:2303.04488, 2023 | 37 | 2023 |
| Can neural networks learn symbolic rewriting? B Piotrowski, J Urban, CE Brown, C Kaliszyk arXiv preprint arXiv:1911.04873, 2019 | 29 | 2019 |
| Stateful premise selection by recurrent neural networks B Piotrowski, J Urban arXiv preprint arXiv:2004.08212, 2020 | 26 | 2020 |
| Online machine learning techniques for coq: a comparison L Zhang, L Blaauwbroek, B Piotrowski, C Kaliszyk, J Urban International Conference on Intelligent Computer Mathematics, 67-83, 2021 | 13 | 2021 |
| Guiding inferences in connection tableau by recurrent neural networks B Piotrowski, J Urban International Conference on Intelligent Computer Mathematics, 309-314, 2020 | 13 | 2020 |
| Machine-learned premise selection for Lean B Piotrowski, RF Mir, E Ayers International Conference on Automated Reasoning with Analytic Tableaux and …, 2023 | 12 | 2023 |
| Towards learning quantifier instantiation in SMT M Janota, J Piepenbrock, B Piotrowski 25th International Conference on Theory and Applications of Satisfiability …, 2022 | 12 | 2022 |
| MizAR 60 for Mizar 50 J Jakubův, K Chvalovský, Z Goertzel, C Kaliszyk, M Olšák, B Piotrowski, ... arXiv preprint arXiv:2303.06686, 2023 | 10 | 2023 |
| Proof-pile, 2022 Z Azerbayev, E Ayers, B Piotrowski URL https://github. com/zhangir-azerbayev/proof-pile, 2022 | 8 | 2022 |
| Guiding theorem proving by recurrent neural networks B Piotrowski, J Urban arXiv preprint arXiv:1905.07961, 2019 | 7 | 2019 |
| Proofpile: A pre-training dataset of mathematical texts Z Azerbayev, E Ayers, B Piotrowski | 5 | 2023 |
| ProofNet: Autoformalizing and formally proving undergraduate-level mathematics (2023) Z Azerbayev, B Piotrowski, H Schoelkopf, EW Ayers, D Radev, J Avigad URL https://arxiv. org/abs/2302.12433, 0 | 5 | |
| Selecting quantifiers for instantiation in smt J Jakubův, M Janota, B Piotrowski, J Piepenbrock, A Reynolds | 3 | 2023 |
| Learning to advise an equational prover CE Brown, B Piotrowski, J Urban Artif. Intell. Theorem Proving, 1-13, 2020 | 3 | 2020 |
| Repurposing language models into embedding models: Finding the compute-optimal recipe AQ Jiang, A Ziarko, B Piotrowski, W Li, M Jamnik, P Miłoś The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024 | 1 | 2024 |
| 14th International Conference on Interactive Theorem Proving (ITP 2023) A Koutsoukou-Argyraki, R Krebbers, M Abdulaziz, C Madlener, ... Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, 2023 | 1 | 2023 |
| Repurposing Language Models into Embedding Models: Finding the Compute-Optimal Recipe A Ziarko, AQ Jiang, B Piotrowski, W Li, M Jamnik, P Miłoś arXiv preprint arXiv:2406.04165, 2024 | | 2024 |
Josef UrbanDistinguished Researcher at Czech Technical University in PragueE-mail confirmado em cvut.cz
