FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
यह शोधपत्र FormalProofBench को पेश करता है, जो Lean 4 में औपचारिक रूप से सत्यापित स्नातक-स्तरीय गणितीय प्रमाण उत्पन्न करने की एआई मॉडलों की क्षमता का मूल्यांकन करने के लिए एक निजी बेंचमार्क है, जो यह प्रकट करता है कि सर्वश्रेष्ठ प्रदर्शन करने वाला मॉडल केवल 33.5% सटीकता प्राप्त करता है और टूल के उपयोग, विफलता के तरीकों और दक्षता का एक व्यापक विश्लेषण प्रदान करता है।