В IBM создали искусственный интеллект, способный совершать научные открытия

Согласно статье, опубликованной в Nature Communication, ИИ AI-Descartes заново «открыл» третий закон Кеплера, вывел уравнение адсорбции газов твердыми поверхностями Ленгмюра, и предложил хорошее приближение формулы замедления времени при высоких скоростях в рамках специальной теории относительности (СТО) Эйнштейна.

Ключевым методом, который использует AI-Descartes, является символьная регрессия, заключающаяся в поиске математических выражений, которые наилучшим способом соответствуют наблюдаемым данным, путем случайного комбинирования операторов (+, -, ×, ÷, квадратный корень, логарифм, экспонента), констант и других «блоков», при этом выражение не должно быть слишком сложным. Сама по себе символьная регрессия имеет ограничения, поскольку не все математические выражения, соответствующие данным, имеют научный смысл.

Чтобы решить эту проблему, разработчики объединили символьную регрессию с автоматизированными инструментами аргументации (англ. reasoning tools). Символьная регрессия проводилась методом смешанно-целочисленного нелинейного программирования (MINLP), а в качестве инструмента аргументации была выбрана KeYmaera X — система автоматизированного доказательства теорем, которая способна к дедукции, алгебраическим или компьютерно-алгебраическим рассуждениям.

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

Для каждой символьной модели, полученной через регрессию, система определяла «расстояние» между сгененированным выражением и наблюдаемыми данными, а также между выражением и теоретическими предпосылками. Например, в случае третьего закона Кеплера такой предпосылкой служили законы Ньютона. «Расстояния» являлась мерой ошибки, которая может возникать из-за погрешностей в измерениях или неполноты и неточности теоретических предпосылок. Если модель не могла быть выведена из набора аксиом, то система аргументации делала вывод, что необходимо получить дополнительные данные либо добавить ограничения. Мера ошибки позволяла очертить круг моделей, которые могли представлять наибольший интерес для дальнейшей проверки.

Таким образом, подход, реализуемый в AI-Descartes, отличается от традиционного научного подхода. Вместо того чтобы из общей теории выводить гипотезы и проверять их на эмпирических данных, ИИ строит из эмпирических данных гипотезы и сверяет их с теорией.