FormalRx：纠正和检查自动形式化中的语义故障

自动形式化中准确的语义对齐对于形式数学推理具有重要意义。然而，现有的评估仅提供不透明的二元判决或标量分数，无法提供有关翻译失败的位置或原因的可解释的见解。这种不透明性严重限制了人类的理解和自动化系统的改进。为了弥补这一差距，我们引入了 FormalRx，这是一个全面的诊断评估框架，可将自动形式化评估从黑盒判断转变为可操作的反馈。其核心是 SCI 错误分类法，这是一种分层分类方案，将自动形式化错误分解为 28 个不同的类别，并具有严格的优先级排序。在此分类的基础上，FormalRx 提供了四种关键的诊断功能：对齐判定、错误分类、错误定位和纠正。我们使用诊断模型 FormalRx-8B 实例化该框架，并使用细粒度诊断注释对 56,287 个 NL-FL 对进行训练，并发布 FormalRx-Test 作为第一个细粒度诊断基准。 FormalRx-8B 的 F1 分数为 0.88（判定）和 0.71（分类），准确度为 0.75（定位）和 0.73（校正），大大优于通用 LLM 和专用基线。通过将评估与可操作的见解联系起来，FormalRx 可以实现自动形式化系统的系统诊断和改进。