როცა 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 წლის მათემატიკური ჰიპოთეზის დამტკიცება — სწორედ ისეთი განცხადება, რომელიც ზემოთ აღწერილი პროცესის მიხედვით, დროებით რჩება მანამ, სანამ ფორმალური ან ექსპერტული ვერიფიკაცია არ დაეწევა მას.
ხშირად დასმული კითხვები
თუ დამტკიცება Lean-ში კომპილირდება, ეს ავტომატურად ჭეშმარიტს ხდის მას?
ეს ნიშნავს, რომ არგუმენტი მართებულად გამომდინარეობს სისტემის საკუთარი აქსიომებიდან და დასკვნის წესებიდან — სწორედ ამიტომაა Lean-ის მსგავსი დამტკიცების დამხმარე პროგრამები ღია კოდის, ფართოდ ტესტირებული და საჯარო შემოწმებისთვის ხელმისაწვდომი, რათა თავად საფუძველიც, რომელთანაც ხდება შემოწმება, სანდო იყოს.
ყველა AI-ის მათემატიკური განცხადება ფორმალურად არის ვერიფიცირებული?
არა. ბევრი გახმაურებული შედეგი არაფორმალური, ბუნებრივ ენაზე დაწერილი არგუმენტია, რომელსაც კვლავ სჭირდება ან ექსპერტის ხელით შემოწმება, ან ფორმალურ სისტემაში თარგმნა, სანამ მათემატიკოსები მას დადასტურებულად ჩათვლიან.
შემიძლია დამტკიცების დამხმარე პროგრამა თავად ვცადო?
დიახ. Lean უფასოა და აქვს როგორც ბრაუზერზე დაფუძნებული, ისე ჩამოსატვირთი ხელსაწყოები; საზოგადოების საწყისი გზამკვლევი სტანდარტული საწყისი წერტილია — მისი გამოსაცდელად მათემატიკის დოქტორის ხარისხი არ გჭირდებათ.
შექმნა თუ არა AI-მ ნამდვილად ახალი, ფორმალურად ვერიფიცირებული შედეგი?
დიახ, შეზღუდულ ფარგლებში — AlphaProof-ის საოლიმპიადო დონის Lean დამტკიცებები და მათემატიკოს-AI თანამშრომლობები, როგორიც ტაოს მაგალითია, რეალური, გადამოწმებული შედეგებია — თუმცა ისინი კვლავ გაცილებით ვიწროა, ვიდრე ღია კვლევითი ჰიპოთეზები, სადაც AI-ის მიერ გენერირებული არგუმენტების ფორმალური ვერიფიკაცია ჯერ კიდევ გამონაკლისია, არა წესი.