Leanstral 1.5: सभी के लिए प्रमाणों की भरपूरता

 (mistral.ai)
1 पॉइंट द्वारा GN⁺ 4 시간 전 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Formal verification को वास्तविक development कार्यों के ज्यादा करीब इस्तेमाल करने की दिशा में, Mistral AI ने Lean 4 के लिए Apache-2.0 मॉडल Leanstral 1.5 जारी किया है
  • मॉडल कुल 119B parameters में से केवल 6B को सक्रिय करता है, और intermediate training, supervised fine-tuning, व CISPO reinforcement learning के जरिए प्रमाण लेखन और code repository कार्यों को साथ में सीखता है
  • miniF2F 100%, PutnamBench 587/672, FATE-H 87%, FATE-X 34% दर्ज करते हुए यह mathematical proof benchmarks और वास्तविक proof engineering evaluations में मजबूत performance दिखाता है
  • वास्तविक code verification में इसने AVL tree की O(log n) time complexity proof और Rust-to-Lean pipeline के जरिए 57 repositories में 11 वास्तविक bugs खोजे
  • Weights और leanstral-1-5 free API उपलब्ध हैं, इसलिए theorem proving, proof debugging और repository contribution जैसे practical proof engineering में इसे तुरंत लागू किया जा सकता है

Leanstral 1.5 की रिलीज़ और मॉडल की विशेषताएं

  • Leanstral 1.5 Lean 4 में proof engineering करने के लिए बनाया गया मॉडल है
  • License Apache-2.0 है, और model scale कुल 119B parameters व 6B active parameters का है
  • Formal verification performance को बेहतर बनाकर इसे mathematical benchmarks के साथ-साथ वास्तविक code property verification में भी इस्तेमाल किया जा सकता है
  • इसने miniF2F को saturate किया, PutnamBench के 672 problems में से 587 हल किए, और FATE-H 87%, FATE-X 34% हासिल किया

Proof feedback सीखने वाली 3-stage training

  • Training intermediate training, supervised fine-tuning, और CISPO-based reinforcement learning—इन 3 stages से बनी है
  • Reinforcement learning में दो environments इस्तेमाल किए गए
    • Multi-turn environment: मॉडल theorem proposition लेकर उसे prove या disprove करता है, और Lean compiler feedback के आधार पर proof को बार-बार revise करता है
    • Proof compile हो जाए तो success माना जाता है; वरना problem solve होने या budget खत्म होने तक loop जारी रहता है
    • Code agent environment: raw filesystem में developer की तरह files edit करता है, bash commands चलाता है, और Lean language server से goals, errors व type information real time में देखता है
  • Code agent environment repository के अंदर partial proofs complete करने, helper lemmas लिखने, और कई rounds के context compression के बाद भी जारी रहने वाले लंबे tasks को संभालता है
  • Final correctness target theorem list के आधार पर Mistral के SafeVerify fork में verify की जाती है

Mathematics और proof engineering benchmarks

  • Evaluation में miniF2F, PutnamBench, FATE-H/FATE-X, FLTEval इस्तेमाल किए गए
    • miniF2F एक formal mathematics benchmark है जिसमें elementary problems से लेकर IMO-level problems तक शामिल हैं
    • PutnamBench, Putnam Mathematical Competition के 672 problems से बना है
    • FATE-H और FATE-X क्रमशः graduate और PhD level abstract algebra benchmarks हैं
    • FLTEval, Fermat’s Last Theorem repository के वास्तविक pull requests के आधार पर proof engineering difficulty को evaluate करता है
  • miniF2F में validation set और test set दोनों पर 100% हासिल किया गया
  • PutnamBench और FATE-H/X में natural-language proof guide के बिना Goedel-Architect, Seed-Prover 1.5 high, AxProverBase से तुलना की गई
  • FATE-H/X performance: {b:87,34}
  • FATE-H में 87%, FATE-X में 34% के साथ नया best performance हासिल हुआ
  • PutnamBench में इसने Seed-Prover 1.5 high से 7 problems ज्यादा हल किए, और प्रति problem cost लगभग 4 dollars रही
    • Seed-Prover की high setting प्रति problem 10 H20-days budget इस्तेमाल करती है और cost 300 dollars से अधिक अनुमानित है
    • Higher-ranked कुछ provers natural-language proof guide पाते हैं, या Aleph Prover की तरह प्रति problem 54–68 dollars लगने वाली अलग conditions में काम करते हैं

