DeepMind के AI ने International Mathematical Olympiad समस्याएं सिल्वर मेडल स्तर पर हल कीं

 (deepmind.google)
3 पॉइंट द्वारा GN⁺ 2024-07-26 | 3 टिप्पणियां | WhatsApp पर शेयर करें
  • कठिन गणितीय reasoning की प्रमुख कसौटी IMO 2024 में Google DeepMind के AlphaProof और AlphaGeometry 2 ने 6 में से 4 समस्याएं हल कर AI के लिए पहली बार सिल्वर मेडल-रेंज का स्कोर हासिल किया
  • कुल 42 अंकों में से 28 अंक मिले; हल की गई सभी समस्याओं में पूरे अंक दिए गए, और यह 2024 के गोल्ड मेडल कटऑफ 29 अंकों से सिर्फ 1 अंक कम था
  • मूल्यांकन IMO की marking rules के अनुसार गणितज्ञों ने किया; algebra और number theory AlphaProof ने संभाली, जबकि geometry AlphaGeometry 2 ने, और इस तरह अलग-अलग reasoning तरीकों को जोड़ा गया
  • समस्याओं को पहले formal mathematical language में मैन्युअली translate किया गया; छात्रों के competition time में 4.5 घंटे के दो sessions होते हैं, जबकि system ने एक समस्या कुछ मिनटों में और अन्य समस्याएं अधिकतम 3 दिनों में हल कीं
  • यह परिणाम दिखाता है कि mathematical AI सिर्फ calculation से आगे बढ़कर proof search और verification तक पहुंच गया है, लेकिन formalized input और लंबा solving time अभी भी महत्वपूर्ण सीमाएं हैं

IMO 2024 में हासिल सिल्वर मेडल-रेंज प्रदर्शन

  • Google DeepMind ने mathematical reasoning system AlphaProof और geometry problem-solving system के बेहतर version AlphaGeometry 2 को पेश किया
  • दोनों systems ने 2024 International Mathematical Olympiad की 6 समस्याओं में से 4 हल कीं
    • AlphaProof: algebra की 2 समस्याएं, number theory की 1 समस्या हल की
    • AlphaGeometry 2: geometry की 1 समस्या का proof दिया
    • combinatorics की 2 समस्याएं हल नहीं कर सके
  • हर समस्या 7 अंकों की होती है और कुल स्कोर 42 अंक होता है
    • system ने हल की गई 4ों समस्याओं में पूरे अंक हासिल कर 28 अंक पाए
    • यह 2024 IMO की सिल्वर मेडल-रेंज के ऊपरी हिस्से के बराबर है
    • 2024 का गोल्ड मेडल कटऑफ 29 अंक था, और official competition में 609 प्रतिभागियों में से 58 गोल्ड मेडल-रेंज तक पहुंचे
  • यह पहला मामला है जब किसी AI system ने IMO में silver medalist level के बराबर प्रदर्शन किया

मूल्यांकन पद्धति और solving conditions

  • समस्याएं IMO आयोजकों द्वारा उपलब्ध कराए गए competition problems से ली गईं
  • उत्तरों का मूल्यांकन IMO के scoring rules के अनुसार किया गया
    • evaluators थे IMO gold medalist और Fields Medal विजेता Prof Sir Timothy Gowers, तथा दो बार IMO gold medalist और IMO 2024 Problem Selection Committee के अध्यक्ष Dr Joseph Myers
  • system समस्याओं को समझ सके, इसके लिए सभी समस्याओं को पहले formal mathematical language में मैन्युअली translate किया गया
  • official competition में छात्र 4.5 घंटे के दो sessions में अपने उत्तर submit करते हैं
    • AI system ने एक समस्या कुछ मिनटों में हल की, और अन्य समस्याओं में अधिकतम 3 दिन लगे
  • AlphaProof द्वारा हल की गई समस्याओं में 2024 IMO की सबसे कठिन समस्या भी शामिल थी, जिसे केवल 5 participants ने हल किया था

