Axiom Math მათემატიკის ხელოვნური ინტელექტის „ნაგვისგან“ (AI slop) დაცვას ცდილობს

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

სტარტაპი Axiom Math, რომლის ღირებულებაც 1.6 მილიარდ დოლარს შეადგენს, ფსონს იმაზე დებს, რომ მათემატიკა ამ ბედს აირიდებს. კომპანიის მიზანია შექმნას ვერიფიცირებული საფუძველი, რომელსაც AI აგენტები დაეყრდნობიან პროგრამული უზრუნველყოფის შესაქმნელად და, საბოლოოდ, სამეცნიერო კვლევებისთვის. ოთხშაბათს კომპანიამ გამოაცხადა, რომ დაასრულა Stacks Project-ის ფორმალური ვერიფიკაცია — ეს არის ადამიანის მიერ ოდესმე დაწერილი მათემატიკური ნაშრომების ერთ-ერთი უდიდესი კრებული.

მათემატიკოსები Stacks-ს განსაკუთრებულ პატივს სცემენ. კოლუმბიის უნივერსიტეტის მათემატიკოსმა პიტერ ვოიტმა განაცხადა, რომ მასთან შედარებით „სხვა არაფერი არსებობს“ და ის ცნობილ „ბურბაკის წიგნებს“ შეადარა — სერიას, რომელმაც XX საუკუნეში მათემატიკა საფუძვლიდან გადააწყო. Stacks Project 2005 წელს ვოიტის კოლეგამ, იოჰან დე იონგმა დაიწყო, როგორც ღია წყაროს მქონე საცნობარო მასალა. მას შემდეგ მათემატიკოსები მასში მუდმივად ამატებენ შედეგებს, დაწყებული კოლეჯის დონის ალგებრიდან, დამთავრებული ალგებრის, გეომეტრიისა და რიცხვთა თეორიის ყველაზე რთული იდეებით.

მათემატიკის ფორმალიზაცია: 16 მილიონი ხაზი კოდი

Axiom Math-ის AI აგენტების ჯგუფმა ბიბლიოთეკის დაახლოებით 7,654 გვერდი კომპიუტერის მიერ შემოწმებად 16 მილიონ ხაზ კოდში გადათარგმნა. მათემატიკის ფორმალიზაცია არის გზა იმის დასადასტურებლად, რომ მისი სტრუქტურა მყარია. მათემატიკოსები მტკიცებულებებს კოდის სახით წერენ პროგრამირების ენაზე, რომელსაც Lean ეწოდება, ხოლო პროგრამა, სახელწოდებით „დამამტკიცებელი ასისტენტი“ (proof assistant), კოდს ხაზ-ხაზობრივად ამოწმებს. თუ მტკიცებულება შემოწმებას გაივლის, მათემატიკოსებს შეუძლიათ დარწმუნებულნი იყვნენ მის ლოგიკურ სისწორეში.

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

რთული სტრუქტურა და AI აგენტების მუშაობა

ეს ურთიერთდაკავშირებულობა თავიდან Axiom-ის გუნდს ეჭვქვეშ აყენებინებდა პროექტის წარმატებას. მათ უნდა შეენარჩუნებინათ ყველა კავშირი 16 მილიონი ხაზის Lean კოდში. „ცხოვრებაში დიდი და დელიკატური რაღაცები ერთმანეთს იშვიათად ეხამება“, — განუცხადა Axiom-ის აღმასრულებელმა დირექტორმა, კარინა ჰონგმა TechCrunch-ს. „Stacks არის მათემატიკური შედეგების კრებული, რომელიც მათემატიკის საფუძველს წარმოადგენს. თქვენ გსურთ, რომ თეორემები იყოს თანმიმდევრული და არა პარადოქსული. გსურთ, რომ განმარტებები ერთმანეთს არ ეწინააღმდეგებოდეს“.

25 წლის აღმასრულებელმა დირექტორმა სტენფორდის მათემატიკის სადოქტორო პროგრამა მიატოვა და კომპანია 2025 წლის მარტში დააარსა. იმავე თვეში Axiom-მა 200 მილიონი დოლარის მოზიდვა შეძლო Menlo Ventures-ის ხელმძღვანელობით. პროექტის განსახორციელებლად, გუნდმა AI აგენტებს თავისუფალი სტრუქტურა მისცა და პარალელურ რეჟიმში მუშაობის საშუალება დართო.

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

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

„შავი ხვრელის“ შევსება და მომავლის გეგმები

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

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

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

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