top | item 30588672

(no title)

awelkie | 4 years ago

Having just skimmed the linked tutorial, it looks like GFlowNets could be useful for automated theorem proving. Anyone with more knowledge know if this is possible?

discuss

order

manux|4 years ago

Yes, although they may not be ideal unless you're able to define a "distance" between a proof that the agent is proposing and whether that proof is correct (i.e. unless you're able to define a reward or energy function).

It may be possible to infer/learn a score from existing proofs though. We have a paper that manages to both learn a flow and an energy function (the score) from data: https://arxiv.org/abs/2202.01361

I don't know much about theorem proving though. Can some value be attributed to partial proofs?

andrewnc|4 years ago

I don't see why not. I think they can be used for anything a GNN / Transformer could be used for, but with better probabilistic qualities.

mcbuilder|4 years ago

What do you see as the application to GNN / Transformer tasks? Both of those networks are best suited for different tasks, and GFlowNetworks seem well suited to quickly approximating the partition function of say an Deep RL reward distribution, something that MCMC is ill suited for because of the incredibly high dimensional space. I see these all as different techniques, perhaps the ideas will combine at some point but GFlowNetworks are not an evolution of GNNs or Transformers.