Ученые определили, как изучить и использовать хорошие алгоритмы выбора шагов рассуждения при доказательстве теорем. Они исследовали методики в исчислении таблиц соединений, реализованных в LeanCoP, где частичная таблица дает четкое и компактное представление о состоянии, к которому может быть применено ограниченное количество выводов. Об этом сообщает портал Arxiv.org.
Специалисты начали с включения современного алгоритма обучения — графической нейронной сети (GNN) в средство доказательства теорем plCoP. Затем они использовали его для наблюдения за поведением системы в условиях обучения с подкреплением.
Несмотря на лучшую способность сопоставления с образцом, GNN изначально работает хуже, чем ранее использовавшийся более простой алгоритм обучения. Специалисты заметили, что более простой алгоритм менее надежен, то есть его рекомендации имеют более высокую энтропию.
Это заставило их исследовать, как энтропия выбора вывода, реализованного через нейронную сеть, влияет на поиск доказательства. Работа ученых связана с исследованиями в области принятия решений человеком в условиях неопределенности и, в частности, с теорией согласования вероятностей.
Результаты показали, что правильная регуляризация энтропии, то есть обучение GNN быть не слишком самоуверенным, значительно улучшает производительность plCoP на большой математической выборке данных.
