More Web Proxy on the site http://driver.im/

research-article

Open access

Aesop: White-Box Best-First Proof Search for Lean

Authors:

Jannis Limperg,

Asta Halkjær FromAuthors Info & Claims

CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 253 - 266

https://doi.org/10.1145/3573105.3575671

Published: 11 January 2023 Publication History

Abstract

We present Aesop, a proof search tactic for the Lean 4 interactive theorem prover. Aesop performs a tree-based search over a user-specified set of proof rules. It supports safe and unsafe rules and uses a best-first search strategy with customisable prioritisation. Aesop also allows users to register custom normalisation rules and integrates Lean's simplifier to support equational reasoning. Many details of Aesop's search procedure are designed to make it a white-box proof automation tactic, meaning that users should be able to easily predict how their rules will be applied, and thus how powerful and fast their Aesop invocations will be.

Since we use a best-first search strategy, it is not obvious how to handle metavariables which appear in multiple goals. The most common strategy for dealing with metavariables relies on backtracking and is therefore not suitable for best-first search. We give an algorithm which addresses this issue. The algorithm works with any search strategy, is independent of the underlying logic and makes few assumptions about how rules interact with metavariables. We conjecture that with a fair search strategy, the algorithm is as complete as the given set of rules allows.

References

[1]

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. 2011. The Matita interactive theorem prover. In CADE 2011. 64–69. https://doi.org/10.1007/978-3-642-22438-6_7

[2]

Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. 2019. HOList: an environment for machine learning of higher order logic theorem proving. In ICML 2019. 454–463. https://proceedings.mlr.press/v97/bansal19a.html

[3]

Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. 2016. Hammering towards QED. Journal of Formalized Reasoning, 9, 1 (2016), 101–148. https://doi.org/10.6092/issn.1972-5787/4593

[4]

The mathlib Community. 2020. The lean mathematical library. In CPP 2020. 367–381. https://doi.org/10.1145/3372885.3373824

Digital Library

[5]

Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. 1995. A Tutorial Introduction to PVS. In Workshop on Industrial-Strength Formal Specification Techniques 1995. http://www.csl.sri.com/papers/wift-tutorial/

[6]

Ł ukasz Czajka. 2020. Practical proof search for Coq by type inhabitation. In IJCAR 2020. 28–57. https://doi.org/10.1007/978-3-030-51054-1_3

Digital Library

[7]

Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 theorem prover and programming language. In CADE 2021. 625–635. https://doi.org/10.1007/978-3-030-79876-5_37

Digital Library

[8]

Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. 2021. TacticToe: Learning to prove with tactics. Journal of Automated Reasoning, 65, 2 (2021), 257–286. https://doi.org/10.1007/s10817-020-09580-x

Digital Library

[9]

Martin Giese. 2001. Incremental closure of free variable tableaux. In IJCAR 2001. 545–560. https://doi.org/10.1007/3-540-45744-5_46

[10]

Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. 2021. Proof artifact co-training for theorem proving with language models. https://doi.org/10.48550/ARXIV.2102.06203

[11]

M. Kaufmann and J. Strother Moore. 1996. ACL2: an industrial strength version of Nqthm. In COMPASS 1996. 23–34. https://doi.org/10.1109/CMPASS.1996.507872

[12]

Boris Konev and Tudor Jebelean. 2005. Solution lifting method for handling meta-variables in TH∃OREM∀. Journal of Mathematical Sciences, 126, 3 (2005), 1182–1194. https://doi.org/10.1007/s10958-005-0090-6

[13]

Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. 2022. HyperTree proof search for neural theorem proving. https://doi.org/10.48550/ARXIV.2205.11491

[14]

Fredrik Lindblad and Marcin Benke. 2004. A tool for automated theorem proving in Agda. In TYPES 2004. 154–169. https://doi.org/10.1007/11617990_10

Digital Library

[15]

Conor McBride and James McKinna. 2004. The view from the left. Journal of Functional Programming, 14, 1 (2004), 69–111. https://doi.org/10.1017/S0956796803004829

Digital Library

[16]

William McCune. 1992. Experiments with discrimination-tree indexing and path indexing for term retrieval. Journal of Automated Reasoning, 9, 2 (1992), 147–167. https://doi.org/10.1007/BF00245458

Digital Library

[17]

Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph. D. Dissertation. Chalmers University of Technology. Göteborg, Sweden. https://www.cse.chalmers.se/~ulfn/papers/thesis.pdf

