Percentage of time used for retrieval #189
-
|
Just curious - how much time does it take to retrieve all the premises? There's ~33k of the premises that are normally retrieved and ranked to use in the theorem prover; what percentage of the total time does it take for the full ReProver retrieval model; what percentage of the total time does it take for Lean Copilot; and if n is the number of premises that are retrieved, what's the time complexity of the ReProver retrieval model? (O(n)? O(n^2)?) Thank you! |
Beta Was this translation helpful? Give feedback.
Replies: 2 comments 2 replies
-
|
Hi, We did observe slowdown due to the retrieval, though we didn't perform a quantitative analysis on that. As for Lean Copilot, it supports premise retrieval and tactic generation separately but doesn't combine them. |
Beta Was this translation helpful? Give feedback.
-
|
Thank you! I'll close the discussion, but how much was the slowdown (in terms of order of magnitude)? 2x? 10x? I have an idea to decrease the number of premises, so I'm wondering how much the speedup would theoretically be. |
Beta Was this translation helpful? Give feedback.
-
|
A lot of the slowdown comes from not the retrieval itself but the increased input length of the generator. You could roughly consider it quadratic w.r.t. the input length |
Beta Was this translation helpful? Give feedback.
-
|
Hum... okay, thank you very much! |
Beta Was this translation helpful? Give feedback.
Hi,
We did observe slowdown due to the retrieval, though we didn't perform a quantitative analysis on that.
As for Lean Copilot, it supports premise retrieval and tactic generation separately but doesn't combine them.