4 ms·
Large Language Models for Mathematicians (2023)
- sylware 2y agoMaths models have very probably significant differences. For instance, they are strapped to a formal solver. Not to mention, they should be in "continuous" ML learning mode. I wonder if from the observation data of particle physics we have, a "physics" model could "infer" a hard mathemical theory using those previous maths models (and probably other tools) which would fit this very observation data. ScyFy: if those mathemical theories are beyond us, we would need other models in order to try to extract some predictions which could be interesting for us to verify with some "real-life"/reasonable experiments.
- amelius 2y agoWaiting for llms for compilers.
- deleted 2y ago[deleted]
- youreth4tguy 2y agoI notice that I trust LLMs a lot nowadays, because I spent a lot of time trying to understand the answer to the first question, thinking I was just "not getting it", until realizing that it's just wrong, and then also realizing that the question doesn't even make sense in the slightest.
- lanstin 2y agoYeah they aren't that good at spotting wrong questions (tho better than a year ago). Claude is especially likely to do this correctly. GPT o whatever will do this push back wrongly. Something in Gemini is positioning Gemini as an all knowing expert rather than a tool for exploring new true statements. It ends almost every thing with "is there anything else I can explain about the distribution of algebraic numbers with a given height".
- lanstin 2y agoActually I just did one of my test questions on GPT o3-mini-high and it got it. Very nice. Back in the lead over Claude. (My last check was with o1; although if they used the whole chat history to train or fine tune I gave the answer and in the end forced o1 to accept it. Lot of arm twisting language tho.)
- mmiyer 2y agoThe question is perfectly valid -https://math.stackexchange.com/questions/60050/find-a-function-f-mathbbr-to-mathbbr-that-is-continuous-at-precisely-o https://math.stackexchange.com/questions/60050/find-a-functi... The paper notes GPT 4 can solve it (they seemed to have asked ChatGPT 3.5 - this paper is old by AI standards, the first version being from Dec 2023).
- wrp 2y agoAbout 20 years ago, I was working on a project to build a vector model over a corpus of math texts. What ultimately killed it was that I couldn't figure a way to automatically reduce the equations to consistent, searchable text. This paper and others I've read ignore that issue. Anyone know how it is actually handled?
- meowkit 2y agoNot sure I follow your question. Pretty sure they tokenize LaTeX, which should be searchable if the unrendered LaTeX is available
- wrp 2y agoWe were doing OCR on printed text. I tried to get access to the Zentralblatt MATH corpus, but no go.
- threeducks 2y agoVisual language models are quite good at converting images to LaTeX or any other kind of representation these days. Here is a demo where you can upload a screenshot of a page with an equation and ask the neural network to e.g. "Transcribe this equation as LaTeX.": https://huggingface.co/spaces/Qwen/Qwen2-VL https://huggingface.co/spaces/Qwen/Qwen2-VL You can also run a smaller model locally if you have enough VRAM, for example Qwen2.5-VL-7B-Instruct: https://github.com/QwenLM/Qwen2.5-VL?tab=readme-ov-file#using---transformers-to-chat https://github.com/QwenLM/Qwen2.5-VL?tab=readme-ov-file#usin... Also works reasonably well with hand-written equations. For searching through similar equations, you can probably embed each as a high-dimensional vector and then search for the closed vector. Here is a ranking of text embedding networks: https://huggingface.co/spaces/mteb/leaderboard https://huggingface.co/spaces/mteb/leaderboard Or if you want something more deterministic, parse the LaTeX equation to create an abstract syntax tree for which there are plenty of similarity measures.
- wrp 2y agoI think LaTeX renderings are not unique. Is there a schema for normalizing them?
- jenny91 2y agoA paper about LLMs for Mathematicians written by four authors, none of whom seem to be actual mathematicians? (At least based on a quick scroll through their past arXiv papers, they seem like ML researchers.) Just call it LLMs for ML Researchers, but then it doesn't sound anywhere as exciting?
- tptacek 2y agoI started with the first author on this paper, Simon Frieder, and found his page: he's a postdoc mathematician (and ML researcher) at Oxford. I don't think this was a particularly sharp critique.
- Ericson2314 2y agoI don't think this article is very good https://xenaproject.wordpress.com/2024/12/22/can-ai-do-maths-yet-thoughts-from-a-mathematician/ https://xenaproject.wordpress.com/2024/12/22/can-ai-do-maths... https://xenaproject.wordpress.com/2025/01/20/think-of-a-number/ https://xenaproject.wordpress.com/2025/01/20/think-of-a-numb... These from the mathlib founder are much more informative!
- kmill 2y agoKevin Buzzard did great work to popularize mathlib among mathematicians (that's how I got involved myself), but he didn't found mathlib! There's a blurb about the history here: https://leanprover-community.github.io/papers/mathlib-paper.pdf https://leanprover-community.github.io/papers/mathlib-paper....
- Ericson2314 2y agoOh thanks, I didn't realize. Though, reading that paper, I should have known! Obvious in hind-site that at least some math was going on beforehand.
- layer8 2y agoThese are about current (and future) mathematical capabilities of LLMs, but not about how mathematicians can employ LLMs in their work.
- Ericson2314 2y agoThat is because Kevin Buzzard does not think they are yet useful at all!
- westurner 2y agoIt makes sense for LLMs to work with testable code for symbolic mathematics; CAS Computer Algebra System code instead of LaTeX which only roughly corresponds. Are LLMs training on the AST parses of the symbolic expressions, or token coocurrence? What about training on the relations between code and tests? Benchmarks for math and physics LLMs: FrontierMath, TheoremQA, Multi SWE-bench: https://news.ycombinator.com/item?id=42097683 https://news.ycombinator.com/item?id=42097683
- kadushka 2y agoThis paper was posted in December and somehow it completely ignores o1 model, which was specifically optimized for reasoning.
- Thorrez 2y agoReminds me of this article about an AI model that can generate proofs for Math Olympiad: https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ https://deepmind.google/discover/blog/ai-solves-imo-problems... Disclosure: I work at Google, but not on AI.
- mgraczyk 2y agoThis paper is over 1 year old and didn't review the literature at the time well enough to see the early work that led to current generation reasoning models. Now it's out of date, automated RL on math problems seems to work and scales with compute. As we scale available compute 100x over the next 5 years and reduce cost of compute by around 10x over the same time frame, it will become increasing clear that LLMs running for a long time are capable of replacing most mathematics research.
- hnax 2y agoI'm afraid you're overlooking the fact that, since AI scales linearly with constraints and exponentially with compute, the importance of knowledge (i.e. constraints) dominates over data (i.e. compute) for AI to be useful.
- mgraczyk 2y agoNot sure what you're talking about, what does it mean to say that it scales "exponentially with compute"? You're talking about scaling laws? In what sense are they "linearly with knowledge"?