$10M एआई गणितीय ओलंपियाड पुरस्कार
एक नए $10M पुरस्कार, जो एक एआई सिस्टम को International Mathematical Olympiad में स्वर्ण पदक जीतने योग्य बनाने के लिए है, ने इस पर बहस छेड़ दी है कि मौजूदा मॉडल वास्तविक उच्च-स्तरीय गणितीय तर्क के कितने करीब हैं। टिप्पणीकार साधारण symbolic manipulation और रचनात्मक proof discovery के बीच अंतर करते हैं, इस लक्ष्य की तुलना Netflix Prize और Millennium Problems जैसी पिछली चुनौतियों से करते हैं, और यह देखते हैं कि क्या LLMs को formal proof assistants के साथ जोड़ने से यह अंतर पाटा जा सकता है। बातचीत में गणित को एक मानवीय पेशे के रूप में, open models के मूल्य, और क्या ऐसा सिस्टम सार्वजनिक रूप से जारी किया जाना चाहिए या एक बार के पुरस्कार के लिए निजी रखा जाना चाहिए, जैसे व्यापक प्रभाव भी शामिल हैं.
पुरस्कार की अवधारणा और लक्ष्य
- एक एआई सिस्टम के लिए $10M का पुरस्कार जो प्राकृतिक-भाषा के प्रश्नों और समाधानों (“informal to informal”) का उपयोग करके IMO स्वर्ण पदक जीतता है।
- कई लोग इसे Netflix Prize के समान मानते हैं: एक केंद्रित चुनौती जो कई टीमों को आकर्षित कर सकती है और एआई गणितीय तर्क में प्रगति को तेज कर सकती है।
- प्रायोजक खुलेपन पर ज़ोर देता है: पहला सार्वजनिक रूप से साझा मॉडल मुख्य पुरस्कार प्राप्त करता है।
व्यवहार्यता और समय-सीमाएँ
- आशावादी: LLM + reinforcement learning 1–5 वर्षों के भीतर IMO-स्वर्ण स्तर तक पहुँच सकता है; कुछ का तर्क है कि कला/छवि प्रगति दिखाती है कि कठिन दिखने वाले क्षेत्र भी तेज़ी से पलट सकते हैं।
- निराशावादी: मौजूदा प्रणालियाँ अभी भी स्कूल-स्तर के गणित और बुनियादी सटीक गणना में संघर्ष करती हैं; Millennium Prize problems या गहन शोध की बातें समय से पहले मानी जाती हैं।
- थ्रेड में उद्धृत Metaculus-जैसे पूर्वानुमान IMO-स्तर के प्रदर्शन के लिए लगभग 4–5 वर्षों के आसपास केंद्रित हैं, लेकिन प्रतिभागी उच्च अनिश्चितता पर ज़ोर देते हैं।
वर्तमान एआई गणितीय क्षमताएँ और सीमाएँ
- GPT‑4 ओलंपियाड-शैली के प्रश्नों को पार्स और पुनः कथित कर सकता है और कभी-कभी उपयोगी पैटर्न पहचान सकता है (जैसे, यह अनुमान लगाना कि एक नमूना IMO समस्या को केवल prime powers ही हल करते हैं)।
- हालांकि, यह अक्सर बुनियादी तार्किक या अंकगणितीय गलतियाँ करता है, तर्कहीन “proofs” लिखता है, या संकेत मिलने पर भी गैर-तुच्छ तर्कों को पूरा करने में विफल रहता है।
- विश्लेषण और प्रतियोगिता समस्याओं के उदाहरण दिखाते हैं कि यह पाठ्यपुस्तक-शैली की नकल कर सकता है, लेकिन अक्सर सुसंगत, अंत-से-अंत तक तर्क की कमी रहती है।
औपचारिक विधियाँ बनाम प्राकृतिक-भाषा तर्क
- एक अलग चल रहा प्रयास (IMO Grand Challenge) “formal to formal” Lean समस्याओं पर केंद्रित है; AI MO Prize मानव-शैली के कथनों और proofs को लक्षित करता है।
- कुछ का तर्क है कि पहले formal-to-formal हल करना सही रास्ता है; अन्य मानते हैं कि अनौपचारिक तर्क एक अलग, कठिन चुनौती है।
- वर्तमान theorem provers और ML-सहायता प्राप्त उपकरण formalized Olympiad समस्याओं के बहुत छोटे उपसमूह को ही हल कर पाते हैं।
गणित और करियर पर प्रभाव
- कुछ माता-पिता और छात्र चिंतित हैं कि एआई गणित-समाधानकर्ता गणित को एक मानवीय पेशे के रूप में कमजोर कर सकते हैं।
- अन्य जवाब देते हैं कि:
- अधिकांश गणित स्नातक पहले से ही pure math में काम नहीं करते।
- नए उपकरण mathematically प्रशिक्षित लोगों की मांग बढ़ा सकते हैं, जैसे compilers ने प्रोग्रामरों की मांग बढ़ाई।
- दिलचस्प समस्याएँ चुनने और परिणामों की व्याख्या करने के लिए मनुष्यों की अभी भी आवश्यकता होगी।
प्रोत्साहन, खुलापन, और आर्थिक मूल्य
- इस पर बहस कि $10M कितना मायने रखता है, जबकि:
- ऐसा मॉडल प्रशिक्षित करने की लागत इससे अधिक हो सकती है।
- एक सफल सिस्टम सैकड़ों मिलियन या उससे अधिक का हो सकता है।
- जवाब:
- पुरस्कार मुख्यतः अकादमिक और open researchers को प्रेरित करता है, न कि profit-maximizing firms को।
- कुछ लोग ऐसे मॉडल को foregone proprietary profits की परवाह किए बिना सार्वजनिक लाभ के लिए जारी करेंगे।
अन्य प्रस्ताव और विषयांतर
- blockchain-आधारित proof bounties बनाम सरल centralized/cryptographic विकल्पों के लिए विचार; कई लोग blockchains को अनावश्यक overhead मानते हैं।
- ऐसे सिस्टम को algorithmic trading में उपयोग करने के प्रश्न; आम सहमति है कि ओलंपियाड-शैली की क्षमता और trading edge काफी अलग हैं।
- कई लोग वेबसाइट की ध्यान भटकाने वाली animated background को खराब UX के रूप में नोट करते हैं।