The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq

31 July 2020

Papers citing "The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq"

16 / 16 papers shown

Title
RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation Nikita Khramov Andrei Kozyrev Gleb Solovev Anton Podkopaev 74 0 0 28 May 2025
A Contemporary Survey of Large Language Model Assisted Program Analysis Jiayimei Wang Tao Ni Wei-Bin Lee Qingchuan Zhao 100 5 0 05 Feb 2025
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification Kyle Thompson Nuno Saavedra Pedro Carrott Kevin Fisher Alex Sanchez-Stern Yuriy Brun J. Ferreira Sorin Lerner E. First LRM 240 4 0 18 Dec 2024
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction Liao Zhang David M. Cerna C. Kaliszyk 59 0 0 02 Nov 2024
CoqPilot, a plugin for LLM-based generation of proofs Andrei Kozyrev Gleb Solovev Nikita Khramov Anton Podkopaev 53 5 0 25 Oct 2024
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning Alex Sanchez-Stern Abhishek Varghese Zhanna Kaufman Dylan Zhang Talia Ringer Yuriy Brun 137 2 0 17 Aug 2024
Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent Mahdi Buali Robert Hoehndorf 94 0 0 05 Jul 2024
Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods George Granberry Wolfgang Ahrendt Moa Johansson 151 4 0 21 Jun 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean Peiyang Song Kaiyu Yang A. Anandkumar 103 28 0 18 Apr 2024
Learning Guided Automated Reasoning: A Brief Survey Lasse Blaauwbroek David M. Cerna Thibault Gauthier Jan Jakubruv C. Kaliszyk Martin Suda Josef Urban LRM 95 5 0 06 Mar 2024
The Tactician's Web of Large-Scale Formal Knowledge Lasse Blaauwbroek 58 4 0 05 Jan 2024
Graph2Tac: Online Representation Learning of Formal Math Concepts Lasse Blaauwbroek Miroslav Olšák Jason Rute F. I. S. Massolo Jelle Piepenbrock Vasily Pestun 96 11 0 05 Jan 2024
The Isabelle ENIGMA Z. Goertzel Jan Jakubruv C. Kaliszyk Miroslav Olvsák Jelle Piepenbrock Josef Urban AIMat 52 13 0 04 May 2022
Online Machine Learning Techniques for Coq: A Comparison Liao Zhang Lasse Blaauwbroek Bartosz Piotrowski Prokop Cerný C. Kaliszyk Josef Urban OffRL 52 11 0 12 Apr 2021
Proof Artifact Co-training for Theorem Proving with Language Models Jesse Michael Han Jason M. Rute Yuhuai Wu Edward W. Ayers Stanislas Polu AIMat 121 127 0 11 Feb 2021
Faster Smarter Induction in Isabelle/HOL Yutaka Nagashima 93 7 0 19 Sep 2020