[18]

Lawrence C. Paulson. 1996. Generic automatic proof tools. University of Cambridge. https://doi.org/10.48456/tr-396

[19]

Lawrence C. Paulson. 1999. A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science, 5, 3 (1999), 73–87. https://doi.org/10.3217/jucs-005-03-0073

[20]

Lawrence C. Paulson, Tobias Nipkow, and Makarius Wenzel. 2019. From LCF to Isabelle/HOL. Formal Aspects of Computing, 31, 6 (2019), 675–698. https://doi.org/10.1007/s00165-019-00492-1

Digital Library

[21]

Geoff Sutcliffe. 2017. The TPTP problem library and associated infrastructure: from CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59, 4 (2017), 483–502. https://doi.org/10.1007/s10817-017-9407-7

Digital Library

[22]

Jørgen Villadsen. 2020. A micro prover for teaching automated reasoning. In PAAR 2020.

[23]

Bohua Zhan. 2016. AUTO2, a saturation-based heuristic prover for higher-order logic. In ITP 2016. 441–456. https://doi.org/10.1007/978-3-319-43144-4_27

Cited By

Kœhler TGoens ABhat SGrosser TTrinder PSteuwer M(2024)Guided Equality SaturationProceedings of the ACM on Programming Languages10.1145/36329008:POPL(1727-1758)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632900
Aliyev Y(2024)Set Theory and Elementary Algebra in LEAN 4 Theorem Prover2024 IEEE 18th International Conference on Application of Information and Communication Technologies (AICT)10.1109/AICT61888.2024.10740429(1-6)Online publication date: 25-Sep-2024
https://doi.org/10.1109/AICT61888.2024.10740429
Fernández Mir RJackson PBhat SGoens AGrosser T(2024)Transforming Optimization Problems into Disciplined Convex Programming FormIntelligent Computer Mathematics10.1007/978-3-031-66997-2_11(183-202)Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-66997-2_11
Show More Cited By

Index Terms

Aesop: White-Box Best-First Proof Search for Lean
1. Mathematics of computing
  1. Mathematical software
2. Theory of computation
  1. Logic

Recommendations

On structuring proof search for first order linear logic

Full first-order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the 'proof search as computation' paradigm. However, Forum still has to deal with ...
Nested proof search as reduction in the Lambda-calculus
PPDP '11: Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming

We present a system for propositional implicative intuitionistic logic in the calculus of structures, which is a generalisation of the sequent calculus to the deep inference methodology. We show that it is sound and complete with respect to the usual ...
Practical Proof Search for Coq by Type Inhabitation
Automated Reasoning
Abstract
We present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. The procedure is more general than any of the automation tactics natively available in Coq. It aims to handle as ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2023

347 pages

ISBN:9798400700262

DOI:10.1145/3573105

General Chairs:
Robbert Krebbers
Radboud University Nijmegen, Netherlands
,
Dmitriy Traytel
University of Copenhagen, Denmark
,
Program Chairs:
Brigitte Pientka
McGill University, Canada
,
Steve Zdancewic
University of Pennsylvania, USA

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2023

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Nederlandse Organisatie voor Wetenschappelijk Onderzoek

Conference

CPP '23

Sponsor:

SIGPLAN

CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 16 - 17, 2023

MA, Boston, USA

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
5,844
Total Downloads

Downloads (Last 12 months)4,873
Downloads (Last 6 weeks)67

Reflects downloads up to 22 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kœhler TGoens ABhat SGrosser TTrinder PSteuwer M(2024)Guided Equality SaturationProceedings of the ACM on Programming Languages10.1145/36329008:POPL(1727-1758)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632900
Aliyev Y(2024)Set Theory and Elementary Algebra in LEAN 4 Theorem Prover2024 IEEE 18th International Conference on Application of Information and Communication Technologies (AICT)10.1109/AICT61888.2024.10740429(1-6)Online publication date: 25-Sep-2024
https://doi.org/10.1109/AICT61888.2024.10740429
Fernández Mir RJackson PBhat SGoens AGrosser T(2024)Transforming Optimization Problems into Disciplined Convex Programming FormIntelligent Computer Mathematics10.1007/978-3-031-66997-2_11(183-202)Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-66997-2_11
Avigad J(2024)Automated Reasoning for MathematicsAutomated Reasoning10.1007/978-3-031-63498-7_1(3-20)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_1

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Table of Contents