AI намери връзка между съвременната геометрия и формули от 19 век

Преди пет години математиците Дауей Чен и Куентин Жандрон работят по предизвикателен проблем в алгебричната геометрия, свързан с диференциали, т.е. инструменти за анализ, които помагат за измерване на „разстояния“ по изкривени повърхности. В един момент те се натъкват на неочакван проблем: ключова стъпка се основава на необичайна формула от теорията на числата, но изследователите не могат нито да я докажат, нито да я обосноват. В крайна сметка резултатът трябваше да бъде формулиран като хипотеза, а не като теорема.

Наскоро Чен се опитал да се върне към проблема с помощта на ChatGPT, като прекарал часове в обработка на заявките с надеждата да получи работещо доказателство, но нямало забележим напредък. Повратният момент настъпва на математическа конференция във Вашингтон: на нея Чен се запознава с Кен Оно, известен математик, който наскоро е напуснал Университета на Вирджиния, за да се присъедини към стартъпа Axiom. Компанията разработва инструменти с изкуствен интелект за доказване на теореми и е съоснована от Карина Хонг, бивша студентка на Оно.

Чен разказал на Оно за своя нерешен проблем и още на следващата сутрин получил готово доказателство, което системата AxiomProver генерирала. Според Чен след това „всичко естествено си дошло на мястото“. Заедно с екипа на Axiom той оформил материала в статия и тя вече е публикувана в arXiv.

Както описва Axiom, техният инструмент открива връзка между проблема на Чен и Гендрон и числено явление, което е изследвано за първи път още през 19 век. След това системата изготвя доказателство и, което е изключително важно за математиката, независимо проверява неговата правилност. Той твърди, че изкуственият интелект е забелязал нещо, което хората са пропуснали.

От Axiom твърдят, че това не е изолиран случай: през последните седмици системата им е предложила няколко нови доказателства за проблеми, които от години остават нерешени от експерти в различни области. Все още не става дума за най-известните и „скъпи“ математически проблеми, а за въпроси, които наистина са забавили напредъка в определени направления. На този фон все повече математици започват да използват инструментите с изкуствен интелект не само за търсене на идеи, но и за довеждане на разсъжденията до строги, проверими доказателства.

От особен интерес е възможното приложение на такива подходи извън рамките на чистата математика. В статията се споменава перспектива за разработване на софтуер, който е по-устойчив на определени класове кибератаки: ако AI може да изготвя и проверява строги доказателства, подобни методи могат да се използват за формална проверка на кода, при която коректността и надеждността се доказват чрез доказуеми свойства, а не чрез тестове.

Подходът на Axiom е изграден върху комбинация от големи езикови модели и AxiomProver – собствена система за разсъждение, усъвършенствана за създаване на доказателства, които могат да бъдат официално проверени.

За тази цел се използва Lean, специализиран математически език и екосистема за проверка. Компанията подчертава, че това отличава техния инструмент от „конвенционалните“ AI модели: той не само генерира текст, но и трябва да бъде проверен във формално представяне, което намалява риска от красиви, но неправилни разсъждения. Google показа подобна идея с AlphaProof през 2024 година, а Хонг твърди, че тяхната система има по-нови техники и забележими подобрения.

В допълнение към историята с хипотезата на Чен и Гендрон, Axiom цитира и други примери. Един от тях е свързан с хипотезата на Фела за синергиите (syzygies), т.е. конструкциите в алгебрата, при които отношенията между изразите се „подреждат“ по определен начин. Забележително е, че тази тема включва формули, открити преди повече от 100 години в трудовете на Шриниваса Рамануджан. Тук, според описанието на компанията, AxiomProver не просто е запълнил пропуск в почти готово решение, а е изградил доказателството в неговата цялост, от началото до края, и след това го е потвърдил официално. Две други доказателства, споменати в статията се отнасят до вероятностен модел на „задънените улици“ в теорията на числата и инструменти, които са израснали от методи, които някога са помогнали да се атакува и в крайна сметка да се реши Великата теорема на Ферма.

Чен, който видя как собствената му хипотеза се превръща в доказана теорема с помощта на AI гледа на бъдещето по-скоро оптимистично. Той сравнява ситуацията с появата на калкулаторите: математиците не са забравили таблицата за умножение, но са получили инструмент, който е разширил възможностите им. Според него AI може да се превърне не просто в помощник, а в интелектуален партньор, който отваря по-широки хоризонти за изследвания.