लंबे reasoning budget में scalability और FLTEval

  • PutnamBench पर token budget बढ़ाने के साथ Leanstral 1.5 की Pass@8 performance smooth और monotonic रूप से बढ़ती है
  • प्रति attempt token budget को 25k से 4M तक बढ़ाने वाले experiment में solved problems की संख्या इस तरह बढ़ी
    • 50k tokens: 44 problems
    • 200k tokens: 244 problems
    • 1M tokens: 493 problems
    • 4M tokens: 587 problems
  • लंबे proofs में रुके बिना लाखों tokens तक reasoning, file editing और revisions जारी रखने वाला behavior performance improvement में बदला
  • FLTEval भी पूरी तरह open source के रूप में जारी किया गया
  • FLTEval में Leanstral 1.5 ने pass@1 को 21.9 से 28.9, और pass@8 को 31.9 से 43.2 तक बढ़ाया
  • pass@8 43.2, Opus 4.6 के 39.6 से अधिक है, और cost उसका 1/7 है
  • Open source models में यह अपने से 3–10 गुना बड़े models से भी आगे performance दिखाता है

वास्तविक code verification cases

  • AVL tree time complexity proof

    • AVL tree एक self-balancing binary search tree है जो insertion और deletion के दौरान rebalancing के जरिए O(log n) height बनाए रखता है
    • Leanstral 1.5 ने वास्तविक implementation के लिए verify किया कि insertion और deletion O(log n) हैं
    • इस task में tree recursive structure को reflect करने वाली structural induction, monad-based time tracking handling, और rebalancing paths पर exhaustive case analysis की जरूरत थी
    • Proof 2.7 million से अधिक tokens और 22 context compressions से होकर आगे बढ़ा
    • Leanstral ने TimeM monad की हर layer को व्यवस्थित रूप से unfold करके control flow के साथ मिली calculations को उजागर किया
    • Insertion के लिए height की प्रति unit 48 steps और constant-term के करीब bound बनाया, और height व tree size को logarithmic relation से जोड़ा

  • Rust code में bugs खोजना

    • Bug detection experiment एक pipeline से बना था जिसमें Aeneas Rust code को Lean में convert करता है, और Leanstral code से user intent infer करके consistency properties generate करता है
    • Leanstral हर property को prove करने के 4 attempts करता है, और सभी fail हों तो उसके negation को फिर 4 attempts में prove करने की कोशिश करता है
    • 57 repositories में 47 violating properties flag हुईं, जिनमें से 11 वास्तविक bugs की ओर इशारा करती थीं
    • वास्तविक bugs में से 5 GitHub पर पहले report नहीं हुए थे
    • datrs/varinteger library के zigzag decoding sign function में एक case मिला
    • Input Std.U64.MAX होने पर (value + 1) expression overflow करता है
    • Debug mode में crash होता है, और release mode में silent data corruption होता है
    • यह edge case सामान्य testing और fuzzing से आसानी से छूट सकता है

Release और उपयोग का तरीका

  • Weights Hugging Face पर उपलब्ध हैं
  • Free API endpoint model card में leanstral-1-5 नाम से उपलब्ध है
  • उपयोग environment के रूप में Mistral Vibe recommended है
  • शुरू करने की प्रक्रिया है: Mistral Vibe setup, Leanstral 1.5 installation, agent run, optional Lean LSP MCP installation, और proof task शुरू करना
  • Lean LSP MCP को ~/.vibe/config.toml में add करके install करना recommended है
  • अगर existing MCP server नहीं है, तो mcp_servers = [] हटाना पड़ सकता है
  • Leanstral का उपयोग theorem solving, proof debugging और repository contribution tasks में किया जा सकता है

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

