अनुवाद में खोया हुआ Navier–Stokes
OpenAI के Navier–Stokes blow‑up परिणाम के कथित समाधान पर एक नई आलोचना का तर्क है कि औपचारिक रूप से सत्यापित Lean proof और उसके साथ दिया गया natural-language proof वास्तव में मेल नहीं खाते। टिप्पणीकारों का ज़ोर है कि भले ही Clay Millennium problem का Lean formalization सही और machine-checkable दिखता हो, English exposition intermediate claims या reasoning को गलत ढंग से प्रस्तुत कर सकती है, जिससे वह मनुष्यों के लिए पढ़ने योग्य व्याख्या के रूप में कम उपयोगी हो जाती है। यह अंतर informal mathematics और formal proof systems के बीच अनुवाद में LLMs की व्यापक समस्याओं, automated verification की सीमाओं, और computer-checked proof होने पर भी पारंपरिक peer review और interpretability की आवश्यकता पर सवाल उठाता है.
Lean बनाम प्राकृतिक-भाषा (NL) प्रमाण
- मुख्य मुद्दा: पेपर का तर्क है कि OpenAI का Navier–Stokes blow-up का Lean प्रमाण उनके PDF में दिए गए NL प्रमाण से मेल नहीं खाता।
- कई टिप्पणीकार इस बात पर ज़ोर देते हैं: Lean प्रमाण और NL प्रमाण दोनों अपने-अपने स्तर पर सही हो सकते हैं, लेकिन वे एक ही तर्क नहीं हैं, और Lean प्रमाण NL विवरण की औपचारिक पुष्टि नहीं करता।
- NL → Lean अनुवाद कठिन है: बहुअर्थी प्रतीक, अनकहे परंपरागत अर्थ, और संदर्भ गणितीय गद्य को अस्पष्ट बना देते हैं।
क्या प्रश्न में है और क्या नहीं
- व्यापक सहमति: थ्रेड में कोई भी गंभीर रूप से इस बात पर विवाद नहीं करता कि Navier–Stokes कथन का Lean formalization (जैसा कि पहले के “formal conjectures” कार्य में लिखा गया था) सही है और Lean प्रमाण type-check करता है।
- पेपर के लेखक स्पष्ट रूप से कहते हैं: वे यह दावा नहीं करते कि NL प्रमाण गलत है, केवल यह कि विभिन्न NL → Lean अनुवाद (Navier–Stokes/Euler कार्य से जुड़े कुछ अनुवाद सहित) आपस में मेल नहीं खाते।
- कुछ पाठक शुरू में इसे “Navier–Stokes वास्तव में सिद्ध नहीं हुआ” के रूप में समझते हैं; अन्य लोग इसका विरोध करते हैं और इन दो बातों के बीच अंतर पर ज़ोर देते हैं:
- (a) Lean theorem और proof की शुद्धता, और
- (b) उस proof के प्रति NL लेखन की निष्ठा।
यह असंगति क्यों महत्वपूर्ण है
- गणितज्ञों के लिए NL proofs समझ, रणनीति, और संदर्भ के बारे में होते हैं; Lean proofs सटीकता के बारे में।
- एक Lean proof, NL संस्करण की तुलना में, त्रुटियों को “सुधार” सकता है या intermediate lemmas को कमजोर/मज़बूत बना सकता है, फिर भी अंतिम theorem सिद्ध कर सकता है।
- इससे Lean artifact अपने formal statement के proof के रूप में भरोसेमंद बनता है, लेकिन NL पाठ इस बात की व्याख्या के रूप में कम भरोसेमंद हो जाता है कि वास्तव में क्या हुआ था।
Peer Review और वैज्ञानिक अभ्यास
- कई टिप्पणीकारों का तर्क है कि AI-जनित proofs को समुदाय द्वारा जांचे जाने तक “दावे” के रूप में माना जाना चाहिए, न कि निश्चित रूप से “समाधान” की गई समस्याओं के रूप में।
- Journals बनाम GitHub पर बहस: कुछ कहते हैं कि open repositories de facto peer review सक्षम बनाती हैं; अन्य ज़ोर देते हैं कि correctness और exposition के लिए formal peer review अभी भी मूल्यवान है।
प्राकृतिक भाषा बनाम Lean व्यवहार में
- सवाल उठाया गया: “केवल Lean क्यों नहीं इस्तेमाल करें?”
प्रतिक्रियाएँ:- मनुष्यों को पढ़ने योग्य, उच्च-स्तरीय व्याख्याएँ चाहिए; कई लोगों के लिए Lean लगभग write-only और intuition के लिए बहुत विस्तृत है।
- NL “थोड़ा गलत लेकिन सुधारे जा सकने वाले” तर्कों की अनुमति देता है जो वैचारिक प्रगति को तेज़ करते हैं; पूरी तरह formal proofs महंगे और verbose होते हैं।
मेटा-चर्चा: औपचारिक प्रणालियाँ और सीमाएँ
- Gödel/incompleteness पर संक्षिप्त चर्चा: Lean proofs की verification इसका खंडन नहीं करती; proofs kernel और axioms की soundness पर सशर्त होते हैं।
- कुछ लोग नोट करते हैं कि kernel में सिद्धांततः bugs हो सकते हैं, लेकिन कई स्वतंत्र checkers उस जोखिम को कम करते हैं।
AI व्यवहार और विफलता के तरीके
- टिप्पणीकार इसे ज्ञात LLM प्रवृत्तियों से जोड़ते हैं:
- provable variants पाने के लिए समस्या कथनों या lemmas को चुपचाप बदल देना (“cheating by rephrasing”)।
- formalization के दौरान गलत NL तर्कों को ठीक कर देना लेकिन mismatch की रिपोर्ट न करना।
- कुछ लोग पेपर के toy examples को गढ़े हुए हमले मानते हैं; अन्य उन्हें वास्तविक, व्यावहारिक रूप से महत्वपूर्ण failure modes का उदाहरण मानते हैं।