DeepSeek-Prover-V2 აერთიანებს არაფორმალურ და ფორმალურ მათემატიკურ აზროვნებას

ხელოვნურმა ინტელექტმა შთამბეჭდავი პროგრესი განიცადა რთული მათემატიკური ამოცანების გადაჭრის კუთხით, თუმცა ინტუიციური მსჯელობის ფორმალურ, მანქანით გადამოწმებად მტკიცებულებებად გარდაქმნა დღემდე მნიშვნელოვან გამოწვევად რჩება.

DeepSeek AI ცოტა ხნის წინ გამოავლინა DeepSeek-Prover-V2, ღია კოდის დიდი ენის მოდელი, რომელიც წარმოადგენს გარღვევას არაფორმალური მათემატიკური ინტუიციისა და ფორმალური მტკიცებულების სისტემებისთვის მოთხოვნილი მკაცრი სიზუსტის შერწყმაში.

DeepSeek AI ცოტა ხნის წინ გამოავლინა DeepSeek-Prover-V2, ღია კოდის დიდი ენის მოდელი ეს წარმოადგენს გარღვევას არაფორმალური მათემატიკური ინტუიციისა და ფორმალური მტკიცებულების სისტემებისთვის მოთხოვნილი მკაცრი სიზუსტის შერწყმაში.

ფორმალური მათემატიკური მსჯელობის გამოწვევა

მათემატიკოსები, როგორც წესი, ამოცანებს ინტუიციის, ევრისტიკისა და მაღალი დონის მსჯელობის გამოყენებით წყვეტენ - ხშირად იყენებენ კოგნიტურ მალსახმობებს, რომლებიც ადამიანებისთვის აშკარაა. ეს მიდგომა მკვეთრად ეწინააღმდეგება ფორმალურ თეორემის დამტკიცებას, რომელიც მოითხოვს სრულ სიზუსტეს, თითოეული ნაბიჯით ნათლად ჩამოყალიბებული და ლოგიკურად გამართლებული.

მიუხედავად იმისა, რომ ბოლო დროს დიდი ენის მოდელები (LLM)-მა აჩვენა შესანიშნავი უნარი, გადაჭრას რთული, შეჯიბრებითი დონის მათემატიკური ამოცანები ბუნებრივი ენის მსჯელობის გამოყენებით, თუმცა მათ უჭირთ ამ ინტუიციური მსჯელობის ფორმალურ მტკიცებულებებად გარდაქმნა, რომელთა გადამოწმებაც მანქანებს შეუძლიათ. ეს ხარვეზი არსებობს შემდეგი მიზეზების გამო:

არაფორმალური მსჯელობა ხშირად შეიცავს მოკლე გზებსა და იმპლიციტურ ნაბიჯებს.

ფორმალური სისტემები მოითხოვს თითოეული ლოგიკური ნაბიჯის ცალსახა დასაბუთებას.

ბუნებრივ ენასა და ფორმალურ ნოტაციას შორის კონვერტაცია სირთულეს ზრდის.

მათემატიკური დადასტურება აბსოლუტურ სიზუსტეს მოითხოვს.

როგორ მუშაობს DeepSeek-Prover-V2: არაფორმალური და ფორმალური მსჯელობის დამაკავშირებელი

DeepSeek-Prover-V2 იყენებს ახალ მიდგომას, რომელიც აერთიანებს როგორც არაფორმალური მსჯელობის, ასევე ფორმალური შემოწმების ძლიერ მხარეებს რეკურსიული თეორემის დამადასტურებელი მილსადენის მეშვეობით.

ინოვაციური სასწავლო არქიტექტურა

მოდელი's ტრენინგის პროცესი რამდენიმე ძირითად ეტაპს მოიცავს:

ეს მიდგომა ქმნის უნიკალურ ჩარჩოს, რომელიც აერთიანებს მაღალი დონის მათემატიკურ ინტუიციას Lean-ის მსგავსი ფორმალური დამოწმების სისტემების მიერ მოთხოვნილ სიზუსტესთან.

