ओलिम्पियाड स्तर का ज्योमेट्री AI सिस्टम AlphaGeometry

 (deepmind.google)
1 पॉइंट द्वारा GN⁺ 2024-01-18 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • International Mathematical Olympiad, AI mathematical reasoning की कसौटी बन गया है; इसी बीच AlphaGeometry ने 30 ज्योमेट्री समस्याओं में से 25 को निर्धारित समय में हल किया, जो मानव गोल्ड मेडलिस्ट औसत 25.9 के करीब है
  • इसकी मुख्य बात neural network language model और rule-based symbolic deduction engine का संयोजन है, जो intuitive construction suggestions और formal logic verification को एक ही loop में संभालता है
  • मानव demonstrations के बिना बनाए गए 100 मिलियन unique synthetic examples ने training bottleneck घटाया, और इनमें से 9 मिलियन में proof के लिए जरूरी auxiliary constructions शामिल हैं
  • सभी Olympiad solutions को computer से verify किया गया; Evan Chen ने आकलन किया कि output machine-verifiable होने के साथ human-readable भी है और छात्रों द्वारा इस्तेमाल किए जाने वाले classical geometry rules का पालन करता है
  • IMO के एक session में आमतौर पर 6 समस्याओं में से केवल 2 ही ज्योमेट्री की होती हैं, इसलिए application scope सीमित है; फिर भी सिर्फ ज्योमेट्री performance के आधार पर 2000 और 2015 IMO bronze medal cutoff पार कर सकने वाला यह पहला AI model बना

IMO ज्योमेट्री benchmark performance

  • Nature में प्रकाशित AlphaGeometry जटिल ज्योमेट्री समस्याओं को मानव Olympiad gold medalists के करीब स्तर पर हल करता है
  • Benchmark में 2000 से 2022 तक के Olympiads से चुनी गई IMO-AG-30 की 30 ज्योमेट्री समस्याएँ शामिल हैं
    • AlphaGeometry: निर्धारित समय में 25 हल कीं
    • मौजूदा best approach Wu’s method: 10 हल कीं
    • मानव gold medalist average: 25.9 हल कीं
  • Google DeepMind ने AlphaGeometry code और model को open source के रूप में जारी किया

Neural-symbolic system architecture

  • AlphaGeometry एक neural-symbolic system है, जिसमें neural network language model और symbolic deduction engine साथ मिलकर जटिल geometry theorems के proofs खोजते हैं
  • Language model data में general patterns और relationships को तेज़ी से identify कर उन constructions का अनुमान लगाता है जिनके उपयोगी होने की संभावना होती है
    • हालांकि, rigorous reasoning या decisions explain करने की क्षमता में कमी हो सकती है
  • Symbolic deduction engine formal logic और स्पष्ट rules का पालन करते हुए conclusions तक पहुँचता है
    • यह explainable और rational है, लेकिन बड़े problems को अकेले handle करते समय slow और कम flexible हो सकता है
  • दोनों components को साथ इस्तेमाल करने पर language model नए points, lines, circles जैसे auxiliary components सुझाता है, और deduction engine उनके आधार पर figure के बारे में additional conclusions निकालता है

Auxiliary constructions खोजने वाला solution loop

  • Olympiad geometry problems अक्सर दिए गए figure से सीधे हल नहीं होते; solution के लिए नए geometric components जोड़ने पड़ते हैं
  • AlphaGeometry की solving process में symbolic deduction और language model suggestions बारी-बारी से काम करते हैं
    • दिए गए figure और theorem premises से symbolic deduction engine नए propositions derive करता है
    • अगर solution नहीं मिलता या नए propositions बनना बंद हो जाते हैं, तो language model एक ऐसा auxiliary component जोड़ता है जिसके उपयोगी होने की संभावना होती है
    • जोड़ा गया component deduction engine के लिए नए paths खोलता है, और solution मिलने तक यह process दोहराई जाती है
  • 2015 International Mathematical Olympiad की problem 3 के लिए AlphaGeometry का solution 109 logical steps से बना था

