@inproceedings{MTMT:34130667,
	title = {Lemmas: Generation, Selection, Application},
	url = {https://m2.mtmt.hu/api/publication/34130667},
	author = {Michael, Rawson and Christoph, Wernhard and Zombori, Zsolt and Wolfgang, Bibel},
	booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods},
	doi = {10.1007/978-3-031-43513-3_9},
	unique-id = {34130667},
	abstract = {Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.},
	year = {2023},
	pages = {153-174}
}

@inproceedings{MTMT:32574859,
	title = {Towards solving the 7-in-a-row game},
	url = {https://m2.mtmt.hu/api/publication/32574859},
	author = {Czifra, Domonkos and Csóka, Endre and Zombori, Zsolt and Makay, Géza},
	booktitle = {2021 IEEE Conference on Games (CoG)},
	doi = {10.1109/CoG52621.2021.9618991},
	unique-id = {32574859},
	year = {2021},
	pages = {01-08}
}

@CONFERENCE{MTMT:32530214,
	title = {Ordering Subgoals in a Backward Chaining Prover},
	url = {https://m2.mtmt.hu/api/publication/32530214},
	author = {Gergő, Csaba Kertész and Papp, Gergely and Péter, Szeredi and Varga, Dániel and Zombori, Zsolt},
	booktitle = {Proceedings of The 6th Conference on Artificial Intelligence and Theorem},
	unique-id = {32530214},
	year = {2021}
}

@CONFERENCE{MTMT:32530209,
	title = {Dreaming to Prove},
	url = {https://m2.mtmt.hu/api/publication/32530209},
	author = {Kristóf, Szabó and Zombori, Zsolt},
	booktitle = {Proceedings of The 6th Conference on Artificial Intelligence and Theorem},
	unique-id = {32530209},
	year = {2021}
}

@inproceedings{MTMT:32529820,
	title = {The Role of Entropy in Guiding a Connection Prover},
	url = {https://m2.mtmt.hu/api/publication/32529820},
	author = {Zombori, Zsolt and Urban, J. and Olšák, M.},
	booktitle = {30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2021, co-located with the 13th International Symposium on Frontiers of Combining Systems, FroCoS 2021},
	doi = {10.1007/978-3-030-86059-2_13},
	volume = {12842 LNAI},
	unique-id = {32529820},
	abstract = {In this work we study how to learn good algorithms for selecting reasoning steps in theorem proving. We explore this in the connection tableau calculus implemented by leanCoP where the partial tableau provides a clean and compact notion of a state to which a limited number of inferences can be applied. We start by incorporating a state-of-the-art learning algorithm — a graph neural network (GNN) – into the plCoP theorem prover. Then we use it to observe the system’s behavior in a reinforcement learning setting, i.e., when learning inference guidance from successful Monte-Carlo tree searches on many problems. Despite its better pattern matching capability, the GNN initially performs worse than a simpler previously used learning algorithm. We observe that the simpler algorithm is less confident, i.e., its recommendations have higher entropy. This leads us to explore how the entropy of the inference selection implemented via the neural network influences the proof search. This is related to research in human decision-making under uncertainty, and in particular the probability matching theory. Our main result shows that a proper entropy regularization, i.e., training the GNN not to be overconfident, greatly improves plCoP ’s performance on a large mathematical corpus. © 2021, Springer Nature Switzerland AG.},
	keywords = {NEURAL NETWORKS; ENTROPY; Decision theory; machine learning; reinforcement learning; reinforcement learning; decision making; Calculations; Theorem proving; Learning algorithms; Graph algorithms; Pattern matching; Automated theorem proving; SIMPLER algorithms; State of the art; Theorem provers; Graph neural networks; Graph neural networks; Probability matching; Monte-Carlo tree searches; Human decision making; Connection calculus; Entropy regularization; Network influences},
	year = {2021},
	pages = {218-235}
}

@inproceedings{MTMT:32529801,
	title = {Towards Finding Longer Proofs},
	url = {https://m2.mtmt.hu/api/publication/32529801},
	author = {Zombori, Zsolt and Csiszárik, Adrián and Michalewski, H. and Kaliszyk, C. and Urban, J.},
	booktitle = {30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2021, co-located with the 13th International Symposium on Frontiers of Combining Systems, FroCoS 2021},
	doi = {10.1007/978-3-030-86059-2_10},
	volume = {12842 LNAI},
	unique-id = {32529801},
	abstract = {We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). Unlike most learning based approaches, we focus on generalising from very little training data and achieving near complete confidence. We use several simple, structured datasets with very long proofs to show that FLoP can successfully generalise a single training proof to a large class of related problems. On these benchmarks, FLoP is competitive with strong theorem provers despite using very limited search, due to its ability to solve problems that are prohibitively long for other systems. © 2021, Springer Nature Switzerland AG.},
	keywords = {machine learning; reinforcement learning; reinforcement learning; automation; Theorem proving; Training data; Automated theorem proving; Automated theorem proving; strong theorems; Large dataset; Learning-based approach; Connection calculus; Guidance system},
	year = {2021},
	pages = {167-186}
}

@CONFERENCE{MTMT:31670485,
	title = {Learning Complex Actions from Proofs in Theorem Proving},
	url = {https://m2.mtmt.hu/api/publication/31670485},
	author = {Zombori, Zsolt and Josef, Urban},
	booktitle = {AITP 2020 - 5th Conference on Artificial Intelligence and Theorem Proving},
	unique-id = {31670485},
	year = {2020},
	pages = {112-118}
}

@CONFERENCE{MTMT:31670480,
	title = {Update on FLoP, a Reinforcement Learning based Theorem Prover},
	url = {https://m2.mtmt.hu/api/publication/31670480},
	author = {Zombori, Zsolt and Csiszárik, Adrián and Henryk, Michalewski and Cezary, Kaliszyk and Josef Urban},
	booktitle = {AITP 2020 - 5th Conference on Artificial Intelligence and Theorem Proving},
	unique-id = {31670480},
	year = {2020},
	pages = {107-111}
}

@article{MTMT:31404516,
	title = {Towards Finding Longer Proofs},
	url = {https://m2.mtmt.hu/api/publication/31404516},
	author = {Zombori, Zsolt},
	doi = {10.4230/DagRep.9.9.1},
	journal-iso = {DAGSTUHL SEMIN PROC},
	journal = {DAGSTUHL SEMINAR PROCEEDINGS},
	volume = {9},
	unique-id = {31404516},
	issn = {1862-4405},
	year = {2020},
	eissn = {1862-4405},
	pages = {16}
}

@inproceedings{MTMT:31404494,
	title = {Prolog Technology Reinforcement Learning Prover: (System Description)},
	url = {https://m2.mtmt.hu/api/publication/31404494},
	author = {Zombori, Zsolt and Urban, J. and Brown, C.E.},
	booktitle = {Automated Reasoning},
	doi = {10.1007/978-3-030-51054-1_33},
	volume = {12167 LNAI},
	unique-id = {31404494},
	abstract = {We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released. © 2020, Springer Nature Switzerland AG.},
	keywords = {Learning systems; reinforcement learning; reinforcement learning; automation; Calculations; Theorem proving; Logic programming; Automated theorem proving; Automated theorem proving; Symbolic learning; PROLOG (programming language); Connection tableau calculus; Automated theorem prover; Machine learners; Monte-Carlo tree searches; Prolog implementations; Python interfaces; System description},
	year = {2020},
	pages = {489-507}
}