search

siddhartha-gadgil / LeanAide

Tools based on AI for helping with Lean 4
Apache License 2.0
65 stars 5 forks source link

Benchmark and optimize steps of translation #8

Closed siddhartha-gadgil closed 1 year ago

siddhartha-gadgil commented 2 years ago

Currently it takes a few seconds to translate a sentence. All steps other than the Codex query should be examined and optimized.

siddhartha-gadgil commented 2 years ago

@ayush1801 I have implemented a nearest neighbour search (copying many things you did, in particular using torch.topk) for the case of prompts. I used a simpler model so this should be faster. But still, I wanted to alert you that I am finding that loading and finding top-k is instantaneous.

It may be worth checking if there is some inefficiency in the main code we use.

siddhartha-gadgil commented 1 year ago

Now most of the time will be taken by GTP 3.5/4 so no point in this.