1 टिप्पणियां

 
GN⁺ 4 시간 전
Hacker News टिप्पणियाँ

  • Mistral के लिए बड़े मॉडलों से प्रतिस्पर्धा करना मुश्किल है, यह आलोचना वाजिब है, लेकिन लगता है कि वास्तव में वह छोटे मॉडलों में खास फीचर्स को उच्च गुणवत्ता के साथ देने पर फोकस कर रहा है
    मैं OCR या file analysis जैसे कामों में Mistral का उपयोग करता हूँ, और अगर अकाउंट में 100 डॉलर डाल दिए जाएँ तो request volume की चिंता के बिना 1 साल तक चल जाता है
    लागत बेहद कम है, इसलिए भले ही यह Opus 4.8 से प्रतिस्पर्धा न कर पाए, फिर भी इसकी पर्याप्त वैल्यू है

    • OCR में यह वास्तव में कितना प्रतिस्पर्धी है, यह जानने की जिज्ञासा है
      कम कीमत पर ठीक-ठाक गुणवत्ता बाद में गलतियाँ कम करने के लिए 10 गुना कीमत देकर सर्वोत्तम गुणवत्ता लेने की तुलना में ज़्यादा niche market जैसी लगती है
    • यूरोपीय मूर्ख लोग पैसे को अधिकतम कमाने के optimization की जगह अच्छा product बनाने के optimization में लगे हैं /s
    • “सालाना 100 डॉलर से कम में 1 साल का document processing” उतना शानदार है या नहीं, इस पर मुझे यकीन नहीं है। कम-से-कम यूरोपीय competitiveness के नज़रिए से देखें तो Mistral अपनी revenue ceiling बहुत नीचे सेट कर रहा है
      OCR पहले से ही लगभग commodity बन चुका है, और open source models या AWS जैसी जगहों पर भी default के रूप में मिलता है
      ऊपर से, सालाना 100 डॉलर का price tag loyalty बनाना मुश्किल करता है, और switching cost भी नहीं है, इसलिए और कम कीमत आते ही ग्राहक तुरंत जा सकते हैं
      अगर आसानी से कॉपी होने वाले low-cost tool में customer lock-in नहीं है, तो वह business से ज़्यादा एक feature जैसा है
      खरीदार के नज़रिए से यह अच्छा हो सकता है, लेकिन अगर हम चाहते हैं कि यूरोपीय कंपनियाँ लंबे समय में वैश्विक प्रतिस्पर्धियों से product capability के आधार पर प्रतिस्पर्धा करें, तो यह खराब रणनीति लगती है

  • काम खुद अच्छा है, लेकिन bug ढूँढ़ने का उदाहरण अजीब लगा
    zigzag decoding की sign function में Std.U64.MAX input पर (value + 1) overflow हो जाता है, जिससे debug mode में crash और release mode में silent corruption होती है — मुझे नहीं पता कि इसे ऐसा boundary condition कहा जा सकता है जिसे test “आमतौर पर छोड़ देते हैं”
    खराब test हो तो छोड़ सकता है, लेकिन सावधान इंसान या machine learning-आधारित coding system “extreme values को test करना चाहिए” वाली बात काफी अच्छी तरह करते हैं। खासकर अगर कोड user input parse कर रहा हो तो और भी
    शायद उन्हें इससे भी अधिक दिलचस्प bugs मिले, लेकिन जल्दी समझाना मुश्किल था, इसलिए यह उदाहरण लिया — ऐसा सोचने पर मजबूर करता है

    • खासकर “fuzzing भी इसे छोड़ देती है” वाला हिस्सा अजीब है। मैंने जो fuzzing देखी है, वह आम तौर पर boundary values को जानबूझकर explore करती है
      ऐसी encoding library के लिए ठीक-ठाक code की baseline expectation ही fuzzing है, और लगभग पक्का है कि यह कुछ सेकंड में पकड़ में आ जाता
      वास्तव में मैंने proptest से बहुत साधारण round-trip test बनाया, और 1 सेकंड से भी कम समय में दर्जनों failures और नीचे दिया गया result मिल गया:
      thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:
      Test failed: attempt to multiply with overflow.
      minimal failing input: value = 4611686018427387904
      successes: 2
      local rejects: 0
      global rejects: 0
    • इसे “आमतौर पर छूट जाता है” कहना मुश्किल है, लेकिन यह वास्तव में मौजूद था, इसलिए कभी-कभी छूट जाने वाला bug तो है ही
      Lean का उपयोग करने का एक फायदा यह दिखता है कि कौन-से examples test करने चाहिए, इसे चतुराई से चुनने की ज़रूरत कम हो जाती है
    • यह बुनियादी quality assurance है। अगर tests ऐसी चीज़ छोड़ दें, तो उनकी उपयोगिता सामान्य अपेक्षा से कहीं अधिक सीमित होगी
      लेखकों की पृष्ठभूमि जानने की जिज्ञासा होती है
    • यह बस घटिया प्रचार है
      लगभग 1980 के आसपास आविष्कृत हर property-based testing system boundary values को explore करता है
      C और C++ की semantics, या उनकी कमी, के कारण असली testing मुश्किल हो सकती है। क्योंकि compiler को उन सभी inputs पर भी “test passed” कहने की छूट होती है जो undefined behavior तक ले जाते हैं

  • लेख के बीच में कई frontier-grade LLMs से तुलना आती है, लेकिन वे सब आधा साल पुराने models हैं
    “हमारा नया model तीन पीढ़ी पुराने चीनी models से बेहतर है” जैसी बात काफ़ी हास्यास्पद लगी

    • यह 6 billion parameter model है, इसलिए यह पूरी तरह अलग श्रेणी में आता है। बल्कि “frontier-grade small language model” कहना ज़्यादा उपयुक्त लगेगा
    • सहमत, लेकिन सिर्फ open weights होने और अपेक्षाकृत छोटा होने भर से भी यह headline-worthy है। यह model काफ़ी अच्छा चलता है

  • वह library https://github.com/datrs/varinteger है
    paper के public होने से एक हफ्ता पहले वही समस्या इस repository में पहले ही आ चुकी थी, इसलिए शायद यही सही है: https://github.com/datrs/varinteger/issues/8
    पता नहीं यह व्यक्ति Leanstral का कर्मचारी है, या Leanstral ने बस यह issue वहीं से उठा लिया
    यह library छोटी है, tests हैरान करने वाली तरह से कमजोर हैं, और 8 साल से लगभग छुई भी नहीं गई है: https://github.com/datrs/varinteger/blob/master/tests/test.r...
    downloads भी कम लगते हैं, लगभग 1 हज़ार प्रतिदिन: https://crates.io/crates/varinteger
    इसलिए इसे एकमात्र उदाहरण के रूप में पेश करने लायक कोई बड़ी सफलता मानना मुश्किल है। automatic detection उपयोगी है, यह सही है, लेकिन इस subfield में यह सचमुच उल्लेखनीय उपलब्धि है या नहीं, इस पर संदेह है
    proof-writing LLM मैंने कभी इस्तेमाल नहीं किए, लेकिन training data कम होना आम बात है, इसलिए अगर वे सामान्य coding models से ज़्यादा rough हों तो हैरानी नहीं होगी
    वैसे https://crates.io/crates/varinteger में इसे https://github.com/mafintosh/varinteger-rs के रूप में दिखाया गया है, लेकिन यह पता https://github.com/datrs/varinteger पर redirect होता है, इसलिए ऊपर से अलग दिखने के बावजूद यह वही library लगती है

    • proof की समस्या यह है कि कभी-कभी उसकी value समझाना मुश्किल होता है
      मुख्य बात bug ढूँढ़ना नहीं, बल्कि यह साबित करना है कि कुछ assumptions के तहत कुछ खास तरह के bugs मौजूद नहीं हैं
      लेकिन यह कहानी बेचना कठिन है, इसलिए marketing अक्सर “हमने यह bug पकड़ा” वाली दिशा में चली जाती है

  • क्या यह उन लोगों के लिए भी उपयोगी हो सकता है जिन्हें Lean के बारे में बिल्कुल पता नहीं है? मैं जिस सॉफ़्टवेयर पर काम कर रहा हूँ उसे verify करना चाहता हूँ, लेकिन formal verification का कोई अनुभव नहीं है
    मैं सोच रहा हूँ कि क्या केवल spec, code, और सीमित learning time के साथ भी काम लायक नतीजे मिल सकते हैं

    • जिस हिस्से को prove करना है उसे समझना ज़रूरी है, लेकिन पूरी proof process को पूरी तरह समझना ज़रूरी नहीं है
      यह गणित से ज़्यादा Haskell types पढ़ने जैसा है, और बस terminology का बड़ा हिस्सा गणित से लिया हुआ लगता है
    • अगर आप लेख का “Bug Discovery: Finding Hidden Flaws” सेक्शन पढ़ें, तो लगता है कि उन्होंने सिर्फ़ Rust code से शुरुआत की और open source Rust में समस्याएँ ढूँढने के लिए मॉडल का इस्तेमाल किया
      application verification के लिए Lean code लिखवाने में बातचीत के ज़रिए मदद मिल सकती है, लेकिन यह पक्का नहीं है
    • कम से कम आपको यह समझना होगा कि code के बारे में कौन-सा theorem prove करना है, और उसे Lean में कैसे व्यक्त करना है
      नहीं तो आप output को verify नहीं कर पाएँगे
      हो सकता है आपने कोई ऐसा proposition prove किया हो जिसे मशीन ने औपचारिक रूप से सही माना हो, लेकिन अगर आपको यह नहीं पता कि उसका मतलब क्या है, और क्या वह सच में उसी चीज़ को कवर करता है जिसे आप verify करना चाहते हैं, तो उसका कोई अर्थ नहीं है
    • Lean4 के बारे में बिल्कुल कुछ न जानने की स्थिति से मैं लगभग 6 महीनों में उस स्तर तक आ गया जहाँ अब ज़्यादातर coding Lean4 में करता हूँ, और यह प्रक्रिया AI assistance की वजह से बहुत तेज़ हुई
      यह काफ़ी चौंकाने वाला है कि models Lean4 में कितनी लगातार fluency दिखाते हैं। सिर्फ़ frontier-level models ही नहीं, छोटे local models भी ऐसे ही थे, और लगता है कि LLMs Lean4 को स्वाभाविक रूप से अच्छी तरह समझते हैं
      अभी भी खुद को Lean4 expert कहने में समय लगेगा, लेकिन अब उपयोगी programs बनाने के लिए assistance अनिवार्य नहीं रही
      लगभग बिना knowledge के भी उन हिस्सों पर भरोसा कर पाना जिन्हें आप पूरी तरह नहीं समझते, learning speed को बहुत बढ़ा देता है। अधूरी जानकारी के साथ भी ऐसे programs मिलना जिन पर निर्भर किया जा सके, व्यावहारिक भी है और प्रेरक भी
      लगता है कि सीमा पूरी intermediate proof steps से नहीं, बल्कि उस language हिस्से से तय होती है जिससे आप अपने axioms और propositions की सतह का वर्णन करते हैं। समय के साथ ज़्यादा करने के लिए ज़्यादा समझना पड़ेगा, लेकिन एक अर्थ में आप N+1 स्तर पर सुरक्षित रूप से काम कर सकते हैं
      Lean4 theorem proving की भूमिका से अलग भी एक मज़ेदार programming language है, और इसकी speed भी हैरान करने वाली है
      मैं इसे io_uring के साथ जोड़कर इस्तेमाल कर रहा हूँ, और कई मामलों में यह C++/libuv या Rust/Tokio से काफ़ी तेज़ है
      कभी-कभी p99.99 latency जैसी जगहों पर बड़ा tail दिखे तो numbers को fixed width में बदलने जैसी tuning करनी पड़ती है, लेकिन C++ और Rust में भी tuning करनी ही पड़ती है

  • यह दिलचस्प है कि Lean 4 को formal verification के लिए आगे बढ़ाया जा रहा है
    मैं समझता था कि यह क्षेत्र Isabelle/HOL और TLA+ की तरफ़ है
    कम से कम मैं ऐसी उम्मीद करता कि model को तीनों का इस्तेमाल करना सिखाया गया होगा। linear algebra की forward derivation के लिए Isabelle/Isar भी बेहतर लगता है; क्या कोई समझा सकता है?

    • यह सही है कि Lean को software verification में Isabelle या पुराने Coq Rocq की तुलना में कम अपनाया गया है
      इस क्षेत्र में Agda का भी इस्तेमाल इससे ज़्यादा रहा है
      फिर भी Lean अभी एक विकल्प के रूप में काफ़ी momentum हासिल कर रहा है, ख़ासकर एक general-purpose functional programming language के रूप में इसकी क्षमता बड़ी है
      व्यक्तिगत रूप से मुझे लगता है कि requirements और specs को मिलाने में Hoare logic या separation logic पर आधारित approaches ज़्यादा practical हैं। मुझे Dafny और F* पसंद हैं

  • Twitter announcement में developers का Le Chaton Fat का हल्का-सा ज़िक्र करना मज़ेदार था
    चाहे वे वास्तव में Le Chaton Fat से जुड़े हों या नहीं, ऐसा लगता है कि सच में कोई “नया large general-purpose” model जल्द आने वाला है
    media uproar के बाद भी उन्होंने इसे सीधे mention किया, इसलिए उम्मीद बढ़ती है। अच्छा होगा अगर नाम “Large 4” से ज़्यादा creative हो

  • नवीनतम OpenATP में Leanstral 1.5 आज़माया जा सकता है
    OpenATP agentic automated theorem proving के लिए एक open source Python package और CLI है, जो Docker में local run या Modal sandbox में remote run को default support देता है
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com