Abstract
Interactive theorem provers (ITPs) are powerful tools for the formalverification of mathematical proofs down to the axiom level. However, theirlack of a natural language interface remains a significant limitation. Recentadvancements in large language models (LLMs) have enhanced the understanding ofnatural language inputs, paving the way for autoformalization - the process oftranslating natural language proofs into formal proofs that can be verified.Despite these advancements, existing autoformalization approaches are limitedto verifying complete proofs and lack the capability for finer, sentence-levelverification. To address this gap, we propose StepProof, a novelautoformalization method designed for granular, step-by-step verification.StepProof breaks down complete proofs into multiple verifiable subproofs,enabling sentence-level verification. Experimental results demonstrate thatStepProof significantly improves proof success rates and efficiency compared totraditional methods. Additionally, we found that minor manual adjustments tothe natural language proofs, tailoring them for step-level verification,further enhanced StepProof's performance in autoformalization.