DeepMind का AI, International Mathematical Olympiad के प्रश्नों को silver medal स्तर पर हल करता है

(deepmind.google)

3 पॉइंट द्वारा GN⁺ 2024-07-26 | 3 टिप्पणियां | WhatsApp पर शेयर करें

Google DeepMind के AlphaProof और AlphaGeometry 2 ने International Mathematical Olympiad के प्रश्न हल किए
- AlphaProof: reinforcement learning-आधारित mathematical reasoning system
- AlphaGeometry 2: बेहतर geometry problem-solving system
- दोनों systems ने इस साल के International Mathematical Olympiad (IMO) में 6 में से 4 प्रश्न हल करके silver medal स्तर का प्रदर्शन हासिल किया

जटिल गणितीय समस्याओं के समाधान में AI की उपलब्धि

IMO परिचय
- 1959 से हर साल आयोजित होने वाली सबसे पुरानी और प्रतिष्ठित युवा गणित प्रतियोगिता
- प्रतियोगिता के प्रश्न algebra, combinatorics, geometry, number theory आदि से दिए जाते हैं
- Fields Medal विजेताओं में से कई IMO पृष्ठभूमि से रहे हैं
AI systems की IMO चुनौती
- AlphaProof और AlphaGeometry 2 ने इस साल के IMO प्रश्न हल किए
- प्रश्नों का स्कोरिंग आधिकारिक प्रतियोगिता नियमों के अनुसार किया गया
- AlphaProof ने 2 algebra प्रश्न और 1 number theory प्रश्न हल किया
- AlphaGeometry 2 ने 1 geometry प्रश्न हल किया
- 2 combinatorics प्रश्न हल नहीं हो सके
- कुल 42 अंकों में से 28 अंक प्राप्त कर silver medal स्तर का प्रदर्शन हासिल किया

AlphaProof: formal reasoning approach

AlphaProof कैसे काम करता है
- गणितीय propositions को formal language Lean में prove करता है
- pre-trained language model और AlphaZero reinforcement learning algorithm का संयोजन
- natural language समस्याओं को formal propositions में अनुवाद कर विभिन्न कठिनाई स्तर की समस्याएँ हल करता है
- समस्या दिए जाने पर AlphaProof समाधान के candidates बनाता है और उन्हें prove या disprove करता है
- सिद्ध परिणाम AlphaProof के language model को मजबूत करते हैं, जिससे अधिक कठिन समस्याएँ हल करने की क्षमता बढ़ती है
प्रशिक्षण प्रक्रिया
- लाखों समस्याओं को prove या disprove करते हुए training की गई
- प्रतियोगिता के दौरान भी training loop लागू करके problem variations को prove किया गया

और अधिक प्रतिस्पर्धी AlphaGeometry 2

AlphaGeometry 2 में सुधार
- Gemini-आधारित language model और neural-symbolic hybrid system
- पिछले version की तुलना में 10 गुना अधिक synthetic data पर training
- geometry problem-solving की गति और सटीकता में सुधार
- नई समस्याएँ हल करते समय knowledge-sharing mechanism का उपयोग
IMO 2024 प्रदर्शन
- पिछले 25 वर्षों के IMO geometry प्रश्नों में से 83% हल किए
- इस साल की प्रतियोगिता में प्रश्न 4 को 19 सेकंड में हल किया

mathematical reasoning की नई frontier

natural language reasoning system पर प्रयोग
- Gemini-आधारित natural language reasoning system पर प्रयोग
- formal language में अनुवाद किए बिना भी समस्या हल करना संभव
- अन्य AI systems के साथ संयोजन की संभावना की पड़ताल
भविष्य की संभावनाएँ
- गणितज्ञ AI tools के साथ मिलकर नई hypotheses की खोज, problem-solving approaches का परीक्षण, और proof process को छोटा कर सकते हैं
- Gemini जैसे AI systems गणित और general reasoning क्षमता को बेहतर बना सकते हैं

GN⁺ का सार

AlphaProof और AlphaGeometry 2 गणितीय reasoning में AI की संभावनाओं को दिखाते हैं
International Mathematical Olympiad में silver medal स्तर का प्रदर्शन हासिल कर AI की गणितीय समस्या-समाधान क्षमता को साबित किया
यह संभावना खोलते हैं कि गणितज्ञ AI के साथ मिलकर नई problem-solving approaches खोज सकते हैं
समान कार्यक्षमता वाले प्रोजेक्ट्स में OpenAI के GPT-3 जैसे natural language processing models शामिल हैं

