3 ms·
I don't think the right way to think about its utility is as a replacement. I see it in terms of a NNUE for Stockfish type augmentation, where a small neural ne
by Vetch 3y ago
I don't think the right way to think about its utility is as a replacement. I see it in terms of a NNUE for Stockfish type augmentation, where a small neural network supercharges search. Small neural network because no LLM, not even GPT4, is good enough that the time lost evaluating with them is gained in disproportionally less search done.
Other uses are: better autocomplete from comments for Coq and Lean VScode envs than generalist tools.
Translation from NL sketch to formal proof. This is different from autocomplete in that it should generate long attempts as an automated spitballer. Leave it running a a long time to see if it finds anything when you're stuck. This works for formal and informal proofs but the latter gets no feedback (this is imagining future tunes able to make better use of interactive prover feedback).
Translating formal proofs to natural language.
Combine it with RAG and have it pull in and summarize references from your personal paper collection and the internet. Particularly useful in place of search when you don't have the vocabulary for a concept. As a basis for non-code based autocomplete of mathematical work.
I see unbounded potential for this combination. And a natural setting where between cost of search and the symbolic prover doing the heavy lifting, it's one of those areas that naturally lends itself to specialist Open over API models.
- aSanchezStern 3y agoOh, I think you might misunderstand what I'm comparing it to. The other tools, like Proverbot9001, are exactly the NNUE scenario you describe, where a small neural network guides a search procedure to find proofs; they are more effective at finding formal proofs than Llemma. For other tasks, like non-formal proof generation, Llemma has novel results as far as I know; it's just in terms of producing formal proofs that it currently seems to lack as compared to the state of the art.
- Vetch 3y agoAh you're right. That makes sense. The autocomplete, informal proofs, translation or autoformalization, reference, search, feedback interactive assistant use-cases do seem promising though.
- jychang 3y agoWhen do you think we’ll have something that can do “verify this proof of the ABC conjecture” and it would check the proof?
- aSanchezStern 3y ago1979 :) https://en.wikipedia.org/wiki/Logic_for_Computable_Functions https://en.wikipedia.org/wiki/Logic_for_Computable_Functions
- schoen 3y agoIf the proof is written in a formal language, we have that now! Even several directly competing efforts (for better and worse). https://www.cs.ru.nl/~freek/100/ https://www.cs.ru.nl/~freek/100/ Some people greatly hope that fully formal proofs become a routine part of math research and communication in the future.