چیدمان کره‌ها؛ ریاضیاتی که پیامک‌های شما را نجات می‌دهد

زمانی که کوهن و الکیس روش خود را در سال ۲۰۰۳ معرفی کردند، هیچ‌کس قدرت واقعی رویکردشان را درک نمی‌کرد. این چارچوب در بعضی ابعاد کوچک به پیشرفت‌های بزرگی منجر شد، اما معلوم نبود آیا می‌تواند رکورد ۴۸ساله‌ی سرعت کاهش تراکم با افزایش ابعاد را نیز بهبود دهد یا خیر.

آستانه‌ی آسترا به این سؤال پاسخ می‌دهد؛ بله، چارچوب کوهن-الکیس می‌تواند رکورد را بهبود ببخشد، ولی تا یک حد مشخص و اکنون آن حد به‌طور دقیق شناخته شده است.

البته یک اثبات ادعاشده معمولاً زمانی به نتیجه‌ای پذیرفته‌شده در ریاضیات تبدیل می‌شود که ریاضی‌دانان دیگر آن را بررسی و تأیید کنند. پیشرفت‌های OpenAI از این نظر مزیت اولیه‌ای دارند، زیرا همانند بسیاری از پیشرفت‌های اخیر هوش مصنوعی در ریاضیات، اثبات‌ها همراه با نسخه‌ای رسمی در زبان دستیار اثبات Lean ارائه شده‌اند.

اثبات‌هایی که در Lean نوشته می‌شوند شبیه کد رایانه‌ای به نظر می‌رسند، با این تفاوت که محتوای ریاضی بسیار بیشتری دارند. درواقع خود سیستم Lean می‌تواند صحت ساختار منطقی اثبات را بررسی کند. شما گزاره‌ی یک قضیه را در زبان Lean می‌نویسید و سپس اثبات را ارائه می‌کنید. اگر اثبات واقعاً قضیه را تأیید کند، Lean هم به آن مهر تأیید می‌زند.

کارشناسان برای تشخیص صحت زنجیره‌ی منطقی اثبات مجبور نیستند تمام جزئیات را دستی بررسی کنند، اما باید مطمئن شوند قضیه‌ای که در Lean نوشته شده، واقعاً همان ادعای ریاضی موردنظر پژوهشگران را منعکس می‌کند. تا زمان انتشار این مقاله، متخصصان این حوزه تنها بخشی از فایل‌های Lean را بررسی کرده‌اند.

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

یکی از سخنگویان OpenAI به جوزف هاولت، گزارشگر ارشد ساینتیفیک امریکن گفت: «ما مسئولیت صحت این نتایج را برعهده می‌گیریم و همان استانداردهایی را رعایت می‌کنیم که معمولاً از ریاضی‌دانان انسانی انتظار می‌رود.»

شرکت OpenAI هزینه‌ی یافتن این ۱۰ اثبات را از منظر استفاده از هوش مصنوعی معادل ۲۰۰۰ دلار اعلام می‌کند؛ هرچند که این عدد هزینه‌ی تلاش‌های ناموفق را در نظر نمی‌گیرد. مدل آسترا به‌خاطر اثباتش برنده مدال فیلدز نخواهد شد، اما اگر نتایج پس از بررسی انسانی تأیید شوند، مرزهای چیدمان کره‌ها را به جلو می‌برد و باید انتظار داشته باشیم که به‌زودی دستاوردهای بیشتری از آن ببینیم.