خلاصه
- هوش مصنوعی داره تو حل مسائل پیچیده ریاضی، مثل المپیاد جهانی (IMO)، پیشرفت میکنه؛ اما مقایسهاش با انسانها پیچیدهتر از چیزیه که به نظر میاد.
- ترنس تائو، ریاضیدان معروف، میگه قوانین المپیاد اگه برای هوش مصنوعی تغییر کنه، نتایج خیلی فرق میکنه؛ مثلا اگه زمان بیشتر یا دسترسی به ابزار داشته باشن.
- مسئله تقلب و عدم شفافیت تو بنچمارکهای هوش مصنوعی نگرانیهای جدیای رو ایجاد کرده، چون شرکتها برای جذب سرمایه به موفقیت نیاز دارن.
- هوش مصنوعی تو کارهای روتین و محاسباتی عالیه، اما هنوز خلاقیت و توانایی یادگیری واقعی مثل انسان رو نداره و بیشتر شبیه یک «دانشجوی تحصیلات تکمیلی متوسط» عمل میکنه.
- ابزارهایی مثل Lean (زبان اثبات صوری) دارن روش تحقیق تو ریاضیات رو متحول میکنن و همکاریهای بزرگ مقیاس رو ممکن میکنن.
- تائو معتقده که باید روی معیارهای کمی مثل هزینه و منابع مورد نیاز هوش مصنوعی برای حل مسائل، تمرکز کنیم نه فقط دستاوردهای کیفی.
- مسائل ریاضیاتی مثل ناویر-استوکس و حدس کاکیا که تائو روشون کار کرده، نشون دهنده عمق و گستردگی تفکر ریاضیاتی هستن که ممکنه هوش مصنوعی هنوز بهش نرسیده باشه.
- برای سنجش واقعی هوش مصنوعی تو ریاضیات، به بنچمارکهای مستقل و شفاف نیاز داریم که متدولوژی و منابع مصرفی مدلها رو از قبل اعلام کنن.
شاید بهترین راه برای فهمیدن تواناییهای هوش مصنوعی امروزی این باشه که اون رو مثل یک انسان در نظر بگیریم. مثلا المپیاد جهانی ریاضی یا همون IMO رو در نظر بگیرید. توی این مسابقه، هر کشور یک تیم شش نفره از دانش اموزهای دبیرستانی میفرسته که یک سرپرست تیم هم دارن که معمولا یک ریاضیدان حرفهای هست. در طول دو روز، هر شرکت کننده هر روز چهار ساعت و نیم وقت داره تا سه تا مسئله خیلی سخت ریاضی رو فقط با قلم و کاغذ حل کنه. هیچ ارتباطی بین شرکت کنندهها یا با سرپرست تیم در این مدت مجاز نیست، هرچند میتونن از مراقبها برای شفافسازی صورت سوالها کمک بگیرن. سرپرست تیم موقع نمره دادن از دانش اموزها جلوی هیئت داوران IMO دفاع میکنه اما مستقیما در ازمون دخالتی نداره.
این المپیاد به عنوان یک معیار خیلی سخت برای سنجش موفقیت ریاضی یک دانش اموز دبیرستانی شناخته میشه. گرفتن مدال، مخصوصا مدال طلا یا نمره کامل، کار خیلی بزرگیه. امسال، کف نمره برای گرفتن طلا ۳۵ از ۴۲ بود که یعنی باید پنج تا از شش تا سوال رو کامل جواب میدادی. حتی جواب دادن کامل به یک سوال هم «تقدیرنامه» به همراه داره.
اما حالا بیایید ببینیم اگه قوانین المپیاد رو کمی تغییر بدیم، سطح سختی مسابقه چطور عوض میشه. فرض کنید این تغییرات رو اعمال کنیم:
- به دانش اموزها به جای چهار ساعت و نیم برای سه سوال، چند روز برای هر سوال وقت بدیم. (برای اینکه این استعاره رو کمی علمی-تخیلی کنیم، میشه سناریویی رو در نظر گرفت که دانش اموزها همون چهار ساعت و نیم رو وقت دارن، اما سرپرست تیم اونها رو توی یک دستگاه شتابدهنده زمان گرون و پرمصرف قرار میده که ماهها یا حتی سالها برای دانش اموزها در این مدت میگذره.)
- قبل از شروع ازمون، سرپرست تیم سوالها رو به شکلی بازنویسی کنه که دانش اموزها راحتتر باهاش کار کنن.
- سرپرست تیم به دانش اموزها دسترسی نامحدود به ماشینحساب، پکیجهای جبر کامپیوتری، دستیارهای اثبات صوری، کتابهای درسی، یا قابلیت جستجو در اینترنت بده.
- سرپرست تیم کاری کنه که هر شش دانش اموز تیم به طور همزمان روی یک مسئله کار کنن و در مورد پیشرفتهای جزیی و بنبستهایی که بهش خوردن با هم در ارتباط باشن.
- سرپرست تیم به دانش اموزها در جهت رویکردهای بهتر راهنمایی کنه و اگه یکی از دانش اموزها داشت بیش از حد روی مسیری که میدونه به احتمال زیاد به نتیجه نمیرسه وقت میذاشت، دخالت کنه.
- هر کدوم از شش دانش اموز تیم، راهحلهای خودشون رو به سرپرست تیم تحویل بدن و بعد سرپرست فقط «بهترین» راهحل برای هر سوال رو برای مسابقه انتخاب کنه و بقیه رو دور بریزه.
- اگه هیچکدوم از دانش اموزهای تیم به یک راهحل رضایتبخش نرسیدن، سرپرست تیم اصلا هیچ راهحلی رو ارسال نکنه و بیسروصدا از مسابقه انصراف بده، بدون اینکه اصلا شرکت کردنشون جایی ثبت بشه.
در تمام این حالتها، راهحلهای ارسالی از نظر فنی هنوز توسط شرکتکنندههای دبیرستانی تولید شدن، نه سرپرست تیم. با این حال، درصد موفقیت گزارش شده دانش اموزها در مسابقه میتونه با چنین تغییراتی در قوانین به شدت تحت تاثیر قرار بگیره. یک دانش اموز یا تیمی از دانش اموزها که شاید در شرایط استاندارد ازمون حتی همیشه به مدال برنز هم نمیرسیدن، ممکنه تحت بعضی از این قوانین تغییر یافته، به عملکرد مطمئن مدال طلا برسن.
بنابراین، وقتی یک متدولوژی ازمون کنترل شده وجود نداره که توسط خود تیمهای رقیب انتخاب نشده باشه، باید در مورد مقایسههای بیش از حد سادهانگارانه و مستقیم بین عملکرد مدلهای مختلف هوش مصنوعی در مسابقاتی مثل IMO، یا بین این مدلها و شرکتکنندههای انسانی، محتاط بود. در همین راستا، ترنس تائو، یکی از بزرگترین ریاضیدانان زنده دنیا، اعلام کرده که در مورد نتایج عملکرد هوش مصنوعی در مسابقاتی که متدولوژی اونها قبل از مسابقه فاش نشده، نظری نخواهد داد.
هوش مصنوعی، المپیاد و معنای واقعی «استدلال»
این دیدگاهها بحثهای زیادی رو به وجود اورده. بعضیها معتقدن که مقایسه هوش مصنوعی با شرکتکنندههای انسانی هدف اصلی این تلاشها نبوده، بلکه هدف مقایسه با پیشرفتهترین مدلهای قبلی هوش مصنوعی بوده. در بعضی گزارشها، تنها جایی که به انسانها اشاره میشه اینه که گفته میشه هوش مصنوعی از همون قوانین پیروی کرده. یک نفر در این مورد میگه که مدل OpenAI در زبان طبیعی کار کرده (یعنی اثباتها رو به زبان طبیعی خروجی میده) و تحت همون قوانین انسانها بوده (مثلا دو جلسه ۴.۵ ساعته، بدون ابزار یا اینترنت). پس هیچ بازخورد خارجی به جز اینکه خود مدل خودش رو تایید کنه وجود نداشته. تیم OpenAI هم به بعضی از این نکات اشاره کرده و گفته: «تحت همون قوانین شرکتکنندههای انسانی: دو جلسه ازمون ۴.۵ ساعته، بدون ابزار یا اینترنت، خوندن صورت سوالهای رسمی و نوشتن اثباتها به زبان طبیعی.» البته یک نکتهای که مطرح میشه اینه که هیچ تایید مستقلی از دیتاسنتر اونها وجود نداره و این نگرانی وجود داره که ممکنه دروغ بگن، چیزی که از نظر تاریخی مشوق تقلب اکادمیک بوده.
یک نفر دیگه استدلال میکنه که هر کسی که برای المپیاد اماده میشه، دقیقا مثل مدلهای زبان بزرگ (LLM) اماده میشه: اطلاعات واقعی رو یاد میگیری و اطلاعات رو برای حل یک پازل جدید ترکیب میکنی. پس جدول امتیازات یک راه منصفانه و معتبر برای اندازهگیری عملکرد LLM هست. از طرفی، یک مشکل بزرگتر هم مطرح میشه: مسابقات (ریاضی، برنامهنویسی، بازی) برای اندازهگیری چیزی طراحی شدن که برای انسانها سخته، اما ابزارها اونقدر متفاوت از ما کار میکنن که موفقیت برای یک ابزار لزوما معنیدار نیست. شرکتهای هوش مصنوعی مدتهاست که چالش بزرگ IMO رو نشانهای برای رسیدن به «هوش مصنوعی عمومی» (AGI) میدونن، اما مهم نیست یک ماشین از چه قوانینی پیروی کنه، دلیلی وجود نداره که باور کنیم موفقیت برای یک ماشین با تواناییهای ریاضیاتی یا «استدلال» گستردهتر، اونطور که در مورد شرکتکنندههای انسانی صدق میکنه، ارتباط داشته باشه.
یک نکته خوب در مورد بنچمارکهای مسابقهای اینه که اندازهگیری اونها خیلی راحته. اما اندازهگیری سوال بسیار مفیدترِ «این ابزارها چقدر میتونن به انسانهایی که از اونها برای ریاضی یا برنامهنویسی استفاده میکنن کمک کنن؟» خیلی سختتره. در یک مهمانی در سیلیکون ولی در سال ۲۰۲۲، دوستانی از OpenAI از تائو پرسیدن که ایا فکر میکنه AGI به زودی اتفاق میفته، و او جواب داده که این سوال پایههای محکمی نداره. بعد ازش در مورد چالش بزرگ IMO پرسیدن و او گفته که بله، به نظر میرسه در چند سال اینده قابل دستیابی باشه، فقط نمیفهمه چرا این موضوع باید نشونهای از چیزی گستردهتر مثل «AGGI» باشه. ازمونها و مسابقاتی که برای انسانها ساخته شدن، همیشه چیزهای جالبی رو در مورد ماشینها اندازهگیری نمیکنن.
آیا مسابقات ریاضی از مسیر اصلی خارج شدهاند؟
یک دیدگاه انتقادی هم وجود داره که میگه این حجم از تلاش، پول و اعتبار که صرف مسابقات ریاضی و علمی میشه، تقریبا هیچ تاثیری روی حل مسائل دنیای واقعی نداره. انگار یک نسل کامل از نوابغ راهی پیدا کردن تا برای شرکت در ازمونهای دانشگاهی پول بگیرن و امتیازات اجتماعی شدیدی نصیب کسانی میشه که در این چالشهای کاملا ساختگی خوب عمل میکنن. در دهههای ۱۹۷۰ و ۱۹۸۰ این درک وجود داشت که عملکرد فوقالعاده در ازمونها لزوما چیزی در مورد توانایی فرد برای حل مشکلات دنیای واقعی نمیگه. اما حالا با دادن جایزههای نقدی بزرگ به کسانی که در ازمونها شرکت میکنن، این وضعیت بهتر نشده. الان ممکنه یک نفر تمام دوران حرفهای خودش رو صرف شرکت در ازمونهای سطح بالا کنه و این به نظر نامتعادل میرسه.
از طرفی، دنیای اکادمیک داره انحصار خودش رو بر فرایند اثبات از دست میده. اعتبار اثبات در حال غیرمتمرکز شدنه، نه از طریق بحثهای کنترل شده تحت یک هستیشناسی، بلکه از طریق دستیارهای اثبات و LLMها که میتونن به طور مستقل استدلالهای صوری بسازن و تایید کنن. دیگه خبری از کنترل، بازبینی همتا، یا توسل به شهود نیست. یا کامپایل میشه یا نمیشه. چه ترنس تائو بفهمدش یا نه.
مسئله اعتماد و تقلب در دنیای هوش مصنوعی
تاکید بر عدم دسترسی به اینترنت کمی بیمورد به نظر میرسه. اگه یک شرکت بخواد تقلب کنه، به سادگی میتونه از سوالهای مسابقه در دادههای اموزشی خودش استفاده کنه. ممکنه بگید اینها سوالهای IMO 2025 هستن و مسابقه تازه برگزار شده، پس نمیتونستن روی اونها اموزش ببینن! اما المپیاد جهانی ریاضی بر پایه اعتماد زیادی کار میکنه. فرایند انتخاب سوال شامل اینه که کشورهای شرکتکننده سوال پیشنهاد میدن. یک کمیته که احتمالا اعضایی از کشورهای غالب و شاید نمایندهای از کشور میزبان داره، سوالها رو انتخاب میکنه و احتمالا کارشون رو به زبان انگلیسی انجام میدن.
بعد سوالها باید به همه زبانها ترجمه بشن و این فقط یک ترجمه ساده نیست، بلکه باید مطمئن شد که نمادگذاری برای هر کشور استاندارده. مثلا در مجارستان، مرکز ارتفاعی معمولا با M نشون داده میشه در حالی که در انگلیسی با H. نکته اینه که سوالها قبل از مسابقه برای تعداد زیادی از افراد شناخته شده هستن. یک نفر که همزمان با ترنس تائو در المپیاد شرکت کرده بود میگه که خیلی زود بعد از مسابقه، کتابی رو دیده که شامل تمام سوالهای پیشنهادی کشورها بوده. این کتاب باید خیلی زودتر برای چاپ اماده شده باشه.
برای مثال، در هیئتهای AIME و AMC که مسابقات ریاضی در امریکا رو برگزار میکنن، بررسی نسخههای نهایی AMC 2025 که برای نوامبر برنامهریزی شده، انجام شده. پیشنهادهای سوال AIME 2027 هم باید تا جولای ۲۰۲۵ تحویل داده میشدن. و این برای یک مسابقه است که عمدتا در یک کشور و به یک زبان برگزار میشه.
با توجه به اینکه:
۱. پول زیادی برای شرکتهای هوش مصنوعی در میونه که بر اساس تصور پیشرفت برای جذب سرمایه کار میکنن و نه بر اساس درامد یا سود.
۲. سابقه طولانی در دستکاری بنچمارکها در حوزههای مختلف وجود داره.
بنابراین، بهتره منتظر یک مدل افلاین باشیم که این کارها رو انجام بده و توسط یک سازمان کاملا مستقل تایید بشه. شرکتهای هوش مصنوعی صادق به زودی برای ایجاد یک رقابت مستقل برای حلکنندههای ریاضی هوش مصنوعی فشار خواهند اورد (و بودجهاش رو تامین خواهند کرد). این باید طوری کار کنه که شرکتها مدل خودشون رو به سازمانی تحویل بدن که اونها رو روی سوالهایی که به طور مستقل تهیه شدن، اجرا کنه.
بعضیها در مورد تواناییهای استدلال LLMها کمی شک دارن، اما ذهن بازی دارن. بالاخره همه مسائل فقط مسائل جستجو هستن. استفاده از هوش مصنوعی مولد برای ایجاد استدلالها و تعاریف جدید پتانسیل زیادی داره. اما در مدلهای در دسترس عموم، توانایی تشخیص یک استدلال درست یا انجام بررسی خودکار اثبات دیده نمیشه.
پیشرفتهای اخیر و اینده پیش رو
سال گذشته، طبق گفته گوگل، یک مدل زبان با کمک ترجمه انسانی، زمان فکر کردن اضافه و دسترسی به Lean (یک زبان اثبات صوری) نمرهای معادل مدال نقره، در استانه طلا، کسب کرد. AlphaProof در زمان خودش یک جهش در توانایی ریاضی بود، اما نه یک جهش خیلی بزرگ. امسال، طبق گفته OpenAI، مجموعهای از مدلهای زبان بدون کمک در ترجمه یا تایید، و با محدودیتهای زمانی سخت، تونستن جوابهایی تولید کنن که نمرهای معادل مدال طلا، در استانه نقره، گرفتن. این هم یک جهش محسوب میشه، اما برای یک سال تحقیق، جهش خیلی بزرگی به نظر نمیرسه.
بنابراین، این باورپذیره که نرمافزاری وجود داره که میتونه ایدههایی از چندین حوزه رو به روشی خلاقانه و به اندازه کافی دقیق ترکیب کنه تا نمرههای بالای IMO بگیره. البته، این نرمافزار در دسترس عموم نیست، احتمالا برای اجرا به یک کلاستر عظیم نیاز داره و نمیتونه یاد بگیره. اما دلیلی وجود داره که باور کنیم اونها کاری که برنامهشون انجام داده رو اشتباه توصیف نکردن. شواهد نهایی سال اینده مشخص میشه، وقتی که سیستمهای خودکار با مستندات خوب در زمان IMO اجرا بشن و احتمالا چندین مدل نمرههای تقریبا کاملی بگیرن. این دیدگاه به یک دانشجوی ریاضی کمک میکنه تا با بحران هویتی که گاهی اوقات با دیدن اینکه هوش مصنوعی میتونه اساسا تمام کارهای پایاننامهاش رو تکرار کنه، کنار بیاد. ابزارها و منابعی که یک انسان داره اساسا با چیزی که هوش مصنوعی داره متفاوته، پس مهمه که در چنین مقایسههایی محتاط باشیم و بپذیریم که اطلاعات کافی برای یک مقایسه خیلی عینی نداریم.
مغز متفکری به نام ترنس تائو
ترنس تائو، که اغلب به عنوان «موتزارت ریاضی» شناخته میشه، به طور گسترده به عنوان یکی از بزرگترین ریاضیدانان تاریخ در نظر گرفته میشه. او مدال فیلدز و جایزه پیشرفت در ریاضیات رو برده و کارهای پیشگامانهای در طیف شگفتانگیزی از زمینههای ریاضیات و فیزیک انجام داده. یک شوخی در جامعه ریاضی وجود داره که میگه اگه نمیتونی یک مسئله ریاضی رو حل کنی، فقط کافیه تائو رو به اون مسئله علاقهمند کنی. فروتنی و مهربانی او هم زبانزد خاص و عامه.
اولین مسئله سخت در سطح تحقیقاتی که تائو باهاش روبرو شد، مسئله «کاکیا» بود. این مسئله تاریخی از یک پازل توسط ریاضیدان ژاپنی سویچی کاکیا در حدود سال ۱۹۱۸ میاد. پازل اینه: شما یک سوزن روی صفحه دارید و میخواید یک دور U شکل بزنید، یعنی سوزن رو بچرخونید، اما میخواید این کار رو در کمترین فضای ممکن انجام بدید. چقدر مساحت برای چرخوندن سوزن لازمه؟ بسیکوویچ نشون داد که در واقع میشه سوزن رو با مساحت هر چقدر کم که بخواید بچرخونید. سوال بعدی این بود که در سه بعد چه اتفاقی میفته؟ فرض کنید تلسکوپ فضایی هابل یک لوله در فضاست و میخواید هر ستارهای در جهان رو رصد کنید. برای چرخوندن تلسکوپ و دیدن هر جهت در اسمان، به چقدر حجم نیاز دارید؟ این مسئله به ظاهر یک پازل ساده است، اما به طور شگفتانگیزی به بسیاری از مسائل در معادلات دیفرانسیل با مشتقات جزیی، نظریه اعداد، هندسه و ترکیبیات مرتبطه.
معادلات ناویر-استوکس و خطر «منفجر شدن»
این مسئله به پدیدهای به نام «تمرکز موج» مرتبطه که میتونه باعث «انفجار» (blowup) بشه، یعنی جایی که دامنه موجها اونقدر زیاد میشه که قوانین فیزیکی که بر اونها حاکمه دیگه معادلات موج نیستن، بلکه چیزی پیچیدهتر و غیرخطی هستن. در فیزیک ریاضی، ما خیلی به این اهمیت میدیم که ایا معادلات خاصی پایدار هستن یا نه. یک مسئله حل نشده معروف به نام «مسئله نظم ناویر-استوکس» وجود داره. معادلات ناویر-استوکس، معادلاتی هستن که جریان سیال برای سیالات تراکمناپذیر مثل اب رو کنترل میکنن. سوال اینه: اگه با یک میدان سرعت صاف از اب شروع کنید، ایا ممکنه اونقدر متمرکز بشه که سرعت در یک نقطه بینهایت بشه؟ این پدیده «تکینگی» (singularity) نامیده میشه. ما این رو در زندگی واقعی نمیبینیم. اگه اب رو در وان حمام به هم بزنید، روی شما منفجر نمیشه. اما به طور بالقوه ممکنه.
این مسئله یکی از هفت مسئله جایزه هزاره بنیاد کلی هست که یک جایزه یک میلیون دلاری برای حل هر کدوم از اونها تعیین کرده. از این هفت مسئله، فقط یکی از اونها حل شده: حدس پوانکاره. تائو در سال ۲۰۱۶ مقالهای با عنوان «انفجار در زمان متناهی برای یک معادله میانگین گرفته شده سه بعدی ناویر-استوکس» منتشر کرد. او میگه: «این به معنای واقعی کلمه سوال یک میلیون دلاریه.» این چیزیه که ریاضیدانها رو از بقیه متمایز میکنه. اگه چیزی ۹۹.۹۹ درصد مواقع درست باشه، برای اکثر کارها کافیه. اما ریاضیدانها از معدود افرادی هستن که واقعا براشون مهمه که ایا ۱۰۰ درصد همه شرایط پوشش داده میشه یا نه.
ایده کامپیوتر مایع
تائو برای نزدیک شدن به حل این مسئله، ایده جالبی رو مطرح کرد: ساخت یک نوع «کامپیوتر مایع» و نشون دادن اینکه مسئله توقف از نظریه محاسبات، پیامدهایی برای دینامیک سیالات داره. او متوجه شد که برای مهندسی کردن یک انفجار در مدل ساده شده خودش، باید یک تاخیر در سیستم برنامهریزی کنه. او این کار رو با ساختن یک غیرخطی بودن پیچیده انجام داد که مثل یک مدار الکترونیکی ساخته شده بود. او میگه که همسرش که مهندس برق بوده، در این مورد بهش الهام داده.
او فهمید که اگه بشه همین کار رو برای معادلات واقعی اب انجام داد، یعنی اگه معادلات اب از یک «محاسبه» پشتیبانی کنن، میشه یک انفجار واقعی ساخت. تصور کنید به جای الکترونها، پالسهایی از اب با سرعت مشخص حرکت میکنن و با هم برخورد میکنن و چیزی شبیه گیتهای منطقی AND یا OR میسازن. با این کار میشه یک ماشین تورینگ ساخت که کاملا از اب ساخته شده. اگه بشه یک ماشین سیال ساخت که هدفش در زندگی این باشه که یک نسخه کوچکتر از خودش رو بسازه و بعد تمام انرژیش رو به اون نسخه کوچکتر منتقل کنه و خاموش بشه، این فرایند میتونه به طور مکرر تکرار بشه و در نهایت یک انفجار در زمان متناهی برای معادلات واقعی ناویر-استوکس ایجاد کنه.
این ایده از کارهای قبلی روی «اتوماتای سلولی» مثل «بازی زندگی» کانوی الهام گرفته شده. در بازی زندگی، با قوانین محلی بسیار ساده، ساختارهای پیچیده و پویایی مثل «گلایدر» و حتی ماشینهای خودتکثیرشونده به وجود میان. تائو میدونست که این کارها انجام شده و این بهش الهام داد که همین ایده رو برای ناویر-استوکس پیشنهاد بده.
هوش مصنوعی، Lean و اینده ریاضیات
تائو به شدت به استفاده از ابزارهای کامپیوتری در ریاضیات علاقهمنده. او در مورد زبان اثبات صوری Lean صحبت میکنه و اینکه چطور میتونه به عنوان یک دستیار اثبات کمک کنه. Lean یک زبان کامپیوتریه که علاوه بر اجرای کد، میتونه «گواهی» یا اثبات برای محاسباتش تولید کنه. نوشتن اثبات در Lean مثل توضیح دادن یک اثبات به یک همکار فوقالعاده دقیق و وسواسیه که هر قدم شما رو زیر سوال میبره. در حال حاضر، تائو تخمین میزنه که زمان و تلاش لازم برای صوری کردن یک اثبات حدود ۱۰ برابر زمان لازم برای نوشتن دستی اونه. این کار شدنیه، اما ازاردهنده است.
با این حال، در بعضی موارد کار کردن به صورت صوری خوشایندتره. مثلا اگه در یک اثبات یک ثابت عددی مثل ۱۲ وجود داشته باشه و بعدا کسی راهی برای بهبود اون به ۱۱ پیدا کنه، در حالت دستی باید خط به خط اثبات رو دوباره چک کرد. اما با Lean، کافیه عدد ۱۲ رو به ۱۱ تغییر بدید و کامپایلر دقیقا به شما میگه کدوم خطوط دیگه کار نمیکنن و فقط اونها رو باید اصلاح کنید.
Lean همچنین همکاری روی اثباتها رو در مقیاس خیلی جزیی ممکن میکنه. یک نفر میتونه روی بخشی از اثبات گیر کنه و دقیقا همون چند خط کد مشکلدار رو با بقیه به اشتراک بذاره و چون تمام زمینه و بستر کار مشخصه، بقیه میتونن به راحتی کمک کنن. تائو میگه: «به خاطر Lean، من میتونم با دهها نفر در سراسر جهان همکاری کنم که بیشترشون رو هرگز شخصا ملاقات نکردم… Lean به من یک گواهی اعتماد میده تا بتونم ریاضیات بدون نیاز به اعتماد انجام بدم.»
او یک پروژه به نام «پروژه نظریههای معادلهای» رو شروع کرده که در اون حدود ۲۲ میلیون گزاره در جبر مجرد بررسی شدن. این پروژه با حدود ۵۰ همکار انجام شد که در ریاضیات عدد بسیار بزرگی محسوب میشه. این پروژه نشون میده که چطور میشه ریاضیات رو به صورت جمعسپاری شده و در مقیاس بزرگ انجام داد، کاری که قبلا ممکن نبود.
دیدگاه تائو در مورد پیشرفتهای هوش مصنوعی
تائو در مورد پیشرفتهای اخیر مثل AlphaProof دیپمایند یا مدل o1 OpenAI نظرات جالبی داره. او میگه که رویکرد فعلی برای حل مسائل سطح بالای ریاضی با هوش مصنوعی، مقیاسپذیر نیست. صرف کردن سه روز از زمان سرور گوگل برای حل یک مسئله المپیاد دبیرستان، با توجه به افزایش نمایی پیچیدگی مسائل، یک چشمانداز عملی نیست. او پیشبینی کرده بود که تا سال ۲۰۲۶، همکاریهای ریاضی با هوش مصنوعی وجود خواهد داشت، نه در سطح برنده شدن مدال فیلدز، بلکه در سطح مقالات تحقیقاتی واقعی. این اتفاق تا حدودی افتاده.
او در اولین تجربهاش با ChatGPT، بهش مسائل سخت ریاضی داد و نتایج خیلی احمقانهای گرفت. متن منسجم و انگلیسی بود، کلمات درست رو ذکر میکرد، اما عمق خیلی کمی داشت. او مدل جدید o1 رو به یک «دانشجوی تحصیلات تکمیلی متوسط، اما نه کاملا بیکفایت» تشبیه کرد. این توصیف خیلی وایرال شد، اما منظور او این بود که این ابزار در نقش یک دستیار پژوهشی اینطور عمل میکنه. یک پروژه تحقیقاتی مراحل خستهکننده زیادی داره و هوش مصنوعی میتونه در انجام محاسبات دستی کمک کنه.
تائو میگه: «با o1، تا حدودی میشه این کار رو کرد. من یک مسئله که بلد بودم رو بهش دادم و سعی کردم راهنماییش کنم. اول یک راهنمایی بهش دادم، اون راهنمایی رو نادیده گرفت و کار دیگهای کرد که جواب نداد. وقتی بهش توضیح دادم، عذرخواهی کرد و گفت باشه، به روش تو انجام میدم. بعد دستورالعملهای من رو نسبتا خوب انجام داد، اما دوباره گیر کرد و من مجبور شدم دوباره تصحیحش کنم. مدل هرگز قدمهای هوشمندانه رو کشف نکرد. میتونست کارهای روتین رو انجام بده، اما خیلی بیتخیل بود.»
یک تفاوت کلیدی بین دانشجوهای تحصیلات تکمیلی و هوش مصنوعی اینه که دانشجوها یاد میگیرن. اما مدلهای فعلی ایستا هستن. بازخوردی که به GPT-4 داده میشه ممکنه به عنوان ۰.۰۰۰۰۱ درصد از دادههای اموزشی GPT-5 استفاده بشه، اما این واقعا مثل یادگیری یک دانشجو نیست.
از «واو» تا «چقدر؟»: بلوغ فناوری هوش مصنوعی
تائو معتقده که وقتی یک فناوری بالغ میشه، تمرکز از دستاوردهای کیفی (مثل اینکه چه کسی اولین بار به یک هدف رسید) به سمت اندازهگیریهای کمی (مثل اینکه چقدر منابع و تخصص برای انجام یک کار لازمه و چقدر تاثیر زیستمحیطی و خطر ایجاد میکنه) تغییر میکنه. این یک گذار ضروری برای رسوندن فناوری از مرحله «اثبات مفهوم» به «پذیرش انبوه» است.
او پرواز رو مثال میزنه. در روزهای اولیه، تاکید روی نقاط عطفی مثل اولین پرواز کنترلشده برادران رایت در ۱۹۰۳ یا اولین پرواز بدون توقف تکنفره لیندبرگ بر فراز اقیانوس اطلس در ۱۹۲۷ بود. اما دههها توسعه خستهکننده اما مهم در هوانوردی جت لازم بود تا هزینه سفر هوایی کاهش پیدا کنه و همزمان استانداردهای ایمنی بهبود پیدا کنه تا جایی که برای یک فرد طبقه متوسط در یک کشور توسعه یافته هم ایمن و هم مقرون به صرفه بشه. در مقابل، برنامههای اپولو در سال ۱۹۶۹ به نقطه عطف ماموریتهای سرنشیندار به ماه رسیدن، اما با هزینهای سرسامآور. برخلاف هوانوردی، پیشرفت قابل توجهی در کاهش هزینه وجود نداشته. برنامه ارتمیس ناسا تخمین زده میشه که برای انجام یک ماموریت مشابه به دهها میلیارد دلار نیاز داره.
به همین ترتیب، در اینده هم به احتمال زیاد مدلهای هوش مصنوعی که منابع بیشتری مصرف میکنن، قویتر از مدلهای ارزانتر خواهند بود. بنابراین، برای هر دو نوع ابزار هوش مصنوعی در کاربردها جا وجود داره. در پروژه نظریههای معادلهای، اکثر ۲۲ میلیون گزاره با تکنیکهای خیلی ساده brute-force (مثل شمارش روی همه ماگماهای کوچک) ثابت شدن. بیشتر باقیماندهها توسط اثباتکنندههای قضیه خودکار با قدرت متوسط حل شدن. از موارد باقیمونده، بیشترشون توسط شرکتکنندههای انسانی حل شدن و چند گزاره نهایی به تلاشهای هماهنگ چندین انسان و ابزارهای ATP نیاز داشتن. تائو انتظار داره پروژههای بزرگ مشابه در اینده هم مسیر مشابهی داشته باشن: هوش مصنوعی «ارزان» برای انجام بخش عمده پروژه استفاده میشه و هوش مصنوعی «گران» برای مراحل نهایی و با همکاری انسانها ذخیره میشه.
در اینده، بنچمارکها و مسابقات استاندارد، که در اونها استفاده از منابع و متدولوژی باید از قبل فاش بشه، برای اندازهگیری دقیق پیشرفت کمی اهمیت بیشتری پیدا میکنن. وضعیت فعلی که هر کس دستاورد خودش رو گزارش میده، ممکنه برای فاز کیفی توسعه فناوری تا حدودی قابل قبول باشه، اما با ورود هوش مصنوعی به فاز پذیرش گسترده، باید جای خودش رو به ارزیابی شفاف و مبتنی بر بنچمارک بده. همانطور که نقاط عطف اولیه پرواز جای خودشون رو به معیارهایی مثل هزینه به ازای هر صندلی-مایل یا نرخ تصادف دادن، هوش مصنوعی هم باید به سمت اندازهگیری قابلیت اطمینان و کارایی به ازای هر واحد کار شناختی حرکت کنه.
اکوسیستم علمی و تهدیدهای پیش رو
تائو که در استرالیا بزرگ شده اما تحصیلات تکمیلی و زندگی حرفهای خودش رو در امریکا گذرونده، عمیقا به اکوسیستم تحقیقاتی این کشور باور داره. او میگه: «من از نزدیک دیدم که چطور سرمایهگذاری پایدار فدرال—که از طریق اژانسهایی مثل بنیاد ملی علوم (NSF) هدایت میشه—به همکاریهایی که دانشگاهها، ازمایشگاههای دولتی و صنعت رو به هم وصل میکنن، قدرت میده.» تحقیقات خود او در موسسه ریاضیات محض و کاربردی UCLA (IPAM) به الگوریتمهایی منجر شد که حالا زمان اسکن MRI رو تا ۱۰ برابر کاهش میدن.
او نسبت به چیزی که «حمله همهجانبه به زیرساختهای علمی» در دولت ترامپ میدونه، ابراز نگرانی میکنه. او در مقالهای مینویسه: «کمکهزینهها در میانه پروژه لغو شدن، فلوشیپها برای نسل بعدی محققان از بین رفتن، و موسسات با بودجه فدرال از منابعی که برای فعالیت نیاز دارن محروم شدن.» او توضیح میده که این تصمیمها نتیجه بازبینی علمی یا بحث کنگره نیستن، بلکه دستورالعملهای سیاسی ناگهانی هستن که هنجارهای دیرینه رو دور میزنن، پروژههای چند ساله رو مختل میکنن و استقلال اکوسیستم تحقیقاتی رو از بین میبرن.
کمکهزینه تحقیقاتی شخصی او که برای حمایت از تحقیقات و سفرهای دانشجویان تحصیلات تکمیلیاش استفاده میشد، در یکی از این اقدامات به حالت تعلیق دراومد. اما تهدید بزرگتر برای IPAM بود که کل دسترسیاش به بودجه ناگهان قطع شد. به گفته تائو، این اقدامات یک تغییر سیاست عادی نیست، بلکه «یک برچیدن عمدی نهادها، بودجه و ازادیهایی است که علم امریکا را برای نسلها حفظ کرده است.» او معتقده که در چنین محیطی، «تجمل عدم مشارکت دیگر یک گزینه عملی نیست.»
ریاضیات، عمیق و گسترده
تائو به خاطر تواناییاش در کار کردن هم عمیق و هم گسترده در ریاضیات شهرت داره. او خودش رو بیشتر یک «روباه» میدونه تا یک «جوجهتیغی». (روباه چیزهای زیادی رو کمی میدونه، اما جوجهتیغی یک چیز رو خیلی خیلی خوب میدونه). او میگه: «من اربیتراژ رو دوست دارم. یاد گرفتن اینکه یک رشته چطور کار میکنه، یاد گرفتن ترفندهای اون چرخ، و بعد رفتن به رشته دیگهای که مردم فکر نمیکنن مرتبطه، اما من میتونم ترفندها رو تطبیق بدم.»
او معتقده که انسانها یک مرکز ریاضی ذاتی در مغز ندارن، بلکه بخشهای دیگه مغز مثل مرکز بینایی یا زبان رو برای انجام ریاضیات بازتنظیم میکنن. برای همین، سبکهای فکری متفاوتی در بین ریاضیدانان وجود داره.
وقتی از او در مورد سختترین مسائل ریاضی مثل حدس ریمان یا حدس اعداد اول دوقلو سوال میشه، او میگه که مسائلی مثل ریمان اونقدر دور از دسترس هستن که حتی با فعال کردن تمام «کدهای تقلب» که بلده، راهی برای رسیدن از نقطه A به B وجود نداره. او معتقده که این مسائل به یک پیشرفت بزرگ در حوزه دیگهای از ریاضیات نیاز دارن. با این حال، او پیشرفتهای چشمگیری در مورد حدس اعداد اول دوقلو داشته و نشون داده که بینهایت جفت عدد اول وجود دارن که فاصلهشون حداکثر ۲۴۶ هست.
او در مورد حدس کولاتز هم که به ظاهر ساده اما به شدت سخته، کارهایی انجام داده. این حدس میگه که اگه یک فرایند ساده تکراری رو روی هر عدد طبیعی شروع کنید (اگه زوج بود تقسیم بر دو، اگه فرد بود ضرب در سه به علاوه یک)، در نهایت همیشه به عدد یک میرسید. تائو ثابت کرده که به صورت اماری، ۹۹ درصد همه ورودیها به سمت اعداد خیلی کوچکتر از عدد اولیه حرکت میکنن. اما مشکل اینه که همیشه یک رویداد استثنایی وجود داره که نمیشه اون رو با روشهای اماری رد کرد. ممکنه یک عدد خاص وجود داشته باشه که به جای پایین اومدن، تا بینهایت بالا بره.
منابع
- [۲] Transcript for Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI | Lex Fridman Podcast #472 – Lex Fridman
- [۴] Terence Tao: “But consider what happens to t…” – Mathstodon
- [۶] As Trump funding cuts hit even maths prodigy Terence Tao, China remains a talent magnet | South China Morning Post
- [۸] I’m an award-winning mathematician. Trump just cut my funding.
دیدگاهتان را بنویسید