AlphaProof: Lean-आधारित formal reasoning

  • AlphaProof एक ऐसा system है जो mathematical propositions को Lean formal language में prove करना सीखता है
  • यह pretrained language model और AlphaZero reinforcement learning algorithm को जोड़ता है
    • AlphaZero वही algorithm है जिसका उपयोग chess, shogi और Go को स्वयं सीखने में किया गया था
  • formal language का उपयोग करने से mathematical reasoning वाले proofs की correctness verification संभव होती है
  • पहले humans द्वारा लिखे गए formal proof data बहुत कम थे, इसलिए machine learning में formal language का उपयोग सीमित था
  • natural-language-based approach बहुत अधिक data का उपयोग कर सकती है, लेकिन वह ऐसे intermediate reasoning steps या solutions बना सकती है जो देखने में plausible लगते हैं पर गलत होते हैं
  • DeepMind ने Gemini model को fine-tune किया ताकि natural language problems को formal propositions में automatically translate किया जा सके, और अलग-अलग difficulty की formal problems की library बनाई
  • AlphaProof को जब कोई problem दी जाती है, तो वह candidate solutions generate करता है, फिर Lean में possible proof steps खोजकर उन्हें prove या disprove करता है
    • खोजे और verify किए गए proofs का उपयोग AlphaProof के language model को reinforce करने में किया जाता है
    • यह iterative process कठिन समस्याएं हल करने की क्षमता बढ़ाने में इस्तेमाल होता है
  • IMO की तैयारी के दौरान इसने कई हफ्तों तक लाखों problems को prove या disprove करते हुए training की
    • competition के दौरान भी, problem के self-generated variants पर proofs को reinforce करते हुए complete solution खोजने वाला learning loop लागू किया गया

AlphaGeometry 2: कठिन geometry problems तक विस्तार

  • AlphaGeometry 2 मौजूदा AlphaGeometry का काफी improved version है
  • इस system में neural networks और symbolic reasoning को जोड़ने वाली neuro-symbolic hybrid architecture है
    • language model Gemini पर आधारित है
    • पिछले version की तुलना में एक order of magnitude अधिक synthetic data पर इसे शुरुआत से train किया गया
  • ज्यादा data और improved model की वजह से यह वस्तुओं की movement, angle, ratio और distance equations वाली अधिक कठिन geometry problems संभाल सकता है
  • AlphaGeometry 2 का symbolic engine पिछले version से दहाई गुना तेज है
  • नई problem मिलने पर यह नए knowledge sharing mechanism के जरिए अलग-अलग search trees के advanced combinations का उपयोग कर अधिक complex problems handle करता है
  • पिछले 25 वर्षों की IMO geometry problems की solving rate: {b:83,53}
    • 2024 competition से पहले के मानदंड पर AlphaGeometry 2 पिछले 25 वर्षों की IMO geometry problems में से 83% हल कर सकता था
    • पिछले AlphaGeometry की solving rate 53% थी
  • IMO 2024 में इसने Problem 4 को formalized input के बाद 19 सेकंड में हल किया

Natural language reasoning और आगे के उपयोग

  • IMO task के हिस्से के रूप में, DeepMind ने Gemini और latest research पर आधारित natural language reasoning system का भी प्रयोग किया
  • इस system को problems को formal language में translate करने की जरूरत नहीं होती, और इसे अन्य AI systems के साथ जोड़ा जा सकता है
  • 2024 IMO problems पर भी इस approach को test किया गया और परिणाम promising स्तर के माने गए
  • AlphaProof की अधिक technical methodology Nature paper के रूप में प्रकाशित हुई
  • DeepMind का लक्ष्य ऐसा भविष्य है जहां mathematicians AI tools के साथ hypotheses explore करें, पुराने problems पर नए approaches आजमाएं, और proofs के time-consuming elements को तेजी से पूरा करें

