В последнее время много шумят о способности языковых моделей доказывать математические теоремы и как, якобы, это что-то значит для наступления сингулярности. Думаю, стоит дать краткую политинформацию для широкой публики.

Еще до начала массового психоза на тему языковых моделей я писал, что формализация математики неинтересна самим математикам по внутрицеховым причинам, и этих средневековых мракобесов скоро начнут бить. Кажется, итс файнали хэппенинг!

Автоматические или хотя бы автоматизированные доказательства теорем это область знания с полувековой историей. Понятно, что ей занимаются ботаники второго порядка (т.е. их гнобят ботаники первого порядка, которых гнобят нормальные люди), и потому никто, кроме них, не знает, что там происходит, и не хочет знать. А знать надо бы.

Доказательство теоремы на компьютере состоит из трех составных частей ( ;) ). Сначала надо записать теорему на языке некоторой логики. Затем пишется собственно доказательство или сценарий поиска доказательства. Наконец, доказательство должно пройти автоматическую проверку в движке, реализующем эту логику.

Программистам аналогия должна быть понятна: записать типы функций, затем их реализации, затем скомпилировать. Если компилируется, теорема доказана.

Языковые модели не решают последний этап, проверку верности доказательства. Это всегда делает уже существующий десятилетиями инструмент вроде Coq или Isabelle, ну или новомодный Lean, которому лишь немногим более десяти лет, т.е. скорее всего в нем полно ошибок, позволяющим «доказывать» (т.е. не отвергать) фальсифицируемые утверждения.

Если бы не была проведена полувековая работа над этими инструментами (никак не связанная ни с каким машинным обучением), никаких «доказательств» языковые модели не смогли бы сделать. Максимум, документ, красиво набранный в LaTeX, но внутренне бессмысленный. Нет автоматической проверки — нет доказательства.

Если записать теорему на формальном языке и затем запустить цикл, в котором языковая модель будет пытаться написать доказательство, а формальный инструмент будет ей указывать на ошибки, то вполне вероятно, что спустя какое-то время доказательство будет найдено. С одним исключением, о котором я скажу чуть ниже.

Это выглядит впечатляюще для профанов, но не ново. Есть множество подходов к автоматическому поиску доказательств, но у большинства у них есть недостаток: они не требуют затрат на графические ускорители, т.е. никак не способствуют росту котировок акций Nvidia. Поэтому о них никто не знает, кроме ботаников второго порядка.

Исключение, в котором ни языковая модель, ни какая-то другая система доказательства теорем не смогут найти доказательство, это случай, когда теорема ложна, т.е. доказательства не может быть. Поэтому прежде чем начинать писать доказательство, нужно сначала попытаться сфальсифицировать теорему, найти контрпримеры.

На днях способность языковых моделей находить контрпримеры попала в новости и сильно удивила профанов. Что-то про опровержение какой-то гипотезы якобиана, я толком не понял, о чем это, потому что плохо разбираюсь в математике. Но я разбираюсь в автоматической генерации контрпримеров, потому что мой научный руководитель изобрел QuickCheck.

(Он пытался коммерциализировать это изобретение, но особого успеха не вышло, и недавно он вышел на пенсию. Совсем немного не дождался. А его давний соавтор устроился работать над языком описания метавселенных в Epic Games, бросил жену и двух детей и заново женился на молодой аспирантке. Правда, я не уверен, что именно в таком порядке.)

Если вы запишете теорему на формальном языке, и она фальсифицируема, вы увидите первые контрпримеры уже спустя несколько секунд. Этой функциональности уже более десяти лет, но она не позволяла очевидным образом раздуть классический пузырь на рынке полупроводников, поэтому о ней никто не знает, кроме ботаников второго порядка.