Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет montag ([info]montag)
Задача несколько иная, чем генерить картинки.
По Карри-Ховарду, теорема - это некая функциональная программа, а процесс доказательства технически идентичен процессу компиляции программы (не вдаваясь в теорию). Компиляторы обычно работают с древовидными структурами данных, а вот машинное обучение делают на графических процессорах или ещё более специализированных устройствах вроде TPU, которые очень быстро обрабатывают тензоры* (коими являются картинки и видео), но которые крайне неэффективно работают с деревьями.
То есть процесс обучения нейросети доказательству теорем требует вычислений, которые слабо ложатся на железо, используемое для машоба. Хотя некий madlad вроде как сумел в компиляцию на GPU: https://scholarworks.iu.edu/dspace/handle/2022/24749

А теоремы и доказательства генерят на компе, почему нет. Просто не нейросетями.

* В computer soyence смысле этого слова


(Читать комментарии)

Добавить комментарий:

Как:
(комментарий будет скрыт)
Identity URL: 
имя пользователя:    
Вы должны предварительно войти в LiveJournal.com
 
E-mail для ответов: 
Вы сможете оставлять комментарии, даже если не введете e-mail.
Но вы не сможете получать уведомления об ответах на ваши комментарии!
Внимание: на указанный адрес будет выслано подтверждение.
Имя пользователя:
Пароль:
Тема:
HTML нельзя использовать в теме сообщения
Сообщение:



Обратите внимание! Этот пользователь включил опцию сохранения IP-адресов пишущих комментарии к его дневнику.