3

FormalAlign: Automated Alignment Evaluation for Autoformalization
FormalAlign addressed a long-lasting challenge in autoformalization - the absence of an effective alignment evaluation metric. It accurately assesses the semantic and logical alignment between the natural language and formal theorems.
Jianqiao Lu, Yingjia Wan, Yinya Huang, Zhengying Liu, Zhijiang Guo
arXiv
FormalAlign: Automated Alignment Evaluation for Autoformalization
Process-Driven Autoformalization in Lean 4
We propose (1) FormL4, a large-scale autoformalization dataset; (2) PDA, a novel process-driven training framework for improving statement autoformalization, which leverages the process-level labels collected from statement+proof compiler feedback.
Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Haiming Wang, Zhicheng Yang, Jing Tang, Zhijiang Guo
Code Dataset arxiv
Process-Driven Autoformalization in Lean 4