研究者らは、自動形式化の評価を不透明な二値判定から実行可能なフィードバックへと転換するために設計された包括的な診断評価フレームワークであるFormalRxを発表した。本システムはSCI Error Taxonomyを活用してエラーを28の明確なカテゴリに分解し、アラインメント判定、エラー分類、局所化、および修正の機能を提供する。

  • FormalRxには、56,287件のNL-FLペアと微細な注釈を用いて訓練された診断モデルFormalRx-8Bが含まれる。
  • 本フレームワークは、自動形式化向けの最初の微細な診断ベンチマークであるFormalRx-Testを公開した。
  • FormalRx-8Bは、判定においてF1スコア0.88、分類において0.71を達成し、局所化で精度0.75、修正で精度0.73を記録した。
  • このモデルは、これらの診断タスクにおいて汎用LLMおよび専門的なベースラインを大幅に上回った。

評価を実行可能な洞察と結びつけることで、FormalRxは自動形式化システムの体系的な診断と改善を可能にする。