Informal Discussion of the Motivation of the Project of Generating Text from Nuprl Proofs
The purpose of this project is to create a system that will allow for the automatic generation of mathematical proofs in English from a formal representation of the proof generated with the Nuprl reasoning assistant. There are a variety of contributions that we anticipate this system will be able to make that we will discuss here.
In the field of natural language generation research, we believe that the domain of mathematics offers unique advantages to the generation task. It is already commonly believed that in order to make progress in learning about the process of natural language generation it is better to restrict oneself to a limited domain of discourse, rather than trying to develop a generation system capable of covering the entire human range of discourse. We have chosen to limit ourselves to mathematics, and specifically the proofs of mathematical theorems, as the domain of discourse. One advantage of this approach is that the language of mathematics is used in very precise ways. Furthermore, the structure of an English proof is directly guided by the structure of the underlying formal proof, making high-level discourse planning easier and allowing us to focus more of our attention on later aspects of the planning process. In addition, by having the reasoning system which produced these proofs available to us and incorporating it into our planner, we hope to be able to make decisions about what types of utterances to produce in a principled manner, rather than having to use heuristics. The reasoning system could be used to provide information about the reasoning process that is not easily obtained from the final formal proof which is produced.
There are many concrete advantages that the Nuprl reasoning assistant will derive from having a natural language component. There is a large corpus of formal math which has already been created with the Nuprl system. Because there is some training required to be able to read these formal proofs, having English versions would make these proofs available to a wider audience. Given the size of the corpus and it's potential rate of growth, this task would be practical only if it could be done automatically. Even if a user locates a single proof that they are interested in and want to communicate to others, the process of translation is time consuming because of the length of formal proofs and it is possible for even expert users, in the process of translating a proof, to make a mistake in the translation process and produce an invalid English translation of a valid formal proof. This is a problem that we hope an automatic system will avoid.
The generation component would also be useful to users while they are using the system to produce proofs. By being able to generate English versions of partially completed proofs, the user will be able to get feedback in a more intuitive format about the progress of the proof. This could be useful both to novice users who may need additional support in learning the formal language of Nuprl and for more advanced users by showing them the structure of their proof from a higher-level perspective.
Finally, we hope that our work will allow us learn more about the nature of the language of mathematics. Just by studying the corpus of human translations that we collected we have observed some very strong patterns across subjects in how the proofs were translated. Further studies will hopefully bring further interesting patterns to light. By studying the corpus that we already have, we have been able to define a categorizing system for grouping inference steps in proofs into a small number of classes. The steps in each class can all be dealt with similarly by the generation system. These categories seem to correspond to common proof techniques used in proofs. We have been able to start making observations about which of many equivalent logical forms people prefer to use when verbalizing a logical statement. It may ultimately be possible for insights such as this to be used in guiding some of the reasoning and presentation choices of the Nuprl system on the formal level.