Yingjia Wan
Yingjia Wan
About
Publications
Experiences
Accomplishments
CV
Blogs
Contact
Light
Dark
Automatic
3
FormalAlign: Automated Alignment Evaluation for Autoformalization
FormAlign addressed a long-lasting challenge in autoformalization systems - the absence of an effective alignment evaluation metric, It accurately assesses the semantic and logical alignment between the natural-language and formal language theorems.
Jianqiao Lu
,
Yingjia Wan
,
Yinya Huang
,
Zhengying Liu
,
Zhijiang Guo
arXiv
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
Cite
×