संबंधित पढ़ाई

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 mathematical language में इंसानों ने खुद translate किया” वाला वाक्य कितना काम अपने भीतर समेटे है, यह स्पष्ट नहीं है
    geometry के अलावा बाकी सभी problems “ऐसे सभी X निकालें जो ... हों” के रूप में थीं, और theorem statement “सभी X का set {foo} है, यह दिखाएँ” के रूप में था
    https://storage.googleapis.com/deepmind-media/DeepMind.com/B... पर download की जा सकने वाली solutions देखकर ही यह समझना मुश्किल है कि translation step में {foo} इंसान ने तय किया था या computer ने खोजा था। मैं मानना चाहता हूँ कि computer ने खोजा, लेकिन इसकी पुष्टि का आधार नहीं मिला

    • computer ने answer खुद खोजा। यानी P1 में even integers, P2 में {1,1}, P6 में 2 खोजा, और हर मामले में साथ में Lean proof भी पेश किया
    • सामान्य रूप से कहें तो वह translation step proof step से कहीं आसान है। automatic translation की समस्या यह है कि translated result गलत हो सकता है
      इंसान भी formal methods को सीधे handle करते समय अक्सर ऐसा कर बैठते हैं, इसलिए researchers ने शायद तय किया होगा कि LLM हो या कोई और tool, अंततः सभी translations को audit करना होगा
    • linked page में लिखा है कि “problem statements को इंसानों ने Lean में formalize किया, लेकिन problem statement के अंदर का answer agent ने generate और formalize किया”
      हालांकि यह साफ नहीं है कि agent को शुरुआत में कौन-सा formal form दिया गया था, जिससे यह step संभव हुआ
    • training data बनाने में इस्तेमाल किया गया एक formalization tool है, लेकिन दिलचस्प है कि यहाँ उसका इस्तेमाल नहीं किया गया। शायद अभी वह पर्याप्त भरोसेमंद नहीं था
    • वर्णन से ऐसा लगता है कि “problem मिलने पर AlphaProof solution candidates generate करता है और फिर Lean में संभावित proof steps explore करके उन्हें prove या disprove करता है”
      यानी AlphaProof किस तरह की “problem” लेता है, और “ऐसे सभी X निकालें जो ... हों” को उसने जैसे भी formalize किया हो, वह शायद candidate theorems Lean में generate करता है। उदाहरण के लिए set किसी formula P के लिए {n: P(n)} के रूप में हो सकता है। इसके बाद वह proof explore करता है
      अगर AlphaProof ने {foo} खोजा नहीं बल्कि उसे दिया गया था, तो यह दावा करना कि उसने problem solve की, काफी बेतुका लगेगा। फिर भी इस result को लेकर मैं बहुत उत्साहित हूँ

  • निश्चित रूप से impressive है, लेकिन IMO का जिक्र करते समय कुछ सावधानी जरूरी है। medals participants, यानी high school students के 50% को दिए जाते हैं, और gold·silver·bronze का ratio 1:2:3 होता है, इसलिए gold और silver winners कुल participants के top 25% में आते हैं
    इसलिए इसे “AI ने IMO problems 75% students से बेहतर solve किए” कहना होगा, और सच कहें तो यह भी और ज्यादा impressive हो सकता है
    लेकिन “एक problem कुछ मिनटों में, और बाकी हर problem अधिकतम 3 दिन में” वाली condition students को मिलने वाले 9 hours से अलग है, इसलिए इसे सही comparison मानना मुश्किल है। अगर students को भी 9 hours की जगह maximum 15 days दिए जाते, तो ज्यादा लोग यह score हासिल करते या उससे आगे जाते
    असल में AI ने students को दिए गए 9 hours के भीतर सिर्फ एक problem solve की, इसलिए शायद medal range से काफी दूर रहता। इतने impressive result को बेवजह apples-to-oranges comparison से धुंधला करने की क्या जरूरत है
    ज्यादा objective तरीके से यह report किया जा सकता है कि time ज्यादा लगा, लेकिन उसने कुल problems के X% solve किए या N में से X points पाए

    • मैं IMO participants से मिल चुका हूँ, और वे सच में अविश्वसनीय रूप से smart होते हैं। ऐसे group से मिलने से पहले मैं कल्पना भी नहीं कर सकता था कि इंसान इतने smart हो सकते हैं। इसलिए इसे पूरे high school students के 0.01% में top 25% के करीब मानना चाहिए
      यहाँ time उतना दिलचस्प axis नहीं है। इंसान विशाल GPU cluster जैसा CPU इस्तेमाल नहीं करते। “क्या पर्याप्त resources दिए जाने पर solution तक पहुँचा जा सकता है” वाली binary बात ज्यादा दिलचस्प है, और GPT/Claude का जवाब साफ तौर पर नहीं था
    • “participant high school students के 50% को medals दिए जाते हैं” यह बात confusing हो सकती है, क्योंकि यहाँ high school students का मतलब सामान्य high school students का sample नहीं है। मेरी जानकारी में, हर देश से competition problem solving के सबसे मजबूत लगभग 6 लोगों की team होती है
    • निजी तौर पर, हालांकि यह Google का stance नहीं है, मुझे लगता है कि इस साल gold medal न पाने की एकमात्र वजह problem selection में bad luck और P3/P5 में partial marks target न करना था
      cutoff के बेहद करीब था, और आम तौर पर थोड़ी-सी progress से भी 1 point मिल सकता है। हालांकि technical reason से gold medal जीता जैसी reporting अच्छी नहीं लगती, इसलिए लगता है कि वे बिना controversy वाले silver medal से संतुष्ट रहे
    • इंसानों को ज्यादा time देने और computer program को ज्यादा time देने में मुख्य अंतर यह है कि इतिहास में दूसरे को faster run कराने में हम कहीं ज्यादा सफल रहे हैं
    • DeepMind की ज्यादातर research company के लिए cost center है। ऐसे press releases investors और public के सामने continued investment को justify करने में मदद करते हैं

  • यह सच में बड़ा है। AlphaGeometry ने बहुत सारे brute-force search से बहुत सीमित problem set हल किया था
    यह नया तरीका कहीं ज़्यादा व्यापक है, और मुझे लगता है कि गणित करने के तरीके पर इसका बड़ा असर पड़ेगा। यह natural-language mathematics से formalized mathematics तक जाता है, और वहां formalization और proof दोनों को train करने वाली self-supplying pipeline को सचमुच implement कर रहा है
    सिद्धांत रूप में यह pipeline auxiliary definitions और lemmas बनाने जैसी बुनियादी theory-building भी सीख सकती है। यह proof assistance की holy grail के काफ़ी करीब है, और मुझे लगता है कि यह हमारे स्वाभाविक रूप से बनाए जाने वाले ज़्यादातर गणित को formalize करने में मदद करेगी। इंसान post-hoc rigorousization के तरीके से काम करेंगे, और details भरने में मशीन मदद करेगी

    • सहमत। यह बड़ी प्रगति है। Geometry problems अलग category में आते हैं, क्योंकि उन्हें polynomial equations के systems में translate करके well-known computer algebra algorithms से हल किया जा सकता है
      इसके उलट, इस तरह का open-ended formalization ऐसा क्षेत्र रहा है जहां प्रगति बहुत धीमी और incremental रही है। 5 साल पहले मैंने पास के क्षेत्र में काम किया था, और यह result traditional automated reasoning techniques से पहुंच से बाहर के स्तर का माना जा सकता है
      असली automated theorem proving pure mathematics से कहीं ज़्यादा व्यापक रूप से उपयोगी है। उदाहरण के लिए, किसी छोटे programming language की axiomatic semantics को Lean में लिखकर “दिखाओ कि इस specification को satisfy करने वाला program मौजूद है” जैसे सवाल पूछे जा सकते हैं
      अगर यह approach scale हुई, तो यह पिछले कुछ वर्षों में आई किसी भी machine learning application से ज़्यादा महत्वपूर्ण होगी
    • Search को कम मत आंकिए। यह brute force जैसा दिख सकता है, लेकिन search ने Go में human level को पार किया और IMO silver-medal level तक पहुंचा
      हमें बनाने वाला evolution भी जबरदस्त brute-force प्रयासों से चलने वाला search ही है, और scientific method की research भी मूल रूप से search ही है
    • इस क्षेत्र में पहले से लोग काम कर रहे हैं
      https://leandojo.org/
      https://machine-learning-for-theorem-proving.github.io/
      https://www.youtube.com/watch?v=P5ew0BrRm_I
      https://paperswithcode.com/task/automated-theorem-proving
      https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
      https://github.com/RiccardoBiosas/LeanGPT
    • ऐसे systems गणितीय research के बाहर कहीं ज़्यादा उपयोगी लगते हैं
      उपयोगी काम करने के लिए बहुत कठिन problems prove करना ज़रूरी नहीं है। कई बार साधारण चीज़ें prove करना ही काफ़ी होता है। अगर आप language model से task complete करवाएं, items organize करवाएं, schedule coordinate करवाएं, X करने वाला code लिखवाएं वगैरह, तो result पर तुरंत भरोसा करना मुश्किल होता है; लेकिन अगर system problem के कुछ हिस्से को logic में translate कर सके और solution खोज सके, तो उस पर भरोसा करना कहीं आसान हो जाएगा
    • नहीं। यह बस solution खोजने के लिए search engine इस्तेमाल करने की सुविधा देने जैसा है, इससे ज़्यादा नहीं

  • मुख्य बात थोड़ी दब गई है: ये लोग Lean इस्तेमाल कर रहे हैं
    यह गणित problems से आगे भी महत्वपूर्ण है। Machine learning models को proof systems से जूझने पर मजबूर करना आम बकवास से बचने का अच्छा तरीका है
    उम्मीद है आगे और लोग Lean या मिलते-जुलते systems में types लिखेंगे, और इसे prompts लिखने के कहीं बेहतर तरीके के रूप में इस्तेमाल करेंगे

    • AlphaProof निश्चित रूप से कमाल है, लेकिन IMO में यह computer को ऐसे फायदे भी देता है जो इंसानों के पास नहीं होते। कोई अपने दिमाग में Gröbner basis नहीं बनाएगा, लेकिन polyrith में बस आठ characters type करने होते हैं। मैंने AlphaProof को nlinarith इस्तेमाल करते हुए भी देखा है
    • हैरान करने वाला। मैं अभी comment करने ही वाला था कि इसे Lean से जोड़ दें तो जबरदस्त होगा। लगता है higher mathematics को आगे ऐसे ही जाना चाहिए। प्रमुख proofs इतने जटिल हो गए हैं कि लगभग कोई भी पूरा puzzle समझ नहीं पाता
      1. https://lean-lang.org/
    • इससे तो Riemann hypothesis को भी target करेंगे, hehe

  • Tim Gowers ने मुख्य caveats समझाते हुए और context देते हुए एक अच्छा छोटा overview दिया है। वे Fields medalist हैं और इस काम में भी शामिल थे: https://x.com/wtgowers/status/1816509803407040909

  • बात सही है, लेकिन हर देश की representative team में आना अपने आप में बहुत कठिन process है। Regional Math Olympiad, National Math Olympiad आदि, हर stage पर बहुत brutal filtering होती है
    उसके बाद इस elite group के लिए additional training होती है, और कुछ मामलों में extra selection भी हो सकता है
    संक्षेप में, किसी देश की IMO representative team में चुना जाना ही बड़ी बात है, और उसके अंदर gold या silver medal जीतना बस एक जबरदस्त achievement है

    • कुछ देश इन बच्चों को पूरे साल school से हटाकर IMO training पर focus करवाते हैं, और अपने देश की top universities में admission की guarantee भी देते हैं
      स्रोत: मेरा एक दोस्त जिसने IMO silver medal जीता था

  • जो लोग यह काम करके पैसे पाते हैं, उनसे सच में ईर्ष्या होती है। यह बेहद मज़ेदार दिखता है, और इस तरह cutting-edge स्तर को आगे बढ़ाना काफी संतोषजनक लगता होगा

    • ज़रूरी नहीं कि ऐसा ही हो। कई बार वे काम जो बहुत संतोषजनक होने चाहिए थे, बेहद उबाऊ या यहाँ तक कि नुकसानदेह दिशा में चले गए, और इसके उलट, ऊपर से सामान्य दिखने वाला काम सच में बहुत रोचक निकला
      काम की संतुष्टि में विषय से ज़्यादा work environment मायने रखता है। भले ही आप दुनिया बदलने वाले विषय पर काम कर रहे हों, अगर team खराब है तो मुश्किल समय गुज़रेगा। कुछ लोगों में हर मज़ा खींच लेने की कला होती है, office politics हर जगह होती है, और खासकर दुनिया बदलने वाले विषयों में तो और भी ज़्यादा
      इसके उलट, ग्राहक data को database में डालने जैसा सबसे उबाऊ दिखने वाला विषय भी हो, अगर team अच्छी हो, architecture अच्छी तरह design की गई हो, और experiments व knowledge sharing का समय हो, तो समय शानदार गुजर सकता है। बस अच्छी तरह काम करने वाली सरल चीज़ों की सुंदरता की मैं लगातार ज़्यादा कद्र करने लगा हूँ। ऐसी चीज़ें scientific breakthroughs से भी ज़्यादा दुर्लभ हो सकती हैं
      बेशक, शानदार work environment और शानदार विषय साथ भी आ सकते हैं, और वह jackpot जैसा होता है, इसलिए ईर्ष्या करने लायक है
    • मैं इसी field में, खास तौर पर LLM pretraining की तरफ काम करता हूँ। यह बाहर से दिखने जितना glamorous नहीं है। इसमें विशाल YAML संभालना और बड़े scale पर regex इस्तेमाल करना शामिल है। बेशक, यह बात थोड़ी simplify करके कही है
      ऐसा काम कर पाने को लेकर उत्साहित और आभारी होना चाहिए, लेकिन घटिया tools काम का बहुत सारा मज़ा छीन लेते हैं
    • शायद jealous नहीं, envious कहना चाहिए
    • हम जो सबसे अच्छा कर सकते हैं, वह है लगातार updated रहना और support करना
    • क्या अब K8s के लिए 3,292,329 lines वाली YML फिर से configure करने का समय नहीं है
      (/s)

  • मशीनों को इंसानों से बेहतर chess खेले हुए दशकों हो चुके हैं
    फिर भी किसी को फर्क नहीं पड़ता। सब Magnus Carlsen को देखने में व्यस्त हैं
    हम इंसान हैं, इसलिए हमें दूसरे इंसानों के किए कामों में रुचि होती है। मशीनों में हमारी रुचि सिर्फ तब तक होती है जब तक वे हमारे लिए उपयोगी हों
    यह सिद्धांत काम और कला पर भी व्यापक रूप से लागू होता है। जब तक इंसान मौजूद हैं, इन क्षेत्रों में इंसानों की जगह हमेशा बनी रहेगी

    • AI चाहे chess और art में कितना भी बेहतर हो जाए, इंसान उन्हें enjoy करते रहेंगे। इसी तरह, शौक के तौर पर गणित पढ़ने वाले लोग भी शायद बने रहेंगे
      लेकिन निकट भविष्य में ऐसे गणितज्ञ बचे रहेंगे या नहीं, जो AI द्वारा अधिकतर या पूरी तरह खोजे न गए नए गणितीय developments publish करें, इस पर मुझे बहुत संदेह है। इंसान को पहला सवाल पूछने की वजह से proof का credit मिल सकता है, लेकिन ऐसी दुनिया की संभावना कम है जहाँ computers meaningful math problems आसानी से हल कर सकते हों, फिर भी इंसानों से उन्हें धीमे और महंगे तरीके से हल करवाने पर ज़ोर दिया जाए
    • सही है, लेकिन उदाहरण के लिए अगर AI Goldbach conjecture साबित कर दे तो वह बहुत बड़ी बात होगी
    • consumer के नजरिए से इससे फर्क नहीं पड़ता कि meat-processing plant या Amazon warehouse 5000 लोगों को employ करता है या 5 लोगों को
      कला पर यह सिद्धांत निश्चित रूप से लागू होता है, लेकिन काम पर यह केवल कुछ या अधिकतर मामलों में लागू होता है
    • कुछ लोग मानते हैं कि chess या art के विपरीत गणित सच में उपयोगी है। अधिकांश गणितज्ञ शायद ऐसा नहीं सोचेंगे, लेकिन अगर थोड़ी देर के लिए इस पागलपन भरे विचार को मान लें, तो proof सिर्फ यह बताने वाला tool है कि “गणित के इस टुकड़े को सही ढंग से लागू किया गया”
      तब proof को समझने की ज़रूरत नहीं रहती, और किसी को फर्क नहीं पड़ता कि कहीं कोई गणितज्ञ उस proof को पूरी तरह समझता है या नहीं। मशीनों का proof खोजने और verify करने में हमसे बेहतर होना ठीक है, बल्कि अपेक्षित ही है
    • मुझे नहीं लगता कि यह सिद्धांत mathematical proofs पर अच्छी तरह लागू होता है। Proof बनाना जितना कठिन है, verify करना उससे कहीं, कहीं ज़्यादा आसान है, और दूसरा proof बस footnote बनकर रह जाता है
      बहुत से गणितज्ञ ऐसे काम में लगे रहना नहीं चाहेंगे। हालांकि IMO और research mathematics के frontier के बीच अभी भी बड़ा अंतर है

  • Theorem proving एक single-player game है जिसका search space अविश्वसनीय रूप से बड़ा है, इसलिए मैंने हमेशा सोचा था कि यह AGI से बहुत पहले solve हो जाएगा
    निजी तौर पर, मैं AlphaProof में सबसे बड़ा योगदान Lean और Mathlib के पीछे मौजूद लोगों का मानता हूँ। क्योंकि उन्होंने पूरे गणित को formalize करने जैसा भारी काम अपने ऊपर लिया
    गणितीय papers में formalization की कमी ने automation की कोशिशों को लगातार खत्म किया। क्योंकि AI researchers को authors की अपनी notation, implicit knowledge, और छोड़े गए proof steps जैसे मानवीय तत्वों से जूझना पड़ता था

    • “Theorem proving एक single-player game है जिसका search space बहुत बड़ा है, इसलिए यह AGI से बहुत पहले solve हो जाएगा” यह बात अजीब लगती है
      मेरे हिसाब से AGI शब्द खुद define नहीं है, लेकिन समझ नहीं आता कि “आम तौर पर बुद्धिमान कोई चीज़”, यानी median human-level intelligence बनाना, “Terrence Tao से बेहतर गणित करना” से कहीं ज़्यादा कठिन क्यों माना जाए
    • उन्होंने पूरे गणित को formalize नहीं किया है। अच्छी बात है कि IMO के लिए पूरे गणित की ज़रूरत नहीं होती। लेकिन उन्होंने IMO के लिए पर्याप्त मात्रा भी formalize नहीं की। शायद इसी वजह से वे combinatorics problem हल नहीं कर पाए

  • सबसे अच्छी चर्चा यहाँ है: https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...
 
chabulhwi 2024-07-26

  • सातवीं राय

    • सबसे अच्छी चर्चा LeanProver के Zulip chat में हुई

वह सबसे अच्छी चर्चा यहां देखी जा सकती है: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learnin…