Para peneliti memperkenalkan FormalRx, sebuah kerangka kerja evaluasi diagnostik komprehensif yang dirancang untuk mengubah penilaian autoformalisasi dari putusan biner yang tidak transparan menjadi umpan balik yang dapat ditindaklanjuti. Sistem ini memanfaatkan SCI Error Taxonomy untuk menguraikan kesalahan ke dalam 28 kategori berbeda dan menyediakan kemampuan untuk putusan penyesuaian, kategorisasi kesalahan, lokalisasi, dan koreksi.
- FormalRx mencakup model diagnostik, FormalRx-8B, yang dilatih pada 56.287 pasangan NL-FL dengan anotasi berbutir halus.
- Kerangka kerja ini merilis FormalRx-Test sebagai benchmark diagnostik berbutir halus pertama untuk autoformalisasi.
- FormalRx-8B mencapai skor F1 sebesar 0,88 untuk putusan dan 0,71 untuk kategorisasi, serta akurasi sebesar 0,75 untuk lokalisasi dan 0,73 untuk koreksi.
- Model ini secara substansial mengungguli baik LLM tujuan umum maupun baseline khusus dalam tugas-tugas diagnostik ini.
Dengan menghubungkan evaluasi dengan wawasan yang dapat ditindaklanjuti, FormalRx memungkinkan diagnosis dan peningkatan sistem autoformalisasi secara sistematis.