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

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

მკვლევრები ერთობლივ განცხადებაში ხელოვნური ინტელექტის ინდუსტრიის მიზნებსა და მათემატიკური საზოგადოების საჭიროებებს შორის „სერიოზულ შეუსაბამობაზე“ საუბრობენ. 11 სექტემბერს გამოქვეყნებულ ტექსტს უკვე 6 000-ზე მეტი სხვა მათემატიკოსი შეუერთდა.

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

მკვლევრები ხაზს უსვამენ, რომ მათემატიკური მტკიცებულება ღირებულებას მხოლოდ ხანგრძლივი ადამიანური პროცესით იძენს. ეს პროცესი მოხსენებებს, განხილვებს, გამარტივებასა და საბოლოოდ ისეთ დამუშავებას მოიცავს, რომელიც სტუდენტების მომავალ თაობებს იდეების გაგებისა და განვითარების საშუალებას აძლევს.

თუმცა თანამედროვე მაგალითები აჩვენებს, რომ ზუსტად ეს პროცესი ზეწოლის ქვეშ ექცევა. 23 წლის ახალგაზრდამ GPT-5.4 Pro-სთვის მიცემული დავალებით ერდეშის 60 წლის პრობლემა ამოხსნა. მათემატიკოსმა ჯარედ ლიხტმანმა ხელოვნური ინტელექტის დაუმუშავებელ პასუხს „საკმაოდ ცუდი“ უწოდა. მთავარი იდეის გამოსაკვეთად პასუხს ადამიანის მიერ ინტენსიური დამუშავება დასჭირდა.

Anthropic-მა ცოტა ხნის წინ მტკიცებულებების დამხმარე პროგრამა Lean-ის გამოყენებით ფერმას ბოლო თეორემის მტკიცებულება 13 მილიონი კოდის ხაზით ფორმალურად გადაამოწმა. პროცესის მონაწილეებმაც აღნიშნეს, რომ ამით ახალი მათემატიკა არ შექმნილა და სამუშაო „მხოლოდ“ ფორმალიზებას ემსახურებოდა. Lean მათემატიკოსებს მტკიცებულებების სრულად ფორმალიზებისა და კომპიუტერით შემოწმების საშუალებას აძლევს. Claude-ის მსგავსი ხელოვნური ინტელექტის სისტემები Lean-ის კოდს უკვე სწრაფად ქმნიან, როგორც ფერმას ბოლო თეორემის შემთხვევაში. თუმცა ადამიანის მიერ მოწესრიგებული Mathlib-ისა და კონცეპტუალური შემოწმების გარეშე ასეთი კონსტრუქციები გამოუსადეგარი რჩება.