Исследователи представляют FormalRx, комплексную диагностическую систему оценки, предназначенную для преобразования оценки автоформализации из непрозрачных бинарных вердиктов в действенную обратную связь. Система использует SCI Error Taxonomy для декомпозиции ошибок на 28 различных категорий и предоставляет возможности для вынесения вердиктов о соответствии, категоризации ошибок, локализации и исправления.
- FormalRx включает диагностическую модель FormalRx-8B, обученную на 56 287 парах NL-FL с детализированными аннотациями.
- Фреймворк выпускает FormalRx-Test как первый детализированный диагностический бенчмарк для автоформализации.
- FormalRx-8B достигает F1-оценок 0.88 для вердиктов и 0.71 для категоризации, а также точности 0.75 для локализации и 0.73 для исправления.
- Модель существенно превосходит как общие LLM, так и специализированные базовые модели в этих диагностических задачах.
Связывая оценку с действенными выводами, FormalRx позволяет проводить систематическую диагностику и улучшение систем автоформализации.