About Theorem.chat
Theorem.chat იღებს მათემატიკური მოთხოვნას და ცდილობს მისი გადაწყვეტა. თქვენ აცხადებთ მოთხოვნას და სტანდარტს, რომელსაც ის უნდა აკმაყოფილებდეს. AI მოდელის პანელი - რამდენიც გსურთ, ნებისმიერი მწარმოებლისგან - ებრძვის მას და კიდევ ერთი მოდელია რეფერენტი. შემდეგ არგუმენტი ფორმალურად Lean 4- ში Mathlib- სთან შედარებით და Lean kernel გადაწყვეტს, არის თუ არა ის დადასტურებული. ეს ბოლო ნაბიჯია პროდუქტი.
რატომ იარაღს, და არა სხვა მოდელს
მოდელს რთული კითხვა დაუსვით და სწორი პასუხი მიიღებთ. რამდენიმე კითხვა და ისინი ხშირად თანხმდებიან, რაც სავარაუდოდ დადასტურებაა და არა: მოდელები ურთიერთგაზიარებას ახდენენ სწავლების მონაცემებს და ურთიერთგაზიარებას ახდენენ ბნელი წერტილების მონაცემებს. მეორე მოდელმა, რომელიც პირველს ამოწურავს, კვლავაც იგივე აზრი აქვს და ამის შესახებ შეიძლება საუბარი. Lean kernel ვერ შეძლებს. ის ან აგებს განცხადებას აქტიუმებიდან და Mathlib- დან, ან არ აკეთებს და დარწმუნება არ ახდენს გავლენას შედეგზე.
ოფიციალური დადასტურების ეგრეთ წოდებული ფუჭად წარმოჩენის ჩვეულებრივი გზები შემოწმებულია და უარყოფილია. დადასტურება, რომელიც sorry- ში ხვრელებს ტოვებს, რომელიც native_decide- ს აპელაციას ახდენს, რომ ბირთვი ნდობის საფუძველზე ჩაატაროს გამოთვლა, ან რომელიც ჩუმად წარადგენს ახალ აკიზომს, იპოვნება და უარყოფილია, ვიდრე წარმატებად ჩაითვლება.
რასაც პანელი ნამდვილად აკეთებს
სკანდალი არის იაფი ნაწილი. პანელი მუშაობს ლიტერატურის - arXiv, OpenAlex, Crossref - ასე რომ ცნობილი შედეგი არის ციტირება, ვიდრე ცუდად გადამდინარე. მას აქვს SageMath და PARI/GP გამოთვლებისთვის, Z3 და CVC5 SMT გადაწყვეტისთვის, OEIS ძიება რიცხვების რიცხვის იდენტიფიცირებისთვის და Python- ის გარემო ქსელის წვდომის გარეშე. ჰიპოთეზა შეიძლება ტესტირება ათასობით შემთხვევის წინააღმდეგ, სანამ ვინმეს დასჭირდება მისი დადასტურების ცდა, და კონტრ მაგალითი წყვეტს დისკუსიას.
Evidence, not eloquence
match არ არის დაფასებული არგუმენტის ხარისხის მიხედვით. განცხადება იშლება მიღების კრიტერიუმებად და კრიტერიუმი მხოლოდ მაშინ განისაზღვრება, როდესაც მის უკან რაღაც შეიძლება განმეორებით შემოწმდეს მესამე მხარის მიერ: წყარო, რომელშიც ახსნილია შესაბამისი მონაკვეთი, ან კოდი, რომელიც რეალურად განხორციელდა მისი რეალური გამონატანით. ადვოკატი თავად განიხილავს ამ მტკიცებულებას გადაწყვეტის წინ და არ შეუძლია match- ს დასრულების განცხადება, როდესაც კრიტერიუმი ჯერ კიდევ გახსნილია.
You set the bar
სტანდარტის არჩევა შენზეა და ჟურნალისტი მას სიტყვასიტყვით ატარებს. ჰკითხე, რას მიიღებდა ყურადღებიანი ექსპერტი და მიიღებ. ჰკითხე სრულ დედუქციურ არგუმენტს ყველა დადგენილი ვარაუდით და შენ ამის საწინააღმდეგოდ გესაჯებიან. ჰკითხე ბარათს, რომელსაც პრიზის მიცემა შეხვდება და ჭეშმარიტი შედეგი ჩვეულებრივ ზუსტად ახსნის, თუ სად დაკარგა პანელი - რაც უფრო მეტს ნიშნავს, ვიდრე დარწმუნებული განცხადება, რომელსაც თქვენ მაინც უნდა შეამოწმოთ.
ნათლად რომ ვთქვათ: ეს არ არის მანქანა, რომელიც ხსნის გახსნილ პრობლემებს. ეს არის მანქანა, რომელიც არ იღებს არგუმენტს როგორც გადაწყვეტილს, როდესაც ის არ არის გადაწყვეტილი და რომელიც გვიჩვენებს ზუსტად რომელი ნაბიჯი ვერ შესრულდა.
A failed formalisation is the useful output
როდესაც Lean არ დახურებს დადასტურებას, თქვენ მიიღებთ ზუსტ მიზანს, რომელიც რჩება. პრაქტიკაში ეს თითქმის ყოველთვის ადგილია, სადაც არაფორმალური არგუმენტი ხელის მხეცით იყო - ნაბიჯი, რომელიც ყველამ წაიკითხა პროზაული ვერსიის წაკითხვისას. ეს მიზანი შემდეგ გადაეცემა იმ ადგილს, რომელიც საუკეთესო ადგილია მისი დაჭრისთვის, ერთად იმასთან, რაც უკვე სცადა და არა სხვა არაფერი. მოდელები დგანან, როდესაც ისინი ჩაკეტილია, თავიანთი სრული ფასით აღდგენა; ერთი კონკრეტული კითხვის გადაცემა სანაცვლოდ ჩვეულებრივ ბლოკავს ტოკენების ნაწილს.
Long work survives
Matches-ის სერვერის მხარეს მუშაობა და სუფთა პაუზა — ბიუჯეტის, პროვაიდერის შეწყვეტის ან თავსატეხების დახურვის გამო — და განახლება ზუსტად იქ, სადაც შეჩერდა.
What this is not for
თეორია არის დედუქციური სიტყვა. ეს საიტი შექმნილია მათემატიკის, ლოგიკის, თეორიული კომპიუტერული მეცნიერების, თეორიული ფიზიკის და ეკონომიკური თეორიისთვის - სფეროები, სადაც დაპირება დადასტურდება. ემპირიული კითხვები ბიოლოგიაში, მედიცინაში, ქიმიაში ან სოციალურ მეცნიერებებში არ წარმოქმნის თეორიებს, ისინი წარმოქმნიან აღმოჩენებს და არანაირი ფორმალიზაცია არ გადაწყვეტს მათ. ჩვენი ძმის საიტი referee.chat ახორციელებს იმავე პანელის და რეფერენტის პროცესს Lean ნაბიჯის გარეშე, ზუსტად ამ კითხვებისთვის.