Mining state-based models from proof corpora. (English) Zbl 1304.68155
Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 282-297 (2014).
Summary: 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.
For the entire collection see [Zbl 1293.68035].
For the entire collection see [Zbl 1293.68035].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
Software:
WEKA; Isabelle/HOL; C4.5; Sledgehammer; Coq; IsaPlanner; ACL2; Metis_; MaSh; ML4PG; FlyspeckReferences:
| [1] | Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. Journal of Automated Reasoning 52(2), 191–213 (2014) · Zbl 1315.68217 · doi:10.1007/s10817-013-9286-5 |
| [2] | Biermann, A., Feldman, J.A.: On the Synthesis of Finite-State Machines from Samples of Their Behavior. IEEE Transactions on Computers C-21(6), 592–597 (1972) · Zbl 0243.94039 · doi:10.1109/TC.1972.5009015 |
| [3] | Böhme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 107–121. Springer, Heidelberg (2010) · Zbl 1291.68327 · doi:10.1007/978-3-642-14203-1_9 |
| [4] | Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120. Springer, Heidelberg (1988) · Zbl 0656.68106 · doi:10.1007/BFb0012826 |
| [5] | Cheng, K.T., Krishnakumar, A.S.: Automatic Functional Test Generation Using the Extended Finite State Machine Model. In: Proceedings of the 30th International Design Automation Conference, DAC 1993, pp. 86–91. ACM, New York (1993) |
| [6] | Dixon, L., Fleuriot, J.: IsaPlanner: A Prototype Proof Planner in Isabelle. In: Baader, F. (ed.) CADE-19. LNCS (LNAI), vol. 2741, pp. 279–283. Springer, Heidelberg (2003) · doi:10.1007/978-3-540-45085-6_22 |
| [7] | Duncan, H.: The Use of Data Mining for the Automatic Formation of Tactics. Ph.D. thesis, University of Edinburgh (2007) |
| [8] | Gold, E.M.: Language Identification in the Limit. Information and Control 10(5), 447–474 (1967) · Zbl 0259.68032 · doi:10.1016/S0019-9958(67)91165-5 |
| [9] | Gonthier, G.: Formal Proof - The Four-Color Theorem. Notices of the American Mathematical Society 55(11), 1382–1393 (2008) · Zbl 1195.05026 |
| [10] | Gonthier, G., et al.: A Machine-Checked Proof of the Odd Order Theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013) · Zbl 1317.68211 · doi:10.1007/978-3-642-39634-2_14 |
| [11] | Grov, G., Kissinger, A., Lin, Y.: A Graphical Language for Proof Strategies. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol. 8312, pp. 324–339. Springer, Heidelberg (2013) · Zbl 1406.68107 · doi:10.1007/978-3-642-45221-5_23 |
| [12] | Grov, G., Komendantskaya, E., Bundy, A.: A Statistical Relational Learning Challenge – Extracting Proof Strategies from Exemplar Proofs. In: ICML 2012 Workshop on Statistical Relational Learning (2012) |
| [13] | Hales, T.C.: Introduction to the Flyspeck Project. In: Coquand, T., Lombardi, H., Roy, M.F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol. 05021. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany (2006) |
| [14] | Hall, M., et al.: The WEKA Data Mining Software: An Update. SIGKDD Explorations 11(1), 10–18 (2009) · doi:10.1145/1656274.1656278 |
| [15] | Heras, J., Komendantskaya, E.: ML4PG in Computer Algebra Verification. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 354–358. Springer, Heidelberg (2013) · Zbl 1390.68780 · doi:10.1007/978-3-642-39320-4_28 |
| [16] | Heras, J., Komendantskaya, E., Johansson, M., Maclean, E.: Proof-Pattern Recognition and Lemma Discovery in ACL2. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol. 8312, pp. 389–406. Springer, Heidelberg (2013) · Zbl 1407.68436 · doi:10.1007/978-3-642-45221-5_27 |
| [17] | Jamnik, M., Kerber, M., Pollet, M., Benzmüller, C.: Automatic Learning of Proof Methods in Proof Planning. Logic Journal of the IGPL 11(6), 647–673 (2003) · Zbl 1042.03012 · doi:10.1093/jigpal/11.6.647 |
| [18] | Kaliszyk, C., Urban, J.: Learning-assisted Automated Reasoning with Flyspeck. CoRR abs/1211.7012 (2012) · Zbl 1314.68283 |
| [19] | Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. CoRR abs/1310.2805 (2013) · Zbl 1356.68191 |
| [20] | Kohavi, R.: A Study of Cross-Validation and Bootstrap for Accuracy Estimation and Model Selection. In: IJCAI, pp. 1137–1145. Morgan Kaufmann (1995) |
| [21] | Komendantskaya, E., Heras, J., Grov, G.: Machine Learning in Proof General: Interfacing Interfaces. In: UITP. EPTCS, vol. 118, pp. 15–41 (2013) |
| [22] | Kühlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: Machine Learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35–50. Springer, Heidelberg (2013) · Zbl 1317.68215 · doi:10.1007/978-3-642-39634-2_6 |
| [23] | Lang, K.J., Pearlmutter, B.A., Price, R.A.: Results of the Abbadingo One DFA Learning Competition and a New Evidence-Driven State Merging Algorithm. In: Honavar, V.G., Slutzki, G. (eds.) ICGI 1998. LNCS (LNAI), vol. 1433, pp. 1–12. Springer, Heidelberg (1998) · doi:10.1007/BFb0054059 |
| [24] | Leroy, X.: Formal Verification of a Realistic Compiler. Communications of the ACM 52(7), 107–115 (2009) · doi:10.1145/1538788.1538814 |
| [25] | Lorenzoli, D., Mariani, L., Pezze, M.: Automatic Generation of Software Behavioral Models. In: ACM/IEEE 30th International Conference on Software Engineering, ICSE 2008, pp. 501–510 (May 2008) · doi:10.1145/1368088.1368157 |
| [26] | The Coq Development Team: The Coq Proof Assistant Reference Manual. Version 8.4. LogiCal Project, http://coq.inria.fr/refman |
| [27] | Meng, J., Paulson, L.C.: Translating Higher-Order Clauses to First-Order Clauses. Journal of Automated Reasoning 40(1), 35–60 (2008) · Zbl 1203.68188 · doi:10.1007/s10817-007-9085-y |
| [28] | Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002) · doi:10.1007/3-540-45949-9 |
| [29] | Paulson, L.C., Susanto, K.W.: Source-Level Proof Reconstruction for Interactive Theorem Proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 232–245. Springer, Heidelberg (2007) · Zbl 1144.68364 · doi:10.1007/978-3-540-74591-4_18 |
| [30] | Quinlan, J.R.: C4.5: Programs for Machine Learning. Morgan Kaufmann (1993) |
| [31] | Walkinshaw, N., Taylor, R., Derrick, J.: Inferring Extended Finite State Machine models from software executions. In: 20th Working Conference on Reverse Engineering (WCRE), pp. 301–310 (October 2013) · doi:10.1109/WCRE.2013.6671305 |
| [32] | Walkinshaw, N., Derrick, J., Guo, Q.: Iterative Refinement of Reverse-Engineered Models by Model-Based Testing. In: Cavalcanti, A., Dams, D. (eds.) FM 2009. LNCS, vol. 5850, pp. 305–320. Springer, Heidelberg (2009) · doi:10.1007/978-3-642-05089-3_20 |
| [33] | Walkinshaw, N., Lambeau, B., Damas, C., Bogdanov, K., Dupont, P.: STAMINA: a competition to encourage the development and assessment of software model inference techniques. Empirical Software Engineering 18(4), 791–824 (2013) · doi:10.1007/s10664-012-9210-3 |
| [34] | Wiedijk, F.: Formal Proof – Getting Started. Notices of the American Mathematical Society 55(11), 1408–1414 (2008) · Zbl 1188.68267 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
