{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:53:53Z","timestamp":1762325633485},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>In this work we extend an instantiation-based theorem prover iProver with machine learning (ML) guidance based on graph neural networks. For this we implement an interactive mode in iProver, which allows communication with an external agent via network sockets. The external (ML-based) agent guides the proof search by scoring generated clauses in the given clause loop. Our evaluation on a large set of Mizar problems shows that the ML guidance outperforms iProver\u2019s standard human-programmed priority queues, solving more than twice as many problems in the same time. To our knowledge, this is the first time the performance of a state-of-the-art instantiation-based system is doubled by ML guidance.<\/jats:p>","DOI":"10.29007\/tp23","type":"proceedings-article","created":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T18:10:10Z","timestamp":1685815810000},"page":"112-99","source":"Crossref","is-referenced-by-count":7,"title":["Guiding an Instantiation Prover with Graph Neural Networks"],"prefix":"10.29007","volume":"94","author":[{"given":"Karel","family":"Chvalovsk\u00fd","sequence":"first","affiliation":[]},{"given":"Konstantin","family":"Korovin","sequence":"additional","affiliation":[]},{"given":"Jelle","family":"Piepenbrock","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T18:10:21Z","timestamp":1685815821000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/5z94"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/tp23","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}