| |
| ▲ | Davidzheng a day ago | parent | next [-] | | Never mind what Aristotle is, verifier llm models are definitely strong enough to verify proofs of elementary methods used here. | |
| ▲ | TeMPOraL a day ago | parent | prev [-] | | Aristotle is an LLM system. | | |
| ▲ | D-Machine a day ago | parent [-] | | "Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver" It is far more than an LLM, and math != "language". | | |
| ▲ | TeMPOraL a day ago | parent [-] | | > Aristotle integrates three main components (...) The second one being backed by a model. > It is far more than an LLM It's an LLM with a bunch of tools around it, and a slightly different runtime that ChatGPT. It's "only" that, but people - even here, of all places - keep underestimating just how much power there is in that. > math != "language". How so? | | |
| ▲ | D-Machine a day ago | parent | next [-] | | Transformer != LLM. See my edited top-level post. Just because Aristotle uses a transformer doesn't mean it is an LLM, just as Vision Transformers and AlphaFold use transformers but are not LLMs. LLM = Large Language Model. Large refers to both the number of parameters (and in practice, depth) of the model, and also implicitly the amount of data used for training, and "language" means human (i.e. written, spoken) language. A Vision Transformer is not an LLM because it is trained on images, and AlphaFold is not an LLM because it is trained molecular configurations. Aristotle works heavily with formalized LEAN statements and expressions. While you can certainly argue this is a language of sorts, it is not at all the same "language" as the "language" in LLMs. Calling Aristotle an "LLM" just because it has a transformer is more misleading than truthful, because every other single aspect of it is far more clever and involved. | | |
| ▲ | TeMPOraL a day ago | parent [-] | | The paper you keep linking literally says they're using a large language model (search for that very string in it). | | |
| ▲ | D-Machine a day ago | parent [-] | | Sigh. If I start with a pre-trained LLM architecture, and then do extensive further training / fine-tuning with different data and loss functions and custom similarity metrics for specialized search and specialized training procedures, and use feedback from other automated systems, we are far, far more than an LLM. That's the point. Calling something like this an LLM is as deeply misleading as calling AlphaFold an LLM. These tools goes far beyond simple LLMs. The special losses and metrics are really so important here and are why these tools can be so game-changing. |
|
| |
| ▲ | XCSme a day ago | parent | prev [-] | | I kind of agree, "math" can be a "language". Same as "images" can be a language. You can use anything as tokens. | | |
| ▲ | raincole a day ago | parent | next [-] | | In this context, we're not even talking about "math" (as a broad, abstract concept). We're strictly talking about converting English to Lean. Both are just languages. Lean isn't just something that can be a language. It's a language. There is no reason or framing where you can say Aristotle isn't a language model. | |
| ▲ | TeMPOraL a day ago | parent | prev [-] | | That's true, and a good fundamental point. But here it's much simpler than that: math is a language the same way code is, and if there's one thing LLMs excel at, it's reading and writing code and translating back and forth between code and natural language. |
|
|
|
|
|
