13 ms·
Once GPT is tuned more heavily on Lean (proof assistant) -- the way it is on Python -- I expect its usefulness for research level math to increase. I work in a
by wenc 2y ago
Once GPT is tuned more heavily on Lean (proof assistant) -- the way it is on Python -- I expect its usefulness for research level math to increase.
I work in a field related to operations research (OR), and ChatGPT 4o has ingested enough of the OR literature that it's able to spit out very useful Mixed Integer Programming (MIP) formulations for many "problem shapes". For instance, I can give it a logic problem like "i need to put i items in n buckets based on a score, but I want to fill each bucket sequentially" and it actually spits out a very usable math formulation. I usually just need to tweak it a bit. It also warns against weak formulations where the logic might fail, which is tremendously useful for avoiding pitfalls. Compare this to the old way, which is to rack my brain over a weekend to figure out a water-tight formulation of MIP optimization problem (which is often not straightforward for non-intuitive problems). GPT has saved me so much time in this corner of my world.
Yes, you probably wouldn't be able to use ChatGPT well for this purpose unless you understood MIP optimization in the first place -- and you do need to break down the problem into smaller chunks so GPT can reason in steps -- but for someone who can and does, the $20/month I pay for ChatGPT more than pays for itself.
side: a lot of people who complain on HN that (paid/good - only Sonnet 3.5 and GPT4o are in this category) LLMs are useless to them probably (1) do not know how to use LLMs in way that maximizes their strengths; (2) have expectations that are too high based on the hype, expecting one-shot magic bullets. (3) LLMs are really not good for their domain. But many of the low-effort comments seem to mostly fall into (1) and (2) -- cynicism rather than cautious optimism.
Many of us who have discovered how to exploit LLMs in their areas of strength -- and know how to check for their mistakes -- often find them providing significant leverage in our work.
- threeseed 2y ago> side Or (4) LLMs simply do not work properly for many use cases in particular where large volumes of trained data doesn't exist in its corpus. And in these scenarios rather than say "I don't know" it will over and over again gaslight you with incoherent answers. But sure condescendingly blame on the user for their ignorance and inability to understand or use the tool properly. Or call their criticism low-effort.
- WhatIsDukkha 2y agoI entirely agree about their utility. HN, and the internet in general, have become just an ocean of reactionary sandbagging and blather about how "useless" LLMs are. Meanwhile, in the real world, I've found that I haven't written a line of code in weeks. Just paragraphs of text that specify what I want and then guidance through and around pitfalls in a simple iterative loop of useful working code. It's entirely a learned skill, the models (and very importantly the tooling around them) have arrived at the base line they needed. Much Much more productive world by just knuckling down and learning how to do the work. edit: https://aider.chat/ https://aider.chat/ + paid 3.5 sonnet
- benterix 2y ago> I've found that I haven't written a line of code in weeks Which is great until your next job interview. Really, it's tempting in the short run but I made a conscious decision to do certain tasks manually only so that I don't lose my basic skills.
- calmworm 2y agoJob interview? You might be surprised at the number of us who don’t code for a job.
- __loam 2y agoI'd bet most people on this forum program professionally.
- calmworm 2y agoI would take that bet.
- idiotsecant 2y agoMe too.
- po76 2y agoGive it a few months. ChatGPT will be recommending GPTs to use or do it automatically. Nothing is static in the way things are moving.
- airstrike 2y agoIt also doesn't help that Lean has had so many breaking changes in such little time. When I tried using GPT-4 for it, it mostly rendered old code that would fail to run unless you already knew the answer and how to fix it, which basically made it entirely unhelpful.
- benterix 2y ago> people who complain on HN that (paid/good - only Sonnet 3.5 and GPT4o are in this category) Correction: I complain that the only decent model in "Open"AI's arsenal, that is GPT-4, has been replaced by a cheaper GPT-4o, which gives subpar answers to most of my question (I don't care it does it faster). As they moved it to "old, legacy" models, I expect they will phase it out, at which point I'll cancel my OpenAI subscriptions and Sonnet 3.5 will become the clear leader for my daily tasks. Kudos to Anthropic for their great work, you guys are going in the right direction.
- bongodongobob 2y agoNah, o1 is fucking impressive. It's really fucking good. I'm guessing you haven't used it yet.
- benterix 2y agoI used it and was really disappointed, maybe because of the hype. It generates a long page of entries that I used to generate in the past, often with better results. Note I use it for code generation, not for problem solving. So I cancelled two of my 3 subscriptions as I realized OpenAI goes in a direction that is not useful for me at all. Claude, on the other hand, is incredibly useful.
- eab- 2y agoWhy do you expect GPT being tuned on Lean will help it for research-level math?
- CamperBob2 2y agoBut many of the low-effort comments seem to mostly fall into (1) and (2) -- cynicism rather than cautious optimism. One good riposte to reflexive LLM-bashing is, "Isn't that just what a stochastic parrot would say?" Some HN'ers would dismiss a talking dog because the C code it wrote has a buffer overflow error.
- jazzyjackson 2y agoId rather live in the world without talking dogs if their main utility is authoring buggy code
- Workaccount2 2y agoIt's understandable that people whose career and lifelong skill set that are seemingly on the precipice of obsolescence are going to be extremely hostile to that threat. How many more years is senior swe work going to be a $175k/yr gig instead of an $75k check-what-the-robot-does gig?
- CamperBob2 2y agoIt depends. If you got into computing because it seemed like the most lucrative career choice to which you might be suited, then yes, I can imagine feeling threatened. Bummer, sucks to be you. But if you got into computing because it seemed like the most interesting thing available to work on, then no, I can't imagine not being fascinated by, and supportive of, the progress being made in the ML field today. Any hostility you feel should be directed at the people who want to lock it all up behind legislative, judicial, or proprietary doors. In my case, it's all I can do not to walk away from everything else I'm doing to follow this particular muse. I don't have a lot of sympathy for my colleagues who see it as a threat. If you're afraid of new ideas, technologies, and methodologies, you picked the wrong line of work.
- riffraff 2y ago_can_ GPT be tuned more heavily on Lean? It looks like the amount of python code in the corpus would outnumber Lean something like 1000:1. Although I guess OpenAI could generate more and train on that.
- EvgeniyZh 2y agoThere is ~3 order of magnitude more Python code in the internet than Lean code (200GB vs 200MB in the stack v2). You can't tune it "the same way"
- agumonkey 2y agoFair point but a lot of python code is redundant and low quality.
- agumonkey 2y agoside question, are there good OR websites / platforms (reddit, mastodon) to get involved in the field ?
- l33t7332273 2y agoI an also working in OR and I have had the complete opposite experience with respect to MILP optimization(and the research actually agrees; there was a big survey paper published earlier this year showing LLMs were mostly correct on textbook problems but got more and more useless as complexity and novelty increased.) The results are boiler plate at best, but misleading and insidious at worst, especially when you get into detailed tasks. Ever try to ask a LLM what a specific constraint does or worse ask it to explain the mathematical model of some proprietary CPLEX syntactic sugar? It hallucinates the math, the syntax, the explanation, everything.
- wenc 2y agoCan you point me to that paper? What version of the model were they using? Have you tried again with the latest LLMs? ChatGPT4 actually (correctly) explains what each constraint does in English -- it doesn't just provide the constraint when you ask it for the formulation. Also, not sure if CPLEX should be involved at all -- I usually just ask it for mathematical formulations, not CPLEX calling code (I don't use CPLEX). The OR literature primarily contains math formulations and that's where LLMs can best do pattern matching to problem shape. Many of the standard formulations are in here: https://msi-jp.com/xpress/learning/square/10-mipformref.pdf https://msi-jp.com/xpress/learning/square/10-mipformref.pdf All the LLM is doing is fitting the problem description to a combination of these formulations (and others).
- l33t7332273 2y agoI was referring to section 4 of A Survey for Solving Mixed Integer Programming via Machine Learning(2024): https://arxiv.org/pdf/2401.03244 https://arxiv.org/pdf/2401.03244. I’ve heard (but not so much observed) that there is substantial difference between recent models, so it’s possible that they are better than when this was written. Anyways, CPLEX has an associated modeling language that features syntactic sugar which has the effect of providing opaqueness to the underlying MILP that it solves. I find LLMs essentially unable to even make an attempt at determining the MILP from that language. PS: How is Xpress? Is there some reason to prefer it to Gurobi or Mosek?
- Davidzheng 2y agoI'm not sure the lean coverage of pure math research is that much (maybe like 1% is represented on mathlib). But I think a system like alpha proof could even today be useful for mathematicians--I mostly dislike systems like o1 where they confidently say nonsense with such high frequency. But i think value is already there.
- lanstin 2y agoThe point about using lean is you don't have to trust you can verify.
- Davidzheng 2y agono I agree I just don't think existing Lean codebase is approaching useful coverage. Should change soon
- lanstin 2y agoI keep asking people in my department about using lean but zero interest so far.
- thelastparadise 2y ago> but for someone who can and does, the $20/month I pay for ChatGPT more than pays for itself. Would you be willing to pay even more, if it meant you were getting proportionally more valuable answers? E.g. $200/month or $2,000/month (assuming the $2,000/month gets into employee/intern/contractor level of results.) This might drive a positive feedback loop.
- sterlind 2y agoI also do OR-adjacent work, but I've had much less luck using 4o for formulating MIPs. It tends to deliver correct-looking answers with handwavy explanations of the math, but the equations don't work and the reasoning doesn't add up. It's a strange experience, like taking a math class where the proofs are weird and none of the lessons click for you, and you start feeling stupid, only to learn your professor is an escaped dementia patient and it was gobbledygook to begin with. I had a similar experience yesterday using o1 to see if a simple path exists through s to t through v using max flow. It gave me a very convincing-looking algorithm that was fundamentally broken. My working solution used some techniques from its failed attempt, but even after repeated hints it failed to figure out a working answer (it stubbornly kept finding s->t flows, rather than realizing v->{s,t} was the key.) It's also extremely mentally fatiguing to check its reasoning. I almost suspect that RLHF has selected for obfuscating its reasoning, since obviously-wrong answers are easier to detect and penalize than subtly-wrong answers.
- mjburgess 2y agoYip. We need research into how long it takes experts to repair faulty answers, vs. generate them on their own. Benchmarking 10,000 attempts on an IQ test is irrelevant if on most of those attempts the time taken to repair an answer is long than the time to complete the test yourself. I find its useful to generate examplars in areas you're roughly familiar with, but want to see some elaboration or a refresher. You can stich it all together to get further, but when it comes time to actually build/etc. something -- you need to start from scratch. The time taken to reporduce what it's provided, now that you understand it, is trivial compared to the time needed to repair its flaws.
- lanstin 2y agoYeah I have been using them to help with learning graduate maths as a grad student. Claude Sonnet 3.5 was unparalleled and the first quite useful one. GPT4o preview seems about equal (based on cutting and pasting the past six months of prompts into it).
- CJefferson 2y agoI'm currently teaching a course on MIP, and out of interest I tried asking 4o about some questions I ask students. It could give the 'basic building blocks' (How to do x!=y, how to do a knapsack), but as soon as I asked it a vaguely interesting question that wasn't "bookwork", I don't think any of it's models were right. I'm interested on how you seem to be getting better answers than me (or, maybe I just discard the answer once I can see it's wrong and write it myself, once I see it's wrong?) In fact, I just asked it to do (and explain) x!=y for x,y integer variables in the range {1..9}, and while the constraints are right, the explanation isn't.
- deleted 2y ago[deleted]
- wenc 2y agoI had to prompt it correctly (tell it to exclude x=y case in the x≠y formulation), but ChatGPT seems to have arrived at the correct answer: https://chatgpt.com/share/66e652e1-8e2c-800c-abaa-92e29e0550d2 https://chatgpt.com/share/66e652e1-8e2c-800c-abaa-92e29e0550...
- CJefferson 2y agoOK, but at that point you've told it basically everything, and this is a really basic book problem! As another example I just gave it a network flow problem, and asked it to convert to maximum flow (I'm using the API, not chatGPT). Despite numerous promptings, it never got it right -- it would not stop putting a limit on the source and sink (usually 1), which mean the flow was always exactly 1, here's the bit of wrong code (it's the last part, it's shouldn't be putting any restrictions on nmap['s'] and nmap['t'], as they represent the source and sink), and I couldn't pursade it this was wrong after several prods: # Constraints: Ensure flow conservation at each vertex A_eq = np.zeros((len(namelist), num_edges)) b_eq = np.zeros(len(namelist)) for i, (u, v, capacity) in enumerate(edges): A_eq[nmap[u], i] = 1 # Outflow from u A_eq[nmap[v], i] = -1 # Inflow to v # Source 's' has a net outflow, and sink 't' has a net inflow b_eq[nmap['s']] = 1 b_eq[nmap['t']] = -1
- andrepd 2y agoI take cynicism over unbridled optimism. People speak as if we were on the cusp of technological singularity, but I've seen nothing to indicate we're not already past the inflection point of the logistic curve, and well into diminishing returns territory.
- RayVR 2y agoI’m amazed you have had any luck with 4o. I found 4 was much better than 4o but still quite bad. I tried to use 4/4o for a MIP several months ago. Frequently, it would iterate through three or four bad implementations over and over. Claude 3.5 has been a significant improvement. I don’t really use chatgpt for anything at this point.