13 миллион жол, 11 күн: Claude Ферма теоремасымен не істеді — және бұл неге теоремадан да маңызды

ЖИ (жасанды интеллект) адамзат үш жарым ғасыр бойы шешуге тырысқан есепті 11 күнде шешкен жоқ. Бірақ болған оқиға одан кем маңызды емес шығар.

1637 жылы Пьер Ферма кітап шетіне белгілі тұжырым жазды: n>2 бүтін сандары үшін a^n+b^n=c^n теңдеуінің оң бүтін сандардағы шешімі жоқ. Ферма дәлелдеуді білетінін айтқан, бірақ оны жазуға кітап шеті жетпеген.

Математика қоғамдастығы қабылдаған алғашқы дәлел тек 1995 жылы пайда болды. Эндрю Уайлстың жұмысы, бастапқы нұсқадағы кемшілік табылғаннан кейін Ричард Тейлормен бірге аяқталып, 129 бетті құрады. Оны тексеру математиктерден бірнеше ай уақыт алды.

Енді Anthropic басқа белесті хабарлады: Claude Ферманың Ұлы теоремасының компьютерде толық тексерілген алғашқы дәлелін жасады.

Мұнда дәлелді ашу мен оны формализациялауды ажырату принципті түрде маңызды.

Claude Уайлске балама нұсқа ойлап тапқан жоқ. Жүйе бар математикалық дәлел желісін формализациялады — атап айтқанда, Анри Дармон, Фред Даймонд және Ричард Тейлордың жеңілдетілген баяндауын пайдаланып, орасан зор математикалық ойлау тізбегін Lean кодына аударды. Онда әрбір логикалық қадамды компьютер тексере алады.

11 күн, 13 миллион жол

Тәжірибе ауқымды деңгейде де қазіргі AI жүйелерінің өлшемімен салыстырғанда ерекше көрінеді.

Claude негізінен дербес түрде шамамен 11 күн жұмыс істеді. Осы уақытта жүйе шамамен 13 млн жол Lean кодын жазды, шамамен 30 300 теореманың компьютерде тексерілетін дәлелін алды, олардың шамамен 29 500-і соңғы дәлелде қолданылды.

Жобаны бір мезгілде Claude агенттерінің ондаған саны жүргізді. Олар шамамен 6 млрд шығыс токен жұмсады. Жол саны бойынша соңғы Lean коды өзі сүйенетін формализацияланған математиканың негізгі кітапханасы Mathlib-тен бес еседен астам үлкен болды. Anthropic бөлек ескертеді: салыстыру шартты — Mathlib әлдеқайда ықшам әрі мұқият өңделген.

Соңғы нәтижені Lean тексерді. Дәлелде дәлелденбеген орындар қалмады, тек Lean-нің үш стандартты аксиомасы ғана қолданылды. Бөлек comparator дәлелденетін теореманың тұжырымы Mathlib-тегі Ферманың Ұлы теоремасының тұжырымына сәйкес келетінін растады.

Claude-тың өзі жеткіліксіз болды

Ең маңыздысы басқа жайт болды.

Алғашқы әрекеттер сәтсіз аяқталды: жекелеген агенттер жергілікті есептермен жақсы айналысты, бірақ жоба өскен сайын жалпы жағдайды жоғалтып, бір-бірімен нашар үйлесе бастады. Мәселе модельдің ойлау қабілетіне де, ондаған агенттің бір орасан зор есеп үстінде жұмысын ұйымдастыру қабілетіне де қатысты болды.

Бетбұрыс Columbia University-дегі Тяньи Пэн мен әріптестері әзірлеген математиканы формализациялауға арналған ашық платформа Prove2Me-ге көшкеннен кейін орын алды.

Prove2Me теоремалар арасындағы бағытталған тәуелділік графын сақтайды. Агенттер қандай тұжырымдар дәлелденгенін, мақсатқа жету үшін тағы не керек екенін көреді, келесі есептерді таңдай алады, қатарлас жұмыс істей алады және бір-бірінің нәтижесін қайта пайдалана алады.

