Concurrent scaling in itp-interface

[RexWzh]

Hey there! 👋

I've been exploring the itp-interface project and it looks super interesting! And I'm particularly curious about the Ray setup for the Parallel Tactic Execution feature mentioned in the paper.

Hence, we created a pooling mechanism that allows us to make multiple instances of the interface module with the same state to execute tactics in parallel (parallelizable across multiple machines on a Ray cluster) for the same theorem. Parallelism is essential for searching for proofs or annotating proofs found at scale.

noticed you've got some neat implementations like the RayResourcePoolActor and TimedRayExec for handling resources and timeouts. Have you done any stress testing with this? I'm wondering about the concurrent REPL instances it can handle (like 100+ or 1000+) and if you have any examples of parallel proving with mathlib theorems.

Thanks in advance!

[amit9oct]

We have tested on a single node with 126 CPUs, 12 GPUs, and about 250 parallel REPL ray instances running. It was working smoothly. However, this was not a stress test. This was just while running our proof search. I think the system should be able to scale beyond that.

[amit9oct]

Just to add the main code for parallel REPL execution with a pool exists here:
https://github.com/trishullab/itp-interface/blob/main/src/itp_interface/rl/simple_proof_env_pool.py

[RexWzh]

Thanks for sharing the details! I'll try out the parallel execution implementation in simple_proof_env_pool.py. Really appreciate the quick and helpful response! 👍

[xukp20]

Hello! Thanks for this great framework.

I'm also trying to use this framework for concurrent theorem proving tasks, but I need a batch of different theorems to be handled simultaneously, instead of searching for different tactics of the same proof state. So for now (before I go through the issues), I just modified the code from the README and wrapped the logic of creating env and applying actions inside a single thread and use asyncio to handle them. However, as I increase the number of theorems handled in parallel, my cores & mems are not fully used, and the speedup is not obvious.

I wonder if you can provide me with instructions about how this framework is designed to be used to handle concurrent tasks (like with ray?), because I am not sure where to find the correct class or entry point to use without enough doc, except for the README. (I believe more docs and examples can help more researchers make full use of this tool, as it seems to have many more supported features than those mentioned in the README 👍)

By the way, what should be the best way to directly provide a complete proof instead of tactics to a theorem and compile it with this framework? I am treating the whole proof as a single action to RUN_ACTION, and it seems a little bit strange 😂.

Thanks again for this great tool!