I suspect that simply by convoluting your code (even while keeping semantics the same!), you can break any so-called stochastic autoformalizer

Let’s say your stochastic natural language autoformalizer works 99% of the time for range of tests.

What might this mean practically? How long in a real project before autoformalization fails, and what does the “manual fix” process look like from there?

Some people are saying it can be done with the combination of an LLM and a formal proof assistant… but to me it seems like the LLM is still the failure point

I saw a paper about improving stochastic autoformalization, but that doesn’t seem to actually solve anything. It will be wrong at some point.

Natural language programming is impossible, right? It’s an oxymoron, like “natural language mathematics”. Natural language doesn’t offer syntactic-semantic guarantees like formal language.

Maybe I’m too ignorant, but I’ve never seen a real counter-argument

!!! I’m so hyped. Having an implementation for these three properties, especially compensation (as it helps define subtraction), is a huge step

Not to keep harping on LLMs, but solving math tests/olympiads is another laughable benchmark.

For as long as LLMs exist, it will be trivial to construct a math problem that you can reliably solve which an LLM cannot. This should be obvious! Trying to do math on tokens is not even a fool’s errand

An LLM will never be an autonomous coding agent for the same reason you can’t solve the halting problem.

I really think it’s that simple. Do people really believe a computer program can analyze the result of another, arbitrary, computer program?

Best of all it’s promoted by self-righteous oligarchs who insist the tech is magic and call YOU ignorant if you argue otherwise.

If you point out something genAI can’t do, you get “but it will in the future”

Meanwhile they know nothing about the relationship between syntax and semantics

GenAI may actually be the worst digital technology ever conceived, possibly even beating the computer virus.

First of all, its primary and most effective use case is deception. SEO spam, phishing, generated video , etc.

When it does solve a real problem, it’s one solved many times before

It’s isomorphism alley

Things are getting really difficult. It turns out that subtraction is an extremely difficult operator to define correctly, even moreso than division.
You have to right shift diagonally-aligned things and it depends on the dimensionality
(and you need to recompensate after a right shift too)

The core flaw of LLMs for coding is that you cannot (!!!) predict the outcome of an algorithm by analyzing its tokens. You have to actually run the algorithm.
However, the scope of algorithms that LLMs can actually run is TINY. It’s nowhere near the capability of a human or even a compiler

At some point I will post a whole bunch about a mostly novel type system i'm working on centred around ADTs