Process-Driven Autoformalization 用 Lean compiler feedback 做 process supervision，开始系统训练自然语言→Lean 转换

Lu 等人提出面向 Lean 4 的 autoformalization benchmark 与 Process-Supervised Verifier（PSV），不仅评估最终 statement / proof 是否正确，还利用 Lean compiler 在中间过程提供精确反馈。论文报告 process information 能让 verifier 更有效使用较少过滤数据，并提升自然语言数学到 Lean statement / proof 的转换质量。