როცა AI სისტემა აცხადებს, რომ ათწლეულების განმავლობაში გადაუწყვეტელი ამოცანა დაამტკიცა, კითხვაზე „მართლა ასეა?“ პატიოსანი პასუხი ასეთია: ჯერ არა — სანამ არგუმენტი გაცილებით მკაცრ შემოწმებას არ გაივლის, ვიდრე უბრალო წაკითხვა და თანხმობის დაქნევაა. მათემატიკოსები AI-ის სავარაუდო დამტკიცებას ისევე ამოწმებენ, როგორც ადამიანისას — ყოველი ლოგიკური ნაბიჯის ხელახლა გამოყვანით და, სულ უფრო ხშირად, არგუმენტის იმ პროგრამულ უზრუნველყოფაში გატარებით, რომელიც მას ხაზ-ხაზ ამოწმებს მათემატიკის აქსიომებთან მიმართებაში. მტკიცება მიღებულ თეორემად მხოლოდ მაშინ იქცევა, როცა ამ პროცესს გაუძლებს.
ორი განსხვავებული სახის „დამტკიცება“
თანამედროვე AI სისტემები მათემატიკურ არგუმენტებს ორი ფორმით ქმნიან, რომლებიც მსგავსად გამოიყურება, მაგრამ არსებითად განსხვავდება. პირველი — არაფორმალური, ბუნებრივ ენაზე დაწერილი დამტკიცებაა: AI მსჯელობას ჩვეულებრივი მათემატიკური პროზით აყალიბებს, ისე, როგორც ადამიანი დაწერდა სამეცნიერო სტატიაში. მეორე — ფორმალური დამტკიცებაა, დაწერილი „proof assistant“-ის (დამტკიცების დამხმარე პროგრამის) შიგნით, როგორიცაა Lean — პროგრამირების ენა, სადაც ყოველი ნაბიჯი უნდა დასაბუთდეს წესით, რომლის ავტომატურად შემოწმებაც კომპიუტერს შეუძლია. Google DeepMind-ის AlphaProof-მა სწორედ ფორმალური გზა აირჩია: განმტკიცების სწავლებით (reinforcement learning) გაწვრთნილმა სისტემამ Lean-ში დამტკიცებები მოძებნა და 2024 წლის მათემატიკის საერთაშორისო ოლიმპიადაზე ვერცხლის მედლის დონის შედეგს შეუწყო ხელი — რამდენიმე საოლიმპიადო ამოცანა Lean-ის შიგნით ფორმალურად დაამტკიცა.
რატომ არის „ფორმალურობა“ ნდობის ზღვარი
ამ ორ ფორმას შორის სხვავება სწორედ ნდობის მთელი საკითხია. ბუნებრივ ენაზე დაწერილი დამტკიცება დამაჯერებლად შეიძლება ჟღერდეს და მაინც მალავდეს ხარვეზს — მათემატიკის ისტორიაში ბევრჯერ მომხდარა, რომ გამოქვეყნებულ დამტკიცებაში ხარვეზი ადამიანმა რეცენზენტებმა თვეების ან წლების შემდეგ აღმოაჩინეს. ფორმალური დამტკიცება კი, როგორც კი Lean-ის მსგავს სისტემაში კომპილირდება, მექანიკურად შემოწმებულია ლოგიკური წესების ფიქსირებულ ნაკრებთან — არ რჩება ადგილი ნაბიჯისთვის, რომელიც უბრალოდ სწორად ჟღერს, რადგან დაუსაბუთებელი ნაბიჯი უბრალოდ არ კომპილირდება. სწორედ ამიტომ, მათემატიკაში ჭეშმარიტების ყველაზე მყარი ფორმა თანდათან გადადის კითხვიდან „საკმარისმა ექსპერტმა წაიკითხა ყურადღებით?“ კითხვისკენ „კომპილირდა თუ არა?“. ეს ახალი არაფერია: 1976 წლის ოთხი ფერის თეორემა პირველად კომპიუტერმა ათასობით შემთხვევის შემოწმებით დაამტკიცა, თუმცა ბევრმა მათემატიკოსმა მას სრულად მხოლოდ 2005 წელს დაუჯერა, როცა დამოუკიდებლად, ფორმალური დამტკიცების დამხმარე პროგრამის საშუალებით გადამოწმდა.
AI ვერიფიკაციის სისტემას ზეწოლის ქვეშ აყენებს
ახალი ის მოცულობაა. ფილდსის მედლის ლაურეატმა თერენს ტაომ აღწერა მზარდი „წინაღობის შეუსაბამობა“ (impedance mismatch): AI-ს უკვე შეუძლია სავარაუდო დამტკიცებების გენერირება გაცილებით სწრაფად, ვიდრე ადამიანი ექსპერტების ნებისმიერ ჯგუფს შეუძლია მათი წაკითხვა და შემოწმება — შესაბამისად, მათემატიკაში „ბოთლის ყელი“ იდეების გენერირებიდან მათ ვერიფიკაციაზე გადადის. ტაო აქტიურად უჭერს მხარს ფორმალიზაციის მასშტაბურ პროექტებს, რომლებიც გამოქვეყნებულ შედეგებს Lean-ის საზოგადოებრივ ბიბლიოთეკაში, mathlib-ში, აკოდირებენ — ბიბლიოთეკამ უკვე 200 000-ზე მეტი ფორმალიზებული თეორემა მოაგროვა — და პირადადაც გამოიყენა ჩატბოტი მთარგმნელად: ათწლეულების წინანდელი, ხელნაწერად დაწერილი ერდიოშის ამოცანის დამტკიცება 1100-ზე მეტ სტრიქონად, Lean-ის კოდად გადააქცია, რომლის ნაბიჯ-ნაბიჯ შემოწმებაც მანქანას შეუძლია. ეს ის მიმართულებაა, საითაც სფერო მიდის: არა მხოლოდ AI, რომელიც დამტკიცებებს წარმოქმნის, არამედ AI, რომელიც მათ ფორმალიზებასა და ვერიფიკაციაშიც ეხმარება — ანუ თავადვე ხურავს იმ ხარვეზს, რომელიც გახსნა.
როცა სათაურებში ჩნდება, რომ რომელიმე AI-მა ცნობილი ჰიპოთეზა დაამტკიცა, პრაქტიკული წესი მარტივია: ის უნდა ჩაითვალოს დროებით მტკიცებად, სანამ (ა) არგუმენტი ფორმალურ სისტემაში, მაგალითად Lean-ში, არ ითარგმნება და სუფთად არ დაკომპილირდება, ან (ბ) დამოუკიდებელი დარგის ექსპერტები ბუნებრივ ენაზე დაწერილ დამტკიცებას ხაზ-ხაზ არ გადაამოწმებენ და თავიანთ შეფასებას არ გამოაქვეყნებენ. არცერთი ეს ნაბიჯი მყისიერად არ ხდება — და სწორედ ამიტომ, თამამი განცხადებები დამტკიცების შესახებ და დადასტურებული თეორემები სხვადასხვა დროში ცხადდება.
სიახლეებში
ამ პროცესის რეალურ დროში მიმდინარეობის ახალი მაგალითია ჩვენი მასალა იმის შესახებ, თუ როგორ განაცხადა OpenAI-ის GPT-5.6 Sol Ultra-მ 50 წლის მათემატიკური ჰიპოთეზის დამტკიცება — სწორედ ისეთი განცხადება, რომელიც ზემოთ აღწერილი პროცესის მიხედვით, დროებით რჩება მანამ, სანამ ფორმალური ან ექსპერტული ვერიფიკაცია არ დაეწევა მას.