Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2506.10558 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916816782098432 |
|---|---|
| author | Hu, Xiaolin Zhou, Qinghua Grechuk, Bogdan Tyukin, Ivan Y. |
| author_facet | Hu, Xiaolin Zhou, Qinghua Grechuk, Bogdan Tyukin, Ivan Y. |
| contents | Interactive theorem provers (ITPs) are powerful tools for the formal verification of mathematical proofs down to the axiom level. However, their lack of a natural language interface remains a significant limitation. Recent advancements in large language models (LLMs) have enhanced the understanding of natural language inputs, paving the way for autoformalization - the process of translating natural language proofs into formal proofs that can be verified. Despite these advancements, existing autoformalization approaches are limited to verifying complete proofs and lack the capability for finer, sentence-level verification. To address this gap, we propose StepProof, a novel autoformalization method designed for granular, step-by-step verification. StepProof breaks down complete proofs into multiple verifiable subproofs, enabling sentence-level verification. Experimental results demonstrate that StepProof significantly improves proof success rates and efficiency compared to traditional methods. Additionally, we found that minor manual adjustments to the natural language proofs, tailoring them for step-level verification, further enhanced StepProof's performance in autoformalization. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_10558 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | StepProof: Step-by-step verification of natural language mathematical proofs Hu, Xiaolin Zhou, Qinghua Grechuk, Bogdan Tyukin, Ivan Y. Logic in Computer Science Artificial Intelligence Interactive theorem provers (ITPs) are powerful tools for the formal verification of mathematical proofs down to the axiom level. However, their lack of a natural language interface remains a significant limitation. Recent advancements in large language models (LLMs) have enhanced the understanding of natural language inputs, paving the way for autoformalization - the process of translating natural language proofs into formal proofs that can be verified. Despite these advancements, existing autoformalization approaches are limited to verifying complete proofs and lack the capability for finer, sentence-level verification. To address this gap, we propose StepProof, a novel autoformalization method designed for granular, step-by-step verification. StepProof breaks down complete proofs into multiple verifiable subproofs, enabling sentence-level verification. Experimental results demonstrate that StepProof significantly improves proof success rates and efficiency compared to traditional methods. Additionally, we found that minor manual adjustments to the natural language proofs, tailoring them for step-level verification, further enhanced StepProof's performance in autoformalization. |
| title | StepProof: Step-by-step verification of natural language mathematical proofs |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2506.10558 |