Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909418041376768 |
|---|---|
| author | Li, Zenan Wu, Yifan Li, Zhaoyu Wei, Xinming Zhang, Xian Yang, Fan Ma, Xiaoxing |
| author_facet | Li, Zenan Wu, Yifan Li, Zhaoyu Wei, Xinming Zhang, Xian Yang, Fan Ma, Xiaoxing |
| contents | Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in mathematics. Recent advancements in large language models (LLMs) have unveiled their promising capabilities to formalize even competition-level math problems. However, we observe a considerable discrepancy between pass@1 and pass@k accuracies in LLM-generated formalizations. To address this gap, we introduce a novel framework that scores and selects the best result from k autoformalization candidates based on two complementary self-consistency methods: symbolic equivalence and semantic consistency. Elaborately, symbolic equivalence identifies the logical homogeneity among autoformalization candidates using automated theorem provers, and semantic consistency evaluates the preservation of the original meaning by informalizing the candidates and computing the similarity between the embeddings of the original and informalized texts. Our extensive experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy, achieving up to 0.22-1.35x relative improvements across various LLMs and baseline methods. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_20936 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency Li, Zenan Wu, Yifan Li, Zhaoyu Wei, Xinming Zhang, Xian Yang, Fan Ma, Xiaoxing Computation and Language Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in mathematics. Recent advancements in large language models (LLMs) have unveiled their promising capabilities to formalize even competition-level math problems. However, we observe a considerable discrepancy between pass@1 and pass@k accuracies in LLM-generated formalizations. To address this gap, we introduce a novel framework that scores and selects the best result from k autoformalization candidates based on two complementary self-consistency methods: symbolic equivalence and semantic consistency. Elaborately, symbolic equivalence identifies the logical homogeneity among autoformalization candidates using automated theorem provers, and semantic consistency evaluates the preservation of the original meaning by informalizing the candidates and computing the similarity between the embeddings of the original and informalized texts. Our extensive experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy, achieving up to 0.22-1.35x relative improvements across various LLMs and baseline methods. |
| title | Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency |
| topic | Computation and Language |
| url | https://arxiv.org/abs/2410.20936 |