research-article

BliStrTune: hierarchical invention of theorem proving strategies

Authors:

Josef UrbanAuthors Info & Claims

CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

Pages 43 - 52

https://doi.org/10.1145/3018610.3018619

Published: 16 January 2017 Publication History

Abstract

Inventing targeted proof search strategies for specific problem sets is a difficult task. State-of-the-art automated theorem provers (ATPs) such as E allow a large number of user-specified proof search strategies described in a rich domain specific language. Several machine learning methods that invent strategies automatically for ATPs were proposed previously. One of them is the Blind Strategymaker (BliStr), a system for automated invention of ATP strategies.

In this paper we introduce BliStrTune -- a hierarchical extension of BliStr. BliStrTune allows exploring much larger space of E strategies by interleaving search for high-level parameters with their fine-tuning. We use BliStrTune to invent new strategies based also on new clause weight functions targeted at problems from large ITP libraries. We show that the new strategies significantly improve E's performance in solving problems from the Mizar Mathematical Library.

References

[1]

J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning, 52(2):191–213, 2014. ISSN 0168-7433. J. Blanchette, C. Kaliszyk, L. Paulson, and J. Urban. Hammering towards QED. Journal of Formalized Reasoning, 9(1):101– 148, 2016a. ISSN 1972-5787

Digital Library

[2]

J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning, 57(3):219–244, 2016b.

Digital Library

[3]

A. Grabowski, A. Korniłowicz, and A. Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153–245, 2010.

[4]

F. Hutter, H. H. Hoos, K. Leyton-Brown, and T. Stützle. ParamILS: an automatic algorithm configuration framework. J. Artificial Intelligence Research, 36:267–306, October 2009.

Digital Library

[5]

J. Jakub˚uv and J. Urban. Extending E prover with similarity based clause selection strategies. In Intelligent Computer Mathematics - 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings, pages 151–156, 2016.

[6]

C. Kaliszyk and J. Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173–213, 2014.

Digital Library

[7]

V. Levenshtein. Binary Codes Capable of Correcting Deletions, Insertions and Reversals. Soviet Physics Doklady, 10:707, 1966.

[8]

W. McCune. Otter 2.0. In International Conference on Automated Deduction, pages 663–664. Springer, 1990.

Digital Library

[9]

W. W. McCune. Otter 1. 0 users’ guide. Technical report, Argonne National Lab., IL (USA), 1989.

[10]

W. W. McCune. Otter 3.0 reference manual and guide, volume 9700. Argonne National Laboratory Argonne, IL, 1994.

[11]

S. Schäfer and S. Schulz. Breeding theorem proving heuristics with genetic algorithms. In G. Gottlob, G. Sutcliffe, and A. Voronkov, editors, Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015, volume 36 of EPiC Series in Computing, pages 263–274. EasyChair, 2015.

[12]

S. Schulz. System description: E 1.8. In K. L. McMillan, A. Middeldorp, and A. Voronkov, editors, LPAR, volume 8312 of LNCS, pages 735–743. Springer, 2013. ISBN 978-3-642-45220-8.

[14]

J. Urban. MPTP - Motivation, Implementation, First Experiments. J. Autom. Reasoning, 33(3-4):319–339, 2004.

Digital Library

[15]

J. Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006

[16]

J. Urban. BliStr: The Blind Strategymaker. In G. Gottlob, G. Sutcliffe, and A. Voronkov, editors, GCAI 2015. Global Conference on Artificial Intelligence, volume 36 of EPiC Series in Computing, pages 312–319. EasyChair, 2015.

Digital Library

[17]

J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskoˇcil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In A. Armando, P. Baumgartner, and G. Dowek, editors, IJCAR, volume 5195 of LNCS, pages 441–456. Springer, 2008. ISBN 978-3-540-71069-1. Z. Wang, F. Hutter, M. Zoghi, D. Matheson, and N. de Feitas. Bayesian optimization in a billion dimensions via random embeddings. Journal of Artificial Intelligence Research, 55:361– 387, 2016.

Digital Library

[18]

K. Zhang and D. Shasha. Simple fast algorithms for the editing distance between trees and related problems. SIAM J. Comput., 18(6):1245–1262, Dec. 1989. ISSN 0097-5397.

Cited By

