Restructuring formal mathematics for natural texts
Robert L. Constable, Amanda M. Holland-Minkley · 2004
In the presence of growing collections of formal mathematics, and renewed interest in formal mathematics and automated theorem proving for new domains such as hardware or code verification, it is vital to be able to present formal content accessibly to broad audiences. We propose a novel approach to constructing a content planner for formal mathematics produced by a tactic-style prover which capitalizes on the inherent structure of the formal proofs. Though it had been posited that high-level formal structure is unsuitable as a source of information for text generation, due to its heuristic nature and necessary lack of details, we are able to show that this is not the case. Tactic-style proofs share significant structural commonality with the discourse structure of corresponding texts. These commonalities allow a content planner to be constructed which need only use low-level logical content as a supplementary information source to the generation process. To show that this is the case, we collected two corpora of texts generated to communicate the proof content of a series of formal proofs produced by the Nuprl theorem proving system. Analysis of these corpora established the structural commonalities between tactic proofs and mathematical discourse structure. We were able to observe significant regularity between the sentences produced to communicate similar reasoning steps found in the source formal proofs. From this insight, and based on the texts from our corpora, we defined fifteen mathematics communication conventions that describe the variety of sentences produced within typical mathematical texts. Comparison of our results across the two corpora drawn from different domains allowed us to verify the generality of our results across mathematical topics and complexity of proofs. We also exhibit the extensibility of our system to more complex proof domains that employ different proof techniques. Finally, we performed a number of evaluations on our generated texts, most significantly a task-oriented evaluation in which readers' understanding of a proof based upon their reading of a generated text was tested. We conclude that content planning based primarily upon tactic-style proofs is effective and allows for construction of an extensible system.