ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
From MaRDI portal
Publication:2305414
DOI10.1007/978-3-030-29436-6_12OpenAlexW2969934262MaRDI QIDQ2305414
Jan Jakubův, Karel Chvalovský, Martin Suda, Josef Urban
Publication date: 10 March 2020
Full work available at URL: https://arxiv.org/abs/1903.03182
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Online machine learning techniques for Coq: a comparison, Fast and slow enigmas and parental guidance, Vampire with a brain is a good ITP hammer, Make E Smart Again (Short Paper), ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), Prolog Technology Reinforcement Learning Prover, Towards finding longer proofs, \textsf{lazyCoP}: lazy paramodulation meets neurally guided search, The role of entropy in guiding a connection prover, Learning theorem proving components, Neural precedence recommender, Improving ENIGMA-style clause selection while learning from history, Layered clause selection for theory reasoning (short paper), Guiding an automated theorem prover with neural rewriting, The 10th IJCAR automated theorem proving system competition – CASC-J10
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 -- July 2, 2016. Proceedings
- A learning-based fact selector for Isabelle/HOL
- MPTP 0.2: Design, implementation, and initial experiments
- IeanCOP: lean connection-based theorem proving
- ProofWatch: watchlist guidance for large theories in E
- Enhancing ENIGMA given clause guidance
- ATPboost: learning premise selection in binary setting with ATP feedback
- Machine learning for first-order theorem proving
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- ENIGMA: efficient learning-based inference guiding machine
- Monte Carlo tableau proof search
- Translating higher-order clauses to first-order clauses
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
- Internal Guidance for Satallax
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- MaLeCoP Machine Learning Connection Prover
- Mizar: State-of-the-art and Beyond
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- Deep Network Guided Proof Search
- A New Class of Automated Theorem-Proving Algorithms
- Hierarchical invention of theorem proving strategies
- Hammering towards QED
