Новости ИИ

[photon]

Статью не смотрел, смущает немного

mihaild в сообщении #1430210 писал(а):

на датасете авторов

[Sender]

photon, авторы достаточно подробно описывают процесс формирования данного датасета.

[photon]

Sender в сообщении #1430505 писал(а):

авторы достаточно подробно описывают процесс формирования данного датасета.

Открыл статью. Конечно, это круто, что нашли подход, придумали как формализовать, но все равно датасет получается специфический. Например, авторы пишут:

Цитата:

Unfortunately, solutions of random problems sometimes do not exist (e.g. the integrals of $f(x) = \exp(x^2)$ or $f(x) = \log(\log(x))$ cannot be expressed with usual functions), or cannot be easily derived.

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

[SiberianSemion]

photon в сообщении #1430515 писал(а):

а авторы просто не берут такие задачи в рассмотрение.

Да. На этапе тренировки алгоритма. Приведенная вами цитата как раз из раздела, где авторы рассказывают, как формировали набор функций и их первообразных для тренировки своего детища.

Но есть ли основания считать, что авторы не брали такие задачи в рассмотрение и во время тестировочного сравнения с Mathematica? Я прямых указаний на это в тексте статьи не нашел. Хотя вполне мог и пропустить: раздел про образование тестировочных заданий сильно нагружен терминами из machine learning, так что я просмотрел его по диагонали.

[photon]

SiberianSemion в сообщении #1430536 писал(а):

Но есть ли основания считать, что авторы не брали такие задачи в рассмотрение и во время тестировочного сравнения с Mathematica?

Думаю, что если бы рассматривали подобные задачи при тестировании, то достигнуть для интегралов 99.6% было бы нереально.

[mihaild]

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

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

[realeugene]

А когда эта система ошибается, она отказывается брать интеграл, или выдаёт неправильный ответ?

[mihaild]

Выдает неправильный ответ. Но т.к. проверить правильность ответа сравнительно просто, то это не очень страшно.

[realeugene]

mihaild в сообщении #1430595 писал(а):

ает неправильный ответ. Но т.к. проверить правильность ответа сравнительно просто, то это не очень страшно.

Тогда до уровня к.ф.-м.н.-а. системе ещё расти и расти. Вообще говоря, таблица интегралов ошибается реже.

[Sender]

realeugene в сообщении #1430609 писал(а):

Тогда до уровня к.ф.-м.н.-а. системе ещё расти и расти.

Если уж сравнивать его с нейронной сетью, он должен брать их в уме.

[mihaild]

realeugene в сообщении #1430609 писал(а):

Вообще говоря, таблица интегралов ошибается реже

Вот только берет интегралы она тоже реже.
Или можно сказать, что оценивается не чисто нейронка, а нейронка + проверка правильности.

[Sender]

mihaild в сообщении #1430595 писал(а):

Но т.к. проверить правильность ответа сравнительно просто, то это не очень страшно.

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

-- Вт дек 17, 2019 12:33:31 --

Кстати, в списке литературы в той статье есть ссылка на другую работу 2017 года, описывающую гибридный метод автоматического доказательства теорем. Там одна из основных проблем, как я понимаю, - это сравнительно небольшой объём имеющихся баз формальных доказательств: авторы говорят о $91877$ доказательствах в логике первого порядка, распределяемых между обучающей и проверочной выборками (для сравнения, в обсуждаемой статье об интегрировании размер обучающей выборки исчисляется десятками миллионов). Тем не менее, им удалось доказать около $7\%$ утверждений из базы Mizar, для которых ранее отсутствовали автоматически сгенерированные доказательства.

[mihaild]

Критика результата выше. Основные моменты - примеры очень специфическое множество, на котором шло сравнение, зависимость от дополнительных методов символьных вычислений, и возможные артефакты в генерации - например при взятии производной композиции сомножители могут выдаваться в определенном порядке, который не учитывает mathematica но учитывает нейронка; соответственно если поменять этот порядок, то нейронка сломается.

[Rasool]

Sender в сообщении #1430251 писал(а):

Да, видимо, не за горами тот день, когда смогут доказывать теоремы лучше среднего к.ф.-м.н.-а.

Я более скептичного мнения об этом. Доказательство математических теорем, ИМХО - это задача для "сильного" ИИ, вполне возможно, это AI - полная задача.

[Mihaylo]

Rasool в сообщении #1432430 писал(а):

Доказательство математических теорем, ИМХО - это задача для "сильного" ИИ

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

Да, AI-полные задачи существуют, но решаются они не сильным интеллектом, а обычным. И никто не говорит, что эти задачи должны непременно решаться с заданным функционалом качества. Нету никакого сильного интеллекта. Это фантазия.