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

181–190 of 527 posts

Re: Terence Tao on O1

#181

Post by nybsjytm »

fragmede wrote: post #150
SOTGO wrote: post #88

Earlier quoted context omitted.

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.

By using Lean, a proof assistant and a functional programming language. Here's @tao on mathstodon saying he's learning it. https://mathstodon.xyz/@tao/111206761117553482

To code proofs in lean, you have to understand the proof very well. It doesn't seem to be very reasonable for someone learning material for the first time.

Re: Terence Tao on O1

#182

Post by l33t7332273 »

wenc wrote: post #5

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

Re: Terence Tao on O1

#183

Post by Davidzheng »

wenc wrote: post #5

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

Re: Terence Tao on O1

#184

Post by thelastparadise »

talldayo wrote: post #174
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.

To be honest, I have gotten 100x more useful answers out of Siri's WolframAlpha integration than I ever have out of ChatGPT. People don't want a "not completely incompetent graduate student" responding to their prompts, they want NLP that reliably processes information. Last-generation voice assistants could at least do their job consistently, ChatGPT couldn't be trusted to flick a light switch on a regular basis.

Wait til you generate WolframAlpha queries from natural language using Claude 3.5 and use it to interpret results as well.

Re: Terence Tao on O1

#185

Post by talldayo »

thelastparadise wrote: post #184
talldayo wrote: post #174

Earlier quoted context omitted.

To be honest, I have gotten 100x more useful answers out of Siri's WolframAlpha integration than I ever have out of ChatGPT. People don't want a "not completely incompetent graduate student" responding to their prompts, they want NLP that reliably processes information. Last-generation voice assistants could at least do their job consistently, ChatGPT couldn't be trusted to flick a light switch on a regular basis.

Wait til you generate WolframAlpha queries from natural language using Claude 3.5 and use it to interpret results as well.

I've tried the ChatGPT integration and it was kinda just useless. On smaller datasets it told me nothing that wasn't obviously apparent from the charts and tables; on larger datasets it couldn't do much besides basic key/value retrieval. Asking it to analyze a large time-series table was an exercise in futility, I remain pretty unimpressed with current offerings.

Re: Terence Tao on O1

#186

Post by thelastparadise »

wenc wrote: post #5

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

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

Re: Terence Tao on O1

#187

Post by Karrot_Kream »

talldayo wrote: post #174
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.

To be honest, I have gotten 100x more useful answers out of Siri's WolframAlpha integration than I ever have out of ChatGPT. People don't want a "not completely incompetent graduate student" responding to their prompts, they want NLP that reliably processes information. Last-generation voice assistants could at least do their job consistently, ChatGPT couldn't be trusted to flick a light switch on a regular basis.

How does this square up with literally what Terence Tao (TFA) writes about O1? Is this meant to say there's a class of problems that O1 is still really bad at (or worse than intuition says it should be, at least)? Or is this "he says, she says" time for hot topics again on HN?

Re: Terence Tao on O1

#188

Post by teaearlgraycold »

gary_0 wrote: post #51

Tao mentions grad students; I wonder how they feel reading this? As LLMs continue to improve I feel like anyone making a living doing the "99% perspiration" part of intellectual labor is about to enter a world of hurt.

Or can everyone now lead research projects and build businesses?

Re: Terence Tao on O1

#189

Post by smallnamespace »

skydhash wrote: post #121
Nadya wrote: post #83

Earlier quoted context omitted.

Ever seen someone try and search something on Google and they are just AWFUL at it? They can never find what they're looking for and then you try and can pull it up in a single search? That's what it is like watching some people try to use LLM's. Learning how to prompt an LLM is as much a learned skill as much as learning how to phrase internet searches is a learned skill. And as much as people decried that "searchin…

I'm not arguing that you can't get result with LLMs, I'm just asking is it worth the actual effort especially when there's better way to get that result you're seeking (or if the result is really something that you want). An LLM is a word (token?) generator which can be amazingly consistent according to its model. But rarely is my end goal to generate text. It's either to do something, to understand something, or to…

> asking is it worth the actual effort

If prompting ability varies then this is not some objective question, it depends on each person.

For me I've found more or less every interaction with an LLM to be useful. The only reason I'm not using it continually for 8 hours a day is because my brain is not able to usefully manage that torrent of new information and I need downtime.

Re: Terence Tao on O1

#190

Post by codr7 »

ben_w wrote: post #101
Nadya wrote: post #83

Earlier quoted context omitted.

Ever seen someone try and search something on Google and they are just AWFUL at it? They can never find what they're looking for and then you try and can pull it up in a single search? That's what it is like watching some people try to use LLM's. Learning how to prompt an LLM is as much a learned skill as much as learning how to phrase internet searches is a learned skill. And as much as people decried that "searchin…

> On average, people are awfully bad at describing exactly what it is they want. Ever speak with a client? And you have to go back and forward for a few hours to finally figure out what it is they wanted? One of them it was the entire duration of me working for them. They didn't understand why it was taking so long despite constantly changing what they asked for.

Building the software is usually like 10% of the actual job, we could do a better job of teaching that.

The other 90% is mostly mushy human stuff, fleshing out the problem, setting expectations etc. Helping a group of people reach a solution everyone is happy with has little to do with technology.

Post reply on HN