کتابخانهٔ Lean برای صورت‌بندی نظریهٔ منظم‌سازی خطی با کمک هوش مصنوعی

پژوهشگران در پیش‌چاپی در arXiv، کتابخانهٔ AutoIP را معرفی کرده‌اند؛ مجموعه‌ای در دستیار اثبات Lean که نظریهٔ کلاسیک منظم‌سازی خطی و مبانی تحلیل تابعی آن را عامل‌های هوش مصنوعی به‌صورت رسمی درآورده‌اند. Lean اثبات‌ها را تا سطح اصول موضوعه بررسی می‌کند و به‌گفتهٔ نویسندگان، عامل‌های هوش مصنوعی نوشتن چنین اثبات‌هایی را کم‌هزینه‌تر کرده‌اند.

بااین‌حال، اثبات ماشینی فقط همان گزارهٔ رسمی را تأیید می‌کند که برایش نوشته شده است. بنابراین، نویسندگان AutoIP کتابخانه را طوری سازمان داده‌اند که بازبین بتواند صورت‌بندی رسمی هر گزاره را با نسخهٔ زبان طبیعی آن مقایسه کند؛ نیازی نیست بازبین خودِ اثبات را بخواند. تجربهٔ آنان نشان می‌دهد خطر اصلی ممکن است در صورت‌بندی گزاره‌ها باشد، نه در اثبات‌ها.

نویسندگان می‌گویند آزمون‌های خودکار ساده روی گزاره‌ها می‌توانند حتی مشکلاتی را در ادبیات تثبیت‌شده آشکار کنند. آن‌ها برای نمونه به قضیه‌ای در یک کتاب درسی اشاره می‌کنند که فرض آن محدودکننده‌تر از چیزی است که در متن ادعا شده است. پژوهشگران از جامعهٔ مسائل معکوس دعوت کرده‌اند کتابخانه را گسترش دهد و بر پایهٔ آن کار کند.