From graph ql + infra to pipelines + agents

Stream: Equational

[Michael Bucko]

I chatted with Vlad and asked him about the current graph-related scripts (esp graph.rb). I think it'd be good to have like an open Neptune or Neo4j installation for researchers who want to explore the results.

Everyone could then write graph ql and perhaps notice new patterns, too.

Eventually, one could

1. run the entire pipeline (from the command line) for any math-related project (like FLT, Liquid Tensor, and so on),
2. use agents to execute and optimize based on the input from the pipeline,
3. the graph (or similar structure) could enable more people to browse the results and discover new patterns.

What do you think?

[Shreyas Srinivas]

I am on a bit out of date on my database knowledge, but wouldn't we need to host it somewhere for researchers to use it?

[Shreyas Srinivas]

Currently the project is running on zero funding

[Shreyas Srinivas]

I see that neo4js has a self hosting option, but then it wouldn't scale easily I suppose

[Michael Bucko]

Shreyas Srinivas schrieb:

I am on a bit out of date on my database knowledge, but wouldn't we need to host it somewhere for researchers to use it?

Yes, it'd be hosted (AWS, GCP, etc.). Amazon (and other companies) offer credits, and I guess it'd be possible to receive such credits for this kind of CLI + pipeline + graph visualization and exploration project. This way we'd open to other researchers as well as enable the creation of artifacts by agents (in the background).

The good news would be that we wouldn't need to reinvent many things (in terms of storage, access, scaling, deployment, and so on), and projects like Equational/FTL/LiqTen could be "deployed" (i.e. you'd run a pipeline from the command line, or from the browser). Part of the deployment work and maintenance (as well as AI companion work) could be done by agents.

It'd feel like every project would have its package.json / npm / docker / jenkins, and storage by default. And there'd be no need to do much Ansible, Terraform, etc.

That kind of math-first deployment. Everyone could focus on creating the most value in math while working with agents.

[Michael Bucko]

Shreyas Srinivas schrieb:

Currently the project is running on zero funding

For many large companies it'd be an opportunity to work with a community like this. They have startup programs. I guess receiving credits for this project should not be a problem.

[Shreyas Srinivas]

If we can get some credits to host this, that would be awesome. I have been a bit queasy about putting our data in large text files in github, but so far the alternatives all seem to cost some money

[Shreyas Srinivas]

If this option is found to be feasible we could change the data hosting scripts run from CI to upload the data to the hosted instances

[Shreyas Srinivas]

Another issue is that this project is as much an experiment on how to manage these kinds of projects as a project in universal algebra

[Shreyas Srinivas]

If these providers do give us some free credits for this project, that's fine, but wouldn't help other researchers who wish to replicate this model if they don't also get such credits

[Michael Bucko]

Shreyas Srinivas schrieb:

Another issue is that this project is as much an experiment on how to manage these kinds of projects as anything else

Exactly. It's a great opportunity to approach this project even more like software and find a structure to deploy any math project with lean, db, visualization, dockerized, with the proper lake/vampire version..

This way all the future projects would profit too.

Also, as long as the pipeline are quite "clean", agents could do lots of work and report when something gets "green".

[Shreyas Srinivas]

What I mean is, we should also explore and report on the almost zero cost route since these companies might not offer similar free credits for all academic projects

[Michael Bucko]

Shreyas Srinivas schrieb:

If these providers do give us some free credits for this project, that's fine, but wouldn't help other researchers who wish to replicate this model if they don't also get such credits

Sure, but we could eventually build a platform (math platform) where every researcher could launch and deploy such projects (and share / collaborate with others).

[Shreyas Srinivas]

Something like DFN or Europractice would be a nice long term solution yes

[Michael Bucko]

Shreyas Srinivas schrieb:

What I mean is, we should also explore and report on the almost zero cost route since these companies might not offer similar free credits for all academic projects

Absolutely.

[Shreyas Srinivas]

Anyway, if someone who has experience in bargaining with these cloud service providers can get these free credits, we can figure out how to configure our CI to work with neo4js

[Shreyas Srinivas]

This is way above my paygrade

[Shreyas Srinivas]

Another point: we are running a bit short on maintainer time, so we will need someone to maintain the graphQL backend

[Michael Bucko]

I think that's doable.

In the meantime, don't those projects always have the following things in common (?)

