🤖 دستاورد بزرگ OpenAI در حل مسائل کلاسیک ریاضی
🚀 تیم تحقیقاتی OpenAI به‌تازگی نتایج خیره‌کننده‌ای را توسط مدل داخلی خود با نام Astra منتشر کرده است. این مدل توانسته است ده مسئله ریاضی را که دهه‌ها حل‌نشده باقی مانده بودند، با موفقیت حل کند و استدلال‌های خود را به‌صورت رسمی در محیط Lean (یک دستیار اثبات قضایا) فرمالیزه کند.
🔬 این مدل موفق به ثبت دستاوردهای شاخصی در حوزه‌های پیچیده ریاضی شده است که شامل موارد زیر است
🔹 گروه‌های غیر-سوفیک: ساخت اولین نمونه صریح از این گروه‌ها که پرسش دیرینه تقریب‌های جایگشت متناهی را حل می‌کند.
🔹 ابطال حدس صلبیت Connes: ساخت بی‌نهایت گروه غیرایزومورف با ویژگی (T) و جبر فون نویمان یکسان.
🔹 بسته‌بندی کره: بهبود کران کلی چگالی بسته‌بندی در ابعاد بالا پس از سال ۱۹۷۸.
🔹 تکرار موازی کوانتومی: اثبات تکرار موازی نمایی برای تمام بازی‌های کوانتومی دوطرفه درهم‌تنیده.
🔗 openai.com
#Astra_model #Lean_prover
🚀 تیم تحقیقاتی OpenAI به‌تازگی نتایج خیره‌کننده‌ای را توسط مدل داخلی خود با نام Astra منتشر کرده است. این مدل توانسته است ده مسئله ریاضی را که دهه‌ها حل‌نشده باقی مانده بودند، با موفقیت حل کند و استدلال‌های خود را به‌صورت رسمی در محیط Lean (یک دستیار اثبات قضایا) فرمالیزه کند.
🔬 این مدل موفق به ثبت دستاوردهای شاخصی در حوزه‌های پیچیده ریاضی شده است که شامل موارد زیر است
🔹 گروه‌های غیر-سوفیک: ساخت اولین نمونه صریح از این گروه‌ها که پرسش دیرینه تقریب‌های جایگشت متناهی را حل می‌کند.
🔹 ابطال حدس صلبیت Connes: ساخت بی‌نهایت گروه غیرایزومورف با ویژگی (T) و جبر فون نویمان یکسان.
🔹 بسته‌بندی کره: بهبود کران کلی چگالی بسته‌بندی در ابعاد بالا پس از سال ۱۹۷۸.
🔹 تکرار موازی کوانتومی: اثبات تکرار موازی نمایی برای تمام بازی‌های کوانتومی دوطرفه درهم‌تنیده.
🔗 openai.com
📊 Data➕Science 🇮🇷 - هوش مصنوعی و علم داده به فارسی
📩 ارتباط با ما
#Astra_model #Lean_prover
🚀 معرفی Palomar: پلتفرم راستی‌آزمایی اثبات‌های ریاضی
با افزایش تولید اثبات‌های ریاضی توسط مدل‌های هوش مصنوعی، تایید صحت این نتایج به چالشی بزرگ تبدیل شده است. برای حل این مشکل، Palomar به عنوان یک مرجع معتبر برای ریاضیاتِ فرمالیزه‌شده در زبان Lean راه‌اندازی شده است.
این ابتکار که با همکاری ICARM شکل گرفته، تضمین می‌کند که ادعاهای ریاضی با اثبات‌های نوع‌بندی‌شده مطابقت دارند. برای ثبت یک اثر در این سامانه، ارائه موارد زیر الزامی است:
- فایل Challenge: برای شرح خوانای نتایج در Lean.
- ماژول Solution: شامل اثبات کامل مسئله.
- فایل formalization.yaml: برای توصیف غیررسمی و ثبت متادیتای نتایج.
فرآیند تایید در دو مرحله انجام می‌شود. ابتدا ابزار Comparator صحت منطقی اثبات را بررسی کرده و سپس یک مدل زبانی، تطابق معنایی توصیف‌های متنی با اثبات‌های فرمال را تایید می‌کند. فرقی نمی‌کند اثبات توسط انسان انجام شده باشد یا هوش مصنوعی؛ آنچه اهمیت دارد دقت علمی است.
📚 مطالعه با جزئیات بیشتر
#Palomar #Lean_prover
با افزایش تولید اثبات‌های ریاضی توسط مدل‌های هوش مصنوعی، تایید صحت این نتایج به چالشی بزرگ تبدیل شده است. برای حل این مشکل، Palomar به عنوان یک مرجع معتبر برای ریاضیاتِ فرمالیزه‌شده در زبان Lean راه‌اندازی شده است.
این ابتکار که با همکاری ICARM شکل گرفته، تضمین می‌کند که ادعاهای ریاضی با اثبات‌های نوع‌بندی‌شده مطابقت دارند. برای ثبت یک اثر در این سامانه، ارائه موارد زیر الزامی است:
- فایل Challenge: برای شرح خوانای نتایج در Lean.
- ماژول Solution: شامل اثبات کامل مسئله.
- فایل formalization.yaml: برای توصیف غیررسمی و ثبت متادیتای نتایج.
فرآیند تایید در دو مرحله انجام می‌شود. ابتدا ابزار Comparator صحت منطقی اثبات را بررسی کرده و سپس یک مدل زبانی، تطابق معنایی توصیف‌های متنی با اثبات‌های فرمال را تایید می‌کند. فرقی نمی‌کند اثبات توسط انسان انجام شده باشد یا هوش مصنوعی؛ آنچه اهمیت دارد دقت علمی است.
📚 مطالعه با جزئیات بیشتر
📊 Data➕Science 🇮🇷 - هوش مصنوعی و علم داده به فارسی
📩 ارتباط با ما
#Palomar #Lean_prover