Pantograph

Stream: Machine Learning for Theorem Proving

[RexWang]

Just found a new tool for research purposes called PyPantograph, which is worth exploring.

Pantograph’s innovative features pave the way for more advanced machine learning models to perform complex proof searches and high-level reasoning, equipping future researchers to design more versatile and powerful theorem provers.

As stated in the paper here:

The main motivation for creating Pantograph is to overcome the limitations of the interface provided by the Lean 4 Language Server Protocol (LSP),…

It is related to the third approach mentioned by @Jason Rute:

3. Using Lean's language server

[GasStationManager]

This looks very cool. We were just wondering in another thread about the possibility of doing Draft-Sketch-Prove in Lean. Will definitely check this out.

[Notification Bot]

2 messages were moved here from #Machine Learning for Theorem Proving > Interacting with Lean 4 by Jason Rute.

[Quinn]

she's in zulip @Leni Aniva

[RexWang]

Hi @Leni Aniva , I've been exploring the Lean tool, and I’m impressed with its quick response(although haven't test the exact time).
The tool also supports features like load_sorrys for sketch proofs and inneraction_analyse for tracking MCTS trees.

However, some cases might lead to incorrect proof states, as noted in this issue. I believe it should be prioritized for resolution.
Also, the tool's interaction relies on the prebuilt pantograph-repl executable, built with Lean version 12. I encounter HeaderErrors when tracing the lean4-example using versions 11 and 13. I'm unsure if there's a workaround for this issue.

[Leni Aniva]

I was going to post this after I add a couple more features into the tool. I'm glad you found it

[Leni Aniva]

RexWang said:

Hi Leni Aniva , I've been exploring the Lean tool, and I’m impressed with its quick response(although haven't test the exact time).
The tool also supports features like load_sorrys for sketch proofs and inneraction_analyse for tracking MCTS trees.

However, some cases might lead to incorrect proof states, as noted in this issue. I believe it should be prioritized for resolution.
Also, the tool's interaction relies on the prebuilt pantograph-repl executable, built with Lean version 12. I encounter HeaderErrors when tracing the lean4-example using versions 11 and 13. I'm unsure if there's a workaround for this issue.

Pantograph's version is anchored to Lean v4.12.0 (or whatever version the lean-toolchain file says), so you can't trace a file in a different version of Lean

[Jason Rute]

