I've realised there must be at least three components of a
reinforcement learning (RL) based automated prover: an environment
(deductive system), a feature extractor, and the RL algorithm itself.
But I still believed it would be beneficial for training to do
feature extraction during the main RL loop. Unfortunately, to
implement it, one must be able to read the raw environment state
inside some RL framework. And for all reasonable frameworks, of which
I'm aware, working with anything but an array is impossible. Smaller
environments like board games suit such a limitation well. Another
vast class (anything using computer vision, from video games to
robots to self-driving cars) also don't need anything but arrays. But
even for natural languages it's not enough. But then you have
language models, which provide word and sentence embeddings with no
problems. These embeddings are independent of any further task
(generating or summarising texts, sentiment analysis, and whatnot).
For automated provers, there is still no such thing as a generic,
simple, and information preserving logic formula embedding. Some
researchers do that, but I'm not aware of any cases of their reuse in
other projects. So I need to build yet another one. I'd rather do
that with pytorch-lightning, and from what I know, DGL is not that
compatible with it. So I have to move back to PyG, which also has a
richer model collection. We'll see.