• (some sort of ) blueprint (already quite standard, no immediate changes needed? I have some ideas, but I guess it's good enough for now),
• Lean project, specific lake version (could be dockerized, and accessible via web, too, through something like Lean 4 Web),
• Generated insights, datasets, artifacts (can be structured, and stored all in one place; structured like ml models, same for math projects),
• Exploration (best as graphs?, could be standardized, LLMs could help),
• Storage (having all these projects accessible in one place; imagine a CLI command "mathplatform run liquidtensorproject", "mathplatform eval dataset.txt", "mathplatform deploy rh.lean"

Three more things I have in mind:

• tools around collaboration (could be a Zulip plugin in this case?),
• chat with the AI next to the problem (most likely good enough - I use Cursor + Lean for that, but I'd love to learn from those with more Lean experience),
• agents doing the work in the background (imagine defining your agents in config files).

[Shreyas Srinivas]

This is the first such project I am aware of. I don't know how the busy beaver people managed their storage, but I think they didn't quite have data.

[Shreyas Srinivas]

For coordination, this time we are using a combination of zulip and Github projects.

[Shreyas Srinivas]

The good thing about github projects is that it tightly integrates into github repositories and CI.

[Shreyas Srinivas]

There are some negatives too.

[Shreyas Srinivas]

Not all data produced in a math project has to be a graph. A project on differential equations combining analytical and numerical methods could produce large tables of numerical data.

[Michael Bucko]

Shreyas Srinivas schrieb:

Not all data produced in a math project has to be a graph. A project on differential equations combining analytical and numerical methods could produce large tables of numerical data.

Exactly. That means storage type and all that would be defined in a project config file. Other projects might output generated Lean (for instance, gen AI projects), text (which others might want to access through embeddings), simply sequences, or even neural nets, and so on. That'd be part of the pipeline.

[Shreyas Srinivas]

I don't have experience in setting up such a pipeline, though I know the basics. Would you be willing to volunteer for this task?

[Shreyas Srinivas]

One important thing is we'll need open access and community ownership of the data (meaning Amazon/Google cannot legally pull the rug from under this project and close access to the data). This means one or more backup methods and archiving on zenodo when the time is ripe for that. I am not a lawyer and this area seems to be the subject of a number of subtle legal disputes.

[Michael Bucko]

Shreyas Srinivas schrieb:

I don't have experience in setting up such a pipeline, though I know the basics. Would you be willing to volunteer for this task?

I am already looking into it (a very quick and dirty PoC) here, but from a slightly different angle: https://github.com/riccitensor/mathplatform

Not an ml-like pipeline experiment, but rather simply GPT-4/O1 (or Claude) with function calling (hoping to add configs, and so on), and a config file (soon). I was going to enable vampire and prover9 too (currently commented out in the file), enable the CLI commands, enable docker per project, and then start by migrating one of the big projects into that kind of environment (the deploy command would essentially run lake update in a dockerized env).

Math pipeline will be different than ml pipelines - at least for now. The way I see it is that I should be able to provide structured and unstructured insights, Lean code, and pick a model (for instance diffusion based) to generate something new that I / Lean could eval. Also, agents should be doing the work in the background: https://arxiv.org/pdf/2410.06209

And the platform / the UX / the collaboration part will matter a lot, too. Since the community is already on Zulip, I guess it needs to work very well with Zulip.

[Michael Bucko]

Perhaps there should simply be something like lean-agents plugin for Cursor :)

[Terence Tao]

Invoking the principle of "if it ain't broke, don't fix it": it appears to me that the current Github-centric framework will be sufficient to accomplish the primary goal of our project, namely to complete the (already >99.99% complete) implication graph, and I am loath to jeapordize that goal with any major transition of platform. However, that said, once that primary goal is complete, I would be willing to experiment with porting some version of the project to another platform, for the purposes of determining feasibility for future projects (particularly ones at an even larger scale at this one, where I suspect the current Github approach, while potentially doable (cf. Mathlib), may encounter new scaling issues that may be easier to resolve on a different platform).

[Shreyas Srinivas]

I think in principle if someone is willing to experiment with the new setup, they could extract the data files we generate from CI in parallel with the project, and host it on a platform of their choice. But I agree that it might be too late to substantially alter the workflow of the project as it is.

[Terence Tao]

From my reading of the Apache 2.0 licence, this project should be freely available to fork by other parties, so long as they retain the Apache 2.0 license. Certainly it is fine by me if others build upon this project in this fashion.