Как пытаются подходить к автоматическому доказательству теорем с помощью ИИ?
К сожалению, у меня не получилось в небольшом посте одновременно объяснить задачу и подход, поэтому сегодня будет только про задачу. Итак, поехали.
Существует Metamath, где формализованы доказательства ~38к утверждений в математике, опираясь друг на друга, и в конечном счёте на базовые аксиомы.
Все доказательства теорем в Metamath базируются на подстановке - это когда мы применяем аксиому или уже доказанную ранее теорему к имеющимся "объектам", чтобы сгенерировать новое промежуточное утверждение. И так, пока не дойдём до теоремы. Этот подход называется forward manner.
Нас же интересует backward manner - это когда у нас есть доказываемое утверждение, и мы применяем к нему тактику, то есть предполагаем, какие промежуточные утверждения, при применении какой-нибудь аксиомы или теоремы, доказали бы желаемое.
Пример: чтобы доказать, что A=C, мы должны доказать, что A=B и B=C, и потом применить транзитивность. Теперь пытаемся доказать, что A=B и B=C.
Таким образом, в backward manner процесс доказательства - это построение дерева.
У каждого утверждения есть дети-тактики - попытки по-разному декомпозировать его на более базовые. И у каждой тактики есть дети-утверждения, все из которых мы должны доказать. Если какая-то вершина оказывается аксиомой или уже доказанным утверждением, то она автоматически доказана. Соответственно, шаг поиска это добавление тактики-ребёнка вместе с его детьми-утверждениями к уже существующей вершине. Это всё похоже на настольную игру. См. картинку.
Буду рад, если математики в комментариях подскажут, какой по сложности является эта задача, если решать её перебором.
А в следующих постах я расскажу о том, как поиск доказательств теорем ускоряют с помощью нейросетей, насколько плохо пока получается, и подумаем над фундаментальными причинами.
@knowledge_accumulator
К сожалению, у меня не получилось в небольшом посте одновременно объяснить задачу и подход, поэтому сегодня будет только про задачу. Итак, поехали.
Существует Metamath, где формализованы доказательства ~38к утверждений в математике, опираясь друг на друга, и в конечном счёте на базовые аксиомы.
Все доказательства теорем в Metamath базируются на подстановке - это когда мы применяем аксиому или уже доказанную ранее теорему к имеющимся "объектам", чтобы сгенерировать новое промежуточное утверждение. И так, пока не дойдём до теоремы. Этот подход называется forward manner.
Нас же интересует backward manner - это когда у нас есть доказываемое утверждение, и мы применяем к нему тактику, то есть предполагаем, какие промежуточные утверждения, при применении какой-нибудь аксиомы или теоремы, доказали бы желаемое.
Пример: чтобы доказать, что A=C, мы должны доказать, что A=B и B=C, и потом применить транзитивность. Теперь пытаемся доказать, что A=B и B=C.
Таким образом, в backward manner процесс доказательства - это построение дерева.
У каждого утверждения есть дети-тактики - попытки по-разному декомпозировать его на более базовые. И у каждой тактики есть дети-утверждения, все из которых мы должны доказать. Если какая-то вершина оказывается аксиомой или уже доказанным утверждением, то она автоматически доказана. Соответственно, шаг поиска это добавление тактики-ребёнка вместе с его детьми-утверждениями к уже существующей вершине. Это всё похоже на настольную игру. См. картинку.
Буду рад, если математики в комментариях подскажут, какой по сложности является эта задача, если решать её перебором.
А в следующих постах я расскажу о том, как поиск доказательств теорем ускоряют с помощью нейросетей, насколько плохо пока получается, и подумаем над фундаментальными причинами.
@knowledge_accumulator