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 (15)
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
This page was built for publication: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
