Leanstral 1.5؛ AI چەوا دشێت هاریکار بیت د سەلماندنا دروستیا کۆدی دا؟

Mistral ل ٢ێ تەممووزا ٢٠٢٦ێ Leanstral 1.5 بەلاڤ کر؛ مۆدێلەکێ تایبەت ب کارێن proof engineering د Lean 4 دا، ب مۆڵەتا Apache 2.0. ئەڤ ڕاپۆرتا ٥ێ تەممووزێ دپرسیت کو ڤی جۆرێ AI چ مفایەک بۆ پروگرامسازییێ هەیە.

ژ بەرسڤێ بەرەڤ سەلماندنێ

کتێبا فەرمی یا Lean جوداهییێ ل ناڤبەرا دۆزینەڤەیا سەلماندنەکێ و پشکنینا دروستیا وێ دکەت. د formal verification دا، داخواز یان تایبەتمەندییەک ب زمانەکێ ورد یێ بیرکاری دهێتە نڤیسین، پاشی کار ل سەر سەلماندنا وێ دهێتە کرن.

بۆ نموونەیەکا فێرکارییێ، وێنە بکە فانکشنەک ژ لیستەکێ ئەندامان دادگریت. پرسیارەک «ئەرێ ئەو د ئەڤان دوو نموونەیان دا کار دکەت؟»ە. پرسیارەکا دی «ئەرێ ئەنجام هەمیشە لدویڤ مەرجێن دیارکری دێ ژمارەیا ئەندامان بپارێزیت؟»ە. ئەڤ دوو پرسیارە هەمان کار نینن.

ڕۆلێ AI و ڕۆلێ Lean

بەلگەنامەیێن Lean ڕوون دکەن کو داخوازییێن بیرکاری و سەلماندن د هەمان بناغەیا زمانێ دا دهێنە نڤیسین. ژبەر ڤێ چەندێ، دەقەکێ سەلماندنێ دبێت لدویڤ پێناسە و یاسایێن سیستەمی بگونجیت.

Mistral د ڕاگەهاندنێ دا باسێ loopەکێ دکەت کو مۆدێل سەلماندنێ پێشنیار دکەت، بەرسڤێ compiler وەردگریت و دووبارە هەوڵ ددەت. واتە پێشنیارکرن و پشکنین ئەرکێن جودانە. مۆدێل ڕێکەکێ دگەڕیت؛ پشکنەری دپشکنیت کو ئەنجام لەگەل داخوازا نڤیسی گونجایە یان نە.

بۆچی نڤیسینا داخوازێ گرنگە؟

ئەگەر تیمەک تایبەتمەندییەکا هەڵە بنڤیسیت، سەلماندنا وێ پرسیارا ڕاستەقینە یا تیمی چارەسەر ناکەت. بۆ نموونە، «ئەنجام لیستەکە» ژ «ئەنجام هەمی ئەندامێن لیستا دەستپێکێ بپارێزیت» جودایە. هەر دوو داخوازە دشێن بۆ هەمان فانکشنێ بهێنە گوتن، بەڵام توانایا وان بۆ پشکنینێ یەک نینە.

بۆ پروگرامسازێن کو نوو دەست پێ دکەن، تمرینەکا مفادار هەلبژارتنا یاسایەکا بچووکە، نڤیسینا مەرجێن وێ و تێگەهشتنا ئەوەیە کو پشکنەر چ دپەژرینیت. پاشی دکرێت هاریکاریا AI ب هەمان پێڤەرێ بهێتە هەڵسەنگاندن.

ئەڤ ئاراستە گرنگە چونکی پرسیارا باوەرییێ ژ شێوازێ نڤیسینا بەرسڤێ دئینیتە سەر شتێ پشکنینبار: چ هاتییە داخوازکرن، چ هاتییە سەلماندن و ب کەیژ مەرجان؟ ئەڤ ڕاپۆرتە لێکدانەکا ڕاگەهاندنێیە؛ تاقیکرنەکا سەربەخۆ یا توانایێن مۆدێلی نینە.