|
Proof Clustering for Proof Plans Matt Humphrey
|
tarix | 08.08.2018 | ölçüsü | 306,5 Kb. | | #61638 |
|
Matt Humphrey Working with: Manuel Blum Brendan Juba Ryan Williams
What is Proof Planning? Informal Definition - See a proof in terms of “ideas”
- Different levels of abstraction
- Represented as a graph, tree, DAG?
- Tool for directing exhaustive proof search
Formal Definition - No perfect all-encapsulating definition
- Usually defined per theorem proving system
- The concept itself is mostly informal
Example Proof Plan
Why Proof Planning? Bridges gap between human/computer Proof = Guarantee + Explanation (Robinson 65) And… - It can be automated
- It has been automated (to some extent)
Why Study This? Artificial Intelligence Perspective - What can/cannot be modeled by computer?
- How to model something so informal
Cognitive Psychology Perspective - Intuitions about human thought process
- Reasoning about human ability to abstract
Practical Perspective - Proving theorems automatically is useful
Learning by Example Previous proofs as hints - What information can be gained?
What has been tried? - Analogical Reasoning
- Strategies (higher level)
- Methods, Tactics (lower level)
- And in most cases a combination of these
Proof Clustering Proof Planning can be aided by: If we can cluster similar proofs, we can: - More easily generalize a strategy or tactic
- Determine which proofs are useful examples
- Build a proof component hierarchy
- Automate the process of learning techniques
Ωmega Proof Planning System with LearnΩmatic Heuristics guide the proof search - Uses learned proof techniques (methods)
- Selects what it feels to be the most relevant methods
LearnΩmatic - Learns new methods from sets of examples
- Increases proving capability on the fly
- Minimizes hard-coding of techniques
- Increases applicability, no domain limitation
Learning Sequence
An Example of Learning… Extended Regular expression format A grouping of ‘similar’ proof techniques: assoc-l, assoc-l, inv-r, id-l assoc-l, inv-l, id-l assoc-l, assoc-l, assoc-l, inv-r, id-l …generalizes to the method: assoc-l*, [inv-r | inv-l], id-l
Problems with the LearnΩmatic Relies on ‘positive examples’ only - User must have knowledge about proofs
- Hard to expand the system’s capabilities
- Could produce bad methods for bad input
Learning new methods is not automated! - Waits for the user to supply clusters
Specific Goal - First: be able to check a cluster for similarity
- Second: be able to identify a ‘good’ cluster
The results can be directly plugged into the learning algorithm for new methods - Proof cluster -> learning algorithm -> newly-learnt proof method -> application
Plan of Attack Determine what constitutes a good group - Maybe a simple heuristic (compression…)
- Maybe a more detailed analysis is necessary
Implement proof clustering on top of the LearnΩmatic system - Ideally: proving theorems on proof clustering
- At least: empirical data from test cases
Some Questions We Have… Are regular expressions appropriate? Do Ωmega and the LearnΩmatic even represent the right approach (bottom-up)? How much will proof clustering aid theorem proving? Can we generalize proof clustering?
References S. Bhansali. Domain-Based program synthesis using planning and derivational analogy. University of Illinois at Urbana-Champaign, May, 1991. A. Bundy. A science of reasoning. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 178--198. MIT Press, 1991. A. Bundy. The use of explicit plans to guide inductive proofs. In Ninth Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 203, pages 111--120. SpringerVerlag, 1988. M. Jamnik, M. Kerber, M. Pollet, C. Benzmüller. Automatic learning of proof methods in proof planning. L. J. of the IGPL, Vol. 11 No. 6, pages 647--673. 2003. E. Melis and J. Whittle. Analogy in inductive theorem proving. Journal of Automated Reasoning, 20(3):--, 1998.
Dostları ilə paylaş: |
|
|