Lean4 ने टेरेंस टाओ के हालिया शोधपत्र में एक छोटा बग खोजने में मदद की
(mathstodon.xyz/@tao)- Terence Tao ने Lean4 formalization project पर काम करते हुए शोधपत्र में एक छोटा लेकिन गैर-तुच्छ त्रुटि पाई
- यह त्रुटि arXiv पेपर
2310.05328के पेज 6 के तर्क में सामने आई, जहाँ1/2 log((n - 1)/(n - k - 1))n = 3, k = 2पर diverge करता है - समस्या केवल छोटे
nमानों तक सीमित है;n >= 8पर मौजूदा तर्क काम करता है और छोटेnको अधिक मोटे तरीके से सीधे संभाला जा सकता है - Lean ने
0 < n - 3का प्रमाण माँगा, लेकिन उपलब्ध मान्यता केवलn > 2थी, इसलिएlinarithtactic आवश्यक विरोधाभास नहीं निकाल सकी - Tao कुछ numerical constants समायोजित कर तर्क को ठीक करने वाले हैं, और नए संस्करण में एक footnote जोड़ेंगे कि पुराना तर्क Lean formalization की कोशिश के दौरान थोड़ा अशुद्ध पाया गया
Lean4 formalization से उजागर हुई त्रुटि
- Terence Tao ने अपने Lean4 formalization project के दौरान पाया कि शोधपत्र में एक छोटी लेकिन गैर-तुच्छ बग है
- formalization का लक्ष्य arXiv पेपर
2310.05328के पेज 6 का तर्क था - समस्या वाला व्यंजक इस प्रकार है
1/2 log((n - 1)/(n - k - 1))
- यह व्यंजक
n = 3, k = 2होने पर diverge करता है
त्रुटि का दायरा और सुधार का तरीका
- यह समस्या केवल छोटे
nमानों पर होती हैn >= 8पर संबंधित तर्क अब भी काम करता है- छोटे
nको अधिक मोटे तरीके से सीधे संभाला जा सकता है, लेकिन constants और खराब हो जाते हैं
- Tao का मानना है कि उस पेज के कुछ numerical constants बदलकर तर्क को ठीक किया जा सकता है
- शोधपत्र के नए संस्करण में एक footnote जोड़ा जाएगा कि पुराना तर्क थोड़ा अशुद्ध था और यह बात Lean से formalize करने की कोशिश में पता चली
Lean जहाँ अटक गया, वह विशिष्ट बिंदु
- जहाँ formalization विफल हुई, वहाँ Lean ने
0 < n - 3साबित करने को कहा- उपलब्ध मान्यता केवल
n > 2थी linarithtactic,0 < n - 3के निषेध से विरोधाभास नहीं निकाल सकी
- उपलब्ध मान्यता केवल
1 टिप्पणियां
Hacker News की रायें
उन्होंने इस महीने की शुरुआत में GPT-4 की मदद से Lean4 सीखना शुरू किया था: https://mathstodon.xyz/@tao/111208692505811257
इस महीने उनकी Mastodon पोस्ट्स में से काफी कुछ सीखने की प्रगति के बारे में था, और यह एक दिलचस्प उदाहरण है कि large language models शीर्ष स्तर के achievers के काम को भी कितना तेज़ कर सकते हैं
दिलचस्प बात यह है कि अगर ऐसे tools का प्रभावी इस्तेमाल सिर्फ highly skilled लोग ही करें, तो ये असमानता को और बढ़ा भी सकते हैं
अगर Lean4 को आसान तरीके से आज़माना चाहते हैं तो Natural Number Game अच्छा है: https://adam.math.hhu.de/#/g/hhu-adam/NNG4
अगर game के बिना सिर्फ पढ़ना चाहते हैं, तो यहां: https://lean-lang.org/theorem_proving_in_lean4/introduction.html
शुरुआत में मैंने Alloy को Allow लिख दिया था
कुछ साल पहले, अपने लिखे programs में गलतियां कम करने का तरीका खोजते हुए मुझे Lamport का TLA+ पता चला, और मैंने state machine के रूप में program behavior सोचते हुए formal specifications लिखना सीखा
TLA+ ने abstractions को साफ़ समझने में मदद की, और बाद में Coq proof assistant का इस्तेमाल करके formally correct software बनाने वाली Software Foundations series भी मिली। exercises छोटे games जैसी थीं, इसलिए उन्हें हल करना काफी मज़ेदार लगा: https://softwarefoundations.cis.upenn.edu/
high-level abstraction वाली formal specification, code को explain करने के लिए dedicated language पर focus करती है, जबकि low-level abstraction वाले code contracts, verification logic को बेहतर model से replace करने के करीब होते हैं। C# में कभी Code Contracts[1] था, और Z3 SMT solver[2] से compile time पर contracts check करने का यह simple लेकिन powerful तरीका था, लेकिन कुछ साल बाद इसे बंद कर दिया गया[3], और .NET Runtime से हटाए जाने के साथ यह प्रभावी रूप से खत्म हो गया। अभी C# में सबसे करीब शायद Dafny[4] है, और C# development side अब भी इसे सीधे language में डालने का तरीका सोच रही है[5]
[1] https://www.microsoft.com/en-us/research/project/code-contracts/
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
[4] https://github.com/dafny-lang/dafny
[5] https://github.com/dotnet/csharplang/issues/105
Idris2 एक general-purpose language बनने का लक्ष्य रखता है, फिर भी theorem proving के लिए ज्यादा advanced type system देता हुआ लगता है: https://github.com/idris-lang/Idris2
Coq की जगह Agda का इस्तेमाल करने वाली, कुछ हद तक derived book भी है: https://plfa.github.io/
अभी पढ़ नहीं पाया हूं, लेकिन list में रखी है, और मुझे लगता है Agda या Idris के Coq की तुलना में programming language जैसे महसूस होने की संभावना ज़्यादा है
dependent types को लेकर सच में उत्साह है। हालांकि कुछ समय तक इनके आने की संभावना कम लगती है
Dependent Haskell पर काम चल रहा है, लेकिन कहा जाता है कि मौजूदा language में बाद में इसे जोड़ना मुश्किल है, और Idris के creator ने भी कहा था कि वे उम्मीद करते हैं Idris दूसरी languages के लिए model बने, लेकिन mainstream adoption मुश्किल दिखता है। Coq, Agda, F* भी general-purpose languages के रूप में design नहीं किए गए हैं। compiler implementation जटिल है और syntax भी verbose हो सकता है, लेकिन जो मैं चाहता हूं वह simplicity है। input और output के बारे में जो कुछ भी पता है, उसे encode करना चाहता हूं। अभी mainstream languages में अक्सर arguments या output के बारे में हमें type system जितना express करने देता है, उससे अधिक पता होता है
TypeScript जैसी gradual approach में, हर जगह सब कुछ prove किए बिना arbitrary जगहों पर type-level value constraints की जानकारी जोड़ पाना अच्छा होगा
उदाहरण के लिए, अगर आपको numbers की list और उसकी length दोनों पता हैं, तो dependent types से ऐसी list type बना सकते हैं जिसमें length explicitly शामिल हो, और compile time पर यह guarantee कर सकते हैं कि operations उस length को बनाए रखें। अगर आपने function को केवल length 3 वाली list लेने के लिए specify किया है और length 4 वाली pass कर दी, तो compile नहीं होगा, जिससे runtime से पहले गलती पकड़ी जा सकती है। यह types को ज़्यादा expressive बनाता है और variables के बीच जटिल relationships तक encode करने वाली extra safety-check layer जैसा लगता है
अगर हमारी पीढ़ी के सबसे तेज़ दिमागों में से एक large language models और automated proving के संयोजन से अपने काम का दायरा बढ़ा सकता है, तो इस तकनीकी संयोजन का भविष्य बहुत आशावादी दिखता है
शुरुआत bug fixes से होगी, फिर verification में मदद मिलेगी, और आखिरकार यह नई discoveries को आगे बढ़ाएगा और सीमाएँ फैलाएगा। Moore's law जैसी dynamics जब उन क्षेत्रों को “infect” करती हैं जिनमें मूल रूप से ऐसी cumulative प्रकृति नहीं थी, तो इस घटना के लिए कोई शब्द चाहिए। अतिरिक्त संदर्भ के तौर पर, Terence Tao Lean सीखने के लिए Copilot का इस्तेमाल कर रहे हैं: https://mathstodon.xyz/@tao/111271244206606941
शायद वे Copilot के बिना भी कर सकते थे, लेकिन नए tool को अपनाने की friction के कारण शायद शुरुआत ही न करते। Large language models में ऐसे “सोच की साइकिल” जैसे हालात में बड़ी संभावना है
कुछ साल पहले Terence Tao के math blog post में भी मैंने एक bug ढूँढा था। उन्हें बताया तो उन्होंने उसे ठीक किया और धन्यवाद भी दिया
बेशक, वह Hacker News के front page पर नहीं आया
मैं चिंतित था कि Lean4 कहीं एक और large language model न हो, लेकिन असल में यह काफ़ी मज़बूत और भरोसेमंद tool निकला
मुझे यह जानने में दिलचस्पी है कि क्या Lean proof checker जैसे formal proof checker को, Lean जैसी formal language में synthetic conjecture-proof pairs बनाने वाले language model के साथ जोड़ा जा सकता है
Lean proof checker से language model द्वारा लिखे गए synthetic proofs को अपने-आप verify किया जा सकता है, और उस जानकारी को मूल language model पर लागू होने वाले reinforcement learning reward signal की तरह इस्तेमाल करके उससे बेहतर proofs लिखवाए जा सकते हैं। या पिछले rounds के सही synthetic proofs को training data बनाकर नया model train किया जा सकता है। इसे और adversarial भी बनाया जा सकता है। conjecture generation model और proof/disproof model में बाँटकर, एक ऐसा model जोड़ा जाए जो यह predict करे कि synthetic proof Lean proof checker में verify होगा या नहीं। predicted correctness probability जितनी कम होगी, वास्तव में सही proof देने पर proof generation model को उतना बड़ा reward मिलेगा। अंत में, किसी खास synthetic conjecture के लिए proof generation model को मिलने वाले reward को predict करने वाला model जोड़ दिया जाए, तो conjecture generation model को ऐसे high expected reward conjectures बनाने के लिए reward मिलेगा जो proof generation model के लिए न बहुत कठिन हों, न बहुत आसान। पूरा system धीरे-धीरे और कठिन synthetic proofs बनाएगा, और यह proof generation model की बेहतर self-learning में बदल सकता है। सिद्धांत रूप में यह proof generation में superhuman क्षमता तक scale हो सकता है, और GAN या AlphaGo Zero के self-play जैसा है। कठिन हिस्सा शुरुआती bootstrapping है, क्योंकि generation model की शुरुआती training के लिए इंसानों द्वारा दिए गए Lean proof data की जरूरत होगी। लेकिन synthetic proofs पर्याप्त अच्छे हो जाएँ तो system अपने-आप self-learning जारी रख सकता है
आखिरकार हमें ऐसा model मिल सकता है जो mathematical literature के सभी theorems और सभी सही proofs जानता हो
मौजूदा proofs से supervised learning शुरू करके नए proofs खोजने के शुरुआती चरण के रूप में TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms) आदि हैं। ज्यादातर के अंदर किसी-न-किसी रूप में language model है, लेकिन अगर आप हाल में बड़ी चर्चा में रहे large language models ढूँढ रहे हैं, तो GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910), COPRA (https://arxiv.org/abs/2310.04353) हैं। हालांकि फिलहाल ये models specialized non-LLM tools जितने प्रभावी नहीं लगते। इंसानों द्वारा लिखे proofs से आगे बढ़कर reinforcement learning से सीखने वाली दिशा में TacticZero (https://openreview.net/forum?id=edmYVRkYZv), OpenAI paper (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), HOList family का काम (https://arxiv.org/pdf/1905.10006.pdf), HyperTree Proof Search (https://arxiv.org/abs/2205.11491) हैं, और University of Massachusetts team और मेरे द्वारा चल रहा काम भी है
Tao ने इस यात्रा में GPT-4 सहित large language model tools का कैसे इस्तेमाल किया, इस पर पिछला context यहाँ है: https://mathstodon.xyz/@tao/111233986893287137
उनकी progress को GitHub पर भी follow किया जा सकता है: https://github.com/teorth/symmetric_project/