OpenAI-ს Navier-Stokes-ის Lean დამტკიცება ბუნებრივი ენის ვერსიას არ ემთხვევა, ამბობენ მათემატიკოსები

ორ დამტკიცებას შორის შეუსაბამობა

OpenAI-მ 8 სექტემბერს განაცხადა, რომ Navier-Stokes-ის ამოცანის ამოხსნა იპოვა, რაც მათემატიკაში ერთ-ერთი ყველაზე ცნობილი ღია პრობლემაა. კომპანიამ დამტკიცება ორ ვერსიად გამოაქვეყნა: ერთი ბუნებრივი ენით დაწერილი, ინგლისურისა და მათემატიკური სიმბოლოების კომბინაცია, როგორც ადამიანი მათემატიკოსი დაწერდა, და მეორე კი კომპიუტერულ ენაზე, Lean-ზე, დაწერილი, რომელიც ფორმალიზაციად იყო გამიზნული და კომპიუტერს ყოველი ლოგიკური დებულების მექანიკურად გადამოწმების საშუალებას აძლევს.

ახლა მათემატიკოსთა ჯგუფი ამბობს, რომ ეს ორი ვერსია ერთმანეთს არ ემთხვევა. კემბრიჯის უნივერსიტეტის ანდერს ჰანსენი და ფაბიან ჩირჩელი, ლონდონის King's College-ის ალექსანდრე ბასტუნისთან ერთად, ამტკიცებენ, რომ OpenAI-ს მოდელმა დამტკიცების ნაწილი არასწორად თარგმნა Lean-ში გადაყვანისას. მკვლევარები ხაზგასმით აღნიშნავენ, რომ ეს არ ნიშნავს, რომ დამტკიცებები არასწორია ან რომ OpenAI-მ პრობლემა ვერ გადაჭრა, თუმცა ეჭვს აჩენს იმაზე, შეიძლება თუ არა ყოველთვის დაეყრდნო AI-ის მიერ გენერირებულ მათემატიკურ შედეგებს.

დასუსტებული ლემა

ჯგუფის მტკიცება ეხება დამტკიცებების იმ ნაწილს, რომელსაც ლემა 8,6 ეწოდება. ბუნებრივი ენით დაწერილ დამტკიცებაში ამ ნაწილის განტოლება მოითხოვს, რომ გარკვეული მნიშვნელობა იყოს m + 4-ზე ნაკლები, სადაც m მთელი რიცხვია. Lean-ის დამტკიცებაში ეკვივალენტური მნიშვნელობა უნდა იყოს m + 5-ზე ნაკლები, რაც მათემატიკურად უფრო სუსტია. ორივე განაცხადი შეიძლება ჭეშმარიტი იყოს, მაგრამ სხვადასხვა რამეს ამბობს და Lean-ის ვერსია მეტ შესაძლო პასუხს იძლევა.

მკვლევარების თქმით, გადახრა იმიტომ ხდება, რომ AI-მ უნდა შექმნას Lean-ის დამტკიცება, რომელიც კომპილირდება, ანუ კოდი სრულად თვითკონსისტენტურია და შეცდომებს არ იძლევა. თუ მოდელი იპოვის ნაწილს, რომელიც არ კომპილირდება, ის შეეცდება იპოვოს შემოვლითი გზა, თუნდაც ეს ნიშნავდეს ბუნებრივი ენით დაწერილი დამტკიცებისგან გადახრას. OpenAI-მ ორ დამტკიცებას იდენტურად წარმოადგენს და Github-ზე აცხადებს, რომ რეპოზიტორია შეიცავს ნაშრომში მოცემული შედეგების Lean 4 ფორმალიზაციებს.

AI-ის დამტკიცებების გადამოწმების ტვირთი

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

პრობლემა განსაკუთრებით აქტუალურია, რადგან OpenAI-მ 722 მათემატიკური ნაშრომის პარტია გამოაქვეყნა, რომელთაგან მხოლოდ ნაწილს ახლავს Lean-ის დამტკიცებები, რომლებიც ხელით არ არის შემოწმებული. ლონდონის Imperial College-ის კევინ ბაზარდმა თქვა, რომ დარწმუნებულია Navier-Stokes-ის პრობლემა სწორად არის გადაჭრილი, მაგრამ გაცილებით ნაკლებად დარწმუნებულია, რომ PDF-ში აღწერილი დამტკიცება სწორია. ჰანსენმა თქვა, რომ მეტი სამუშაოა საჭირო მდგრადი ავტოფორმალიზაციის ტექნიკის შემუშავებაზე და რომ ამის საბოლოო გზა სრულიად უცნობია.

წყაროები: newscientist.com