چارلز هاسکینسون، بنیانگذار کاردانو، در ۹ سپتامبر گفت که هوش مصنوعی در ریاضیات رسمی بیش از آنچه انتظار داشت پیشرفت کرده است.

اظهارات او پس از ادعای OpenAI مطرح شد مبنی بر اینکه یک سیستم داخلی راه‌حلی برای مسئله جایزه هزاره Navier–Stokes ارائه کرده است.

هاسکینسون در یک پخش زنده، قابلیت‌های گزارش شده را «بسیار قابل توجه» خواند. با این حال، او همچنین به سوالات حل‌نشده‌ای در مورد منشأ این کار و حفظ حریم خصوصی تحقیقات ارسال شده به خدمات هوش مصنوعی مبتنی بر ابر پرداخت.

بنیانگذار کاردانو می‌گوید هوش مصنوعی فراتر از ابزارهای همکاری حرکت کرده است

هاسکینسون گفت که در ابتدا انتظار داشت سیستم‌های رسمی به تیم‌های بزرگ‌تری از ریاضیدانان کمک کنند تا در اثبات‌های نوشته شده توسط انسان همکاری کرده و آن‌ها را تأیید کنند. او انتظار نداشت که مدل‌های زبان بزرگ به این زودی خودشان اثبات‌های کامل را تولید کنند.

هاسکینسون گفت: «ما هرگز تا این حد که هوش مصنوعی وارد میدان شود، پیش‌بینی نمی‌کردیم.» او افزود که ایده نوشتن کامل یک اثبات توسط هوش مصنوعی پیش از این «بسیار دور از انتظار» به نظر می‌رسید.

هاسکینسون ارتباط مستقیمی با تحقیقات ریاضیات رسمی دارد. بر اساس اعلام دانشگاه، او در سال ۲۰۲۱، ۲۰ میلیون دلار به دانشگاه کارنگی ملون اهدا کرد تا مرکز هاسکینسون برای ریاضیات رسمی را تأسیس کند.

آخرین اظهارات او همچنین با آزمایش‌های گسترده‌تر کاردانو با هوش مصنوعی مطابقت دارد. همانطور که پیشتر crypto.news گزارش داده بود، هاسکینسون از آزمایش‌های عامل هوش مصنوعی کاردانو که شامل ارتباطات، فعالیت‌های جامعه و اکوسیستم متمرکز بر حریم خصوصی Midnight می‌شود، دفاع کرده است.

OpenAI ادعا می‌کند که سیستمش مسئله Navier–Stokes را حل کرده است

OpenAI تحقیقات خود را در ۸ سپتامبر منتشر کرد. این شرکت گفت که یک مدل داخلی تقریباً ۱۰,۰۰۰ عامل را هماهنگ کرده و پس از ۸۸ ساعت، راه‌حلی پیشنهادی ارائه داده است. سپس GPT-6 Astra ۱۷ ساعت دیگر را صرف رسمی‌سازی و بررسی استدلال در Lean کرد.

این اثبات تلاش می‌کند تا نشان دهد که یک سیال اولیه هموار و ایستا می‌تواند در زمان محدود و تحت تأثیر یک نیروی خارجی هموار، دچار تکینگی شود. OpenAI گفت که این امر با بیانیه‌های C و D در فرمول‌بندی رسمی جایزه هزاره مطابقت دارد.

این شرکت همچنین یک مقاله تحلیلی و کد Lean منتشر کرد. رسمی‌سازی Lean تأیید قابل بررسی توسط ماشین را فراهم می‌کند که گام‌های کدگذاری شده از مفروضات ذکر شده پیروی می‌کنند. این به طور مستقل ثابت نمی‌کند که هر تعریف و فرضیه به طور دقیق مسئله ریاضیاتی مورد نظر را نشان می‌دهد.

OpenAI گفت که قصد ندارد جایزه ۱ میلیون دلاری مرتبط را دنبال کند. با این حال، این شرکت کار خود را به عنوان راه‌حلی برای این مسئله توصیف کرد.

انستیتو کِلِی راه‌حل ادعا شده را به رسمیت نشناخته است

انستیتو ریاضیات کِلِی (Clay Mathematics Institute) همچنان مسئله Navier–Stokes را «حل نشده» می‌داند. وب‌سایت آن در زمان گزارش، اثبات پیشنهادی OpenAI را به عنوان یک راه‌حل پذیرفته شده به رسمیت نشناخته بود.

کِلِی راه‌حل‌های پیشنهادی را از طریق ارسال مستقیم نمی‌پذیرد. طبق قوانین آن، یک راه‌حل باید در یک نشریه واجد شرایط منتشر شود. سپس حداقل دو سال باید بگذرد و کار باید پذیرش عمومی جامعه جهانی ریاضیات را کسب کند.

این فرآیند به این معنی است که اعلامیه و اثبات رسمی OpenAI به منزله شناسایی رسمی فوری توسط نهاد نیست. ریاضیدانان باید بررسی کنند که آیا این ساختار با بیانیه دقیق مسئله مطابقت دارد و آیا استفاده آن از نیروی خارجی به سوال آن‌طور که معمولاً فهمیده می‌شود، پاسخ می‌دهد یا خیر.

اختلاف بر سر منشأ، سوالات حریم خصوصی تحقیق را مطرح می‌کند

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

باک‌مستر این سوال را مطرح کرد که آیا کار خصوصی وارد شده به سیستم Codex شرکت OpenAI می‌تواند در نتیجه این شرکت نقش داشته باشد یا خیر. او از ادعای سوءرفتار اثبات شده خودداری کرد و گفت: «نمی‌دانم آیا از داده‌های ما استفاده شده است یا خیر.»

OpenAI دسترسی به کار خاص آنها را رد کرد. با این حال، این شرکت گفت که نمی‌تواند به طور کامل احتمال اینکه داده‌های ناشناس شده (de-identified data) از استفاده محصول آنها به بهبود مدل‌هایش کمک کرده باشد را رد کند. OpenAI تأکید کرد که اثبات آن به طور مستقل توسعه یافته و با کار محققان متفاوت است.

هاسکینسون استدلال کرد که این اختلاف باید مورد توجه محققانی باشد که با ایده‌های منتشر نشده سروکار دارند. او گفت که محققانی که از خدمات هوش مصنوعی متمرکز استفاده می‌کنند باید در نظر بگیرند که آیا دستورات (prompts)، یادداشت‌ها و گزارش‌های تحقیقاتی محرمانه باقی می‌مانند یا خیر.

مرحله بعدی شامل بررسی عمومی مقاله OpenAI و رسمی‌سازی Lean خواهد بود. تا زمانی که متخصصان فرضیات را بررسی نکرده و شرایط رسمی انستیتو کِلِی برآورده نشود، این کار یک راه‌حل ادعا شده باقی می‌ماند و نه یک راه‌حل به رسمیت شناخته شده.