Google DeepMind-ის მკვლევარებმა წარმოადგინეს ახალი სამეცნიერო ნაშრომი, რომელიც დეტალურად აღწერს ავტომატიზებული სისტემის, AlphaProof Nexus-ის შესაძლებლობებს. arXiv-ზე გამოქვეყნებული მასალის მიხედვით, ამ სისტემამ დამოუკიდებლად ამოხსნა 353-დან 9 ღია Erdos-ის მათემატიკური ამოცანები.
ეს არის მნიშვნელოვანი შემთხვევა, როდესაც დიდ ენობრივ მოდელზე დაფუძნებულმა აგენტმა შეძლო ასეთი სირთულის ღია კვლევითი პრობლემების დაძლევა ადამიანის ჩარევის გარეშე. კვლევაში მითითებულია, რომ თითოეული ამოცანის ამოხსნის პირდაპირი გამოთვლითი ხარჯი (inference cost) მხოლოდ რამდენიმე ასეულ დოლარს შეადგენდა.
სარჩევი
AlphaProof Nexus სისტემამ ასევე წარმატებით დაამტკიცა ათობით სხვა ღია ვარაუდი და გადაჭრა რთული ოპტიმიზაციის პრობლემები. ფაქტობრივი მონაცემები მიუთითებს იმაზე, რომ ავტომატიზებულ აგენტებს უკვე შეუძლიათ სტაბილური შედეგების დადება ფორმალურ მეცნიერებებში.
როგორ მუშაობს AlphaProof Nexus სისტემა
დიდი ენობრივი მოდელები (LLM) ბუნებრივი ენის გენერირებაში ეფექტურია, თუმცა მათემატიკურ მსჯელობაში ისინი ხშირად უშვებენ ლოგიკურ შეცდომებს. ასეთ შეცდომებს “ჰალუცინაციებს” უწოდებენ. ბუნებრივი ენით დაწერილი მტკიცებულებები რთული გადასამოწმებელია.
მათემატიკაში თუნდაც ერთ შუალედურ ნაბიჯში დაშვებულმა მცირე ხარვეზმა შეიძლება მთელი მტკიცებულება გააბათილოს და შემდგომი გამოთვლები არასწორი მიმართულებით წაიყვანოს. სწორედ ამ პრობლემის მოსაგვარებლად შეიქმნა AlphaProof Nexus.
ეს სისტემა იყენებს კომპლექსურ მიდგომას: ხელოვნური ინტელექტი აგენერირებს მტკიცებულების ნაბიჯებს, ხოლო ცალკეული ვერიფიკაციის პროგრამა, სახელწოდებით Lean, ამოწმებს თითოეულ ლოგიკურ დეტალს. Lean არის კომპილატორი და ფორმალური ენა, რომელიც მკაცრად ამოწმებს სინტაქსსა და ლოგიკას. თუ მტკიცებულება არასწორია, კომპილატორი მას უარყოფს.
ამის შემდეგ იწყება უკუკავშირის პროცესი, რასაც მკვლევარები “აგენტურ მარყუჟებს” (agentic loops) უწოდებენ. AlphaProof Nexus აგრძელებს მტკიცებულების დახვეწას და ხელახლა შემოწმებას. პროცესი მთავრდება მხოლოდ მაშინ, როცა სისტემა სრულყოფილად დაამტკიცებს მას, ან დაასკვნის, რომ ამოცანის ამოხსნა არ შეუძლია.
სრულყოფილი (full-featured) ვერსია იყენებს ევოლუციურ ალგორითმს. ეს ალგორითმი კოორდინაციას უწევს სხვადასხვა ქვე-აგენტს, რომლებიც დამოუკიდებლად ეძებენ ამოხსნის გზებს. ამ მეთოდმა აჩვენა ბევრად უკეთესი ეფექტურობა, ვიდრე სისტემის საბაზისო ვერსიამ.
Erdos-ის ისტორიული ამოცანები და მიღწეული შედეგები
პოლ ერდოში ისტორიაში ერთ-ერთი ყველაზე პროდუქტიული მათემატიკოსი იყო. მან ჩამოაყალიბა ასობით პრობლემა კომბინატორიკაში, რიცხვთა თეორიასა და გრაფთა თეორიაში. დღემდე, Erdos-ის მათემატიკური ამოცანები დიდ გამოწვევას წარმოადგენს მეცნიერებისთვის.
ერდოში ხშირად პირადად აწესებდა ფულად ჯილდოებს მათთვის, ვინც ამ პრობლემებს გადაჭრიდა. ახალმა სისტემამ 353 ღია ამოცანის ამოხსნა სცადა და 9 მათგანის შემთხვევაში წარმატებას მიაღწია. აღსანიშნავია, რომ ზოგიერთი ეს ამოცანა ათწლეულების განმავლობაში გადაუჭრელი იყო.
მაგალითად, სისტემამ ამოხსნა ორი ისეთი კითხვა, რომელიც ღია იყო ზუსტად 56 წლის განმავლობაში. კვლევის მიხედვით, ამოხსნილ ამოცანებს შორისაა ვარიანტები #125, #138, #741 და #12 ერდოშის ამოცანების კატალოგიდან.
მიღებული მტკიცებულებები უკვე ხელმისაწვდომია erdosproblems.com-ის სადისკუსიო პლატფორმაზე. ყველა ფორმალური მტკიცებულება და ზოგიერთი ბუნებრივი ენით დაწერილი ვერსია განთავსებულია GitHub-ის საჯარო რეპოზიტორში
მთელ რიცხვთა მიმდევრობები და ოპტიმიზაცია
გარდა ერდოშის ამოცანებისა, სისტემამ მნიშვნელოვან წარმატებას მიაღწია სხვა მიმართულებებითაც. მან შეძლო 44 ღია ვარაუდის დამტკიცება 492-დან მთელ რიცხვთა მიმდევრობების ონლაინ ენციკლოპედიიდან (OEIS). OEIS არის მნიშვნელოვანი მონაცემთა ბაზა, რომელიც ათასობით სხვადასხვა რიცხვთა მიმდევრობას აერთიანებს.
უფრო მეტიც, ხელოვნურმა ინტელექტმა ამოხსნა ღია კითხვა ოპტიმიზაციაში. კონკრეტულად, მან დაამტკიცა ზუსტი 𝒪(1/t) კონვერგენციის მაჩვენებელი Anchored Gradient Descent-Ascent (GDA) ალგორითმისთვის მინ-მაქს ამოცანებში. ეს პრობლემა მკვლევარებისთვის წლების განმავლობაში რთულ ამოცანას წარმოადგენდა.
ეს კონკრეტული შედეგი აუმჯობესებს წინა კვლევებს და უფრო ზუსტს ხდის მანამდე არსებულ საზღვრებს. ძველი მიდგომები ძირითადად იყენებდნენ უწყვეტი დროის ჩვეულებრივ დიფერენციალურ განტოლებებს (ODE). ამის საპირისპიროდ, სისტემამ გამოიყენა დისკრეტული დროის რეკურენციული მიდგომა, რამაც ამოხსნა შესაძლებელი გახადა.
რატომ არის ეს მნიშვნელოვანი
ეს კვლევა აჩვენებს, რომ შესაძლებელია ენობრივი მოდელების პრაქტიკული გამოყენება მკაცრი მეცნიერული მტკიცებულებებისთვის. აქამდე, მსგავსი ტექნოლოგიების წარმატება ძირითადად შემოიფარგლებოდა საკონკურსო, ოლიმპიადის დონის მათემატიკით ან ადამიანის მიერ წინასწარ დაწერილი არგუმენტების ფორმალიზებით.
ახლა უკვე დადასტურებულია, რომ ავტომატიზებულ სისტემას შეუძლია დამოუკიდებლად აწარმოოს კვლევის დონის სამუშაო. შეცდომების მყისიერი აღმოფხვრა Lean სისტემის მეშვეობით უზრუნველყოფს იმას, რომ მიღებული შედეგები არის ტექნიკურად ზუსტი.
ეს პროცესი აღარ საჭიროებს ადამიანის მხრიდან ძვირადღირებულ და დროში გაწელილ საექსპერტო შემოწმებას სისწორეზე. მტკიცებულებების ღია ხელმისაწვდომობა ნებისმიერ მკვლევარს აძლევს საშუალებას, გადაამოწმოს და გამოიყენოს ეს შედეგები საკუთარ სამუშაოში.
რას ნიშნავს ეს AI ინდუსტრიისთვის
ინდუსტრიისთვის ეს სიახლე მიუთითებს ახალი ტიპის ეფექტურობაზე და ხარჯების ოპტიმიზაციაზე. თითოეული ამოცანის ამოხსნის ინფერენციის ფასი მხოლოდ რამდენიმე ასეულ დოლარს შეადგენდა.
ეს ფაქტი ცვლის წარმოდგენას იმაზე, თითქოს რთული ამოცანების გადაჭრა ყოველთვის მოითხოვს კოლოსალურ ფინანსურ რესურსებს. AlphaProof Nexus-ის სრულყოფილი არქიტექტურა, რომელიც იყენებს ევოლუციურ ალგორითმს, ეკონომიური და მასშტაბირებადი აღმოჩნდა.
DeepMind-ის განცხადებით, მსგავსი აგენტები უკვე აქტიურად ინერგება სხვადასხვა მიმართულებით. მათ შორისაა კომბინატორიკა, ოპტიმიზაცია, გრაფთა თეორია, ალგებრული გეომეტრია და კვანტური ოპტიკის კვლევები. ინდუსტრია გადადის ეტაპზე, სადაც ხელოვნური ინტელექტი ხდება სანდო ინსტრუმენტი სპეციფიკური სამეცნიერო დარგებისთვის.
დასკვნა
AlphaProof Nexus სისტემა ნათლად აჩვენებს ენობრივი მოდელებისა და ფორმალური ვერიფიკაციის ინსტრუმენტების სინერგიის პრაქტიკულ შედეგს. 353-დან 9 Erdos-ის მათემატიკური ამოცანები და ათობით სხვა ღია ვარაუდი დამოუკიდებლად იქნა ამოხსნილი, თანაც მინიმალური ფინანსური დანახარჯებით.
ეს ნაშრომი ადასტურებს, რომ ტექნოლოგიას შეუძლია დაეხმაროს მკვლევარებს ათწლეულების განმავლობაში გადაუჭრელი პრობლემების დაძლევაში. ამოხსნის მაღალი სიზუსტე მიუთითებს, რომ მსგავსი სისტემების ინტეგრაცია სამეცნიერო პროცესებში სამომავლოდ კიდევ უფრო ინტენსიური გახდება.
ხშირად დასმული კითხვები (FAQ)
- რა არის AlphaProof Nexus?
ეს არის Google DeepMind-ის მიერ შექმნილი სისტემა, რომელიც აერთიანებს დიდ ენობრივ მოდელებსა და ფორმალური ვერიფიკაციის პროგრამას (Lean). მისი მიზანია დამოუკიდებლად აგენერიროს და შეამოწმოს რთული მათემატიკური მტკიცებულებები ლოგიკური შეცდომების გარეშე. - ვინ იყო პოლ ერდოში და რა არის მისი ამოცანები?
პოლ ერდოში იყო ცნობილი მათემატიკოსი, რომელმაც შექმნა ასობით ამოცანა გრაფთა თეორიაში, კომბინატორიკასა და რიცხვთა თეორიაში. მან ბევრი ამ ამოცანის ამოსახსნელად ფულადი ჯილდოც დააწესა. - რა დაუჯდა სისტემას ერთი ამოცანის ამოხსნა?
arXiv-ზე გამოქვეყნებული კვლევის (2605.22763v1) მიხედვით, თითოეული ამოცანის ამოხსნის გამოთვლითი დანახარჯი (inference cost) მხოლოდ რამდენიმე ასეულ დოლარს შეადგენდა. - სად შეიძლება მტკიცებულებების ნახვა?
ყველა ფორმალური მტკიცებულება ხელმისაწვდომია GitHub-ის საჯარო რეპოზიტორში. გარდა ამისა, ამოხსნები განიხილება სპეციალიზებულ პლატფორმაზე erdosproblems.com. - რატომ იყენებს სისტემა Lean კომპილატორს?
დიდი ენობრივი მოდელები ხშირად უშვებენ ლოგიკურ შეცდომებს. Lean არის პროგრამა, რომელიც მკაცრად ამოწმებს ყოველ ლოგიკურ ნაბიჯს და უარყოფს არასწორ მტკიცებულებას, რითაც სრულად გამოირიცხება ჰალუცინაციები.
სხვა თემები
ჯეფ დინი Google-ს ტოვებს, ჰასაბისი ახალ პოზიციაზე გადადის
Pacing the Frontier: AI-ს შემქმნელების წერილი
Google-მ Gemma 4 12B წარადგინა – რას მოიცავს მოდელი