Mining state-based models from proof corpora
From MaRDI portal
Abstract: Interactive theorem provers have been used extensively to reason about various software/hardware systems and mathematical theorems. The key challenge when using an interactive prover is finding a suitable sequence of proof steps that will lead to a successful proof requires a significant amount of human intervention. This paper presents an automated technique that takes as input examples of successful proofs and infers an Extended Finite State Machine as output. This can in turn be used to generate proofs of new conjectures. Our preliminary experiments show that the inferred models are generally accurate (contain few false-positive sequences) and that representing existing proofs in such a way can be very useful when guiding new ones.
Recommendations
Cites work
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- scientific article; zbMATH DE number 5486212 (Why is no real title available?)
- A graphical language for proof strategies
- A machine-checked proof of the odd order theorem
- Automatic Learning of Proof Methods in Proof Planning
- Formal proof - the four color theorem
- Language identification in the limit
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- ML4PG in computer algebra verification
- MaSh: machine learning for Sledgehammer
- MizAR 40 for Mizar 40
- On the Synthesis of Finite-State Machines from Samples of Their Behavior
- Premise selection for mathematics by corpus analysis and kernel methods
- Proof-pattern recognition and lemma discovery in ACL2
- Sledgehammer: judgement day
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Translating higher-order clauses to first-order clauses
Cited in
(5)
Describes a project that uses
Uses Software
This page was built for publication: Mining state-based models from proof corpora
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5495930)
