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.

MR-BEN is a comprehensive process-based benchmark to evaluate advanced `meta-reasoning’ skills, where models are asked to locate and analyse errors in the provided CoT solutions. It comprises 5,975 multi-domain samples with annotated groundtruths.

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.

AutoPSV proposes a simple, effective, and efficient method to automatically annotate reasoning steps (even without requiring grountruth answers).