Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Terence Tao on O1

mathstodon.xyz

Post reply on HN
Print view View original

321–330 of 527 posts

Re: Terence Tao on O1

#321

Post by Davidzheng »

lanstin wrote: post #302
Davidzheng wrote: post #183

Earlier quoted context omitted.

I'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.

The point about using lean is you don't have to trust you can verify.

no I agree I just don't think existing Lean codebase is approaching useful coverage. Should change soon

Re: Terence Tao on O1

#322

Post by wenc »

l33t7332273 wrote: post #318
wenc wrote: post #217

Earlier quoted context omitted.

Can 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…

I was referring to section 4 of A Survey for Solving Mixed Integer Programming via Machine Learning(2024): 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…

Thanks for sharing that, I appreciate it. It looks like they used open-source Llama models which are not great. I tested these models offline using Ollama and outside of being character chat bots, they weren't very good at much (the only models that give good answers are Sonnet 3.5 or ChatGPT 4). However the paper's conclusion is essentially correct even for state-of-the-art models:

"Overall, while LLM made several errors, the provided formulations can serve as a starting point for OR experts to create mathematical models. However, OR experts should not rely on LLM to accurately create mathematical models, especially for less common or complex problems. Each output needs to be thoroughly verified and adjusted by the experts to ensure correctness and relevance."

I wouldn't recommend anyone inexperienced to use LLMs to create entire models from scratch, but rather use LLMs as a search tool for specific formulations which are then verified and plugged into a larger model. For this, it works really well and saves me a ton of time. As MIP modeler, I have an intuition on the shape of the answer, so even if ChatGPT makes mistakes, I know how to extract the correct bits and it still saves me a ton of time.

The CPLEX API doesn't have a lot of good examples out in the wild, so I don't expect the training to be good. I've always used CPLEX through a modeling language like AMPL, and even AMPL code is rare so I can't expect an LLM to decipher any of it. On the other hand, MIP formulations abound in PDFs of journal publications.

In the vibes department, I feel Xpress is second to Gurobi and CPLEX and it does the job just fine. But it's been a while since I used CPLEX and Gurobi so I have no recent points of comparison (corporate licensing is prohibitively expensive).

Re: Terence Tao on O1

#323

Post by Davidzheng »

SOTGO wrote: post #88
perihelions wrote: post #30

Earlier quoted context omitted.

Because I'm verifying everything by hand, as is the whole point of studying pure mathematics.

How can you verify a proof though? Pure math isn't really about computations, and it can be very hard to spot subtle errors in a proof that an LLM might introduce, especially since they seem better at sounding convincing rather than being right.

are you questioning the entire premise of pure mathematics?

Re: Terence Tao on O1

#324

Post by mhuffman »

Kiro wrote: post #281
skydhash wrote: post #68

Earlier quoted context omitted.

> Much Much more productive world by just knuckling down and learning how to do the work. The fact everyone that say they've become more productive with LLMs won't say how exactly. I can talk about how VIM have make it more enjoyable to edit code (keybinding and motions), how Emacs is a good environment around text tooling (lisp machine), how I use technical books to further my learning (so many great books out here)…

You clearly have made up your mind that it can't be right but to me it's like arguing against breathing. There are no uncertainties or misunderstandings here. The productivity gains are real and the code produced is more robust. Not in theory, but in practice. This is a fact for me and you trying to convince me otherwise is just silly when I have the result right in front of me. It's also not just boilerplate. It's a…

>There are no uncertainties or misunderstandings here. The productivity gains are real and the code produced is more robust. Not in theory, but in practice.

So, that may be a fact for you but there are mixed results when you go out wide. For example [1] has this little nugget:

>The study identifies a disconnect between the high expectations of managers and the actual experiences of employees using AI.

>Despite 96% of C-suite executives expecting AI to boost productivity, the study reveals that, 77% of employees using AI say it has added to their workload and created challenges in achieving the expected productivity gains. Not only is AI increasing the workloads of full-time employees, it’s hampering productivity and contributing to employee burnout.

So not everyone is feeling the jump in productivity the same way. On this very site, there are people claiming they are blasting out highly-complex applications faster than they ever could, some of them also claiming they don't even have any experience programming. Then others claiming that LLMs and AI copilots just slow them down and cause much more trouble than they are worth.

It seems like just with programming itself, that different people are getting different results.

[1]https://www.forbes.com/sites/bryanrobinson/2024/07/23/employ...

Re: Terence Tao on O1

#325

Post by CJefferson »

wenc wrote: post #319
CJefferson wrote: post #307

Earlier quoted context omitted.

I'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…

I 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-92e29e0550...

OK, 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

Re: Terence Tao on O1

#326

Post by crooked-v »

mewpmewp2 wrote: post #261
dartos wrote: post #254

Earlier quoted context omitted.

> At this point, such sentiments feel either willfully ignorant, or said in bad faith. I feel exactly the same, but in the opposite direction. As someone who’s been programming for 17 years and working professionally for 10, I’m unable to get any huge productivity boosts from AI tools. They’re better than Google+stack overflow for asking random questions, but in a specific context and they’re good for repetitive, but…

Most gains are from using Copilot, do you use that?

I tried it. It ended up just being slightly better, significantly slower autocomplete.

Re: Terence Tao on O1

#327

Post by wenc »

CJefferson wrote: post #325
wenc wrote: post #319

Earlier quoted context omitted.

I 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-92e29e0550...

OK, 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 wron…

Sure, but that is nature of LLM prompting. It does take some doing to set up the right guardrails. It's still a good starting point.

Also a trick when the LLM fights you: start from scratch, and put guardrails in your initial prompt.

LLM prompting is a bit like gradient descent in a bumpy nonconvex landscape with lots of spurious optima and saddle points -- if you constrain it to the right locality, it does a better job at finding an acceptable local optimum.

Re: Terence Tao on O1

#328

Post by [deleted] »

JumpCrisscross wrote: post #246
fnordpiglet wrote: post #149

Rewind your mind to 2019 and imagine reading a post that said “The experience seemed roughly on par with trying to advise a mediocre, but not completely incompetent, graduate student.” With regard to interacting with the equivalent of Alexa. That’s a remarkable difference in 5 years.

The first profession AI seems on track to decimate is programming. In particular, the brilliant but remote and individual contributor. There is an obvious conflict of interest in this forum.

[deleted]

Re: Terence Tao on O1

#329

Post by [deleted] »

cjbgkagh wrote: post #114
WhatIsDukkha wrote: post #26

Earlier quoted context omitted.

I 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 lea…

In my view these models produce above average code which is good enough for most jobs. But the hacker news sampling could be biased towards the top tier of coders - so their personal account of it not being good enough can also be true. For me the quality isn't anywhere close to good enough for my purposes, all of my easy code is already done so I'm only left working on gnarly niche stuff which the LLMs are not yet h…

[deleted]

Re: Terence Tao on O1

#330

Post by fumeux_fume »

fnordpiglet wrote: post #149

Rewind your mind to 2019 and imagine reading a post that said “The experience seemed roughly on par with trying to advise a mediocre, but not completely incompetent, graduate student.” With regard to interacting with the equivalent of Alexa. That’s a remarkable difference in 5 years.

Rewind your mind to 1950 and reading that the future is chatting with bots about solving math homework.
Post reply on HN