6 ms·
I work at Harmonic, the company behind Aristotle. To clear up a few misconceptions: - Aristotle uses modern AI techniques heavily, including language modeling
by maxwells-daemon 8mo ago
I work at Harmonic, the company behind Aristotle.
To clear up a few misconceptions:
- Aristotle uses modern AI techniques heavily, including language modeling.
- Aristotle can be guided by an informal (English) proof. If the proof is correct, Aristotle has a good chance at translating it into Lean (which is a strong vote of confidence that your English proof is solid). I believe that's what happened here.
- Once a proof is formalized into Lean (assuming you have formalized the statement correctly), there is no doubt that the proof is correct. This is the core of our approach: you can do a lot of (AI-driven) search, and once you find the answer you are certain it's correct no matter how complex the solution is.
Happy to answer any questions!
- xiphias2 8mo agoFirst congrats! Sometimes when I'm using new LLMs I'm not sure if it’s a step forward or just benchmark hacking, but formalized math results always show that the progress is real and huge. When do you think Harmonic will reach formalizing most (even hard) human written math? I saw an interview with Christian Szegedy (your competitor I guess) that he believes it will be this year.
- maxwells-daemon 8mo agoThank you! It depends on the topic. Some fields (algebra, number theory) are covered well by Lean's math library, and so I think we are already there; I recommend trying Aristotle for yourself to see how reliably it can formalize these theorems! In other fields (topology, probability, linear algebra), many key definitions are not in Mathlib yet, so you will struggle to write down the theorem itself. (But in some cases, Aristotle can define the structure you are talking about on the fly!) This is not an intrinsic limitations of Lean, it's just that nobody has taken the time to formalize much of those fields yet. We hope to dramatically accelerate this process by making it trivial to prove lemmas, which make up much of the work. For now, I still think humans should write the key definitions and statements of "central theorems" in a field, to ensure they are compatible with the rest of the library.
- zozbot234 8mo ago> ... But in some cases, Aristotle can define the structure you are talking about on the fly! ... Do you have any plans to characterize these cases more fully, and perhaps propose your own contributions to mathlib itself on that basis?
- tachim 8mo agoThere have been many contributions to mathlib from Aristotle already, it’s a major use case for our users
- pvillano 8mo agoIs anyone working on applying these techniques to formal verification of software? My limited understanding of Rust is that it applies a fixed set of rules to guarantee memory safety. The rules are somewhat simple and limiting, for ease of understanding and implementation, but also because of undecidability. Programmers run into situations where they know that their code won't cause memory errors, but it doesn't follow the rules. Wouldn't it be cool if something like Aristotle was integrated into the compiler? Any code for which a proof of correctness could be written would pass/compile, without having to add more and more rules
- maxwells-daemon 8mo agoWe are! We very recently announced some results on formally proving the correctness of programs: https://harmonic.fun/news#blog-post-verina-bench-sota https://harmonic.fun/news#blog-post-verina-bench-sota Formal methods are cool because, by contrast to tools like the borrow checker, you can prove some very "nonlocal" properties: this system does not deadlock, or it makes progress at least every N steps, etc.
- vatsachak 8mo agoDoes Aristotle produce TLA+ output? For example can it read rust async code and prove that there are no deadlocks in TLA+, or some equivalent in Lean?
- zozbot234 8mo agoTLA+ is generally used to specify a "toy model" of some complex distributed system. It's not intended for end-to-end proof, for that you'd just use Coq/Rocq or Lean itself. Lean is certainly expressive enough, but you'll have to translate the time and non-determinism modalities of TLA+ as part of the Lean development.
- NetMageSCW 8mo agoHow is “this system doesn’t deadlock” not the same as the halting problem?
- aidenn0 8mo agoHow do you verify that the AI translation to Lean is a correct formalization of the problem? In other fields, generative AI is very good at making up plausible sounding lies, so I'm wondering how likely that is for this usage.
- roenxi 8mo agoYou're looking for the practical answer, but philosophically it isn't possible to translate an informal statement into a formal one 'correctly'. It is informal, ie, vaguely specified. The only certain questions are if the formal axioms and results are interesting which is independent of the informal formalisation and that can only be established by inspecting the the proof independently of the informal spec.
- wizzwizz4 8mo agoPhilosophically, this is not true in general, but that's for trivial reasons: "how many integers greater than 7 are blue?" doesn't correspond to a formal question. It is absolutely true in many specific cases. Most problems posed by a mathematician will correspond to exactly one formal proposition, within the context of a given formal system. This problem is unusual, in that it was originally misspecified.
- red75prime 8mo agoI suppose there's no formally defined procedure that accepts a natural language statement and outputs either its formalization or "misspecified". And "absolutely true" means "the vast majority of mathematicians agree that there's only one formal proposition that corresponds to this statement".
- varjag 8mo agoI think you suppose wrong. A statement like "the area of the square whose side is the hypotenuse is equal to the sum of the areas of the squares on the other two sides" doesn't seam out of reach of an algorithmic procedure like a classical NLP.
- jjmarr 8mo agoWhat are the benefits of Aristotle over a general-purpose coding assistant like Claude Code?
- maxwells-daemon 8mo agoAristotle's output is formally verified in Lean, so you can run it for days on a hard problem and be assured that the answer, no matter how complex, is right without needing to manually check it. Claude Code can write lean, but we do a heck of a lot of RL on theorem proving, so Aristotle winds up being much better at writing Lean than other coding agents are.
- jjmarr 8mo agoSeeing 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?
- runeblaze 8mo agoIs it though? There is a reason gpt has codex variants. RL on a specific task raises the performance on that task
- jjmarr 8mo agoPost-training doesn't transfer over when a new base model arrives so anyone who adopted a task-specific LLM gets burned when a new generational advance comes out.
- runeblaze 8mo agoResouce-affording, if you are chasing the frontier of some more niche task you redo your training regime on the new-gen LLMs
- Davidzheng 8mo ago
- pfdietz 8mo agoDo you have plans to apply this broadly to the historical math literature?
- maxwells-daemon 8mo agoYes! I think that working with Mathlib is the best long term solution, because it's how people already collaborate on building out the formal "universe of mathematics." We want to speed that up, and hopefully we'll cover all of the common topics very soon!
- wslh 8mo agoThis is the forst time I heard about Aristotle and find it very interesting. First question first: is it available for the general public? I don't know if this is the page to try it? [1] Second, when you say language modeling support, it means that can better understand code representation (ASTs) or something else? I am just an AI user, not very knowledgeable in the field. My main interest is if it would be great for static analysis oriented to computer security (SAST). [1] https://aristotle.ai/ https://aristotle.ai/
- tachim 8mo agoYes it’s available! https://aristotle.harmonic.fun/ https://aristotle.harmonic.fun/
- qnleigh 8mo ago> If the proof is correct, Aristotle has a good chance at translating it into Lean How does this depend on the area of mathematics of the proof? I was under the impression that it was still difficult to formalize most research areas, even for a human. How close is Aristotle to this frontier?
- bjt12345 8mo agoWhat occurs when this process is reversed - translate from lean to informal english, and does iterating this then help research better approaches toward writing proofs in human language?
- hannasm 8mo agoI had the same thought but unfortunately even if that translation is accurate it could still be bidirectional hallucinating and would not really be sufficient evidence... It's another reformulation rather than a true proof. Now, instead of wanting a proof of a theorem, now we just need to prove that this proof is actually proving the theorem. The proof itself being so incomprehensible that it can't on its own be trusted, but if it can be shown that it can be trusted then the theorem must be true.
- EE84M3i 8mo ago> there is no doubt that the proof is correct. Do you have any links to reading about how often lean core has soundness bugs or mathlib has correctness bugs?
- nateberkopec 8mo ago>assuming you have formalized the statement correctly That's a pretty big assumption, though, isn't it? As we saw the Navier-Stokes psychosis episode over the New Year holiday, formalizing correctly really isn't guaranteed.
- nottorp 8mo agoSo what did the "AI" actually do? Translate an informal description of the proof into this Lean?
- dpe82 8mo agoTFA says ChatGPT wrote the informal description.
- uoaei 8mo agoYou seem to be openly contradicting your company's PR and language. Your description very clearly describes the "AI" as a tool to translate relatively informal specifications into formal proof logic, but does not itself do the proving.
- 101008 8mo agoAny chance Harmonic accept full remote employees? :)