ATPboost: learning premise selection in binary setting with ATP feedback

DOI10.1007/978-3-319-94205-6_37MaRDI QIDQ1799117zbMATH OpenOpenAlexFDO

Authors Bartosz Piotrowski, Josef Urban

Publication date 18 October 2018

Full work available at URL https://arxiv.org/abs/1802.03375

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Random forests for premise selection
• Improving stateful premise selection with transformers
• Premise selection for mathematics by corpus analysis and kernel methods
• Lemmatization for stronger reasoning in large theories
• Premise selection in the Naproche system

Cited in

(9)

• Alien coding
• Towards the automatic mathematician
• Graph sequence learning for premise selection
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• ATPboost
• Machine-learned premise selection for Lean
• Improving stateful premise selection with transformers
• Online machine learning techniques for Coq: a comparison
• Random forests for premise selection

Describes a project that uses

Uses Software

• Isabelle/HOL
• TPTP
• Mizar
• HOL
• MaLeCoP
• E Theorem Prover
• MaLARea
• XGBoost
• FEMaLeCoP
• TacticToe

This page was built for publication: ATPboost: learning premise selection in binary setting with ATP feedback

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