Interactive theorem proving is not adversarially robust
Like… sure, but I think they are much closer than other systems, and if we had to find anything adversarially robust to train RL system against, fixing up ITPs would seem like a promising avenue?
Put another way, I think Lean’s lack of adversarial robustness is due to a lack of effort by the Lean devs[1], and not due to any fundamental difficulty. E.g. right now you can execute arbitrary code during compile time, this alone makes the whole system unsound. But AFAIK the kernel itself has no known holes.
Would be nice to see some focused effort e.g. by these “autoformalization companies” on making Lean actually adversarially robust.
Right now I make sure to write the top-level theorem statements with as little AI assistance as possible, so they are affected only by my (hopefully random) mistakes and not by any adversarial manipulation. I manually review Lean code written by AIs to check for any custom elaborators (haven’t seen an AI attempting hacking like that so far). And I hope that the tactics in Lean and Mathlib don’t have any code execution exploits.
I also think—and I believe that the Harmonic folks are on the same page here—that we need a variety of (purely static) techniques for compressing proof-history context about things like, “what tactics have we tried and how did they fail? How is the (potentially very large) proof in which this particular thm lives structured?” etc.
In short, I agree that there is a lot of work to be done around improving ITPs (especially Lean which seems to be the dominant choice for this kind of work) to work well in the kind of RL environments we are discussing :)
Like… sure, but I think they are much closer than other systems, and if we had to find anything adversarially robust to train RL system against, fixing up ITPs would seem like a promising avenue?
Put another way, I think Lean’s lack of adversarial robustness is due to a lack of effort by the Lean devs [1] , and not due to any fundamental difficulty. E.g. right now you can execute arbitrary code during compile time, this alone makes the whole system unsound. But AFAIK the kernel itself has no known holes.
Would be nice to see some focused effort e.g. by these “autoformalization companies” on making Lean actually adversarially robust.
Right now I make sure to write the top-level theorem statements with as little AI assistance as possible, so they are affected only by my (hopefully random) mistakes and not by any adversarial manipulation. I manually review Lean code written by AIs to check for any custom elaborators (haven’t seen an AI attempting hacking like that so far). And I hope that the tactics in Lean and Mathlib don’t have any code execution exploits.
The Lean devs are awesome, I am just saying that this does not seem like their top priority.
I agree with everything you said here.
I also think—and I believe that the Harmonic folks are on the same page here—that we need a variety of (purely static) techniques for compressing proof-history context about things like, “what tactics have we tried and how did they fail? How is the (potentially very large) proof in which this particular thm lives structured?” etc.
In short, I agree that there is a lot of work to be done around improving ITPs (especially Lean which seems to be the dominant choice for this kind of work) to work well in the kind of RL environments we are discussing :)
I just noticed that there now is a Lean checking system that’s intended to be adversarially robust: https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-comparator
https://github.com/leanprover/comparator
Yes! I believe Axiom AI has been involved with this effort.