Обычный подход при применении обучения с подкреплением к
автоматическим доказательствам теорем заключается в том, что
логические формулы разбирают в абстрактные синтаксические деревья
(Abstract Syntax Trees, AST), которые, не смотря на название, в
строгом смысле деревьями не являются. Потому что они не графы
(порядок ребёр, исходящих из вершины, важен, потому что, в общем
случае, важен порядок аргументов функций). А графовые фреймворки, как
это ни странно, работают с графами:) Поэтому обычно AST обогащают
дополнительными рёбрами так, чтобы они однозначно отображались на
ациклические ор-графы. И дальше уже используют графовые нейронные
сети (Graph Neural Networks, GNN). И мне это казалось логичным до
поры до времени. Сейчас же я понимаю, что здесь налицо лишний шаг ---
отображение AST в графы. Неужели никто не строит нейронки сразу на
AST? Конечно, строит, для поиска дубликатов кода и его
автоматического аннотирования, например. Вроде бы разумно попробовать
делать то же самое и с логическими формулами (потому что они всё
равно записываются на формальных языках, описываемых какой-то
BNF-совместимой грамматикой), но не тут-то было. Многие работы по
вложению AST публикуются вообще без кода, либо с кодом, который
невозможно запускать, но даже лучшие образцы (например, code2vec),
сильно зависят от конкретных языков программирования. И это печально,
потому что, по идее, должны бы они зависеть только от AST, которые
как бы разные в разных языках, но сука, всё-таки одинаковые. Но нет
блять, все всё делают по-разному. Добро пожаловать в исследования!
