- Google DeepMind के Gemini Deep Think मॉडल ने 2025 के अंतरराष्ट्रीय गणित ओलंपियाड (IMO) में गोल्ड मेडल मानक स्कोर (35 अंक) हासिल किया
- इस मॉडल ने 6 में से 5 प्रश्न पूरी तरह हल किए, और IMO की आधिकारिक जजिंग टीम ने इसकी स्पष्ट और सटीक गणितीय व्याख्या को मान्यता दी
- पिछले साल AlphaProof·AlphaGeometry 2 के सिल्वर मेडल स्तर (28 अंक) से बड़ी छलांग लगाते हुए, इसने प्राकृतिक भाषा में औपचारिक प्रश्नों को समझा और 4.5 घंटे के भीतर इंसानों की तरह प्रूफ पूरा किया
- Deep Think मोड parallel thinking और नवीनतम reinforcement learning लागू करता है, जिससे कई समाधान एक साथ खोजे और संयोजित किए जा सकते हैं, और यह IMO-स्टाइल प्रश्नों के समाधान के लिए अनुकूलित है
- Google आगे गणितज्ञों के साथ सहयोग का विस्तार करने और गणितीय reasoning व औपचारिक verification क्षमता को जोड़ने वाली अगली पीढ़ी की AGI के विकास की दिशा में बढ़ने की योजना बना रहा है
Breakthrough Performance at IMO 2025 with Gemini Deep Think
- Google DeepMind का Gemini Deep Think 2025 अंतरराष्ट्रीय गणित ओलंपियाड (IMO) में कुल 35 अंक (6 में से 5 प्रश्नों का पूर्ण समाधान) प्राप्त कर, आधिकारिक तौर पर गोल्ड मेडल मानक तक पहुंच गया
- IMO की आधिकारिक जजिंग टीम ने इसकी स्पष्टता, सटीकता और आसानी से समझ आने वाली व्याख्या की सराहना की, और IMO अध्यक्ष Prof. Dr. Gregor Dolinar ने आधिकारिक बयान में कहा कि "Google DeepMind ने 35 अंकों का गोल्ड मेडल स्कोर हासिल किया है"
- पिछले साल AlphaGeometry·AlphaProof में विशेषज्ञों को प्रश्नों का प्राकृतिक भाषा से डोमेन-विशिष्ट भाषा (Lean आदि) में अनुवाद करना पड़ता था, और गणना में दो दिन से अधिक समय लगता था। इस साल Gemini ने प्रश्न समझने से लेकर प्रूफ लिखने तक की पूरी प्रक्रिया प्राकृतिक भाषा के आधार पर, IMO प्रतियोगिता समय (4.5 घंटे) के भीतर पूरी की
Making the most of Deep Think mode
- Gemini Deep Think एक उन्नत reasoning मोड है जिसमें parallel thinking जैसी नवीनतम शोध तकनीकों का उपयोग किया गया है, और यह कई समाधान-पथों को एक साथ खोजकर सबसे उपयुक्त समाधान निकालता है
- मॉडल को जटिल गणितीय समस्याओं के समाधान के लिए reinforcement learning तकनीकों और विविध IMO-स्टाइल प्रूफ डेटा पर प्रशिक्षित किया गया, और IMO प्रश्नों के एप्रोच से जुड़े सामान्य hints और tips भी अतिरिक्त रूप से दिए गए
- इस Deep Think मॉडल का test version पहले कुछ विश्वसनीय गणितज्ञों और विशेषज्ञों को उपलब्ध कराया जाएगा, और बाद में इसे Google AI Ultra सब्सक्राइबर्स के लिए जारी करने की योजना है
The Future of AI and Mathematics
- Google DeepMind गणित समुदाय के साथ सहयोग जारी रखते हुए, प्राकृतिक भाषा आधारित reasoning के अलावा AlphaGeometry·AlphaProof जैसी औपचारिक प्रणाली-आधारित रिसर्च भी समानांतर रूप से कर रहा है
- आगे चलकर, प्राकृतिक भाषा समझ और औपचारिक तथा verify की जा सकने वाली गणितीय reasoning क्षमता को मिलाने वाला AI गणित, विज्ञान, इंजीनियरिंग और रिसर्च के क्षेत्रों में एक प्रमुख टूल बन सकता है
- DeepMind इस उपलब्धि को AGI (Artificial General Intelligence) की दिशा में एक महत्वपूर्ण प्रगति मानता है और भविष्य में इससे भी अधिक जटिल और उच्च-स्तरीय गणितीय समस्याओं को हल करने की चुनौती लेने की योजना रखता है
उत्तर सत्यापन और IMO की आधिकारिक स्थिति
- IMO आयोजन समिति ने आधिकारिक तौर पर पुष्टि की कि जमा किए गए उत्तर पूर्ण और सटीक समाधान हैं
- हालांकि, IMO ने यह भी स्पष्ट किया कि उसकी समीक्षा में सिस्टम, प्रक्रिया या मूल मॉडल स्वयं का सत्यापन शामिल नहीं है
- विस्तृत जानकारी और आधिकारिक संदर्भ के लिए IMO के बयान को देखें (और पढ़ें)
5 टिप्पणियां
OpenAI, 2025 अंतरराष्ट्रीय गणित ओलंपियाड (IMO) में गोल्ड-मेडल स्तर की उपलब्धि हासिल करने की घोषणा
2 दिन पहले OpenAI ने पहले ही घोषणा कर दी थी, इसलिए थोड़ा असर कम हो गया, लेकिन यह भी कहा गया कि OpenAI के Alexander Wei ने IMO से किसी चर्चा के बिना पहले बात करके शिष्टाचार नहीं दिखाया।
आधिकारिक तौर पर IMO की ओर से मान्यता भी नहीं मिली थी, फिर भी घोषणा कर दी गई, इसलिए कहा गया कि इसने AI नहीं बल्कि सामान्य प्रतिभागियों के लिए होने वाली बधाई और श्रेय छीन लिया।
इस वजह से OAI ने बस अपने ही panel से उसका verification कराया, और स्थिति यह हो गई कि उसे IMO की आधिकारिक scoring भी नहीं मिली। ऊपर से, अगर देखें कि कई लोगों की राय है कि जवाबों की quality भी Gemini की थोड़ी बेहतर थी... तो यह और भी शर्मनाक स्थिति लगती है। प्रतिष्ठा को लेकर कोई risk लिए बिना, सफल हो जाए तो announcement कर दो (वह भी ऐसी स्थिति में जो आधिकारिक scoring नहीं थी), और नतीजा खराब आए तो पीछे हट जाओ — benchmark में ऐसा करना शायद चल सकता है, लेकिन जिस प्रतियोगिता में प्रतिभागी अपना नाम दांव पर लगाकर उतरते हैं, वहाँ यह सही रवैया नहीं लगता।
Google और OpenAI के LLM परफ़ॉर्मेंस भले ही लगभग बराबर हों, लेकिन कंपनियों की मंज़ी हुई परिपक्वता का फ़र्क यहाँ दिखता है।
Hacker News की राय
AlphaGeometry और AlphaProof ने पहले natural language समस्याओं को Lean जैसी domain-specific language में अनुवाद किया, फिर proof के परिणामों को वापस natural language में बदला, और computation में 2–3 दिन लगे; इस साल के Gemini मॉडल ने end-to-end तरीके का इस्तेमाल किया, जो सिर्फ natural language के आधार पर आधिकारिक problem statement से सीधे mathematical proof बनाता है; यानी पहले Lean में अनुवाद नहीं किया गया। हालांकि, यह स्पष्ट नहीं है कि अंदरूनी तौर पर Lean, internet search, calculator, Python जैसे tools इस्तेमाल किए गए या नहीं। OpenAI ने कहा था कि उसके मॉडल में ऐसे tools का उपयोग नहीं हुआ, लेकिन यह दावा Gemini पर भी ठीक-ठीक लागू होता है या नहीं, यह स्पष्ट नहीं है। मैं यह भी जानना चाहता हूँ कि दोनों systems ने लगभग कितनी computation, यानी cost, इस्तेमाल की। अगर कीमत बहुत ज़्यादा है, तो इसका मतलब है कि अभी इसकी practical utility कम है। अभी सार्वजनिक जानकारी नहीं है, इसलिए मेरा अनुमान है कि यह बेहद महँगा रहा होगा। और यह लिंक भी साझा किया गया कि “कोई tool use नहीं, कोई internet connection नहीं” की पुष्टि हुई थी https://x.com/FredZhang0/status/1947364744412758305
इस साल का Gemini मॉडल सिर्फ natural language के आधार पर आधिकारिक problem statement से mathematical proof बनाता है, और पूरी प्रक्रिया 4.5 घंटे की contest time limit के भीतर हुई। किसी बाहरी tool का उपयोग नहीं किया गया।
आधिकारिक तौर पर तो कहा जाता है कि Lean जैसे formal verification tools का उपयोग IMO problems को वास्तव में हल करने में नहीं किया जाता, लेकिन मैं जानना चाहता हूँ कि मॉडल को train करने की प्रक्रिया में क्या उनका इस्तेमाल होता है। Google के 2024 IMO research में natural language proofs को formally verifiable language में बदलने की तकनीक है। मुझे लगता है कि इसे RLVR (reinforcement learning via verification reward) training में उपयोग करना अगला स्वाभाविक कदम है। अगर math LLM द्वारा बनाए गए हर reasoning step का अनुवाद और verification करके reward signal के रूप में इस्तेमाल किया जा सके, तो reward signal कहीं अधिक dense हो जाएगा। पूर्ण formal proof पाना अभी भी कठिन होगा, लेकिन गलत reasoning या अपठनीय वाक्यों से बचने के लिए यह उपयोगी होगा। बहुत बड़े computation के साथ IMO difficulty की problems भी हल की जा सकती हैं। AlphaProof की तरह Lean proofs और LLM output के बीच आना-जाना करके reasoning space को कुशलता से explore करने से पहले ही दिखाया जा चुका है कि IMO-स्तर की problems हल की जा सकती हैं। अगर बीच के steps हटाकर RLVR से LLM को formal reasoning की नकल करना सिखाया जाए, तो शायद समान efficiency और problem-solving क्षमता हासिल की जा सकती है।
मैं यह भी जानना चाहता हूँ कि Lean का उपयोग क्यों नहीं किया जा रहा। क्या इसका मतलब यह है कि आजकल Lean का उपयोग करने पर problem solving बहुत आसान हो जाती है, या फिर Lean खुद ही एक बाधा है?
“कोई tool use नहीं, कोई internet connection नहीं” का क्या वास्तव में मतलब यह है कि यह Google infrastructure के बिना offline भी चल सकता है, यानी ज़रूरत पड़ने पर क्या इसे local deployment के रूप में इस्तेमाल किया जा सकता है?
इस साल कहा गया है कि उन्नत Gemini मॉडल ने सिर्फ natural language से आधिकारिक problem statement से सीधे mathematical proofs बनाए, लेकिन मुझे उल्टा यह खटकता है कि हम formalization technology से दूर जा रहे हैं। अगर हमें गणित को सच में automate करना है, या उदाहरण के लिए हज़ारों पन्नों के proofs को मशीन से तैयार कराने के स्तर तक पहुँचना है, तो formalization के अलावा कोई रास्ता नहीं है। वरना अब भी human reviewer की ज़रूरत पड़ेगी, और proof पर सच में भरोसा करने का कोई तरीका नहीं रहेगा।
अगर LLM natural language में सख्त proof बना सकता है, तो Lean जैसी formal language में proof करना भी बहुत कठिन नहीं होना चाहिए। AlphaProof में Lean का उपयोग काफ़ी सीमित था और खास math problems के लिए specialized था। दूसरी ओर, अगर RL approach और natural language के माध्यम से वही हासिल किया जाए, तो इसे verification कठिन होने वाले विभिन्न क्षेत्रों तक बढ़ाया जा सकता है।
यह भी साझा किया गया कि DeepMind इस समय formally unresolved problems को formalize करके रिकॉर्ड करने वाले repositories इकट्ठा कर रहा है https://github.com/google-deepmind/formal-conjectures
मैं गणितज्ञ हूँ, लेकिन अब research नहीं करता। मैं थोड़ा संदर्भ देना चाहता हूँ कि क्यों कई गणितज्ञ formal methods को लेकर बहुत उत्साहित नहीं होते। व्यवहारिक रूप से, हज़ारों पन्नों के proof बनाना formalization के बिना संभव नहीं है, और किसी चीज़ पर “भरोसा” करने के लिए formal verification ज़रूरी है—इससे मैं सहमत हूँ। लेकिन वास्तव में गणितज्ञ जो चाहते हैं, वह यह है कि परिणाम सही क्यों है, इसकी explanation। असली उत्पाद yes-no answer नहीं, बल्कि उसकी interpretation और कारण है। उदाहरण के लिए, लगभग सभी मानते हैं कि Riemann hypothesis शायद सही है, लेकिन वे सिर्फ अंतिम उत्तर का इंतज़ार नहीं कर रहे। यहाँ तक कि “अगर Riemann hypothesis सही है, तो यह नया theorem सही होगा” जैसे बहुत से परिणाम हैं। Proof से अपेक्षा मूलतः नई insight, या number theory के बारे में गहरी समझ देने की होती है। अगर Lean जैसी कोई चीज़ सिर्फ यह verify कर दे कि कथन सही है, लेकिन इंसान उसे समझ ही न सके, तो उसका लगभग कोई अर्थ नहीं।
सटीक formalization आम तौर पर problem solving से आसान होती है, इसलिए पहले problem solve करके बाद में उसे formalize करके verify करना भी संभव है।
IMO problems मूल रूप से ऐसे designed होते हैं कि इंसान उन्हें tools के बिना हल करे। अगर मॉडल से इससे कठिन problems हल करानी हों, तो तब उसे पर्याप्त tools दिए जा सकते हैं। कम से कम पहले human-level क्षमता को tools के बिना reproduce करना एक अच्छी दिशा लगता है।
OpenAI और Gemini के जवाबों की तुलना करें, तो Gemini की writing style कहीं अधिक स्पष्ट लगती है। प्रस्तुति थोड़ी और बेहतर हो सकती थी, लेकिन proof की सामग्री खुद समझने में आसान है, और यह OpenAI के जवाब से छोटा होते हुए भी अधिक व्यवस्थित वाक्यों में लिखा गया है।
Google का proof शायद बाद में summarize किया गया परिणाम हो सकता है, और Tree of Thoughts जैसे mechanism का कोई हिस्सा इस summarization process में शामिल रहा हो सकता है। ऐसा नहीं लगता कि यह बस एक साधारण, passive “final answer दे दो” निर्देश का परिणाम है।
OpenAI और Google के जिन IMO proof results का उल्लेख हुआ, उन्हें क्रमशः Google proof PDF और OpenAI proof example Repository में देखा जा सकता है।
OpenAI और Google दोनों ने इस बात पर ज़ोर दिया कि “पूरी प्रक्रिया 4.5 घंटे की contest के भीतर पूरी हुई”, लेकिन मुझे संदेह है कि इस सीमा का वास्तव में कितना महत्व है। संभव है कि उन्होंने एक साथ लाखों parallel reasoning processes चलाकर proof ढूँढा हो। निश्चित रूप से ऐसा करने के लिए परिणामों का मूल्यांकन करने और अंत में submit करने योग्य proof चुनने वाले evaluator model में भी भारी computation लगी होगी। संभव है कि वास्तव में सैकड़ों वर्षों के GPU time के बराबर computation इस्तेमाल हुई हो। फिर भी, यह कि इस तरह से उत्तर खोजे जा सकते हैं, और parallelization इस स्तर तक संभव है, अपने आप में चौंकाने वाला है। चाहे AGI अधिक computing से हासिल हो या नहीं, मानव मस्तिष्क इस तरह आसानी से scale नहीं होता, इसलिए इस परिणाम का महत्व स्पष्ट है।
पिछले साल के Lean-specialized system से natural language आधारित general-purpose LLM + RL की ओर बदलाव बहुत दिलचस्प है। उम्मीद है कि यह approach math competitions से बाहर के क्षेत्रों में भी performance improvement लाएगी। यह आगे कहाँ तक scale हो सकती है, इसे लेकर उत्सुकता है। और ऐसा भी लगता है कि यह system इस गर्मी में public होने वाले “DeepThink” model/feature से बहुत अलग नहीं है।
अभी ऐसा महसूस होता है जैसे हम मशीनों के साथ गणितीय प्रतिस्पर्धा में Deep Blue बनाम Kasparov वाले दौर जैसा कोई क्षण देख रहे हैं। कुछ ही साल पहले की तुलना में बहुत बड़ी प्रगति हुई है, लेकिन मुझे फिर भी लगता है कि हम एक असली AI mathematician से अभी बहुत दूर हैं। फिर भी, हम सचमुच अद्भुत समय में जी रहे हैं।
हाल की एक podcast में Terrence Tao ने भी ऐसे tools के साथ काम करने में गहरी रुचि दिखाई। उन्होंने कहा कि निकट भविष्य में इसका सबसे अच्छा उपयोग शायद यह होगा कि इंसान ideas/parameters तय करे और LLM exploration, proof आदि parallel में आज़माए। Chess engine की उपमा भी उपयुक्त है। पहले शीर्ष chess players के पास भी analysis में मदद करने वाली expert teams होती थीं, लेकिन अब supercomputers और software असंख्य positions का विश्लेषण करके सबसे अच्छे ideas निकालते हैं और खिलाड़ी तक पहुँचाते हैं।
मुझे यह Deep Blue और किसी child prodigy के मुकाबले के अधिक करीब लगता है। IMO प्रतिभागी विश्व-स्तरीय गणितज्ञ नहीं, बल्कि high school students होते हैं।
यहाँ फ़र्क यह है कि केवल brute force से समय सीमा के भीतर उच्च score पाना संभव नहीं है। यह एक वास्तविक technical milestone है, और Deep Blue के समय की “सिद्धांततः संभव” वाली स्थिति से अलग है।
6वाँ प्रश्न उलझाने वाला है। openai और deepmind दोनों कोई उत्तर नहीं दे पाए। इंसान तो कम से कम partial answer देता है, लेकिन AI का बिना उत्तर रह जाना अजीब है। इससे यह सवाल उठता है कि क्या LLM ने खुद पहचान लिया कि वह इसे हल नहीं कर सका। LLM की सीमाओं में से एक यह है कि उसे “यह नहीं पता कि उसे नहीं पता”, और ऐसे में solver के बिना logical consistency की जाँच करना लगभग असंभव लगता है।
संभवतः ऐसा इसलिए हुआ कि contest time limit के भीतर वह “सोचने” की प्रक्रिया पूरी नहीं कर पाया और “output” चरण तक पहुँच ही नहीं सका।
यह सीमा केवल सबसे बुनियादी pretrained LLM text generation पर लागू होती है। इसके अलावा एक linear probe (सरल neural network layer) को train करके confidence score output कराया जा सकता है। बेशक, यह 100% भरोसेमंद नहीं होगा, लेकिन math जैसे सीमित domain में इसे काफ़ी विश्वसनीय बनाया जा सकता है।
Formal verification tools के बिना इसे वास्तविक उपयोग में लाना अभी भी काफ़ी जोखिम भरा हो सकता है। पुराना o3, भले अब नवीनतम न हो, references ढूँढने और नई inequalities सुझाने में अच्छा था। लेकिन वास्तविक proof चरण में यह ऐसे जवाब दे सकता था जो देखने में काफ़ी persuasive हों, पर details में गलत statements या algebraic mistakes हों। मॉडल जितना बेहतर होगा, ऐसी सूक्ष्म त्रुटियाँ शायद उतनी ही पकड़ना कठिन हो जाएँगी।
मैं सोच रहा हूँ कि वे theorem prover का उपयोग न करने पर इतना ज़ोर क्यों दे रहे हैं। आखिर मॉडल की performance बढ़ाने के लिए कोई भी tool उपयोगी हो तो उसका इस्तेमाल करना चाहिए, है न? ऊपर से Gemini भी IMO के हिसाब से विशेष रूप से तैयार किया गया था। reinforcement learning के माध्यम से multi-step reasoning / problem solving / theorem proving data पर मॉडल को train किया गया, और उच्च-गुणवत्ता वाले math solution manuals तथा IMO problem approaches पर hints भी दिए गए।
मेरा अनुमान है कि “Gemini Deepthink का advanced version” वास्तव में release होने वाले Gemini Ultra subscription product में आने वाले Deepthink से अलग होगा, या उसमें test-time computation कहीं अधिक इस्तेमाल हुई होगी। फिर भी, OpenAI और Google को प्रतिस्पर्धा करते देखना दिलचस्प है।
1-6 तक के सभी सवाल हल करने वाले context engineering system prompt का लिंक साझा कर रहा हूँ; इसे o3 या Gemini 2.5 के साथ इस्तेमाल किया जा सकता है, बस पूरा prompt डालें, फिर सवाल डालकर कहें कि समस्या हल करे। https://github.com/redcrash0721/freederia/blob/main/imo6kr.pdf