ATPs

Stream: Equational

[Mikoláš Janota]

I ran vampire and can solve all but 1,030. I'm cursious how other ATP/SMTs perform. Is that something that people are interested in? I could collect some statistics from this.

[Bernhard Reinke]

What do you mean when you say you "can solve all but 1,030"? Find nontrivial models for the equations?

[Mikoláš Janota]

Bernhard Reinke said:

What do you mean when you say you "can solve all but 1,030"? Find nontrivial models for the equations?

@Bernhard Vampire can saturate, which means that we know that the implication does not hold but it's non trivial to extract the model from the solver.

[Bernhard Reinke]

Ok, my question was what "all" is in your context. I guess you mean for the 4694 equational laws involving at most four magma operations, you can decide all of the 4694*(4694-1) implications save 1,030?

[Mikoláš Janota]

Yes, that's right. Out of the 22 million or so, the are 1030 not solved by purely automated means. With the caveat that when vampire saturates, there is no immediate way of going to a lean proof.

[Terence Tao]

Statistics, such as the run time vampire takes to resolve each of the implications that it can reach, would be quite useful; they would be hardware dependent of course, but would allow for a relative difficulty comparison between different implications. Also if you could provide the scripts used to do the runs so that they can be replicated, that would also be very helpful for others.

[Mikoláš Janota]

image.png

[Mikoláš Janota]

I'm getting this distribution, the interesting part is that vampire can obtain lot of counterexamples by saturation (where we do not have an explicit model)

[Mikoláš Janota]

It appears to be the case that vampire can discharge all implications that hold (true)

[Terence Tao]

Thanks! Would it also be possible to provide a table that identifies the time required (or method required) for specific implications? Having a "difficulty score" for each given implication could be very useful for all kinds of implications (and could potentially be a neat addition to the Equation Explorer, as well).

[Mikoláš Janota]

Sure. I could probably make a zenodo repository out of the things I ran. I'll create a jason out of the raw data, then I'll see if this can also be made into some classification wrt difficulty. The fact that vampire saturates on infinite-model implications is quite interesting and probably very fragile.

[Mikoláš Janota]

The heatmap is quite fun, even though most is very fast and one needs to zoom in to find the hard problems https://people.ciirc.cvut.cz/~janotmik/drop/heatmap.pdf I tried averaging times over rhs https://people.ciirc.cvut.cz/~janotmik/drop/avgs.txt not sure if that reveals anything? One more thing to look at is something like the hardest K problems.

[Shreyas Srinivas]

@Mikoláš Janota : looks like one could write an experience report for next year's CAV

[Mikoláš Janota]

http://people.ciirc.cvut.cz/~janotmik/drop/heatmap_hres.pdf https://people.ciirc.cvut.cz/~janotmik/drop/hardest1000.txt

[Mikoláš Janota]

@Shreyas Srinivas I think that these are more directed to FM in industry. Ijcar might be interested in this but probably it would have to be deeper than what I did up till now

[Terence Tao]

Would it be possible to upload some of the raw data files to the project itself (in the "data" subdirectory)? It could be quite valuable to other people using the ETP implications as a test set for other applications to have this difficulty benchmark available.

[Mikoláš Janota]

@Terence Tao I pushed the raw data into the data folder. Would the priority be to put it in the explorer?

[Terence Tao]

Thanks! It would be nice to have the data somehow integrated in the explorer for a friendlier UI, but at least now anyone with some rudimentary coding skills can access it, which is the more important thing.

[Mikoláš Janota]

short report and zenodo https://people.ciirc.cvut.cz/~janotmik/eq_vam.pdf, I uploaded to arxiv but they're put it on hold, they might not like vampires :)

[Shreyas Srinivas]

For the citation you might want to use the bibtex entry from either our GitHub repository or google scholar

[Mikoláš Janota]

In the end, arxiv approved the report https://arxiv.org/abs/2508.15856. @Shreyas Srinivas which bibtex entry do you mean?

[Shreyas Srinivas]

The one you get on google scholar

@techreport{bolan2024equational,
  title={The equational theories project: Using lean and github to complete an implication graph in universal algebra},
  author={Bolan, Matthew and Brox, Jose and Carneiro, Mario and Dvorak, Martin and Goens, Andres and Husum, Harald and Kocsis, Zoltan and Meiburg, Alex and Monticone, Pietro and Renshaw, David and others},
  year={2024},
  institution={Technical report}
}

[Shreyas Srinivas]

Or our github repository page

[Mikoláš Janota]

Shreyas Srinivas said:

Or our github repository page

I'm not quite sure what you mean. I'm not seeing any bib entry there. The bib entry you're pasting is not in a good shape, which kinda makes sense since the paper's not yet finished. So I might just wait until it's finished

[Shreyas Srinivas]

github cite link.png

[Shreyas Srinivas]

It's fine if the bibtex is incomplete. It is still a proper citation that attributes credit to all authors.

[Kevin Buzzard]

The bibtex above does not seem to attribute credit to the person who ran the project.

[Shreyas Srinivas]

The google scholar citation bibtex above lists all the authors who have volunteered their names for authorship already. The project was run by me, Pietro and Terence Tao and the others contributed other parts

[Shreyas Srinivas]

Oh wait it does skip my name

[Shreyas Srinivas]

But the paper does appear on my scholar profile

[Shreyas Srinivas]

Oh it also leaves out Terence Tao

[Shreyas Srinivas]

@software{Bolan_The_Equational_Theories_2024,
author = {Bolan, Matthew and Breitner, Joachim and Brox, Jose and Carneiro, Mario and Dvorak, Martin and Goens, Andres and Hill, Aaron and Husum, Harald and Kocsis and Zoltan and Le Floch, Bruno and Luccioli, Lorenzo and McNeil, Douglas and Meiburg, Alex and Monticone, Pietro and Paolini, Giovanni and Petracci, Marco and Reinke, Bernhard and Renshaw, David and Rossel, Marcus and Roux, Cody and Scanvic, Jeremy and Srinivas, Shreyas and Tadipatri, Anand Rao and Tao, Terence and Tsyrklevich, Vlad and Weber, Daniel and Zheng, Fan},
month = sep,
title = {{The Equational Theories Project}},
url = {https://github.com/teorth/equational_theories},
version = {0.1.0},
year = {2024}
}

[Shreyas Srinivas]

I think this list is more complete

[Shreyas Srinivas]

I believe this entry is also somewhat complete. It is being used in the BB(5) preprint:
#Equational > 🦫 BB5 "pre-preprint", feedback phase until June 30th 2025 @ 💬