研究人员推出了 FormalRx，这是一种全面的诊断评估框架，旨在将自动形式化的评估从模糊的二元判决转变为可操作的反馈。该系统利用 SCI Error Taxonomy 将错误分解为 28 个不同的类别，并提供对齐判决、错误分类、定位和纠正的能力。

  • FormalRx 包含一个诊断模型 FormalRx-8B，该模型在带有细粒度注释的 56,287 个 NL-FL 对上进行了训练。
  • 该框架发布了 FormalRx-Test，作为首个用于自动形式化的细粒度诊断基准测试。
  • FormalRx-8B 在判决和分类方面分别取得了 0.88 和 0.71 的 F1 分数，同时在定位和纠正方面达到了 0.75 和 0.73 的准确率。
  • 在这些诊断任务中，该模型显著优于通用 LLM 和专业基线模型。

通过将评估与可操作的见解相连接，FormalRx 使得自动形式化系统的系统性诊断和改进成为可能。