dumaiИИ научили выбирать менее похожие на известные математические теоремы
Препринт, ещё не рецензирован · ранние данные
Кратко
Авторы предложили оценивать интересность математической теоремы по отношению длины доказательства к длине её формулировки и обучили модель выбирать такие теоремы. В вычислительных экспериментах она создавала больше новых вариантов, а их доля совпадений с уже известными теоремами в библиотеке Mathlib снизилась с 91,9% до 30,6%.
Зачем это знать?
Такой показатель может помочь компьютерам выбирать, какие предположения проверять в математических библиотеках с автоматически проверяемыми доказательствами. Но это пока результат вычислительных экспериментов, а не математических открытий, подтверждённых людьми.
Разбор
Авторы проверяли не только, умеет ли модель доказать утверждение, но и насколько оно может быть полезным продолжением уже накопленной математики. Для этого они сравнивали, сколько места занимает доказательство, с длиной самой формулировки. Затем отдельно обучили модель оценивать, насколько трудно доказать утверждение, если заранее разрешить использовать определённый набор известных фактов. Такая оценка помогает отсеивать простые переформулировки знакомых результатов ещё до долгого поиска доказательства.
Важный результат — выбранный показатель связан не только с формальными свойствами текста, но и с внешней оценкой дальнейшей пользы теоремы. Модель научилась предсказывать сложность доказательств точнее, чем универсальные передовые модели, а затем использовала эту оценку в несколько шагов: сначала предлагала возможные утверждения, потом выбирала наиболее интересные и добавляла их в расширяющуюся библиотеку. В итоге система сама формировала новые цели для следующего цикла, не получая от человека заранее список задач.
Раньше автоматические системы в основном старались доказать уже поставленные человеком утверждения или находили близкие варианты того, что уже есть в библиотеке. Здесь авторы сместили задачу: компьютеру предложили самому решать, какие утверждения стоит проверять. Это всё ещё не означает, что машина нашла важные математические идеи: речь идёт о формально записанных и проверяемых кандидатах, а их практическая ценность требует отдельной оценки.
Ключевые цифры
Можно ли доверять
Это препринт с arXiv, поэтому его ещё не проверили независимые рецензенты. Результаты получены в вычислительных экспериментах с формальной математической библиотекой, а не подтверждены людьми как полезные новые теоремы; абстракт также не сообщает независимой проверки качества найденных утверждений.
- Это препринт, поэтому результаты ещё не прошли независимую проверку.
- Связь метрики с полезностью показана в рамках формализованных математических библиотек и не доказывает, что сгенерированные теоремы важны для математики в целом.
- Результаты относятся к вычислительным экспериментам с моделями, а не к практическим математическим открытиям, подтверждённым людьми.
Пересказано ИИ по научной статье. Это научпоп, а не совет врача. Как это устроено