FormalRx：修正与审查形式化过程中的语义失败

自动形式化中准确的语义对齐对形式化数学推理至关重要。然而，现有评估仅提供不透明的二元判决或标量分数，缺乏对翻译失败原因的可解释洞察。为此，本文提出 FormalRx，一个将评估从黑盒判断转化为可操作反馈的综合诊断框架。其核心是 SCI 错误分类法，将错误细分为 28 类。基于此，FormalRx 提供判决、分类、定位及修正四种诊断能力。实验表明，专用模型 FormalRx-8B 在各项指标上显著优于通用大模型，实现了系统的诊断与改进。