Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
यह शोध पत्र यह तर्क देता है कि प्राकृतिक-भाषा-से-लीन (natural-language-to-Lean) औपचारिकीकरण का मूल्यांकन करने के लिए केवल लीन संकलन दरों (Lean compilation rates) पर निर्भर रहना भ्रामक है क्योंकि सिंटैक्टिक वैधता और सिमेंटिक निष्ठा के बीच एक महत्वपूर्ण अंतर है, और यह एक कठोर मानव-कैलिब्रेटेड सर्वसम्मति मीट्रिक का प्रस्ताव करता है तथा औपचारिक कथन की सटीकता में सुधार के लिए एलैबोरेशन फीडबैक (elaboration feedback) को सबसे महत्वपूर्ण हस्तक्षेप के रूप में पहचानता है।