/ai/ – pfpmd AI laboratory


b1a28b1a28937226b4800ad1dbb001a97dc6f – ``Автоматическое доказательство теорем''

@45f69ce3c92a46b9a35d9ab5225ffddc fulmar 2021-08-18 12:07:27
Тред автоматического доказательства теорем.
Почему это важно: @f4d81@f4d81bb441fe4b11baf12123b1df2f7b @880c2@880c21c50af14718ba8c55005383e04a @36b4f@36b4f43dc083451e85276d58173c7e33
Я думаю, что подход к этой задаче должен быть следующий. Нужно проанализировать существующие доказательства и вычленить из них все эвристики, которые использует человек. Задача усложняется тем, что
1. подавляющее большинство существующих доказательств не записаны на формальном языке. И автоматически перевести их в формальный язык - это очень сложная задача.
2. доказательства не содержат всех эвристик, которые привели человека к открытию этого доказательства. Не хватает важных записей о мотивации и интуиции.
3. даже если бы у нас был огромный трейнинг сет из пар (теорема, доказательство), не получится применить обычное машинное обучение т.к. мы не имеем тут дело с дифференцируемыми функциями и поэтому backpropagation не будет работать.
@632e96c06ea648dcba4b59ef7f9ca489 fulmar 2021-08-19 00:31:31
Мне не нравится любой подход, который начинается с того, что conjecture приводится к conjunctive normal form. Люди так не доказывают теоремы.
@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 не существует в интуиционистской логике. А меня интересует именно она, потому что мне нужны конструктивные доказательства существования.