3 टिप्पणियां

chabulhwi 2024-07-26

जितने अधिक गणितज्ञ formal mathematics libraries के विकास में योगदान देंगे, उतना ही बेहतर प्रदर्शन करने वाला math AI बनाना आसान होगा। मेरी जानकारी के अनुसार, इस समय ऐसे 3 कोरियाई हैं जो अपने द्वारा सीधे Lean proof assistant की भाषा में formalize किए गए mathematical theories को Lean की mathematics library Mathlib में स्थानांतरित कर रहे हैं।

मैंने पिछले वर्ष Mathlib को Lean 3 से Lean 4 में स्थानांतरित करने के काम में थोड़ा हिस्सा लिया था, और इस वर्ष मैंने Lean 4 Batteries library के एक unresolved theorem को सिद्ध किया।

GN⁺ 2024-07-26

Hacker News टिप्पणियाँ

पहली टिप्पणी
- मैं इस प्रोजेक्ट को लेकर बहुत उत्साहित हूँ, लेकिन गणित की समस्याओं को formal language में अनुवाद करने की प्रक्रिया में कंप्यूटर का योगदान कितना था, यह स्पष्ट नहीं है
- डाउनलोड की जा सकने वाली solutions में यह साफ नहीं है कि अनुवाद प्रक्रिया में क्या इंसानों ने तय किया और क्या कंप्यूटर ने खोजा
दूसरी टिप्पणी
- IMO में मेडल 50% प्रतिभागियों को दिए जाते हैं, और gold, silver, bronze medals का अनुपात 1:2:3 होता है
- AI ने 75% छात्रों से बेहतर समाधान किया, यह प्रभावशाली है
- लेकिन AI को समस्याएँ हल करने में जितना समय लगा, वह छात्रों को परीक्षा में दिए गए समय से अलग है, इसलिए सीधी तुलना उचित नहीं है
तीसरी टिप्पणी
- AlphaGeometry ने सीमित समस्याएँ हल की थीं, लेकिन इस बार की विधि गणित पर अधिक व्यापक प्रभाव डालेगी
- यह natural language mathematics को formalized mathematics में बदलने वाली pipeline लागू कर रही है, और यह बुनियादी theory building भी सीख सकती है
- यह proof assistants की holy grail है, और इससे इंसान गणित को अधिक स्वाभाविक ढंग से formalize कर सकेंगे
चौथी टिप्पणी
- अगर सिस्टम को समस्या हल करने में 3 दिन लगे, तो यह साधारण brute force से अलग नहीं है
- यह वास्तविक reasoning नहीं है
पाँचवीं टिप्पणी
- यह Lean का उपयोग कर रहा है
- यह सिर्फ गणित की समस्याओं के लिए ही नहीं, बल्कि सामान्य रूप से निरर्थक परिणामों से बचने के लिए भी महत्वपूर्ण है
- आशा है कि अधिक लोग Lean जैसे systems में types लिखेंगे
छठी टिप्पणी
- मुझे इस प्रोजेक्ट पर काम करने वाले लोगों से ईर्ष्या होती है
- cutting-edge technology को आगे बढ़ाना बहुत मज़ेदार और संतोषजनक होगा
सातवीं टिप्पणी
- सबसे अच्छी चर्चा LeanProver की Zulip chat में होती है
आठवीं टिप्पणी
- Fields Medal विजेता Tim Gowers ने मुख्य सावधानियाँ समझाते हुए और संदर्भ देते हुए एक अच्छा overview दिया है
नौवीं टिप्पणी
- theorem proving एक single-player game है, जिसमें खोज का क्षेत्र बहुत बड़ा होता है
- AlphaProof के सबसे बड़े योगदानकर्ता Lean और Mathlib के developers हैं
- गणितीय papers में formalization की कमी ने automation के प्रयासों में बाधा डाली है
दसवीं टिप्पणी
- मशीनें दशकों से शतरंज में इंसानों से बेहतर रही हैं
- लेकिन लोग आज भी Magnus Carlsen को देखते हैं
- इंसानों की रुचि दूसरे इंसानों के कामों में होती है
- मशीनों में रुचि केवल तब तक है, जब तक वे इंसानों के लिए उपयोगी हैं