100 मिलियन synthetic data generation

  • Geometry space, distance, shape और relative position की समझ पर आधारित है, और art, architecture, engineering जैसी कई fields की नींव है
  • AlphaGeometry की synthetic data generation method बड़े पैमाने पर उस प्रक्रिया की नकल करती है जिसमें इंसान figures को देखकर existing knowledge के आधार पर नई geometric properties और relationships खोजते हैं
  • System ने highly parallelized computing के जरिए 1 बिलियन random diagrams generate किए
    • हर diagram में points और lines के बीच सभी relationships को पूरी तरह derive किया गया
    • हर diagram में शामिल सभी proofs खोजे गए
    • उन proofs तक पहुँचने के लिए कौन से additional components जरूरी हैं, इसे reverse track किया गया
  • इस process को symbolic deduction and traceback कहा जाता है
  • विशाल data pool को similar examples हटाने के लिए filter किया गया, और आखिर में अलग-अलग difficulty वाले 100 मिलियन unique training examples बने
    • इनमें से 9 मिलियन cases में auxiliary components जोड़े गए थे
    • Language model ने auxiliary constructions से proof तक पहुँचने वाले कई examples सीखे, जिससे वह Olympiad problems में भी नए constructions सुझा सकता है

Verifiability और application limits

  • AlphaGeometry द्वारा दिए गए सभी Olympiad problem solutions को computer से check और verify किया गया
  • Results की तुलना पिछले AI methods और Olympiad में मानव performance से की गई
  • Mathematics coach और former Olympiad gold medalist Evan Chen ने कुछ solutions का मूल्यांकन किया
    • AlphaGeometry का output verifiable और clean है
    • पहले proof-based competition problems के AI solutions कभी सही और कभी गलत होते थे, इसलिए मानव verification की जरूरत पड़ सकती थी
    • AlphaGeometry के solutions machine-verifiable structure रखते हुए भी human-readable हैं
    • यह coordinate system के जरिए massive algebraic calculations को brute-force नहीं करता, बल्कि students की तरह angles और similar triangles जैसे classical geometry rules इस्तेमाल करता है
  • IMO का एक session 6 problems का होता है, और आमतौर पर उनमें से सिर्फ 2 geometry-focused होती हैं
    • इसलिए AlphaGeometry एक session की लगभग one-third problems पर ही लागू हो सकता है
    • फिर भी केवल geometry ability के आधार पर 2000 और 2015 IMO bronze medal cutoff पास कर सकने वाला यह पहला AI model बना

Mathematical reasoning AI की ओर विस्तार

  • AlphaGeometry दिखाता है कि AI की logically reason करने और नया knowledge discover और verify करने की क्षमता बढ़ रही है
  • Olympiad-level geometry problems हल करना गहरे mathematical reasoning और अधिक advanced general-purpose AI systems की दिशा में एक महत्वपूर्ण milestone है
  • Large-scale synthetic data से AI को scratch से train करने का approach mathematics से आगे science और AI में नए knowledge discovery methods को प्रभावित कर सकता है
  • AlphaGeometry, Google DeepMind और Google Research के mathematical reasoning AI workstreams पर आधारित है
  • Long-term goal ऐसा AI system बनाना है जो कई mathematical fields में generalize करे, general-purpose AI systems के लिए जरूरी sophisticated problem solving और reasoning विकसित करे, और human knowledge की boundaries को expand करे

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

