Multi-shot translation - Githubissues

siddhartha-gadgil / LeanAide

Tools based on AI for helping with Lean 4

Apache License 2.0

65 stars 5 forks source link

Multi-shot translation #46

Open siddhartha-gadgil opened 1 month ago

siddhartha-gadgil commented 1 month ago

In case of failure, various things to try:

Find relevant definitions, translate these first, include in instructions.
In case of roundtrip failure, add the response as the final example and then give instructions to correct it given the difference in statements.

siddhartha-gadgil commented 3 weeks ago

Experiments suggest that adding the response and error is unhelpful. The root source of translation in the examples was missing definitions. The error can help uncover these and fixing can be based on these.