This is why AI coding assistance will leap ahead in the coming years. Chat AI has no clear reward function (basically impossible to judge the quality of responses to open-ended questions like historical causes for a war). Coding AI can write tests, write code, compile, examine failed test cases, search for different coding solutions that satisfy more test cases or rewrite the tests, all in an unsupervised loop. And then whole process can turn into training data for future AI coding models.
I expect language models to also get crazy good at mathematical theorem proving. The search space is huge but theorem verification software will provide 100% accurate feedback that makes real reinforcement learning possible. It's the combination of vibes (how to approach the proof) and formal verification that works.
Formal verification of program correctness never got traction because it's so tedious and most of the time approximately correct is good enough. But with LLMs in the mix the equation changes. Having LLMs generate annotations that an engine can use to prove correctness might be the missing puzzle piece.
Does programming have a clear reward function? A vague description from a business person is not it. By the time someone (a programmer?) has written a reward function that is clear enough, how would that function look compared to a program?
Programming has a clear reward function when the problem being solving is well-specified, e.g., "we need a program that grabs data from these three endpoints, combines their data in this manner, and returns it in this JSON format."
The same is true for math. There is a clear reward function when the goal is well-specified, e.g., "we need a sequence of mathematical statements that prove this other important mathematical statement is true."
I’m not sure I would agree. By the time you’ve written a full spec for it, you may as well have just written a high level programming language anyway. You can make assumptions that minimise the spec needed… but also programming APIs can have defaults so that’s no advantage.
I’d suggest that the Python code for your example prompt with reasonable defaults is not actually that far from the prompt itself in terms of the time necessary to write it.
However, add tricky details like how you want to handle connection pooling, differing retry strategies, short circuiting based on one of the results, business logic in the data combination step, and suddenly you’ve got a whole design doc in your prompt and you need a senior engineer with good written comms skills to get it to work.
Thanks. I view your comment as orthogonal to mine, because I didn't say anything about how easy or hard it would be for human beings to specify the problems that must be solved. Some problems may be easy to specify, others may be hard.
I feel we're looking at the need for a measure of the computational complexity of problem specifications -- something like Kolmogorov complexity, i.e., minimum number of bits required, but for specifying instead of solving problems.
Apologies, I guess I agree with your sentiment but disagree with the example you gave as I don't think it's well specified, and my more general point is that there isn't an effective specification, which means that in practice there isn't a clear reward function. If we can get the clear specification, which we probably can do proportionally to the complexity of the problem, and not getting very far up the complexity curve, then I would agree we can get the good reward function.
Ah, got it. I was just trying to keep my comment short!
Remember all those attempts to transform UML into code back in the day? This sounds sorta like that. I’m not a total genai naysayer but definitely in the “cautiously curious” camp.
Absolutely, we've tried lots of ways to formalise software specification and remove or minimise the amount of coding, and almost none of it has stuck other than creating high level languages and better code-level abstractions.
I think generative AI is already a "really good autocomplete" and will get better in that respect, I can even see it generating good starting points, but I don't think in its current form it will replace the act of programming.
Yeah, an LLM applied to converting design docs to programs seems like, essentially, the invention of an extremely high level programming language. Specifying the behavior of the program in sufficient detail is… why we have programming languages.
There’s the task of writing syntax, which is the mechanical overhead of the task of telling the computer what to do. People should focus on the latter (too much code is a symptom of insufficient automation or abstraction). Thankfully lots of people have CS degrees, not “syntax studies” degrees, right?
20 years, number of "well specified" requirements documents I've received: 0.
A couple of problems that is impossible to prove from the constructivism angle:
1) Addition of the natural numbers 2) equality of two real numbers
When you restrict your tools to perceptron based feed forward networks with high parallelism and no real access to 'common knowledge', the solution set is very restricted.
Basically what Gödel proved that destroyed Russel's plans for the Mathmatica Principia applies here.
Programmers can decide what is sufficient if not perfect in models.
the reason why we spend time programming is because the problems in question are not easily defined, let alone the solutions.
If you’re the most junior level, sure.
Anything above that, things get fuzzy, requirements change, biz goals shift.
I don’t really see this current wave of AI giving us anything much better than incremental improvement over copilot.
A small example of what I mean:
These systems are statistically based, so there’s no probability. Because of that, I wouldn’t even gain anything from having it write my tests since tests are easily built wrong in subtle ways.
I’d need to verify the test by reviewing it and, imo, writing the test would be less time than coaxing a correct one, reviewing, re-coaxing, repeat.
can you give an example of what "in this manner" might be?
This could make programming more declarative or constraint-based, but you'd still have to specify the properties you want. Ultimately, if you are defining some function in the mathematical sense, you need to say somehow what inputs go to what outputs. You need to communicate that to the computer, and a certain number of bits will be needed to do that. Of course, if you have a good statistical model of how-probably a human wants a given function f, then you can perform that communication to the machine in 1/log(P(f)) bits, so the model isn't worthless.
Here I have assumed something about the set that f lives in. I am taking for granted that a probability measure can be defined. In theory, perhaps there are difficulties involving the various weird infinities that show up in computing, related to undecideability and incompleteness and such. But at a practical level, if we assume some concrete representation of the program then we can just define that it is smaller than some given bound, and ditto for a number of computational steps with a particular model of machine (even if fairly abstract, like some lambda calculus thing), so realistically we might be able to not worry about it.
Also, since our input and output sets are bounded (say, so many 64-bit doubles in, so many out), that also gives you a finite set of functions in principle; just think of the size of the (impossibly large) lookup table you'd need to represent it.
Exactly, and people have been saying this for a while now. If an "AI software engineer" needs a perfect spec with zero ambiguity, all edge cases defined, full test coverage with desired outcomes etc., then the person writing the spec is the actual software engineer, and the AI is just a compiler.
Sounds like this work would involve asking questions to collaborators, guess some missing answers, write specs and repeat. Not that far ahead of the current sota of AI...
Same reason the visual programming paradigm failed, tbe main problem is not the code.
While writing simple functions may be mechanistic, being a developer is not.
'guess some missing answers' is why Waterfall, or any big upfront design has failed.
People aren't simply loading pig iron into rail cars like Taylor assumed.
The assumption of perfect central design with perfect knowledge and perfect execution simply doesn't work for systems which are for more like an organism than a machine.
Waterfall fails when domain knowledge is missing. Engineers won't take "obvious" problems into consideration when they don't even know what the right questions to ask are. When a system gets rebuild for the 3rd time the engineers do know what to build and those basic mistakes don't get made.
Next gen LLMs, with their encyclopedic knowledge about the world, won't have that problem. They'll get the design correct on their first attempt because they're already familiar with the common pitfalls.
Of course we shouldn't expect LLMs to be a magic bullet that can program anything. But if your frame of reference is "visual programming" where the goal is to turn poorly thought out requirements into a reasonably sensible state machine then we should expect LLMs to get very good at that compared to regular people.
What makes you think they'll need a perfect spec?
Why do you think they would need a more defined spec than a human?
A human has the ability to contact the PM and say, "This won't work, for $reason," or, "This is going to look really bad in $edgeCase, here are a couple options I've thought of."
There's nothing about AI that makes such operations intrinsically impossible, but they require much more than just the ability to generate working code.
We’ve also learned that starting off by rigidly defined spec is actually harmful to most user facing software, since customers change their minds so often and have a hard time knowing what they want right from the start.
This is why most of the best software is written by people writing things for themselves and most of the worst is made by people making software they don't use themselves.
Reminds me of when computers were literally humans computing things (often women). How time weaves its circular web.
This is not quite right - a specification is not equivalent to writing software, and the code generator is not just a compiler - in fact, generating implementations from specifications is a pretty active area of research (a simpler problem is the problem of generating a configuration that satisfies some specification, "configuration synthesis").
In general, implementations can be vastly more complicated than even a complicated spec (e.g. by having to deal with real-world network failures, etc.), whereas a spec needs only to describe the expected behavior.
In this context, this is actually super useful, since defining the problem (writing a spec) is usually easier than solving the problem (writing an implementation); it's not just translating (compiling), and the engineer is now thinking at a higher level of abstraction (what do I want it to do vs. how do I do it).
I mean, that's already the case in many places, the senior engineer / team lead gathering requirements and making architecture decisions is removing enough ambiguity to hand it off to juniors churning out the code. This just makes very cheap, very fast typing but uncreative and a little dull junior developers.
Exactly. This is what I tell everyone. The harder you work on specs the easier it gets in the aftermath. And this is exactly what business with lofty goals doesn’t get or ignores. Put another way: a fool with a tool…
Also look out for optimization the clever way.
Much business logic is really just a state machine where all the states and all the transitions need to be handled. When a state or transition is under-specified an LLM can pass the ball back and just ask what should happen when A and B but not C. Or follow more vague guidance on what should happen in edge cases. A typical business person is perfectly capable of describing how invoicing should work and when refunds should be issued, but very few business people can write a few thousand lines of code that covers all the cases.
What should the colleagues of the business person review before deciding that the system is fit for purpose? Or what should they review when the system fails? Should they go back over the transcript of the conversation with the LLM?
How does a business person today decide if a system is fit for purpose when they can't read code? How is this different?
They don't, the software engineer does that. It is different since LLMs can't test the system like a human can.
Once the system can both test and update the spec etc to fix errors in the spec and build the program and ensure the result is satisfactory, we have AGI. If you argue an AGI could do it, then yeah it could as it can replace humans at everything, the argument was for an AI that isn't yet AGI.
The world runs on fuzzy underspecified processes. On excel sheets and post-it notes. Much of the world's software needs are not sophisticated and don't require extensive testing. It's OK if a human employee is in the loop and has to intervenes sometimes when an AI-built system malfunctions. Businesses of all sizes have procedures where problems get escalated to more senior people with more decision-making power. The world is already resilient against mistakes made by tired/inattentive/unintelligent people, and mistakes made by dumb AI systems will blend right in.
Excel sheets are not fuzzy and underspecified.
I've never worked on software where this was OK. In many cases it would have been disastrous. Most of the time a human employee could not fix the problem without understanding the software.
All software that interops with people, other businesses, APIs, deals with the physical world in any way, or handles money has cases that require human intervention. It's 99.9% of software if not more. Security updates. Hardware failures. Unusual sensor inputs. A sudden influx of malformed data. There is no such thing as an entirely autonomous system.
But we're not anywhere close to maximally automated. Today (many? most?) office workers do manual data entry and processing work that requires very little thinking. Even automating just 30% of their daily work is a huge win.
As an LLM can output source code, that's all answerable with "exactly what they already do when talking to developers".
There are two reasons the system might fail:
1) The business person made a mistake in their conversation/specification.
In this case the LLM will have generated code and tests that match the mistake. So all the tests will pass. The best way to catch this before it gets to production is to have someone else review the specification. But the problem is that the specification is a long trial-and-error conversation in which later parts may contradict earlier parts. Good luck reviewing that.
2) The LLM made a mistake.
The LLM may have made the mistake because of a hallucination which it cannot correct because in trying to correct it the same hallucination invalidates the correction. At this point someone has to debug the system. But we got rid of all the programmers.
This still resolves as "business person asks for code, business person gets code, business person says if code is good or not, business person deploys code".
That an LLM or a human is where the code comes from, doesn't make much difference.
Though it does kinda sound like you're assuming all LLMs must develop with Waterfall? That they can't e.g. use Agile? (Or am I reading too much into that?)
How do they do this? They can't trust the tests because the tests were also developed by the LLM which is working from incorrect information it received in a chat with the business person.
The same way they already do with humans coders whose unit tests were developed by exactly same flawed processes:
Mediocrely.
Sometimes the current process works, other times the planes fall out of the sky, or updates causes millions of computers to blue screen on startup at the same time.
LLMs in particular, and AI in general, doesn't need to beat humans at the same tasks.
Well, to give an example: the complexity class NP is all about problems that have quick and simple verification, but finding solutions for many problems is still famously hard.
So there are at least some domains where this model would be a step forward.
But in that case, finding the solution is hard and you generally don't try. Instead, you try to get fairly close, and it's more difficult to verify that you've done so.
No. Most instances of most NP hard problems are easy to find solutions for. (It's actually really hard to eg construct a hard instance for the knapsack problem. And SAT solvers also tend to be really fast in practice.)
And in any case, there are plenty of problems in NP that are not NP hard, too.
Yes, approximation is also an important aspect of many practical problems.
There's also lots of problems where you can easily specify one direction of processing, but it's hard to figure out how to undo that transformation. So you can get plenty of training data.
I have a very simple integer linear program and it is really waiting for the heat death of the universe.
No, running it as a linear program is still slow.
I'm talking about small n=50 taking tens of minutes for a trivial linear program. Obviously the actual linear program is much bigger and scales quadratically in size, but still. N=50 is nothing.
The reward function could be "pass all of these tests I just wrote".
Lol. Literally.
If you have those many well written tests, you can pass them to a constraint solver today and get your program. No LLM needed.
Or even run your tests instead of the program.
Probably the parent assumes that he does have the tests, billions of them.
One very strong LLM could generate billions of tests alongside the working code and then train another smaller model, or feed it into the next iteration of training same the strong model. Strong LLMs do exist for that purpose, Nemotron 320B and Llama 3 450B.
It would be interesting if a dataset like that would be created like that, and then released as open source. Many LLMs proprietary or not, could incorporate the dataset in their training, and have on the internet hundreds of LLMs suddenly become much better at coding, all of them at once.
I think you could set up a good reward function for a programming assistance AI by checking that the resulting code is actually used. Flag or just 'git blame' the code produced by the AI with the prompts used to produce it, and when you push a release, it can check which outputs were retained in production code from which prompts. Hard to say whether code that needed edits was because the prompt was bad or because the code was bad, but at least you can get positive feedback when a good prompt resulted in good code.
GitHub Copilot's telemetry does collect data on whether generated code snippets end up staying in the code, so presumably models are tuned on this feedback. But you haven't solved any of the problems set out by Karpathy here—this is just bankshot RLHF.
That could be interesting but it does seem like a much fuzzier and slower feedback loop than the original idea.
It also seems less unique to code. You could also have a chat bot write an encyclopedia and see if the encyclopedias sold well. Chat bots could edit Wikipedia and see if their edits stuck as a reward function (seems ethically pretty questionable or at least in need of ethical analysis, but it is possible).
The maybe-easy to evaluate reward function is an interesting aspect of code (which isn’t to say it is the only interesting aspect, for sure!)
Very good point. For some types of problems maybe the answer is yes. For example porting. The reward function is testing it behaves the same in the new language as the old one. Tricky for apps with a gui but doesn't seem impossible.
The interesting kind of programming is the kind where I'm figuring out what I'm building as part of the process.
Maybe AI will soon be superhuman in all the situations where we know exactly what we want (win the game), but not in the areas we don't. I find that kind of cool.
Even for porting there's a bit of ambiguity... Do you port line-for-line or do you adopt idioms of the target language? Do you port bug-for-bug as well as feature-for-feature? Do you leave yet-unused abstractions and opportunities for expansion that the original had coded in, if they're not yet used, and the target language code is much simpler without?
I've found when porting that the answers to these are sometimes not universal for a codebase, but rather you are best served considering case-by-case inside the code.
Although I suppose an AI agent could be created that holds a conversation with you and presents the options and acts accordingly.
“A precise enough specification is already code”, which means we'll not run out of developers in the short term. But the day to day job is going to be very different, maybe as different as what we're doing now compared to writing machine code on punchcards.
Doubtful. This is the same mess we've been in repeatedly with 'low code'/'no code' solutions.
Every decade it's 'we don't need programmers anymore'. Then it turns out specifying the problem needs programmers. Then it turns out the auto-coder can only reach a certain level of complexity. Then you've got real programmers modifying over-complicared code. Then everyone realizes they've wasted millions and it would have been quicker and cheaper to get the programmers to write the code in the first place.
The same will almost certainly happen with AI generated code for the next decade or two, just at a slightly higher level of program complexity.
There's no reward function in the sense that optimizing the reward function means the solution is ideal.
There are objective criteria like 'compiles correctly' and 'passes self-designed tests' and 'is interpreted as correct by another LLM instance' which go a lot further than criteria that could be defined for most kinds of verbal questions.
You can define one based on passed tests, code coverage, other objectives, or weighted combinations without too much loss of generality.
If we will struggle to create reward functions for AI, then how different is that from the struggles we already face when divvying up product goals into small tasks to fit our development cycles?
In other words, to what extent does Agile's ubiquity prove our competence in turning product goals into de facto reward functions?
+1
There's levels to this.
Certainly "compiled" is one reward (although a blank file fits that...) Another is test cases, input and output. This doesn't work on a software-wide scale but function-wide it can work.
In the future I think we'll see more of this test-driven development. Where developers formally define the requirements and expectations of a system and then an LLM (combined with other tools) generates the implementation. So instead of making the implementation, you just declaratively say what the implementation should do (and shouldn't).
If they get permission and don't mind waiting, they could check if people throw away the generated code or keep it as-is.
My reward in Rust is often when the code actually compiles...
Full circle but instead of determinism you introduce some randomness. Not good.
Also the reasoning is something business is dissonant about. The majority of planning and execution teams stick to processes. I see way more potential automating these than all parts in app production.
Business is going to have a hard time, when they believe, they alone can orchestrate some AI consoles.
Unless you want an empty test suite or a test suite full of `assert True`, the reward function is more complicated than you think.
Code coverage exists. Shouldn't be hard at all to tune the parameters to get what you want. We have really good tools to reason about code programmatically - linters, analyzers, coverage, etc.
In my experience they are ok (not excellent) for checking whether some code will crash or not. But checking whether the code logic is correct with respect to the requirements is far from being automatized.
But for writing tests that's less of an issue. You start with known good/bad code and ask it to write tests against a spec for some code X - then the evaluation criteria is something like did the test cover the expected lines and produce the expected outcome (success/fail). Pepper in lint rules for preferred style etc.
But this will lead you to the same problem the tweet is talking! You are training a reward model based on human feedback (whether the code satisfies the specification or not). This time the human feedback may seem more objective, but in the end it's still non-exhaustive human feedback which will lead to the reward model being vulnerable to some adversarial inputs which the other model will likely pick up pretty quickly.
It's based on automated tools and evaluation (test runner, coverage, lint) ?
The input data is still human produced. Who decides what is code that follows the specification and what is code that doesn't? And who produces that code? Are you sure that the code that another model produces will look like that? If not then nothing will prevent you from running into adversarial inputs.
And sure, coverage and lints are objective metrics, but they don't directly imply the correctness of a test. Some tests can reach a high coverage and pass all the lint checks but still be incorrect or test the wrong thing!
Whether the test passes or not is what's mostly correlated to whether it's correct or not. But similarly for an image recognizer the prompt of whether an image is a flower or not is also objective and correlated, and yet researchers continue to find adversarial inputs for image recognizer due to the bias in their training data. What makes you think this won't happen here too?
So are rules for the game of go or chess ? Specifying code that satisfies (or doesn't satisfy) is a problem statement - evaluation is automatic.
I'd be willing to bet that if you start with an existing coding model and continue training it with coverage/lint metrics and evaluation as feedback you'd get better at generating tests. Would be slow and figuring out how to build a problem dataset from existing codebases would be the hard part.
The rules are well defined and you can easily write a program that will tell whether a move is valid or not, or whether a game has been won or not. This allows you generate virtually infinite amount of data to train the model on without human intervention.
This would be true if you fix one specific program (just like in Go or Chess you fix the specific rules of the game and then train a model on those) and want to know whether that specific program satisfies some given specification (which will be the input of your model). But if instead you want the model to work with any program then that will have to become part of the input too and you'll have to train it an a number of programs which will have to be provided somehow.
This is the "Human Feedback" part that the tweet author talks about and the one that will always be flawed.
Who writes the spec to write tests against?
In the end, your are replacing the application code by a spec, which needs to have a comparable level of detail in order for the AI to not invent its own criteria.
Code coverage proves that the code runs, not that it does what it should do.
If you have a test that completes with the expected outcome and hits the expected code paths you have a working test - I'd say that heuristic will get you really close with some tweaks.
It's easy to imagine why something could never work.
It's more interesting to imagine what just might work. One thing that has plagued programmers for the past decades is the difficulty of writing correct multi-threaded software. You need fine-grained locking otherwise your threads will waste time waiting for mutexes. But color-coding your program to constrain which parts of your code can touch which data and when is tedious and error-prone. If LLMs can annotate code sufficiently for a SAT solver to prove thread safety that's a huge win. And that's just one example.
Rust is that way.
Adversarial networks are a straightforward solution to this. The reward for generating and solving tests is different.
That's a good point. A model that is capable of implementing a nonsense test is still better than a model that can't. The implementer model only needs a good variety of tests. They don't actually have to translate a prompt into a test.
It's not trivial to get right but it sounds within reach, unlike “hallucinations” with general purpose LLM usage.
This reads as a proper marketing ploy. If the current incarnation of AI + coding is anything to go by - it'll take leaps just to make it barely usable (or correct)
My take is the opposite: considering how good AI is at coding right now I'm eager to see what comes next. I don't know what kind of tasks you've tried using it for but I'm surprised to hear someone think that it's not even "barely usable". Personally, I can't imagine going back to programming without a coding assistant.
write performance oriented and memory safe C++ code. Current coding assistants are glorified autocomplete for unit tests or short api endpoints or what have you but if you have to write any safety oriented code or you have to think about what the hardware does it's unusable.
I tried using several of the assistants and they write broken or non-performant code so regularly it's irresponsible to use them.
Isn't this a good reward function for RL? Take a codebase's test suite. Rip out a function, let the LLM rewrite the function, benchmark it and then RL it using the benchmark results.
I've also had trouble having assistants help with CSS, which is ostensibly easier than performance oriented and memory safe C++
I've been playing with it recently, and I find unless there are very clear patterns in surrounding code or on the Internet, it does quite terribly. Even for well-seasoned libraries like V8 and libuv, it can't reliably not make up APIs that don't exist and it very regularly spits out nonsense code. Sometimes it writes code that works and does the wrong thing, it can't reliably make good decisions around undefined behavior. The worst is when I've asked for it to refactor code, and it actually subtly changes the behavior in the process.
I imagine it's great for CRUD apps and generating unit tests, but for anything reliable where I work, it's not even close to being useful at all, let alone a game changer. It's a shame, because it's not like I really enjoy fiddling with memory buffers and painstakingly avoiding UB, but I still have to do it (I love Rust, but it's not an option for me because I have to support AIX. V8 in Rust also sounds like a nightmare, to be honest. It's a very C++ API).
I've seen them all over the place.
The best are shockingly good… so long as their context doesn't expire and they forget e.g. the Vector class they just created has methods `.mul(…)` rather than `.multiply(…)` or similar. Even the longer context windows are still too short to really take over our jobs (for now), the haystack tests seem to be over-estimating their quality in this regard.
The worst LLM's that I've seen (one of the downloadable run-locally models but I forget which) — one of my standard tests is that I ask them to "write Tetris as a web app", and it started off doing something a little bit wrong (square grid), before giving up on that task entirely and switching from JavaScript to python and continuing by writing a script to train a new machine learning model (and people still ask how these things will "get out of the box" :P)
People who see more of the latter? I can empathise with them dismissing the whole thing as "just autocomplete on steroids".
TDD approach could play the RL role.
But what makes you think the ai generated tests will correctly represent the problem at hand?
I'm pretty interested in the theorem proving/scientific research aspect of this.
Do you think it's possible that some version of LLM technology could discover new physical theories (that are experimentally verifiable), like for example a new theory of quantum gravity, by exploring the mathematical space?
Edit: this is just incredibly exciting to think about. I'm not an "accelerationist" but the "singularity" has never felt closer...
Current LLMs are optimized to produce output most resembling what a human would generate. Not surpass it.
The output most pleasing to a human, which is both better and worse.
Better, when we spot mistakes even if we couldn't create the work with the error. Think art: most of us can't draw hands, but we can spot when Stable Diffusion gets them wrong.
Worse also, because there are many things which are "common sense" and wrong, e.g. https://en.wikipedia.org/wiki/Category:Paradoxes_in_economic..., and we would collectively down-vote a perfectly accurate model of reality for violating our beliefs.
My hunch is that LLMs are nowhere near intelligent enough to make brilliant conceptual leaps. At least not anytime soon.
Where I think AI models might prove useful is in those cases where the problem is well defined, where formal methods can be used to validate the correctness of (partial) solutions, and where the search space is so large that work towards a proof is based on "vibes" or intuition. Vibes can be trained through reinforcement learning.
Some computer assisted proofs are already hundreds of pages or gigabytes long. I think it's a pretty safe bet that really long and convoluted proofs that can only be verified by computers will become more common.
https://en.wikipedia.org/wiki/Computer-assisted_proof
They don't need to be intelligent to make conceptual leaps. DeepMind stuff just does a bunch of random RL experiments until it finds something that works.
I think the answer is almost certainly no, and is mostly unrelated to how smart LLMs can get. The issue is that any theory of quantum gravity would only be testable with equipment that is much, much more complex than what we have today. So even if the AI came up with some beautifully simple theory, testing that its predictions are correct is still not going to be feasible for a very long time.
Now, it is possible that it could come up with some theory that is radically different from current theories, where quantum gravity arises very naturally, and that fits all of the other predictions of of the current theories that we can measure - so we would have good reasons to believe the new theory and consider quantum gravity probably solved. But it's literally impossible to predict whether such a theory even exists, that is not mathematically equivalent to QM/QFT but still matches all confirmed predictions.
Additionally, nothing in AI tech so far predicts that current approaches should be any good at this type of task. The only tasks where AI has truly excelled at are extremely well defined problems where there is a huge but finite search space; and where partial solutions are easy to grade. Image recognition, game playing, text translation are the great successes of AI. And performance drops sharply with the uncertainty in the space, and with the difficulty of judging a partial solution.
Finding physical theories is nothing like any of these problems. The search space is literally infinite, partial solutions are almost impossible to judge, and even judging whether a complete solution is good or not is extremely difficult. Sure, you can check if it's mathematically coherent, but that tells you nothing about whether it describes the physical world correctly. And there are plenty of good physical theories that aren't fully formally proven, or weren't at the time they were invented - so mathematical rigour isn't even a very strong signal (e.g. Newton's infinitesimal calculus wasn't considerered sound until the 1900s or something, by which time his theories had long since been rewritten in other terms; the Dirac delta wasn't given a precise mathematical definition until much later than it's uses; and I think QFT still uses some iffy math even today).
IIRC, there have been people doing similar things using something close to brute-force. Nothing of real significance has been found. A problem is that there are infinitely many physically and mathematically correct theorems that would add no practical value.
Will this be able to be done without spending absurd amounts of energy?
Energy efficiency might end up being the final remaining axis on which biological brains surpass manufactured ones before the singularity.
The amount of energy is truly absurd. I dont chug a 16 oz bottle of water every time I answer a question.
Computer energy efficiency is not as constrained as minimum feature size, it's still doubling every 2.6 years or so.
Even if they were, a human-quality AI that runs at human-speed for x10 our body's calorie requirements in electricity, would still (at electricity prices of USD 0.1/kWh) undercut workers earning the UN abject poverty threshold.
Writing tests won't help you here, this problem is the same as other generation tasks. If the test passes, everything seems okay, right? Consider this: you now have a 50-line function just to display 'hello world'. It outputs 'hello world', so it scores well, but it's hardly efficient. Then, there's a function that runs in exponential time instead of the standard polynomial time that any sensible programmer would use in specific cases. It passes the tests, so it gets a high score. You also have assembly code embedded in C code, executed with 'asm'. It works for that particular case and passes the test, but the average C programmer won't understand what's happening in this code, whether it's secure, etc. Lastly, tests written by AI might not cover all cases, they could even fail to test what you intended because they might hallucinate scenarios (I've experienced this many times). Programming faces similar issues to those seen in other generation tasks in the current generation of large language models, though to a slightly lesser extent.
One can image critics and code rewriters that optimize for computational, code style, and other requirements in addition to tests.
Future coding where developers only ever write the tests is an intriguing idea.
Then the LLM generates and iterates on the code until it passes all of the tests. New requirements? Add more tests and repeat.
This would be legitimately paradigm shifting, vs. the super charged auto complete driven by LLMs we have today.
Tests don’t prove correctness of the code. What you’d really want instead is to specify invariants the code has to fulfill, and for the AI to come up with a machine-checkable proof that the code indeed guarantees those invariants.
Once you have enough data points, from current usage, and these days every company is tracking EVERYTHING even eye movement if they could, it's just a matter of time. I do agree though that before we reach an AGI we have these agents who are really good in a defined mission (like code completion).
It's not even about LLMs IMHO. It's about letting a computer crunch many numbers and find a pattern in the results, in a quasi religious manner.
Yes, same for maths. As long as a true reward 'surface' can be optimized. Approximate rewards are similar to approximate and non admissible heuristics,search eventually misses true optimal states and favors wrong ones, with side effects in very large state spaces.
Indeed, systems like AlphaProof / AlphaGeometry are already able to win a silver medal at the IMO, and the former relies on Lean for theorem verification [1]. On the open source side, I really like the ideas in LeanDojo [2], which use a form of RAG to assist the LLM with premise selection.
[1] https://deepmind.google/discover/blog/ai-solves-imo-problems...
[2] https://leandojo.org/
Unless if it takes maximizing code coverage as the objective and starts deleting failed test cases.
This is interesting, but doesn't it still need supervision? Why wouldn't it generate tests for properties you don't want? It seems to me that it might be able to "fill in gaps" by generalizing from "typical software", like, if you wrote a container class, it might guess that "empty" and "size" and "insert" are supposed to be related in a certain way, based on the fact that other peoples' container classes satisfy those properties. And if you look at the tests it makes up and go, "yeah, I want that property" or not, then you can steer what it's doing, or it can at least force you to think about more cases. But there would still be supervision.
Ah -- here's an unsupervised thing: Performance. Maybe it can guide a sequence of program transformations in a profile-guided feedback loop. Then you could really train the thing to make fast code. You'd pass "-O99" to gcc, and it'd spin up a GPU cluster on AWS.
Models aren't going to get really good at theorem proving until we build models that are transitive and handle isomorphisms more elegantly. Right now models can't recall factual relationships well in reverse order in many cases, and often fail to answer questions that they can answer easily in English when prompted to respond with the fact in another language.