341–350 of 527 posts
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.
Earlier quoted context omitted.
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
Earlier quoted context omitted.
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…
I think this is just a case of different people wanting to work differently (and that's fine). I can only tell this is wrong because I fully understand it -- and if I fully understand it, why not just write it myself rather than fight against an LLM. If I was trying to solve something I didn't know how to do, then I wouldn't know it was wrong, and where the bug was.
For MIPs, correctness can often (not always but usually) be checked by simply flipping the binaries and checking the inequalities. Coming up the inequalities from scratch are not always straightforward so LLMs often provide good starting points. Sometimes the formulation is something specific from a paper that that one has never read. LLMs are a way to "mine" those answers (some sifting required).
I think this the mindset that is needed to get value out of LLMs -- it's not about getting perfect answers on textbook problems, but working with an assistant to explore the space quickly at a fraction of the effort.
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…
Very good at giving a textbook answer ("give a Python/ Numpy function that returns the Voronoi diagram of set of 2d points").
Now, I ask for the Laguerre diagram, a variation that is not mentioned in textbooks, but very useful in practice. I can spend a lot of time spoon-feeding the answer, I just have the bullshiting student answers.
I tried other problems like numerical approximation, physics simulation, same experience.
I don't get the hype. Maybe it's good at giving variations of glue code ie. Stack Overflow meet autocomplete ? As a search tool it's bad because it's so confidently incorrect, you may be fooled by bad answers.
Earlier quoted context omitted.
> 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.
> Helping a group of people reach a solution everyone is happy with has little to do with technology.
This one specific thing, is actually something that ChatGPT can help with.
It's not as good as the best human, or even a middling human with 5 year's business experience, but rather it's useful because it's good enough at so many different domains that it can be used to clarify thoughts and explain the boundaries of the possible — Google Translate for business jargon, though like Google Translate it is also still often wrong — the ultimate "jack of all trades, master of none".
He mentions that he posed to O1 the same challenge he posed to a previous GPT (which he also previously blogged about), so I am wondering how much O1 benefited from potentially "seeing" this discussion in its training set (which probably contains a very well recent snapshot of the world wide web).
Earlier quoted context omitted.
Thing is, I'm used to hearing a very similar sentiment on how e.g. using vim keybindings is so literally going to make me a 10x 100x whatever rockstar developer - and it's like what, enabling me to edit text a bit faster? And it's always anecdotes that yeah, from-qualia you feel so fast. But from-qualia I run like a marathon runner and sound like a radio host. I personally did find some use cases for it and it does a…
> using vim keybindings is so literally going to make me a 10x 100x whatever rockstar developer - and it's like what, enabling me to edit text a bit faster? Yes, to me LLM is exactly like this: from nano to vim.
Earlier quoted context omitted.
Productivity is not the only aspect of our profession that matters, and in fact it's probably not even the most important part. I'm not suggesting we get stuck or handcraft every aspect of our code, and there are multitudes of abstractions and tools that enhance productivity, including everything from frameworks to compilers. What I'm saying is what the original comment is doing, having the LLM write all their code,…
You don't need to call them at 4am, you can keep a git log of the prompts that were used to generate the code and some professional 4am debugger can sit there and use an LLM to fix it. Probably not a practical option yet, but if we're looking at the long term that is where we are heading. Or, realistically, the even longer term where the LLM self-heals broken systems.
Earlier quoted context omitted.
Me too.
Somebody tested people on Hacker News to evaluate programming competency. This was part of a larger evaluation comparing the Hacker News population to people on Reddit programming subreddits. Here is a very heated discussion of the result: https://news.ycombinator.com/item?id=33293522 It appears that Hacker News is perhaps NOT populated by the programming elite. In contrast, there are real wizards on Reddit. Surprisi…