The Isabelle Archive of Formal Proofs has grown to a significant size in the past years. It makes up for an impressive body of research, which enables a number of statistical approaches to various aspects in theorem proving, and has not yet been utilized exhaustively. However, the growing size also poses some challenges to address: Material becomes increasingly harder to find, reusability and ease of understanding become more important. This thesis abstract summarizes my research plans on those topics and briefly touches on preliminary results, which indicate that the node in-degree of the dependency graph of the archive follows a scale-free distribution.
Isabelle is an interactive theorem prover [
The entities defined by those theories and their relationships can be described as a dependency
graph (sometimes also referred to as General Dependency Network [
scale-free, i.e. it follows some power law Pr( ) ∝ in contrast to random graphs where each possible edge is present with a fixed probability − [4], (Erdős–Rény model). Graphs with such topological properties are called complex networks, which have been studied in the context of real-world graphs from many diferent areas [ 5]. In contrast to research focused on object-oriented characteristics (e.g., classes and inheritance), structural analysis on dependency graphs of software systems can be transferred to the field of formal theories more directly.
Another important application of this dependency network is proof automation. Data mining methods to extract patterns from graphs have been extensively studied, for instance frequent itemset mining to find subsets of nodes that frequently occur together [ 6, 7]. The AFP provides https://www21.in.tum.de/home/~huch (F. Huch) enough data to enable pattern mining for proofs as well as evaluate the efectiveness of derived automation.
Regarding the AFP, empirical analysis has already been done by Blanchette et al. in [8]. They measured the AFP size and authorship distribution and how those evolved over time, computed the session graph, proof depths, and compared proof size to definition size and statement complexity (by number of clauses). Moreover, they benchmarked how many theorems sledgehammer could solve on a representative test suite. This research provides a good baseline of empirical data; I plan to follow up on it by analyzing the underlying GDN of AFP theories, which can possibly yield some deeper results.
Very recently, usability of the AFP has also gotten some attention. Two diferent search engines for theory contents were introduced: The FindFacts search by Huch and Krauss in [9], and the concept-oriented SErAPIS engine by Stathopoulos et al. in [10]. Additionally, MacKenzie et al. evaluated usability of the AFP webpage in [11] and built the prototype for a re-design.
Complex networks for software systems were first introduced by Myers in [4]. In [12], Zimmermann and Nagappan measured the correlation between software defects and a comprehensive list of network metrics; Šubelj and Bajec later surveyed quality indicators, and performed package prediction by clustering on the network [13]. While there is no concern about defects in theorem proving due to the nature of the field, my aim is to transfer some of those findings to formal theories in order to detect structural problems that impair reusability and readability.
For proof automation, the idea of learning from existing material has been around for some time. In Isabelle, Duncan derived tactics from proofs script sequences using Markov models and genetic programming with the goal of full automatization in [14], which was successful for less complex lemmas. More recently, Nawaz et al. used high utility itemset mining on a syntactic level to discover patterns in proofs scripts of PVS [15]. In contrast, I aim to extract patterns from the more fine-grained theorem dependency graph. This also makes it possible to utilize structured Isar proofs in the pattern extraction.
In the following, my research plans are separated into concrete questions and topics that involve engineering tasks.
RQ1: Do theory dependency networks follow the topological patterns typically found in complex networks? RQ2: Which metrics are relevant quality indicators for formal theories? Can they expose structural problems? RQ3: Is it possible to detect elements that need to be refactored? Can theory- and sessionstructure be predicted to generate refactoring recommendations? RQ4: How can visualization be helpful to better understand the structure of formalizations? RQ5: Which patterns can we learn from theorem networks? Can they be used to improve automation?
There are several aspects I want to improve on in the AFP. By introducing digital object identifiers, entries can be much better referenced. Identifiers could potentially even be assigned to individual concepts of an entry, though creating such a mapping poses lots of challenges. Moreover, introducing more fields for entries, such as subject classification and links to (print)publications, can help organizing the AFP in the future. Finally, the AFP website needs to be improved for better usability – there is already a prototype (as discussed in section 2), which still needs to be integrated.
Currently, the AFP does not allow proofs by s o r r y (which are admitted with the help of an oracle [16]). However, it is often desirable to have what is sometimes referred to as Formal Abstract [17]: a formalization of results from literature without rigorous proofs. To that end, I want do add a proof by reference mechanism, which weakly checks references and allows such proofs to be added to the AFP in a separate, less trusted, session group.
In Isabelle, I plan to integrate the FindFacts search into the prover IDE (and add support for type-classes and locales), as well as tooling for clone detection and advanced IDE functionality such as structural search and replace.
The dependency graph of Isabelle and the AFP (release 2021) consists of approximately 2.1 ⋅ 106 nodes and 2.5 ⋅ 108 directed edges (when considering all types of entities and relationships). Figure 1 shows the in-degree distribution of that graph. For > 2, it is clearly linear on the log-log scale; this indicates a power-law distribution, which is typical for scale-free networks [5]. The individual AFP components show similar characteristics; this illustrates why complex network science is relevant to the topic. 10−1 10−2 ) 10−3 ( r P 10−4 10−5 10−6 100 101 102 104 105
106 103 [4] C. R. Myers, Software systems as complex networks: Structure, function, and evolvability of software collaboration graphs, Phys. Rev. E 68 (2003) 046116. doi: 1 0 . 1 1 0 3 / P h y s R e v E . 6 8 . in complex networks, Complexity 8 (2002) 20–33. doi:1 0 . 1 0 0 2 / c p l x . 1 0 0 5 5 . [12] T. Zimmermann, N. Nagappan, Predicting defects using network analysis on dependency graphs, in: Proceedings of the 30th International Conference on Software Engineering, ICSE ’08, Association for Computing Machinery, New York, NY, USA, 2008, p. 531–540. [13] L. Šubelj, M. Bajec, Software systems through complex networks science: Review, analysis and applications, in: Proceedings of the First International Workshop on Software Mining, SoftwareMining ’12, Association for Computing Machinery, New York, NY, USA, 2012, p. 9–16. doi:1 0 . 1 1 4 5 / 2 3 8 4 4 1 6 . 2 3 8 4 4 1 8 . [14] H. Duncan, The Use of Data-Mining for the Automatic Formation of Tactics, Ph.D. thesis,
University of Edinburgh, 2007. [15] M. S. Nawaz, P. Fournier-Viger, J. Zhang, Proof Learning in PVS with Utility Pattern
Mining, IEEE Access 8 (2020) 119806–119818. doi:1 0 . 1 1 0 9 / A C C E S S . 2 0 2 0 . 3 0 0 4 1 9 9 . [16] M. Wenzel, et al., The Isabelle/Isar reference manual, Technische Universität München, 2021. [17] T. Hales, Big conjectures, in: Computer-aided mathematical proof, 2017.