New AI Venture Focuses on Mathematical Reasoning

Of possible interest to philosophers working in logic and philosophy of math, as well as anyone curious about the reasoning abilities of artificial intelligence [insert scare quotes where you need to] is a new model from Harmonic called “Aristotle”.

[Klein Bottle Bottle Opener by Bathsheba Grossman]

In tests, Aristotle is doing very well on MiniF2F, “a dataset of formal Olympiad-level mathematics problems statements intended to provide a unified cross-system benchmark for neural theorem proving,” getting scores of 90%.

Harmonic also recently introduced a natural language interface. The model reasons in the programming language Lean 4, but now can automatically translate between natural language and Lean 4 (“autoformalization”) and back. According to Harmonic:

Autoformalization enables Aristotle to collaborate with mathematicians and educators who may not know Lean, checking their work and filling in details grounded by formal understanding. It also makes the world of existing natural-language math, in the form of textbooks, research papers, and blog posts, available as training data for formal reasoning.  

You can check out an example of this and learn more here.

Thinker Analytix: innovative tools for teaching clear and courageous thinking
Notify of

1 Comment
Newest Most Voted
Inline Feedbacks
View all comments
Fenner Tanswell
7 days ago

Unless I’ve missed something, I cannot find anything on this website like a proper description of what they’ve done (the two other “state of the art” approaches they compare themselves to have arXiv preprints at least). Nor does it even say who they are on their own website.

Linking up LLMs with Lean (or another ITP) does seem to be the way things are going, but for now I am pretty sceptical of their claims, without substantial evidence. Autoformalisation is tricky, in part because there is not much useful training data (relative to the huge size of most training sets LLMs are using), so claims that they’ve managed it should not be taken at face value unless they can provide receipts.

Something from this area of more interest to philosophers is the pair of issues of the Bulletin of the AMS on AI in Mathematics:

While most of these are reflections by mathematicians, the second issue contains an article by the philosopher Silvia De Toffoli (IUSS Pavia).