OpenAI كومپانياسىنىڭ Astra مودەلىنىڭ ىشكى نۇسقاسى ماتەماتيكا سالاسىندا سەرپىلىس جاساپ، ون جىلدان استام ۋاقىت بويى اشىق كۇيىندە قالعان ماتەماتيكا مەن ينفورماتيكانىڭ 10 ەسەبىن شەشتى. ناتيجەلەر قاتاڭ دالەلدەمەلەر تۇرىندە ۇسىنىلدى، دەپ حابارلايدى infohub.kz سايتى.
OpenAI كومپانياسى GitHub پلاتفورماسىندا Apache 2.0 ليسەنزياسىمەن 10 شەشىلمەگەن ەسەپكە ارنالعان 249 بەتتىك قولجازبا جيناعىن جانە Lean 4 سيفرلىق سەرتيفيكاتتارىن جاريالادى. الگوريتم ارقىلى شىعارىلعان بارلىق دالەلدەمەلەر لوگيكالىق تىزبەكتەردە بىردە-بىر ولقىلىقسىز فورمالدى ماشينالىق تەكسەرۋدەن ءساتتى ءوتتى.
شەشىلگەن ماسەلەلەردىڭ ىشىندە — 1980 جىلى ۇسىنىلعان كونننىڭ قاتاڭدىق گيپوتەزاسىن جوققا شىعارۋ، نەسوفيالىق توپتىڭ بار ەكەندىگىنىڭ دالەلدەمەسىن قۇرۋ، سونداي-اق پول ەردوشتىڭ كوپ ءتۇستى رامسەي ساندارىنا قاتىستى №183 ەسەبىن شەشۋ. سونىمەن قاتار، Astra كوپ ولشەمدى كەڭىستىكتەردە سفەرالاردى وراۋ، كۆانتتىق قايتالاۋ جانە الگوريتمدەردىڭ كۇردەلىلىگى سالالارىندا دا شەشىمدەر تاپتى.
جاڭا Astra جۇيەسى بىرنەشە اگەنتتەردىڭ جۇمىسىن ۇيلەستىرۋ ارقىلى كۇردەلى ەسەپتەرمەن ۇزاق ۋاقىت جۇمىس ىستەۋگە ارنالعان. زەرتتەۋشى نوام براۋننىڭ ايتۋىنشا، توكەندەرگە جۇمسالعان شىعىن نەبارى 2000 دوللاردى قۇرادى. دەگەنمەن، ۇسىنىلعان ناتيجەلەردىڭ ءبارى ءالى دە عالىمداردىڭ ساراپتامالىق رەسەنزياسىنان ءوتۋى ءتيىس.