Нәтижесінде математикалық есеп шешетін жай LLM емес, тұтас архитектура пайда болды:

Claude → ондаған агент → есептер графы мен ортақ жад → Lean → формальды тексеру.

Ферма теоремасының өзінен де осы архитектура маңыздырақ болуы мүмкін.

ЖИ қатесін қалай жіберіп алмау керек

LLM-нің басты мәселесі жақсы белгілі: модель ұзақ, сенімді көрінетін, бірақ қате пайымдау құра алады.

Әдетте бұл мәселені модельдің өзін жетілдіру немесе тексеруші ретінде басқа модельді пайдалану арқылы шешуге тырысады.

Формальды верификация мүлде басқа тәсіл ұсынады.

ЖИ міндетті түрде қатесіз болуы шарт емес. Оның қатесі тексеруден өте алмайтын орта құру керек.

Тұйық цикл пайда болады:

ЖИ шешім ұсынады → формальды жүйе тексереді → қате қабылданбайды → ЖИ түзетеді → тексеру қайталанады.

Соңында тек біреуі маңызды: Claude жасаған құрылым тәуелсіз формальды тексеруден өте ме, жоқ па.

Бұл неге математикадан әлдеқайда алысқа шығады

Мұндай архитектура ауқымды деңгейде дамыса, ең қызық салдарлар ЖИ жұмысының нәтижесін қатаң тексеруге болатын салаларда пайда болуы мүмкін: бағдарламалау, микросхема жобалау, инженерлік есептеулер және басқа формализациялауға келетін салалар.

Сонда AI сенімділігінің мәселесі мүлде басқаша қойылады.

Бүгін біз көбіне қателігі азайған сайын азая беретін модель жасауға тырысамыз.

Басқа жол — AI іздеу үстінде қанша қаласа да қателесе алатын, бірақ қате соңғы нәтижені қабылдауға болмайтын жүйелер құру.

Бұл модельдің абсолютты қатесіздігіне қарағанда әлдеқайда шынайы инженерлік мақсат.

Формализация — әлі жаңалық емес

Мұнда Anthropic-тің екі түрлі жетістігін шатастырмау маңызды.

Ферманың Ұлы теоремасы жағдайында жаңа жетістік — ең алдымен бар математиканы автоматты формализациялау мен верификациялау. Anthropic бұл айырмашылықты тікелей атап көрсетеді.

Басқа экспериментте Claude Риман болжамына қатысты есеп үстінде жұмыс істеп, жаңа математикалық нәтиже алды: дзета-функцияның критикалық түзудегі тривиал емес нөлдер үлесінің белгілі төменгі шегін шамамен 41,6%-дан 67,2%-ға дейін жақсартты. Риман болжамын Claude дәлелдеген жоқ.

Айырмашылық түбегейлі:

Ферма — AI бар білімді формализациялайды.

Риман — AI жаңа білім жасауға қатысады.

Осы екі мүмкіндіктің — жаңа математика жасау мен оны кейін машиналық верификациялаудың — қосылуы, мүмкін, ең қызық болашақты білдіреді.

Қазіргі математикалық әдебиеттің барлығын автоматты формализациялау әлі келген жоқ. Anthropic-тің өз нәтижесі Mathlib-ке және Imperial College London мен flt-regular жобаларының бұрын жасалған ашық әзірлемелеріне сүйенеді. Бұл «бірнеше ғасырлық адами математиканың орнына 11 күн» дегенді білдірмейді.

Бірақ шекара айқын жылжыды.

Мүмкін, ЖИ дамуының келесі кезеңі — нәтижесі автоматты түрде дұрыс екені дәлелденетін машина болар.

---

Дереккөздер:

• Anthropic — Formalizing Fermat's Last Theorem

• Дәлелдің толық Lean коды — GitHub Anthropic

• Prove2Me — Scaling Math Formalization

• Anthropic — Claude-тың Риман дзета-функциясы бойынша нәтижелері