Holden EKorovin K(2024)Graph Sequence Learning for Premise SelectionJournal of Symbolic Computation10.1016/j.jsc.2024.102376(102376)Online publication date: Aug-2024
https://doi.org/10.1016/j.jsc.2024.102376
Jakubův JJanota MUrban J(2024)Solving Hard Mizar Problems with Instantiation and Strategy InventionIntelligent Computer Mathematics10.1007/978-3-031-66997-2_18(315-333)Online publication date: 29-Jul-2024
https://doi.org/10.1007/978-3-031-66997-2_18
Sutcliffe GSuttner CKotthoff LPerrault CKhalid Z(2024)An Empirical Assessment of Progress in Automated Theorem ProvingAutomated Reasoning10.1007/978-3-031-63498-7_4(53-74)Online publication date: 1-Jul-2024
https://doi.org/10.1007/978-3-031-63498-7_4
Show More Cited By

Index Terms

BliStrTune: hierarchical invention of theorem proving strategies
1. Computing methodologies
2. Theory of computation

Recommendations

Hierarchical invention of theorem proving strategies

State-of-the-art automated theorem provers (ATPs) such as E and Vampire use a large number of different strategies to traverse the search space. Inventing targeted proof search strategies for specific problem sets is a difficult task. Several machine ...
Theorem Proving Modulo
Abstract
Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate ...
On Automatic Theorem Proving with ML
MICAI '14: Proceedings of the 2014 13th Mexican International Conference on Artificial Intelligence

In this paper, we describe the development of a series of automatic theorem provers for a variety of logics. Provers are developed from a functional approach. The first prover is for Classical Propositional Calculus (CPC), which is based on a ...

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences

CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

January 2017

234 pages

ISBN:9781450347051

DOI:10.1145/3018610

Program Chairs:
Yves Bertot
Inria, France / Université Cote d'Azur, France
,
Viktor Vafeiadis
MPI-SWS, Germany

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 January 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

H2020 European Research Council

Conference

CPP '17

CPP '17: Certified Proofs and Programs

January 16 - 17, 2017

Paris, France

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
142
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Holden EKorovin K(2024)Graph Sequence Learning for Premise SelectionJournal of Symbolic Computation10.1016/j.jsc.2024.102376(102376)Online publication date: Aug-2024
https://doi.org/10.1016/j.jsc.2024.102376
Jakubův JJanota MUrban J(2024)Solving Hard Mizar Problems with Instantiation and Strategy InventionIntelligent Computer Mathematics10.1007/978-3-031-66997-2_18(315-333)Online publication date: 29-Jul-2024
https://doi.org/10.1007/978-3-031-66997-2_18
Sutcliffe GSuttner CKotthoff LPerrault CKhalid Z(2024)An Empirical Assessment of Progress in Automated Theorem ProvingAutomated Reasoning10.1007/978-3-031-63498-7_4(53-74)Online publication date: 1-Jul-2024
https://doi.org/10.1007/978-3-031-63498-7_4
Bártek FChvalovský KSuda M(2024)Regularization in Spider-Style Strategy Discovery and Schedule ConstructionAutomated Reasoning10.1007/978-3-031-63498-7_12(194-213)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_12
Hůla JJakubův JJanota MKubej L(2022)Targeted Configuration of an SMT SolverIntelligent Computer Mathematics10.1007/978-3-031-16681-5_18(256-271)Online publication date: 17-Sep-2022
https://doi.org/10.1007/978-3-031-16681-5_18
Holden EKorovin K(2021)Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem ProvingIntelligent Computer Mathematics10.1007/978-3-030-81097-9_8(107-123)Online publication date: 26-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81097-9_8
Nikolić MMarinković VKovács ZJaniă?Ić P(2019)Portfolio theorem proving and prover runtime prediction for geometryAnnals of Mathematics and Artificial Intelligence10.1007/s10472-018-9598-685:2-4(119-146)Online publication date: 1-Apr-2019
https://dl.acm.org/doi/10.1007/s10472-018-9598-6
Chvalovský KJakubův JSuda MUrban J(2019)ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for EAutomated Deduction – CADE 2710.1007/978-3-030-29436-6_12(197-215)Online publication date: 27-Aug-2019
https://dl.acm.org/doi/10.1007/978-3-030-29436-6_12
Jakubův JUrban JFontaine PKaliszyk CSchulz SUrban J(2018)Hierarchical invention of theorem proving strategiesAI Communications10.3233/AIC-18076131:3(237-250)Online publication date: 1-Jan-2018
https://dl.acm.org/doi/10.3233/AIC-180761
Bibel W(2017)A Vision for Automated Deduction Rooted in the Connection MethodAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-319-66902-1_1(3-21)Online publication date: 30-Aug-2017
https://doi.org/10.1007/978-3-319-66902-1_1

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten