وقتی سختترین بخش پژوهش دیگه سخت نیست
هوش مصنوعیخلاصهٔ کاملتر
چند روز پیش مقالهای با عنوان Tracking Borrows with Regular Expressions توی OOPSLA'26 پذیرفته شد؛ مقالهای که یه سیستم تایپ تازه برای Move — یه زبان قرارداد هوشمند شبیه Rust — معرفی میکنه و از عبارتهای منظم برای گرفتن heap reachability، یعنی اینکه از هر مرجع چه بخشهایی از حافظه قابل دسترسه، استفاده میکنه. ولی حرف اصلی نویسنده خود این ایده نیست؛ اینه که مقاله چطور ساخته شد.
به گفتهی نویسنده، مکانیزهکردن متاتئوری و اثباتهای صوری سلامت — همون بخشی که معمولاً ۸۰ تا ۹۰ درصد انرژی یه مقالهی طراحی زبان رو میبلعه — یهنفره، توی Lean و با کمک یه LLM پیشرو، در حدود چهار هفته و در مقیاس یه کامپایلر واقعی (نه یه calculus اسباببازی) تموم شد. وقتی مارس امسال دربارهش نوشت، واکنش جامعهی پژوهش زبانهای برنامهنویسی از شک («پس لابد فرمالسازی سخت نبوده») تا رد کامل («این روش درست انجام تئوری زبان نیست») بود.
نویسنده معتقده همین واکنشها یه چیزی دربارهی فرهنگ انتشار مقاله میگن: تا وقتی یه پژوهش مقدار زیادی زحمت انسانیِ قابلدیدن نشون نده، جدی گرفته نمیشه. ایدهی خوشساخت رو دوست داریم، ولی ترجیح میدیم توی هشت تا ده نفر-ماه کار بستهبندی بشه: یه پیادهسازی بزرگ، بنچمارک مفصل، یا اثباتهای ماشینچکشدهای که دستی جلو رفتن. به گفتهی او اون بستهبندی حالا از بین رفته.
مثال دیگهای که میزنه Martin Rinard، استاد MIT ـه: حدود یه ماه طول کشید تا یه کامپایلر بهینهساز رو کامل توی Lean فرمال کنه و مقالهش رو بفرسته، اون هم بدون اینکه قبلش اصلاً با Lean کار کرده باشه. اثرش توی آمار هم پیداست: مقالههای ارسالی POPL امسال تقریباً دو برابر شده، از حدود ۳۵۰ به ۶۰۰. نکتهی غیرمنتظره اینه که سهم محتوای بیکیفیت و ماشینساز بینشون کمه؛ بیشترشون پژوهش درستوحسابیان که فقط ده برابر سریعتر جلو رفتن.
قبلاً داشتن بیشتر از دو مقاله توی یه POPL یا PLDI یا OOPSLA یا ICFP نشونهی یه گروه پرکار و شبکهی همکاری گسترده بود؛ حالا همون حجم کار از دست یه فارغالتحصیل دکترای تنها با ایدههای خوب برمیاد. نویسنده پیشبینی میکنه تا یکی دو سال دیگه سه چهار مقالهی تکنویسنده توی یه کنفرانس درجهیک عادی بشه — و بعدش جامعه مجبوره سطح رو ببره بالا، چون وقتی هر کسی میتونه CompCert یا میکروکرنل seL4 رو از صفر بسازه، مقالهی قدیمیسبک دیگه ارزش وقت گذاشتن نداره.
نکات کلیدی:
- مقالهی Tracking Borrows with Regular Expressions یه سیستم تایپ تازه برای زبان Move ارائه میکنه و توی OOPSLA'26 پذیرفته شده.
- اثباتهای صوری و مکانیزهکردن متاتئوری، که معمولاً ۸۰ تا ۹۰ درصد کار یه مقالهی PL ـه، یهنفره و توی چهار هفته با Lean و یه LLM انجام شد.
- Martin Rinard از MIT بدون سابقهی کار با Lean، توی حدود یک ماه یه کامپایلر بهینهساز رو فرمال کرد و مقالهش رو فرستاد.
- مقالههای ارسالی POPL امسال از حدود ۳۵۰ به ۶۰۰ رسید و سهم محتوای بیکیفیت بینشون کم بود.
- کد Lean این پروژه توی مخزن گیتهاب ilyasergey/lean-move در دسترسه.
