alt Hacker NewsSeeing a task-specific model be consistently better at anything is extremely surprising given rapid innovation in foundation models.
Have you tried Aristotle on other, non-Lean tasks? Is it better at logical reasoning in general?
Seeing a task-specific model be consistently better at anything is extremely surprising given rapid innovation in foundation models.
Have you tried Aristotle on other, non-Lean tasks? Is it better at logical reasoning in general?
Is it though? There is a reason gpt has codex variants. RL on a specific task raises the performance on that task