@Leni Aniva when you are ready to make an official announcement, feel free to post it here or another thread (or if you think it is something the broader lean community is interested in, you could announce it in #announcements and then post it a like to this thread for follow-up discussions). Also, I have some comments about this work, but maybe I’ll save them until you feel it is ready (unless you would like them earlier).

[Leni Aniva]

Jason Rute said:

Leni Aniva when you are ready to make an official announcement, feel free to post it here or another thread (or if you think it is something the broader lean community is interested in, you could announce it in #announcements and then post it a like to this thread for follow-up discussions). Also, I have some comments about this work, but maybe I’ll save them until you feel it is ready (unless you would like them earlier).

if you have feature suggestions feel free to post them now

[Leni Aniva]

RexWang said:

However, some cases might lead to incorrect proof states, as noted in this issue. I believe it should be prioritized for resolution.

I believe that issue was an indication of a pathological tactic behaviour in Lean 4, and not bug in Pantograph. I've reached out to the author of it for further details.

[Leni Aniva]

GasStationManager said:

This looks very cool. We were just wondering in another thread about the possibility of doing Draft-Sketch-Prove in Lean. Will definitely check this out.

We have an example for DSP in experiments/dsp folder.

[Jason Rute]

Leni Aniva said:

Pantograph's version is anchored to Lean v4.12.0 (or whatever version the lean-toolchain file says), so you can't trace a file in a different version of Lean

I'm not sure what your plan is moving forward, but I just want to give you a cautionary tale about versioning. Our Graph2Tac automated theorem prover for Coq as well as Tactician API used to interface it to Coq (for data and Coq interaction) are fixed to Coq v8.11. But Coq is now on v8.20. A bunch of new AI for Coq papers have come out recently, none of which could compare with Graph2Tac because of the version differences (and benchmark differences). We really don't have a good idea how Graph2Tac would do on their benchmarks. Also, no one uses Graph2Tac as a tool. (That may also be for other reasons besides the version differences.) Honestly, it is a bit depressing to have 2 years of work be quickly ignored by the community. In general, I think folks will want to build models and do benchmarks using the newest version of Mathlib. If your system is tied to an outdated version of Lean (or worse if your system is left to bitrot), I think people will quickly move to another system even if yours is superior.

[Leni Aniva]

Jason Rute said:

Leni Aniva said:

Pantograph's version is anchored to Lean v4.12.0 (or whatever version the lean-toolchain file says), so you can't trace a file in a different version of Lean

I'm not sure what your plan is moving forward, but I just want to give you a cautionary tale about versioning. Our Graph2Tac automated theorem prover for Coq as well as Tactician API used to interface it to Coq (for data and Coq interaction) are fixed to Coq v8.11. But Coq is now on v8.20. A bunch of new AI for Coq papers have come out recently, none of which could compare with Graph2Tac because of the version differences (and benchmark differences). We really don't have a good idea how Graph2Tac would do on their benchmarks. Also, no one uses Graph2Tac as a tool. (That may also be for other reasons besides the version differences.) Honestly, it is a bit depressing to have 2 years of work be quickly ignored by the community. In general, I think folks will want to build models and do benchmarks using the newest version of Mathlib. If your system is tied to an outdated version of Lean (or worse if your system is left to bitrot), I think people will quickly move to another system even if yours is superior.

I plan to update to v4.14 in the next minor version release, and backport the changes if someone wants it for a different version

[Leni Aniva]

If I were to deliver Pantograph for multiple versions, would it be a good idea to do it via Nix? I'm also the creator of lean4-nix. I don't know if most people in ML research would like this idea

[Kim Morrison]

Just make sure there is a v4.X.0 tag for each X, which uses that stable toolchain.

[Kim Morrison]

(Ideally, if you have any upstream dependencies, you pin them also to the v4.X.0 tag at the moment.)

[Kim Morrison]

Our current approach to version compatibility in Lean is everyone striving to release compatible versions of libraries for each release. It's far from ideal, but it's what we can do right now. Batteries/Aesop/ProofWidgets/Verso/lean-repl/import-graph/Mathlib all do this.

[Bas Spitters]

Jason Rute said:

I'm not sure what your plan is moving forward, but I just want to give you a cautionary tale about versioning. Our Graph2Tac automated theorem prover for Coq as well as Tactician API used to interface it to Coq (for data and Coq interaction) are fixed to Coq v8.11.

@Jason Rute What happened? I'm maintaining Coq packages going back two decades. The coq community and coq platform are very helpful in updating to new versions.

[Jason Rute]

@Bas Spitters I'll DM you the details to avoid cluttering this thread. It is not an insurmountable technical issue, but a prioritization of work (made more complex by how we designed things).

[Leni Aniva]

RexWang said:

However, some cases might lead to incorrect proof states, as noted in this issue. I believe it should be prioritized for resolution.

This bug has been fixed. I'm asking the author of the issue to verify it before I merge it into the mainline

[Leni Aniva]

Kim Morrison said:

Just make sure there is a v4.X.0 tag for each X, which uses that stable toolchain.

If I tag each version then I can't backport features from future versions into the "past", so I think a better solution is to create backport branches on demand from the users.

[Leni Aniva]

There are some features I did not write in the paper: Pantograph can

1. Pickle goal states and environments allowing for distributed training and proof search
2. Output s-expressions for any Lean expression. This may be of interest for transpiling
3. Catalog environment including display of which file contains a symbol
4. Modify the environment
5. Output the "parent expression" of a goal state

[Eric Wieser]

Does your picking in 1. also pickle the state of environment extensions?

[Leni Aniva]

Eric Wieser said:

Does your picking in 1. also pickle the state of environment extensions?

No. Do you want this feature?

[Eric Wieser]

My memory is that unfortunately many tactics rely on environment extensions (such as auxiliary declarations generated by simp), and so in practice you can't correctly restore from a pickled environment alone.

[Leni Aniva]

Eric Wieser said:

My memory is that unfortunately many tactics rely on environment extensions (such as auxiliary declarations generated by simp), and so in practice you can't correctly restore from a pickled environment alone.

I'll add that (tracking issue https://git.leni.sh/aniva/Pantograph/issues/137). The pickling mechanism in pantograph is the same as lean-repl.

Are the env extensions totally opaque objects in Lean? I don't see their definitions.

[Mario Carneiro]

yes, they are basically dynamically typed

[Leni Aniva]

Mario Carneiro said:

yes, they are basically dynamically typed

I see. I'll do some engineering to ensure this works out with distributed proof search and terminal state insertion

[Mario Carneiro]

when you declare an environment extension you say what type it will have, and the types are erased by the framework

[Leni Aniva]

Mario Carneiro said:

when you declare an environment extension you say what type it will have, and the types are erased by the framework

Where are extensions referenced in CoreM/MetaM/TermElabM? If there is some extension with ptr 0x123456, does that mean another ptr somewhere else will point to the same place?

[Mario Carneiro]

Environment extensions are indexes into an array stored in the environment

[Leni Aniva]

Mario Carneiro said:

Environment extensions are indexes into an array stored in the environment

I know this. I'm just asking are these extensions referenced anywhere else other than Environment?

[Mario Carneiro]

I'm not sure what you mean

[Mario Carneiro]

The registration mechanism is all global state

[Leni Aniva]

Mario Carneiro said:

The registration mechanism is all global state

when simp adds some extension to the environment, does it store the pointer to the extension anywhere else? If I resurrect a proof state from a pickled file the proof state would need to load the extension into the environment, and any reference to the extension would need to be redirected to this reloaded copy of the extension ptr

[Mario Carneiro]

I don't think simp adds extensions to the environment? Simp is an extension to the environment

[Mario Carneiro]

There is no pointer comparing involved

[Mario Carneiro]

an environment extension is logically just an allocation of a particular number which will henceforth be in the arrays of every environment

[Mario Carneiro]

so it doesn't matter whether you hold on to the extension object itself

[Mario Carneiro]

the thing you get back from the registration function is just some sugar to make it easy to index into an arbitrary environment and cast the result to the right type

[Leni Aniva]

Is there a simple example of a proof where env extensions get generated?

[Mario Carneiro]

There is usually one environment extension per "system component", you don't generate environment extensions dynamically usually

[Mario Carneiro]

most attributes are associated with an environment extension

[Mario Carneiro]

So you would not expect a proof to be creating any environment extensions

[Mario Carneiro]

but tactics sometimes define new env extensions

[Mario Carneiro]

the main entry point is src#Lean.registerPersistentEnvExtension

[Mario Carneiro]

you can see that it is modifying the global variable persistentEnvExtensionsRef there

[Mario Carneiro]

and the unsafeCast there is doing a lot of work

[Mario Carneiro]

the setImportedEntries function pulls extension data out of the "pickled" ModuleData in olean files by matching them up by name

[Eric Wieser]

To be clear, I was referring to the simp tactic, which I think keeps a cache of generated lemmas in an extension, not the @[simp] attribute which stores the lemmas in the simp database

[Leni Aniva]

Mario Carneiro said:

So you would not expect a proof to be creating any environment extensions

Is it sufficient to replay the constant map like what repl does?

[Leni Aniva]

I updated Pantograph to v0.2.23: https://github.com/lenianiva/PyPantograph/pull/50

• fix: An unsoundness bug that is also present in LeanDojo and REPL which causes errenous acceptance of tactics. Note that if you use the proof collection feature (goal.print, existed for 1 year already) at the end of each proof, Pantograph would never become unsound.
• feat: Pickle environments and goal states (the pickling of goal states is experimental)
• feat: Collect newly generated constants for each compilation unit
• feat: Turn type errors into goals, and show exactly where each error happens
• feat: Show used constants in each tactic execution
• feat: MCTS interface (in PyPantograph)