Elamur Research⌕
☰
home / papers / 2024 / Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4

Paper · 2024 · Leni Aniva, Chuyue Sun, Brando Miranda et al.

Summary

Machine learning agents that search for proofs in Lean 4 depend on an interface to the proof assistant. The standard Language Server Protocol was built for humans: it tracks cursor positions and offers no easy way to collect tactic data or to leave proof gaps for automation. Pantograph is an API and REPL written entirely in Lean 4 and designed for machine users. Agents can work on goals independently, which makes tree search methods such as Monte Carlo Tree Search practical, and the tool handles metavariable coupling between dependent goals. Pantograph also supports high-level tactics, gives step-by-step feedback inside partially executed conv/calc blocks, and can resume drafts that contain sorry. It extracts training data such as goal states before and after each tactic, proof scripts with comments, and proofs represented as programs. To demonstrate the tool, the authors built what they describe as the first Lean 4 implementation of draft-sketch-prove (DSP). Without any training, it proved up to 28.4% of MiniF2F test theorems, setting a baseline for future hybrid LLM and formal-reasoning provers.

Key points

  • Compared with LeanDojo, Pantograph has no external dependencies such as Docker and interacts faster. It also supports have, let, conv and calc incrementally, whereas LeanDojo only allows some of these as monolithic steps or not at all.
  • The DSP pipeline works in three stages:
    • An LLM writes an informal proof of the MiniF2F statement.
    • The same LLM turns it into Lean 4 sketches containing sorry.
    • Pantograph converts the resulting holes into goals, which the hammers aesop, simp and linarith then try to close.
  • Models were GPT-4o and o1-preview, run with max tokens 2048, top P 0.95 and temperature 0.8.
  • Success rates on MiniF2F:
    • GPT-4o with 3 sketches: 23.6% on validation and 28.4% on test.
    • One sketch: 12.7%/14.7% for GPT-4o and 10.9%/16.0% for o1-preview.
  • o1-preview averaged about 73–88 s per problem versus roughly 17–36 s for GPT-4o, without a clear accuracy gain. Code is available at github.com/stanford-centaur/PyPantograph.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Stanford UniversityStanford · United States567 works · 335,190 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett and Sanmi Koyejo. 2024. Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. arXiv:2410.16429.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2410.16429 · arXiv 2410.16429

@misc{aniva2024pantograph,
  title = {{Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4}},
  author = {Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett and Sanmi Koyejo},
  year = {2024},
  doi = {10.48550/arxiv.2410.16429},
  eprint = {2410.16429},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2410.16429}
}

References

5 references, 4 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. 1. Hello gpt-4o. — TacticToe: Learning to Prove with Tactics https://openai.com/index/hello-gpt-4o/ (9 2024) 2. Introducing openai o1-preview. https://openai.com/index/ introducing-openai-o1-preview/ (9 2024) 3. Aya developers: The aya proof assistant. https://www.aya-prover.org (2021) 4. Browne, C.B., Powley, E., Whitehouse, D., Lucas, S.M.,… ↗
  2. Cambridge University Press (2017) 8. Jiang, A.e.a.: Draft, sketch, and prove: Guiding formal theorem provers with informal proofs (Oct 2022). https://doi.org/10.48550/arXiv.2210.12283, https://arxiv.org/abs/2210.12283v2 9. Jiang, A.Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygóźdź, T., Miłoś,… ↗
  3. CPP 2023, Association for Computing Machinery, New York, NY, USA (2023). https://doi.org/10.1145/3573105.3575671, https://doi.org/10.1145/3573105.3575671 14. mathlib: The lean mathematical library. CoRR abs/1910.09336 (2019), http://arxiv.org/abs/1910.09336 15. de Moura, L., Ullrich, S.: The lean… ↗
  4. Springer International Publishing, Cham (2021) 16. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, vol. 2283. find
  5. Springer Science & Business Media (2002) 17. Silver, D., Hubert, T., Schrittwieser, J., Antonoglou, I., Lai, M., Guez, A., Lanctot, M., Sifre, L., Kumaran, D., Graepel, T., Lillicrap, T., Simonyan, K., Hassabis, D.: A general reinforcement learning algorithm that masters chess, shogi, and go through… — Learning to Prove Theorems by Learning to Generate Theorems

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/aniva-2024-pantograph-machine-machine-interaction-interface/