1 टिप्पणियां

 
GN⁺ 2024-01-18
Hacker News की राय

  • IMO जैसी प्रतियोगिताओं के लिए problem setter रह चुका हूं, और इस नज़रिए से मैंने यह पेपर बहुत दिलचस्पी से पढ़ा। साथ ही मुझे लगता है कि AI, यानी स्मार्ट knowledge index और reasoning-method index, के सामने सबसे पहले ढहने वाला विषय ज्यामिति ही होना था
    गणित ओलंपियाड के विषयों में ज्यामिति के प्रश्न आम तौर पर सबसे ज़्यादा “mechanical” होते हैं। अगर किसी समस्या को coordinates, जैसे XY coordinates या complex plane, में व्यक्त किया जा सके, तो कंप्यूटर के पास समाधान खोजने के लिए इस्तेमाल किए जा सकने वाले सीमित चरणों का एक सेट बन जाता है। बेशक IMO के वास्तविक माहौल में time limit और मानवीय गलतियां इसे व्यावहारिक होने से रोकती हैं। पहले मैं इसी तरह अपने बनाए हुए ज्यामिति प्रश्नों और conjectures के proofs को WolframAlpha से verify किया करता था
    बीजगणित, खासकर inequalities, भी कुछ ऐसा ही है; ज़ोरदार computation लगा दें तो अक्सर जवाब निकल आता है
    जिस क्षेत्र में मैं intelligent systems की असली प्रगति देखना चाहता हूं, वह number theory और combinatorics है। search space कहीं ज़्यादा जटिल है, और अक्सर यह साबित करना पड़ता है कि कोई चीज़ असंभव है। ऐसे प्रश्न brute-force computation से हल करना मुश्किल है

    • उन समस्याओं को हल करने वाले के रूप में, पहले तो धन्यवाद। हाई स्कूल खत्म हुए दशकों हो गए, फिर भी कभी-कभी उन्हें मज़े से हल करता हूं
      मैं सहमत हूं कि ज्यामिति पहले आएगी। यहां मैंने जो देखा, उसमें algebraic geometry, vectors, complex-number solutions पर निर्भर करने के अर्थ में यह “brute force” नहीं है, लेकिन “दिलचस्प” auxiliary constructions को खंगाल कर खोजने के अर्थ में यह brute-force search के करीब है
      ज्यामिति हमेशा मेरा सबसे खराब विषय था, लेकिन सही construction मिल जाए तो समस्या बहुत आसान हो जाती है, ऐसा मुझे लगता था। बस ऐसे constructions जल्दी सूझने की intuition मैं विकसित नहीं कर पाया। इस AI में भी वैसी intuition लगती नहीं है, लेकिन यह उन्हें कहीं तेज़ी से उगल सकता है। perpendicular lines, parallel lines, angle bisectors जैसी बनाई जा सकने वाली candidates आखिरकार सीमित ही हैं, और angles और ratios को पूरा फैलाकर देखने या power of a point आज़माने जैसे तरीकों से उन्हें काफी mechanical तरीके से evaluate किया जा सकता है
      बहुत प्रभावशाली है, लेकिन “engine बनाम AI” के अर्थ में यह DeepMind:Kasparov::AlphaGeo:Terry Tao जैसा दिखता है
      मैं सहमत हूं कि अगला नंबर शायद algebra का होगा। ज्यामिति की तरह, आम तौर पर बस एक-दो-तीन clever substitutions खोजनी होती हैं, और choices सीमित होती हैं
      combinatorics की कुछ समस्याएं भी इस search strategy में फिट हो सकती हैं। उदाहरण के लिए, एक ही object को दो तरीकों से count करने वाली समस्याएं। लेकिन वह पुल अभी और दूर है, और कुल समस्याओं में से केवल कुछ को ही पकड़ पाएगा
      number theory शायद पूरे 42 अंक तक पहुंचने से पहले की आखिरी सीमा होगी
    • ऐसे developments को सकारात्मक रूप से देखने वाला रवैया अच्छा है। मुझे उत्सुकता है कि गणित में बहुत अच्छा होने की क्षमता भी जल्द ही मशीनों के हाथों पीछे छूट सकती है, इस संभावना से क्या आपको कोई loss महसूस होता है? या आपको लगता है कि ऐसा निकट भविष्य में होने की संभावना नहीं है?
    • मुझे उत्सुकता है कि ऐसे problem setter के पद तक आप कैसे पहुंचे। क्या कोई तरह की application process होती है?
      यह verify करने के बाद कि समस्या हल की जा सकती है, final problem set में कौन-सी खास problems जाएंगी, यह कैसे चुना जाता है, यह भी जानना चाहूंगा। voting से, या किसी और evaluation method से?
    • शुरू में मुझे लगा था कि तीन-variable inequalities सबसे पहले ढहेंगी। क्योंकि किसे proof माना जाए, इस बारे में ambiguity कम होती है। लेकिन मुझे नहीं पता था कि पीछे वाली problem तो 2000 में ही solve हो चुकी थी (http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf)
      किसी को synthetic geometry को adventure game बनाना चाहिए। Lean से सरल proof-writing language इस्तेमाल की जा सकती है, और visually भी अच्छा बनाया जा सकता है

  • अगर मैंने पेपर सही पढ़ा है, तो यह सचमुच का काम लगता है। पिछले महीने DeepMind ने खुले गणितीय शोध-समस्या को हल करने का दावा करते हुए जिस AI गणित पेपर का गलत प्रचार किया था, उससे यह कहीं ज़्यादा जायज़ है। फिर भी इसकी संरचना आम तौर पर सोची जाने वाली automated reasoning/intelligence से कितनी अलग है, यह काफ़ी साफ़ दिखता है
    मेरी समझ यह थी कि Transformer को लाखों elementary geometry theorems पर train किया गया है और proof की brute-force search में इस्तेमाल किया जाता है। elementary geometry के संदर्भ की वजह से संरचना अनिवार्य रूप से elementary है, और true/false को symbolically आसानी से तय किया जा सकता है। मुझे लगा कि जब brute-force search fail हो जाती है, तो midpoint जोड़ने जैसे auxiliary geometric constructions random तरीके से और जोड़े जाते हैं, और देखा जाता है कि उन अतिरिक्त materials से search हो पाती है या नहीं
    edit: Imnimo के correction के मुताबिक, मैंने इसे उल्टा समझा था। brute-force search शुद्ध brute-force search है, और Transformer का इस्तेमाल यह predict करने के लिए होता है कि कौन-सा auxiliary construction जोड़ा जाए
    साथ ही, blog post में नहीं है, लेकिन असली problem statements को भी modify/adapt करना पड़ा था। उदाहरण के लिए original “मान लें triangle ABC की altitudes AH1, BH2, CH3 हैं…” जैसा वाक्य, “ABC को एक triangle मानें। AI point I को इस तरह define करे कि वह angle BAC का bisector हो और CI angle ACB का bisector हो…” जैसी कहीं अधिक explicit definitions की list में बदल गया, और अंत में “T1I=IZ prove करें” के रूप में हो जाता है

    • यह explanation थोड़ी सही नहीं लगती। brute-force search Transformer नहीं, बल्कि symbolic solver करता है। जब नए inferences नहीं निकलते, तब Transformer से possible auxiliary constructions suggest कराए जाते हैं; इन्हें random तरीके से नहीं जोड़ा जाता
    • समझ नहीं आता कि इसे automated reasoning/intelligence के सामान्य विचार से दूर क्यों माना जा रहा है। reasoning मूल रूप से search problem ही है
      आपने जो process बताया है, वह इंसानों के इस्तेमाल किए जाने वाले process जैसा ही है। जो चीज़ उपयोगी लगती है उसका guess लगाते हैं, फिर details को mechanically solve करते हैं। अटकने पर दूसरा guess करते हैं। अंततः यह tree search करने जैसा ही है
      लोगों ने 1955 में ही यह process समझ लिया था, और theorem prove कर सकने वाला working prototype भी बना लिया था: https://en.wikipedia.org/wiki/Logic_Theorist असली बात अच्छी heuristics इस्तेमाल करने पर निर्भर करती है। neural networks data से heuristics निकाल सकते हैं, इसलिए यहाँ इसका मतलब बनता है
      मुझे जिज्ञासा है कि आप “automated reasoning” का सामान्य विचार क्या मानते हैं। क्या कोई magical device जो किसी भी problem को एक single linear pass में solve कर दे?
    • “brute-force search fail होने पर midpoint जोड़ने जैसे auxiliary geometric constructions जोड़कर, उन extra materials से search हो सकती है या नहीं देखना” बिल्कुल वैसा ही था जैसा school में geometry सीखी थी, और मुझे यह सच में नापसंद था
      university में mathematics department में जाने के बाद ही सही तरीका सीख पाया और इसका आनंद ले पाया
    • auxiliary lines खींचने की भूमिका में LLM का इस्तेमाल बहुत inefficient है। एक simple IMO problem solve करने के लिए ढेर सारी machines लगती हुई कल्पना करना मुश्किल है
      यह field अभी शुरुआती stage में है, और बहुत काम बाकी लगता है। search वाले हिस्से को छोटे neural network से replace करना चाहिए, और reasoning वाला हिस्सा मुश्किल नहीं है तथा उसमें बहुत बड़े सुधार की ज़रूरत भी नहीं लगती
      अब self-play से performance बढ़ाने का समय है। plane geometry problem में जिस conclusion को prove करना है उसे figure के एक point के रूप में, और conditions को दूसरे point के रूप में देखा जा सकता है, और दो players को data share करते हुए जितना हो सके एक-दूसरे की ओर move करने दिया जा सकता है। इस process में हर player के contribution को Go के win/loss calculation से तुलना करके performance improvement में इस्तेमाल किया जा सकता है

  • यह specific model generalize कर पाएगा ऐसा नहीं लगता, लेकिन neuro-symbolic approach बहुत promising लगती है
    यह current machine learning के ज़्यादातर, यानी लगातार powerful होते जा रहे “System 1” tools को logical proof generation जैसे structured “System 2” tools से जोड़ने का तरीका है। System 2 plan बना सकता है और output की truthfulness या value check कर सकता है
    System 2 तब तक आगे बढ़ता है जब तक अटक न जाए, और अटकने पर System 1 intuitively guess देता है कि state space के किस हिस्से को next check करना है
    यहाँ computer से proofs generate किए जा सकते हैं, इसका उपयोग करके 100 million proofs का dataset बनाया गया, जिससे scalable self-supervised learning संभव हुई। symbolic domains ऐसे data generation की अच्छी अनुमति देने वाले रूप में दिखते हैं। individual instances की value कम हो सकती है, लेकिन मिलकर वे useful pretraining को संभव बना सकते हैं
    इन elements को मिलाने पर यह approach काफ़ी दूर तक जा सकता है
    मुख्य milestone यह है कि किसी specific formal/symbolic domain पर निर्भर रहने की ज़रूरत से बाहर निकला जाए, और ऐसा pretraining system बनाया जाए जो उस domain में सीखी गई techniques को generalize कर सके

    • सब कुछ एक साथ solve करने की ज़रूरत नहीं है। इस approach में mathematics और programming दोनों को बदलने की क्षमता है। क्योंकि यह formal verification को सिर्फ़ niche tools, जिनका कुछ ही उपयोग होता है, से उठाकर सभी practitioners के सामान्य toolbox का हिस्सा बना सकता है
      साथ ही applicable domain के अंदर, यह मौजूदा AI trend में “hallucination” कहे जाने वाले एक fundamental problem को पूरी तरह solve करता है। हालांकि वह solution इसलिए संभव है क्योंकि accuracy prove करने वाला non-AI system मौजूद है
      बड़े picture में यह approach बहुत नया नहीं है। biochemistry में AI से candidate molecules खोजने और physics experiments से verify करने का तरीका इस्तेमाल होता रहा है
      combinatorial game AI भी AI को पुराने तरीके की Monte Carlo search के input के रूप में लंबे समय से इस्तेमाल करता रहा है
    • यह किसी तरह की artificial general intelligence तक पहुँचने की सबसे नज़दीकी संभावना जैसा लगता है

  • पेपर के साथ code और weights release करने के लिए आभारी हूँ। जहाँ तक मुझे याद है, executable reasoning code और checkpoint release करने वाला यह पहला famous DeepMind paper है। अगर इससे पहले कोई case है तो correction welcome है
    अभी released training set या example training code नहीं दिख रहा, लेकिन फिर भी उन्होंने कुछ ऐसा दिया है जिस पर दूसरे researchers build कर सकते हैं—यह अच्छी प्रगति है। आखिर academic paper का उद्देश्य भी यही होता है

    • dataset भी missing है, यह अफ़सोस की बात है। कहा गया है कि उन्होंने 100 million synthetic examples बनाए; क्या ये examples AlphaGeometry से generate किए गए थे? इस synthetic data को बनाने के लिए filtering code और initial inputs कहाँ हैं?
      अगर मैं गलत नहीं हूँ तो क्या t5 model इस्तेमाल हो रहा है? कम-से-कम SentencePiece t5 vocabulary इस्तेमाल होती दिखती है
      यह भी जानना चाहूँगा कि इस model training में कितना GPU time लगा, और कौन-से training parameters इस्तेमाल हुए
      गलत न समझें। यह system fascinating है, और applied engineering कैसी होनी चाहिए यह दिखाता है। बस training details, initial data, और synthetic data generation method के बारे में और जानना चाहता हूँ

  • मैं बहुत उत्सुक हूँ कि language model उपयोगी constructions कितनी बार बनाता है। जाहिर है, यह random से बेहतर होगा, लेकिन समझ नहीं आता कि वह कोई अच्छा construction मिलने तक हजारों constructions फेंकता है, या फिर मानव विशेषज्ञ जैसी दर से उपयोगी सुझाव देता है
    पेपर में कहा गया है कि “क्योंकि language model decoding प्रक्रिया k अलग-अलग sequences लौटाती है जो k वैकल्पिक auxiliary constructions का वर्णन करती हैं, इसलिए प्रत्येक beam के score को value function की तरह इस्तेमाल करते हुए इन k options पर beam search किया जाता है। इस setup में beams के बीच parallelization बहुत आसान है, इसलिए parallel computing resources उपलब्ध हों तो यह काफी तेज हो जाता है। प्रयोगों में beam size k=512, maximum iterations 16, और प्रत्येक node का branching factor, यानी decoding batch size 32 इस्तेमाल किया गया”
    लेकिन 512 और 16 कुल प्रस्तावित constructions की संख्या में कैसे बदलते हैं, यह मुझे पूरी तरह समझ नहीं आया। यह भी कहा गया है कि beam size और maximum iterations हटाने पर भी performance केवल कुछ हद तक ही घटती है। क्या इसका मतलब है कि model वास्तव में उपयोगी constructions को top पर काफी अच्छी तरह रखता है, और केवल सबसे कठिन समस्याओं में ही हजारों की जरूरत पड़ती है?

    • मेरा निजी अनुमान है कि यह हिस्सा भाषा और मानव-मशीन analogy की सीमाओं से जोरदार टकराता है
      फिर भी कोशिश करें तो summary 262,144 है, लेकिन इसे शाब्दिक रूप से नहीं लेना चाहिए
      decoding function का output tokens होता है, जो roughly शब्दों के 3/4 जितना होता है, लेकिन मान लेते हैं कि 1 token = 1 शब्द
      प्रति output token विचार किए जाने वाले tokens की संख्या beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262,144 है
      sample solution के शब्दों की संख्या गिन सकते हैं: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      solution के कुल tokens 2289 हैं, और विचार किए गए कुल tokens 262,144 * 2289 = 600,047,616 हैं
      जबरन गणना में “विचार किए गए solutions की संख्या” को कुल विचार किए गए tokens / solution के कुल tokens मानें, तो 262,144 आता है। यह हर iteration step में देखे गए tokens की संख्या के बराबर है, इसलिए बात बनती है

  • यह दिलचस्प है कि इस्तेमाल किया गया Transformer छोटा है। पेपर के मुताबिक इसे Meliad library की default settings से train किया गया, और इसमें 12 layers, embedding dimension 1,024, 8 attention heads, तथा ReLU activation का उपयोग करने वाली dimension 4,096 की inter-attention dense layer है
    input और output heads की embedding layers को छोड़ दें, तो पूरे Transformer में 151 million parameters हैं। custom tokenizer को SentencePiece के ‘word’ mode में train किया गया और vocabulary size 757 है। maximum context length 1,024 tokens तक सीमित रखी गई और T5-style relative position embeddings का इस्तेमाल किया गया। sequences में से 90% से अधिक length 200 से कम हैं, इसलिए sequence packing भी इस्तेमाल की गई

    • इसे छोटा कहना मुश्किल है। LLM field के बाहर यह काफी सामान्य आकार है। उदाहरण के लिए, यह सामान्य आकार के language model, translation model, या acoustic model जैसा है। कुछ लोग इसे भी बड़ा कहेंगे
    • यह result संकेत देता है कि अगर ठीक से formalize किया जा सके, तो Transformer के लिए hard sciences में हाथ लगाने लायक और भी low-hanging fruit हो सकते हैं। यह मामला scaling size की समस्या नहीं लगता

  • मेरे लिए सच में नई बात यह थी कि पिछला state-of-the-art system भी ऐसी 10 समस्याएँ हल कर सकता था। मैंने सुना था कि plane geometry problems के लिए decision algorithms होते हैं, लेकिन नहीं पता था कि वे practical algorithms हैं। खोजने पर reference के रूप में http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf मिला

    • सही। और AlphaGeometry का non-neural हिस्सा, यानी symbolic processing और linear algebra components भर से भी पिछली best performance को पार किया जा सकता है। यहाँ काफी काम neural network के अलावा वाले components में भी गया है
    • दिलचस्प है, लेकिन Evan Chen की किताब में दिए formulas से barycentric coordinate calculations को brute-force किया जाए, तो लगता है कि आधुनिक laptop पर भी IMO की करीब 30% समस्याएँ हल हो सकती हैं। यह देखते हुए कि ज्यादातर triangle problems हैं, ऐसा संभव लगता है

  • ऐसे results को लेकर मैं आम तौर पर “यह मानव proof जैसा नहीं है” वाली शंका के लिए तैयार था, लेकिन जब देखा कि Evan Chen ने इसे सचमुच साफ और इंसान के पढ़ने लायक proof कहा है, तो मेरा विचार बदल गया
    Evan Chen olympiad math community में प्रसिद्ध व्यक्ति हैं और एक मशहूर olympiad geometry book के author भी हैं[1], इसलिए इस बार मानना पड़ेगा कि machine ने IMO problems के कुछ हिस्से को वाकई जीत लिया है
    [1]: https://web.evanchen.cc/geombook.html

    • हालांकि supplementary material[1] के पूरे proof में IMO P3 proof Fig1.f और Step 26 में गलती लगी। उसमें ∠GMD = ∠GO2D कहा गया है, लेकिन यह गलत है और मुझे लगता है कि ∠GMD + ∠GO2D = π होना चाहिए। मैंने logic follow करने की कोशिश की, लेकिन Step 25 समझ नहीं पाया। लगा कि शायद यह step hallucination है
      फिर भी O2 के nine-point circle पर होने का idea सही है
      edit: मैं अपनी बात वापस लेता हूँ। लगता है कि वे directed angles[2] इस्तेमाल कर रहे हैं, और तब वह statement सही है
      [1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      [2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...

  • इससे जुड़ा https://www.nytimes.com/2024/01/17/science/ai-computers-math... भी देखने लायक है
    यह https://news.ycombinator.com/item?id=39030186 के जरिए आया है, और संबंधित थ्रेड को यहां मर्ज किया जाएगा

  • संबंधित: https://aimoprize.com/
    IMO में अच्छा प्रदर्शन करने वाले model के लिए 1 करोड़ डॉलर का इनाम