by Glaive Team
Many things happened in the last few months which delayed this report. In part:
Our work diligently continues and we will have more to share soon. In the meantime, here is a general summary of where we are heading and how our different technologies are coming together.
While we internally run multiple projects in parallel, they all converge toward a unified vision. Our goal is to provide accurate, explainable, performant models that are representative of today’s theorem proving workflow.
Currently we are able to connect a language model to a proof assistant via very basic means. Proofs are checked by the proof assistant and the only method of interacting is via strings and files.
flowchart LR
LM[Language Model] -->|String output| PA[Proof Assistant]
In those diagrams, squares denote software boundaries, and arrows denote messages sent to another piece of software. The text labels the nature of the message.
By abstracting over the interface of a proof assistant, we can filter messages that do not make sense to the theorem prover, only allowing valid forms of interaction.
This accelerates the feedback loop usually provided by the compiler where one would try a tactic, see if the goal has changed, and if it has not or produces an error, try something else. Here, we are only using valid tactics and so we don’t need to explore the ones that do nothing or cause errors.
In addition this moves some responsibility away from the compiler, catching errors ahead of time, and into the harness which can be much faster since it does not rely on IO nor needs to carry the current compiler state.
flowchart LR
LM[Language Model] -->|String Output| Parser[Parser]
Parser -->|Valid Message| PA[Proof Assistant]
In addition to generating well-formed messages, we can further catch mistakes and inconsistencies by matching the type of a tactic with its current goal before it reaches the theorem prover and its kernel. This further reduces the search space for a well-formed proof and reduces reliance on the compiler to produce feedback for the AI assistant.
flowchart LR
LM[Language Model] -->|String Output| Parser[Parser]
Parser -->|Valid Message| TC[tactic checker]
TC -->|Valid Tactic| PA[Proof Assistant]
This is where we stand right now, we are currently integrating tighter feedback loops that take into account the current proof state and only allow valid proof steps forward by using MCP’s notification system to update the harness of the capabilities offered by the proof assistant. With that said, we plan to take this even further.
By internalising the structure of valid prover interaction in the model we can entirely eliminate the parser stage from this picture. This has two performance benefits, first we do not need to ever retry generating token that are not valid editor messages. Second, we now learn a much smaller, simpler language, where the unit of learning is not general purpose language tokens but specialised units of theorem proving interaction. Because the learnable domain is smaller we expect the computing properties of such models to be equally economical.
flowchart LR
LM[Language Model] -->|valid message| TC[tactic checker]
TC -->|Valid Tactic| PA[Proof Assistant]
As our work on Polylang continues, we expect to be able to write tactics in polylang directly rather than in an intermediate encoding in Lean. This will in turn remove the need for the system to talk to the proof assistant in commands and talk directly in tactics. This change is enabled by the polylang compiler which provides a natural data set to learn from, rather than learning from Lean syntax and running the theorem prover to compute loss.
flowchart LR
PM[Polylang Structure Model] -->|Valid Tactic| PA[Proof Assistant]