2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2, 3, 4, 5, 6, 7, 8  След.
 
 Re: Новости ИИ
Сообщение14.12.2019, 20:23 
Заслуженный участник
Аватара пользователя


16/07/14
8344
Цюрих
Нейронки обогнали матпакеты в символьном интегрировании и решении диффуров (на датасете авторов нейронка берет 99.6% интегралов, 97% ОДУ первого порядка и 81% второго, а Mathematica - 84%, 77.2% и 61.6% соответственно).

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение15.12.2019, 01:25 


14/01/11
2916
Да, видимо, не за горами тот день, когда смогут доказывать теоремы лучше среднего к.ф.-м.н.-а. :-)

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение16.12.2019, 12:29 
Экс-модератор
Аватара пользователя


23/12/05
12046
Статью не смотрел, смущает немного
mihaild в сообщении #1430210 писал(а):
на датасете авторов

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение16.12.2019, 12:40 


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

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение16.12.2019, 13:11 
Экс-модератор
Аватара пользователя


23/12/05
12046
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 может для квадрата экспоненты предложить решение в виде ряда или спец.функции, а авторы просто не берут такие задачи в рассмотрение.

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение16.12.2019, 15:53 
Аватара пользователя


24/03/19
147
photon в сообщении #1430515 писал(а):
а авторы просто не берут такие задачи в рассмотрение.

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

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

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение16.12.2019, 17:12 
Экс-модератор
Аватара пользователя


23/12/05
12046
SiberianSemion в сообщении #1430536 писал(а):
Но есть ли основания считать, что авторы не брали такие задачи в рассмотрение и во время тестировочного сравнения с Mathematica?

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

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение16.12.2019, 21:23 
Заслуженный участник
Аватара пользователя


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

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

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение16.12.2019, 22:27 


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

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение17.12.2019, 00:08 
Заслуженный участник
Аватара пользователя


16/07/14
8344
Цюрих
Выдает неправильный ответ. Но т.к. проверить правильность ответа сравнительно просто, то это не очень страшно.

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение17.12.2019, 02:19 


27/08/16
9426
mihaild в сообщении #1430595 писал(а):
ает неправильный ответ. Но т.к. проверить правильность ответа сравнительно просто, то это не очень страшно.
Тогда до уровня к.ф.-м.н.-а. системе ещё расти и расти. Вообще говоря, таблица интегралов ошибается реже.

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение17.12.2019, 03:31 


14/01/11
2916
realeugene в сообщении #1430609 писал(а):
Тогда до уровня к.ф.-м.н.-а. системе ещё расти и расти.

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

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение17.12.2019, 11:22 
Заслуженный участник
Аватара пользователя


16/07/14
8344
Цюрих
realeugene в сообщении #1430609 писал(а):
Вообще говоря, таблица интегралов ошибается реже
Вот только берет интегралы она тоже реже.
Или можно сказать, что оценивается не чисто нейронка, а нейронка + проверка правильности.

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение17.12.2019, 11:54 


14/01/11
2916
mihaild в сообщении #1430595 писал(а):
Но т.к. проверить правильность ответа сравнительно просто, то это не очень страшно.

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

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

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

 Профиль  
                  
 
 Re: Новости ИИ
Сообщение25.12.2019, 13:37 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 120 ]  На страницу Пред.  1, 2, 3, 4, 5, 6, 7, 8  След.

Модераторы: Karan, Toucan, PAV, maxal, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group