როგორც YouTube-ზე ბოლოდროინდელ ანალიზშია ახსნილი: „ისინი იყენებენ DeepSeek-V3-ს, მათ დიდ ენობრივ მოდელს ქვემიზნების დაშლის სამართავად და შემდეგ აერთიანებენ მას გაძლიერების სწავლება, რომელიც ქმნის ერთ მოდელს, რომელსაც შეუძლია როგორც არაფორმალური მსჯელობის, ასევე ფორმალური მტკიცებულებების გენერირების დამუშავება“.

რეკორდსმენი შესრულება

DeepSeek-Prover-V2's შესრულება აჩვენებს მნიშვნელოვან პროგრესს ნეირონულ თეორემაში, რომელიც ადასტურებს:

მოდელი ხელმისაწვდომია ორ ზომაში:

ორივე ვერსია შთამბეჭდავ შესაძლებლობებს აჩვენებს, ხოლო უფრო დიდი 671B ვარიანტი ამკვიდრებს „miniF2F ტესტის ახალ, უახლეს შესრულებას, CoT გენერაციის სტრატეგიის გამოყენებით მხოლოდ 32 ნიმუშით უპრეცედენტო სიზუსტის მიღწევას“.

ადამიანისა და მანქანური აზროვნების შორის არსებული უფსკრულის შევიწროება

DeepSeek-Prover-V2-ს განსაკუთრებით მნიშვნელოვანს ის ხდის, თუ როგორ აგვარებს ის დიდი ხნის განმავლობაში არსებულ განხეთქილებას ადამიანების მათემატიკისადმი მიდგომასა და ფორმალური ვერიფიკაციის სისტემების ფუნქციონირებას შორის.

ეს იმაზე მიუთითებს, რომ ჩვენ უფრო ახლოს ვართ AI სისტემები, რომლებსაც არა მხოლოდ მათემატიკური ამოცანების გადაჭრა შეუძლიათ, არამედ ფორმალურ მათემატიკურ სტანდარტებს დაცვით დადასტურებადი მტკიცებულებების შექმნაც შეუძლიათ.

ეს განვითარება ორი მნიშვნელოვანი მიმართულებით მნიშვნელოვან წინგადადგმულ ნაბიჯს წარმოადგენს:

აპლიკაციები და მომავალი შედეგები

DeepSeek-Prover-V2 კარს უხსნის მრავალ აპლიკაციას სხვადასხვა სფეროში:

კვლევის წინსვლამათემატიკური აღმოჩენების დაჩქარება ფორმალური ვერიფიკაციის ავტომატიზაციით

საგანმანათლებლო ინსტრუმენტები: სტუდენტებისთვის მათემატიკური მსჯელობის სწავლაში დახმარება ეტაპობრივი ფორმალიზაციის გზით

პროგრამული უზრუნველყოფის ვერიფიკაციაფორმალური დამტკიცების ტექნიკის გამოყენება კრიტიკული პროგრამული სისტემების დასადასტურებლად

ალგორითმული კვლევაფორმალური მეთოდების გამოყენებით ალგორითმების ოპტიმალურობის აღმოჩენა და დამტკიცება

Quantum Zeitgeist-ის მკვლევარები. აღნიშნა,

დასკვნა

DeepSeek-Prover-V2 ხელოვნური ინტელექტით მართული მათემატიკის თამაშის წესების შემცვლელია, რომელიც არღვევს ძველ ბარიერებს ადამიანის ინტუიციასა და ფორმალურ მტკიცებულებას შორის. მისი ღია კოდის გამოშვებით, ჭკვიანი ქვემიზნების დაშლით და რეკორდული საორიენტაციო სტატისტიკა, ეს ახლა ყველაზე მნიშვნელოვანი ინსტრუმენტია ყველასთვის, ვისაც ხელოვნური ინტელექტით მართული მათემატიკური ვერიფიკაცია ან განათლება აინტერესებს.

თუ უფრო მაღალი დონის სიზუსტეს ეძებთ და გსურთ ნახოთ AI გულწრფელად „ვფიქრობ„როგორც ა მათემატიკოსიDeepSeek-Prover-V2-ში მოქმედებაა.