Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure
This addresses the challenge of making formal proofs accessible to non-experts, though it appears incremental as it builds on existing LLM capabilities for a specific domain.
The paper tackles the problem of translating machine-verifiable formal proofs into natural language by using LLMs to informalize proof steps and recursively summarize along the proof structure. It demonstrates the method generates highly readable and accurate natural language proofs when applied to formal proof data from a textbook and the Lean proof assistant library.
This paper proposes a natural language translation method for machine-verifiable formal proofs that leverages the informalization (verbalization of formal language proof steps) and summarization capabilities of LLMs. For evaluation, it was applied to formal proof data created in accordance with natural language proofs taken from an undergraduate-level textbook, and the quality of the generated natural language proofs was analyzed in comparison with the original natural language proofs. Furthermore, we will demonstrate that this method can output highly readable and accurate natural language proofs by applying it to existing formal proof library of the Lean proof assistant.