FormalRx is a diagnostic evaluation framework for autoformalization built on the SCI Error Taxonomy (28 error categories). It supports alignment verdicts, error categorization, localization, and correction, and introduces FormalRx-8B and the FormalRx-Test benchmark.

FaStfact is a multi-agent pipeline for evaluating long-form generation factuality that achieves the highest alignment with human evaluation and time/token efficiency among existing baselines. An annotated FaStfact-bench is also open-sourced.

FormalAlign aims to address 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.