Everyone saying you could replace Jev or decision type models with an LLM with bolted schema output constraining are missing the point completely. Its about extreme speed and cost effectiveness with high quality, neither of which you are going to get with LLMs even with these KV-cache tricks
The main reason to learn something is actually being able to communicate in the language of that subject. There are complex ideas in math that cannot be easily captured by the language of other fields. Pepole who don't study math cannot even understand what a worthwhile goal in math even is or how it could be useful to other fields.
You can't simply prompt a model to be "better" when "better" isnt even properly defined
> Officials said some users expected Maven to flag stale records or contradictions in the intelligence assembled for potential targets, though it is not clear why they thought the system would do that
This is what happens when people who don't understand AI and its limitations embrace it wholeheartedly, thinking it's going to behave like The ultimate analyst. Except it's not. Its got blind spots in more places than anyone knows. And not to mention the system itself has multiple areas of failure.
No, this is what happens when software developers don't understand how users actually use their products.
This was a totally expected outcome, similar to how CV cameras arrest the wrong minorities in neighboring states 100s of miles away because it told the officer it was them; or how health insurance companies use ML algorithms to deny Americans care.
It's going to happen in other sectors of life and it will continue killing innocent civilians.
No, I'm saying health insurance companies routinely deny American civilians life saving care because they'd make more money and routinely use similar software that also allowed 200 school age girls to be murdered. Recalling that a CEO was murdered and the person excused is being hailed as a hero over just this. Think people care about this a lot actually.
For better or worse, health care providers at least in the US are for profit businesses. There's been plenty of arguments made to change that, but as it stands we shouldn't be surprised when a for profit business decides what service they provide and to whom they provide it.
Likewise, we shouldn't be surprised when someone who puts profits over other's lives gets ventillated by one of those lives in downtown New York. And what do you know, nobody was.
My post very unambiguously explains that is an unsurprising thing. It does not explicitly say it was a good thing, so no, "good" is not specifically what I am saying in that post.
Chatbots in general can be quite opaque in how they operate, the biggest issue with agent products is communicating it's capabilities and limitations to users. If you have a bank app it's pretty clear whether or not it can send wire transfers, but a if that's a chatbot, users will have to think to ask it (and even then it could hallucinate)
Come on, they understand it perfectly well. They blew up a school! Of course they’ll happily blame the AI when journos nudge nudge wink wink suggest that they’ll take that as a perfectly good explanation.
The real headline is “Americans blow up school, blame AI”
Actually, no. Murder is the deliberate killing of a person. If the person in your example believed the gun wouldn't go off, then it isn't murder. Negligent as hell, yes. Manslaughter, certainly. But not murder, because it doesn't meet the definition.
The entire point of the post is that it isn't credible that the person actually thought their killing machine couldn't kill: pointing a gun at someone with the intention of killing, and pulling the trigger, counts as murder, even if you thought the person would magically survive if they were innocent.
You're free to try to make a case otherwise, but it'll be an uphill battle against reason.
Based on my admittedly limited research, it seems like you should use Laya for much more deterministic tasks where you have some training data. It won't be as good as Jev for zero shot cases.
I did that on a little macbook m4 last night on my model of the innate immune system—fine tuning took 15m or so. Just wish it had a larger context window
Note that this proof while impressive does not add any value to mathematics as a
human pursuit. But it does show we can throw these LLM beasts at much gnarlier
problems than we could have imagined previously. Maybe even formally verify papers the day they are posted?
I'd love to see an e2e compiler or OS kernel verification or Full-stack chip design with formal equivalence checking at each stage that would be pretty cool.
What else is interesting is how they staged this problem : (a) maintain an explicit DAG/roadmap of sub-goals rather than one flat prompt, (b) separate statements from proofs so many agents can work on different nodes without stepping on each other, (c) keep a natural-language index alongside the formal one so search/reuse works... I feel like this is the future of long horizon agents and how you can do work that's making the most of every agent. This approach will likely be baked into the next versions of coding harnesses
> Note that this proof while impressive does not add any value to mathematics as a human pursuit.
I don't see how this can be stated with such certainty. We don't yet know what the implications of large scale autoformalization and proof verification will be on the human pursuit of mathematics. I'm open to the idea that it might be a benefit to the human pursuit once the human pursuit adapts.
> one might naively expect that the natural question to ask with regards to a given problem X in a field is "What is the answer to X?". But in many cases the more valuable question is "What can be learned from studying X?"
And later
> But the currently fashionable practice of pointing a powerful AI tool at the task of answering a problem X, unguided by any human expert in the field X resides in, has created an unprecedented divergence between the production of answers, and the production of insight, to the point where the two questions have become _negatively correlated_:
That seems narrow minded. Theres both "learnings directly related to the thing studied" and "learnings downstream from the thing studied". If you imagine mathematics being a huge sudoku puzzle of unknowns you are trying to fill in, each previously empty square you are able to fill in (or gain a smaller bound on) has implications in all sorts of other areas.
It's important to remember that most mathematics is not science - large parts of it are mostly esthetic pursuits that bring joy to certain mathematicians, and sometimes happen to have unexpected benefits to science or engineering (like how number theory suddenly became important to cryptography in the 20th century).
Fermat's last theorem is a great example - it is in itself a completely irrelevant observation, not used (so far) in any larger theory. It was only pursued because (a) Fermat casually claimed to have easily proved it (almost certainly being mistaken about it), and (b) it sparked the curiosity of mathematicians because it looks so simple but turned out to be so hard.
So what does humanity gain by knowing that the theorem holds? Basically nothing. What does humanity gain from the process of proving it? As far as it is known for now, basically nothing (though it is somewhat likely that the complex theories created to prove it will find other applications). However, those that have worked on it, and the guy who did prove it, gained a huge amount of personal insight into mathematics, and surely grew as mathematicians, and will hopefully use those skills in working on other problems that may prove more directly useful. Plus, they had a great time doing it.
What this means is that, if the proof had been discovered entirely by AI, basically nothing would have been gained. LLMs don't learn by doing, so no personal experience growth would have come from this; and as I mentioned, both the result and the proof are, so far, quite irrelevant even for mathematics more broadly. So it would have been actively detrimental, or at best neutral, compared to letting human mathematicians work on this problem, in a way that is never the case in science or engineering, where any bit of knowledge is in itself useful to at least some extent.
In your letter of December 14, you ask me whether mathematics is a worthwhile endeavor. Mathematics absolutely is not a worthwhile endeavor! I can imagine only three possible reasons for studying mathematics:
(1) Entertainment.
(2) To promote technological progress.
(3) To promote one’s own career.
Reason (1) is harmless; but one doesn’t refer to entertainment as a “worthwhile endeavor”; it’s just a pastime.
As for reason (2), modern technology is the worst thing that ever happened to the world, and to promote its progress is nothing short of criminal. Read Our Final Century, by Martin Rees; or read “Why the Future Doesn’t Need Us,” an article by Bill Joy that appeared in Wired magazine, April, 2000.
As for reason (3), to choose mathematics as one’s career would be very risky. Not long ago I received a letter from a gravestone sculptor whose craft had been rendered obsolete by a laser-guided machine that carved gravestones automatically. He was in his forties, unable to find work, and depressed. Maybe you think that can’t happen to you if you become a mathematician. But you’re wrong. Martin Rees, Bill Joy, and many other distinguished experts believe that within a few decades machines will be developed that will be more intelligent than even the smartest human beings. When that happens, people will be obsolete; they will be phased out and will be replaced by computers and robots. This will happen to everyone eventually, but mathematicians probably will become obsolete before anyone else does, because mathematics is more amenable to computerization than any other field. Hence, computers probably will surpass humans in mathematics before they do so in other areas.
> He skips over understanding our world which is probably the reason most pure maths is done.
I'm not sure I agree with this. I suppose it could be that we have different defintions of what "our world" means.
You might like the quote below. I suspect you're arguing that most pure math is performed for option #2 below (utilitarian purposes). Like I said, I'm not so sure.
In the temple of science are many mansions, and various indeed are they that dwell therein and the motives that have led them thither. Many take to science out of a joyful sense of superior intellectual power; science is their own special sport to which they look for vivid experience and the satisfaction of ambition; many others are to be found in the temple who have offered the products of their brains on this altar for purely utilitarian purposes. Were [someone to] drive all the people belonging to these two categories out of the temple, the assemblage would be seriously depleted, but there would still be some men, of both present and past times, left inside. Our Planck is one of them, and that is why we love him.
I guess I was including maths and imagine mathematicians investigate stuff of the general type like the riemann hypothesis, whether all non-trivial zeros of the Riemann zeta function lie on the critical line where the real part equals 1/2, which are interesting but of little practical value.
Personally, I found that people are impressed with AI for subjects they simply don't understand, and when an expert works with AI, they're often underwhelmed. So while we're seeing some mathematics being automated and proved, I think there's a long way to go before we automate proofs with meaningful human value.
Google doesnt even use its own Go build system internally. Its all blaze / bazel, so they are not even taking advantage of the so called compiler feedback of Go. Also if languages are to be designed for agents not humans, its not clear whether the verbosity of Go will help agents at all
