FormalAlign: Automated Alignment Evaluation for Autoformalization
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_ | 1866909347660955648 |
|---|---|
| author | Lu, Jianqiao Wan, Yingjia Huang, Yinya Xiong, Jing Liu, Zhengying Guo, Zhijiang |
| author_facet | Lu, Jianqiao Wan, Yingjia Huang, Yinya Xiong, Jing Liu, Zhengying Guo, Zhijiang |
| contents | Autoformalization aims to convert informal mathematical proofs into machine-verifiable formats, bridging the gap between natural and formal languages. However, ensuring semantic alignment between the informal and formalized statements remains challenging. Existing approaches heavily rely on manual verification, hindering scalability. To address this, we introduce \textsc{FormalAlign}, the first automated framework designed for evaluating the alignment between natural and formal languages in autoformalization. \textsc{FormalAlign} trains on both the autoformalization sequence generation task and the representational alignment between input and output, employing a dual loss that combines a pair of mutually enhancing autoformalization and alignment tasks. Evaluated across four benchmarks augmented by our proposed misalignment strategies, \textsc{FormalAlign} demonstrates superior performance. In our experiments, \textsc{FormalAlign} outperforms GPT-4, achieving an Alignment-Selection Score 11.58\% higher on \forml-Basic (99.21\% vs. 88.91\%) and 3.19\% higher on MiniF2F-Valid (66.39\% vs. 64.34\%). This effective alignment evaluation significantly reduces the need for manual verification. Both the dataset and code can be accessed via~\url{https://github.com/rookie-joe/FormalAlign}. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_10135 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | FormalAlign: Automated Alignment Evaluation for Autoformalization Lu, Jianqiao Wan, Yingjia Huang, Yinya Xiong, Jing Liu, Zhengying Guo, Zhijiang Computation and Language Artificial Intelligence Formal Languages and Automata Theory Machine Learning Autoformalization aims to convert informal mathematical proofs into machine-verifiable formats, bridging the gap between natural and formal languages. However, ensuring semantic alignment between the informal and formalized statements remains challenging. Existing approaches heavily rely on manual verification, hindering scalability. To address this, we introduce \textsc{FormalAlign}, the first automated framework designed for evaluating the alignment between natural and formal languages in autoformalization. \textsc{FormalAlign} trains on both the autoformalization sequence generation task and the representational alignment between input and output, employing a dual loss that combines a pair of mutually enhancing autoformalization and alignment tasks. Evaluated across four benchmarks augmented by our proposed misalignment strategies, \textsc{FormalAlign} demonstrates superior performance. In our experiments, \textsc{FormalAlign} outperforms GPT-4, achieving an Alignment-Selection Score 11.58\% higher on \forml-Basic (99.21\% vs. 88.91\%) and 3.19\% higher on MiniF2F-Valid (66.39\% vs. 64.34\%). This effective alignment evaluation significantly reduces the need for manual verification. Both the dataset and code can be accessed via~\url{https://github.com/rookie-joe/FormalAlign}. |
| title | FormalAlign: Automated Alignment Evaluation for Autoformalization |
| topic | Computation and Language Artificial Intelligence Formal Languages and Automata Theory Machine Learning |
| url | https://arxiv.org/abs/2410.10135 |