/ai/ – pfpmd AI laboratory


Start a New Thread


@45f69ce3c92a46b9a35d9ab5225ffddc fulmar 2021-08-18 12:07:27
Тред автоматического доказательства теорем.
Почему это важно: @f4d81@f4d81bb441fe4b11baf12123b1df2f7b @880c2@880c21c50af14718ba8c55005383e04a @36b4f@36b4f43dc083451e85276d58173c7e33
Я думаю, что подход к этой задаче должен быть следующий. Нужно проанализировать существующие доказательства и вычленить из них все эвристики, которые использует человек. Задача усложняется тем, что
1. подавляющее большинство существующих доказательств не записаны на формальном языке. И автоматически перевести их в формальный язык - это очень сложная задача.
2. доказательства не содержат всех эвристик, которые привели человека к открытию этого доказательства. Не хватает важных записей о мотивации и интуиции.
3. даже если бы у нас был огромный трейнинг сет из пар (теорема, доказательство), не получится применить обычное машинное обучение т.к. мы не имеем тут дело с дифференцируемыми функциями и поэтому backpropagation не будет работать.
1 replies omitted. Click here to view the first page.
@34e639b309c343458f499f9fbba45ee5 fulmar 2021-08-19 09:53:25
>не получится применить обычное машинное обучение т.к. мы не имеем тут дело с дифференцируемыми функциями
Нет, я ошибался. Можно использовать graph neural networks, а логическое высказывание представляется в виде дерева.
@36dd8928027b4954a5d8351eced334da fulmar 2021-08-19 09:55:50
Точнее не в виде дерева, а в виде DAG.
@dfdbce7ffb1a4852b2fe1fb0aef95023 fulmar 2021-08-19 22:26:48
@632e9@632e96c06ea648dcba4b59ef7f9ca489 Мне это не нравится также потому, что cnf не существует в интуиционистской логике. А меня интересует именно она, потому что мне нужны конструктивные доказательства существования.

@c2ff72b8b4064a6689789e0194729c7f Anonymous 2020-03-02 08:01:21
Тред про искусственные нейросети.
37 replies omitted. Click here to view the first page.
@e00d95fcfcd14c68a82c8221d5151567 Anonymous 2020-03-05 12:02:49
@55e5b3bc3db44d6abd29ab87d9c4e261 Anonymous 2020-03-05 12:42:57
@e00d9@e00d95fcfcd14c68a82c8221d5151567
> There is the Decoupled Neural Interfaces (DNI) from Google Deepmind. Instead of using backpropagation, it uses another set of neural networks to predict how to update the parameters
Вот это круто. Действительно, почему бы сами нейронки не использовать для задачи обучения.
@b98df067784b401e9d522c76f6eb10c9 Anonymous 2020-03-11 10:40:56