| |||
|
|
Задача несколько иная, чем генерить картинки. По Карри-Ховарду, теорема - это некая функциональная программа, а процесс доказательства технически идентичен процессу компиляции программы (не вдаваясь в теорию). Компиляторы обычно работают с древовидными структурами данных, а вот машинное обучение делают на графических процессорах или ещё более специализированных устройствах вроде TPU, которые очень быстро обрабатывают тензоры* (коими являются картинки и видео), но которые крайне неэффективно работают с деревьями. То есть процесс обучения нейросети доказательству теорем требует вычислений, которые слабо ложатся на железо, используемое для машоба. Хотя некий madlad вроде как сумел в компиляцию на GPU: https://scholarworks.iu.edu/dspace/hand А теоремы и доказательства генерят на компе, почему нет. Просто не нейросетями. * В computer soyence смысле этого слова Добавить комментарий: |
||||