Efficient neural clause-selection reinforcement

DOI10.1007/978-3-031-99984-0_22MaRDI QIDQ6869938zbMATH OpenFDO

Authors Martin Suda

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_22

zbMATH Keywords

clause selectiondeep reinforcement learningsaturation-based theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• AVATAR: The Architecture for First-Order Theorem Provers
• Deep network guided proof search
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• ENIGMA: efficient learning-based inference guiding machine
• Faster, higher, stronger: E 2.3
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• scientific article; zbMATH DE number 3089544 (Why is no real title available?)
• Implementing Superposition in iProver (System Description)
• Improving ENIGMA-style clause selection while learning from history
• Learning guided automated reasoning: a brief survey
• Learning theorem proving components
• Limited resource strategy in resolution theorem proving
• MizAR 40 for Mizar 40
• Performance of clause selection heuristics for saturation-based theorem proving
• Property invariant embedding for automated reasoning
• Regularization in Spider-style strategy discovery and schedule construction
• Reinforcement learning. An introduction
• Simple statistical gradient-following algorithms for connectionist reinforcement learning
• Stepping stones in the TPTP world
• The role of entropy in guiding a connection prover
• Vampire getting noisy: Will random bits help conquer chaos? (system description)
• Vampire with a brain is a good ITP hammer

This page was built for publication: Efficient neural clause-selection reinforcement

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869938)