Tactician’s API provides external machine learning agents with Coq’s internal
knowledge-base of mathematics. It can extract large-scale datasets from a wide
variety of Coq packages for the purpose of offline machine learning.
Additionally, it allows agents to interact with Coq. Proving servers can be
connected to Tactician’s `synth`

tactic and prove theorems for Coq users.
Additionally, servers can do proof exploration through the `Tactician Explore`

command. Examples of external proving agents include Graph2Tac & Text2Tac.

The data provided to agents includes definitions, theorems, proof terms and a machine-readable representation of tactical proofs. The data is provided both in Coq’s standard text-based human-readable format and as a semantic graph. The semantic graph is a single interconnected object that includes the entire mathematical universe known to Coq (at a given moment in time). As such, it provides external agents with “complete information” of Coq’s internal state, instead of “incomplete information”. The agent does not need to query Coq for information about theorems or definitions, because it has an always-up-to-date view.

The graph is designed to represent the semantic meaning of a mathematical object
as faithfully as possible, minimizing the amount of implicit knowledge needed to
interpret the object. For example, when a definition `X`

refers to another
definition `Y`

, such a dependency is encoded explicitly using an edge in the
graph. No definition lookup table is need. We also shy away from using names or
de Bruijn indices as variables. Instead, variables point directly to their
binders, so that name lookup becomes a trivial operation. Such an encoding
reduces alpha-equivalence between terms to the graph-theoretic notion of
bisimilarity, and allows us to globally deduplicate any alpha-equivalent terms
in the graph.

A simple example of the semantic graph is shown below. An entire Coq document is
converted into a single graph. Alpha-equivalent sub-terms, such as `2*`

are
globally shared. The graph includes all transitive objects referenced by
the document, such as `nat`

, `=`

, `+`

and `*`

(shown with a truncated tree here).

A zoomed-out view of the graph is visualized on the top of this page. This graph contains all information encoded in Coq’s Prelude. See the paper for details on the construction of the graph.

Communication with agents happens through the Cap’n
Proto serialization format and remote procedure calling
(RPC) protocol. It supports a wide variety of programming languages, including
Python, OCaml, C++, Haskell, Rust and more. This serialization was chosen
because it allows us to memory-map (`mmap`

) large graph datasets, allowing fast
random-access to graphs that may not fit into main memory. Furthermore, Cap’n
Proto’s RPC protocol, based on the distributed
object-capability model,
allows us to export Coq’s proof states to external agents. Agents can inspect
the proof states, and execute tactics on them, allowing exploration of the proof
search space in arbitrary order.

### Overview of the platform

Tactician’s API is meant to provide a bridge between the machine learning community and the proof engineering community. On the one hand, ML researchers can leverage the formal knowledge generated by proof engineers to build, train and evaluate agents. In return, these agents can be provided to proof engineers to assist them in synthesizing more formal knowledge. Agents can be integrated into the day-to-day workflow of proving and programming in Coq.

Components include:

**Graph2Tac & Text2Tac**: Pre-trained models that can make tactic predictions and integrate with Tactician’s`synth`

command. The first model uses the graph-based representation while the second model uses human-readable text.**Datasets**: Pre-made, large-scale datasets of formal knowledge extracted from a variety of Coq developments. Interactively explore the dataset here. The dataset includes hierarchies of modules, global context information, definitions, tactical proofs and tactic proof transformations.**Coq Commands**: Outlines the commands added to Tactician by the package`coq-tactician-api`

for the purpose of interacting with external agents.**PyTactician**: A Python library build on top of Cap’n Proto to facilitate reading the dataset and interface with Coq.**Benchmarking**: Tools to evaluate the proving strength of agents on arbitrary Opam packages. Benchmarks can be run on a laptop, a high-powered server and even massively parallelized on a High Perfomance Computing (HPC) cluster.