Rover: Reasoning over Rules

Their synthetic language is basically Prolog, disguised as natural-ish English: their "rules" and "facts" are Horn clauses (a conjuction of "premises" that imply a "conclusion") with implicitly universally quantified variables and negation is Negation As Failure under a closed-world assumption. They restrict their rules to have a single variable and their predicates to only binary relations (xRy) and even transform monadics to dyadics (is(Alan,Big) rather than big(Alan)).

While it's easy to see how their technique could be useful in Natural Language Processing, they do a very poor job of supporting their claim that it's useful in formal theorem proving -'as a kind of limited "soft theorem prover"'. Well, what does "kind of limited" and "soft" mean? They make no attempt to compare their work to actual theorem provers and only compare their work to other work with transformers. And yet there is ample scope for comparison with theorem provers: since they try to derive statements from other statements in a restricted Horn-clause language they could directly compare their work to a Resolution-based theorem prover (well, Prolog) that does exactly that and explain what are the advantages and disadvantages of their approach. But they don't do anything like that. They fail completely to place their work in the context of formal theorem proving even as they claim repeatedly that their work somehow fits right into it.

Suffice it to say that their claims of "theorem proving" are far from convincing. Cursory testing with their live demo (as in my other comment in this conversation) suggests that their architecture does not "emulate" the behaviour of a theorem prover, it just does what language models do best: capture statistical regularities in their training dataset. Which is useful in certain contexts, for sure- but nothing like "emulating" the "i/o" of a theorem prover.

From my point of view, as someone coming from the symbolic reasoning side of things, this is a very sloppy attempt to tackle some hard problems that already have perfectly serviceable solutions, but without showing any willingness to put in the work to understand those problems, or why they are hard in the first place.

I'm sorry to rip into this work so harshly, but this is typical of the worst that modern machine learning research has to offer: an ill-informed attempt to impress with bold claims addressed at an audience that lacks the background to evaluate them adequately. It's disturbing to think that this work will be cited henceforth as "evidence that transformers can perform reasoning" and that it may initiate a trend of more claims along the same lines.