CORRECTION: March 13, 2024 Around the same time as Czerwiński and Orlikowski's 2021 paper that raised the lower bound to Leroux and Schmitz’s Ackermann upper bound, Leroux obtained an equivalent result, working independently. Both papers proved the same lower bound and the teams coordinated to publish the papers at the same time. Links to their work can be found here: The Reachability Problem for Petri Nets is Not Primitive Recursive, Leroux ieeexplore.ieee.org/document/9719763 Reachability in Vector Addition Systems is Ackermann-complete, Czerwiński and Orlikowski ieeexplore.ieee.org/document/9719806 Read the full article for links to papers: www.quantamagazine.org/an-easy-sounding-problem-yields-numbers-too-big-for-our-universe-20231204/

@raheelrehmatbc

2 ай бұрын

Nn m mm mmmmmk m m

Note: Ackermann function is often presented as A(m, n), i.e. it has two parameters. What's presented in the video is the "diagonalized" single-param version. Actually, there are "many" Ackermann functions, and the original had three arguments: A(m, n, p) = the "p-th" hyperoperation on m and n. A(2,3,0) = 2 + 3. A(2, 3, 2) = 2^3, etc. The single param version in the video seems to use m = n = p.

@PluetoeInc.

2 ай бұрын

they avoided "generalization" , which is a chargeable offence in mathematics community . In the math world there would people lined up to sue them .

@ouchywouchys345

Ай бұрын

Can n go beyond 4? what would it be if n = 5 so A(2, 3, 5) ?

The video glosses over just how difficult Lipton found the problem to be in 1976. His paper 4:40 showed that the VAS reachability problem requires exponential space. This already means that any perfect algorithm for it will be highly impractical. For people interested in solving other problems -like problems in program verification- it means that reducing their problems to VAS reachability is not all that useful. We knew it was at least bad; now we know it’s worse than bad.

It blows my mind that there are people out there that are intelligent enough to come up with such wonderful abstractions to describe and help solve real physical problems. I would've never been able to see the connection between vector addition and determining the end state of an algorithm. This is blowing my mind because of how much sense it makes.

@Scriabinfan593

2 ай бұрын

@@acmhfmggru Being able to determine when critical systems will have an unforeseen error, by calculating the reachability to a state of error from any given state. Imagine if your car’s braking system is about to have an error and your car is able to determine that and warn you and help you take actions that will minimize victims or something.

@Scriabinfan593

2 ай бұрын

@@acmhfmggru Who would’ve ever guessed that a problem about algorithms is a digital algorithmic problem? Thanks for the groundbreaking info lol. I said it can help solve real physical problems because these problems are easily applicable to the real world, and they aren’t just conceptual problems. Perhaps that wasn’t the right wording but I thought it got my point across.

@Scriabinfan593

2 ай бұрын

@@acmhfmggru ok

@grdfhrghrggrtwqqu

2 ай бұрын

Vectors are in literally everything at one point or another. Same deal with algebra, and arithmetic, criticality states, etc. It's not a profoundness of insight, but how one measures it.

@sprinklehomie5811

2 ай бұрын

@@acmhfmggru these problems often address physical ones through the technology that they employ... whatever form that may be. if you're caught up between real-world bodies that are understood from our conception of physics, then you're looking at this problem at a smaller scope than you realize.

Gonna be honest, I disagree with the premise. It sounds extremely unbelievably hard to solve. I mean, maybe I'm biased as a programmer, but I don't know how you could look at this area and think its going to be easy.

@tvinforest5255

2 ай бұрын

I thought they meant "easy to formulate" problem. Many questions are hard to understand to begin with.

@rcnhsuailsnyfiue2

2 ай бұрын

The premise relates to how “easy” it is for a computer to be mathematically certain of a program’s output. But knowing (and proving!) this, with mathematical certainty, is incredibly hard! 😊

@zoobie2000

2 ай бұрын

You must be fun at parties

@meh5647

2 ай бұрын

Formal methods of verification are essential to the field of software engineering and algorithms. Not sure what you're getting at here.

@Kurushimi1729

2 ай бұрын

​@@meh5647 He's right though. This problem sounds really challenging

Formal proofs do help with implementation bugs, but the real big bugs are specification and requirement bugs. If you apply formal proof to those, you just end up with a proof that the program implement the broken requirements, without telling you that they are broken.

@debasishraychawdhuri

2 ай бұрын

The thing is, requirement bugs are caught when working on the formal specification.

@jonwatte4293

2 ай бұрын

@@debasishraychawdhuri Only contradictory requirements are caught that way. (Which, yes, that's nice!) But there are tons of specifications that are just not describing a good solution, or might even have gotten the problem wrong.

@maxbaugh9372

2 ай бұрын

"Well sir we have good news and bad news. The good news: the program does exactly what you wanted. The bad news: you wanted the wrong thing"

@Sonny_McMacsson

2 ай бұрын

@@maxbaugh9372The genie bug.

@shilangyu

2 ай бұрын

I don't think there is any way around this fundamental issue. If you incorrectly express what you want, you get the wrong thing. That said, it's still much better than relying on an implementation which is usually much more complex than a specification.

It's not just a CS issue. If you can't ask a perfect question, you won't get the answer you might expect. That's why disciplined CS design revolves around requirements. The old project management saying of "garbage in = garbage out" applies.

@eddyr1041

2 ай бұрын

Which do you prefer... iterative dev or popularly named as agile (I like it with formal spec) or gigolo prevention with strict discipline?

quanta magazine is the most underrated channel imo

@cf7571

2 ай бұрын

"underrated" doesn't mean what you think it means. It is very highly rated, and correctly so. Maybe you mean that it is known as it should be?

@stuartspence9921

2 ай бұрын

Nearly 1M subscribers is not too shabby.

@MIKAEL212345

2 ай бұрын

The reason it is so good is that it is funded by the Simons foundation, which is funded by Jim Simons. This is the mathematician that founded Renaissance Technologies, the hedge fund that was wildly successful and that only hired people really good at math, e.g. math phds, physics phds, etc. Basically, quanta magazine is not beholden to corporate profitability demands, so they can just focus on quality content.

FORMAL VERIFICATION MENTIONED 🔥🔥🔥 🗣️💯🗣️ 💯

Note also that if we want to detect bugs in general, it is way harder in the Turing Machine model, as it is at least as hard as the halting problem, if not harder.

Best channel other than scishow for showing new developments in interesting ways

1:03 The guy sounds like Stephen Hawking’s chair.

@gosnooky

2 ай бұрын

So it wasn't just me

Amazing video

3:25 For a Fibonacci iterator, the rule would be [x, y]->[y, x+y], and the (typical) initial state is [0,1]. This basically means that a Fib function is a program with 2 parameters, which can be efficiently predicted using Binet's Formula (for Complex numbers) or the Matrix form (for Integers)

Thank you so much for producing this content! It's amazing to see our species pushing at the boundaries of what we know.

We had to learn some kind of verification like this in college called Hoare logic. I don't think I ever got how it really works

5:57 As you said earlier in the video, there was at least one long-known algorithm with a higher complexity than the lower bound, so it seems false that discovering the elevated lower bound "confirmed that the problem was far more complex than anyone had imagined." I'm not familiar with vector addition systems, but I suspect Czerwiński's "surprise" was not because he thought the old lower bound was precise, but simply because it's not every day that he makes such fruitful progress on a longstanding question.

Verifying and solving algorithms are difficult problems, but if you can prove P=NP, then you can polynomially reduce the universe of arbitrary problems into the NP-complete Boolean satisfiability problem.

Astronomical amount of choices, which programming allows to make, is one of the reasons why I like it. Regular people may think that there is single possible solution for some programming problem, but in fact there are way more options available.

There's a guy called Ross Ashby, he wrote the law of requisite variety. You've probably read it.

I wish the video had just said ACKERMAN right from the beginning. When I took Computer Science, we studied the Ackerman function when we studied recursion.

Note that if we use Turing Machines as the model of programs, rather than the vector addition system, it gets even harder, and is at least as hard as the halting problem for the reachability problem for Turing Machines.

First thought this is about p=np

I remember when a VP put out a call for someone to write a program to do root cause analysis: find why a program failed. I didn’t know about reachability at the time, but I replied, with a very polite answer, saying what he was asking for, was either impossible or incredibly difficult.

From the introduction I thought it was undecidable. Sounds very exciting

Isn't that like the Halting Problem? The video basically reconfirms that it's phsycially impossible. I don't see how you can represent machine's state in a vector grid when the state isn't even a measurable number.

@cassandrasinclair8722

2 ай бұрын

A state transition system is different to a full on turing machine. The state machine is finite and bounded, the halting problem assumes a turing machine which has an infinite tape.

@Amonimus

2 ай бұрын

@@cassandrasinclair8722 If the video said "state transition system" from the start, then that's an understandable. But it starts discussing arbitrary software program, then uses an "abstract machine with states" as if it's an analogy.

@desmond-hawkins

2 ай бұрын

You don't need to solve the Halting Problem to determine whether there's a set of state transitions (computations) that get you to an undesirable state. The state _can_ be represented as a vector, in the broadest sense the entire set of bytes used by the program is a very large vector with each value in the vector being the value of a specific byte at a unique offset. If you change one byte, you changed one value in the vector and therefore moved to a different point in that space. Obviously you can't use this large a vector, but think about the different values that you want to verify and just collect them in a vector, and that's your state. Any computation mutates that state, and the question here is whether you can reach states that lead to crashes or undesirable outcomes as you hop from vector to vector by performing computations.

@meh5647

2 ай бұрын

The halting problem is an issue of computability, not complexity.

@nukeeverything1802

2 ай бұрын

The configuration of a Turing machine has a finite description, even tho the tape is infinite. In CS literature its often defined as a triple (k, q, n) where k is the string on the tape (sometimes encoded as a number), q is the current state of the TM's atomaton, and n is the position of the head. You may think that k would be an infinitely long string, but remember that in any configuration the TM head has only moved a finite number of times. You only need to keep track of where it has been, and every other cell that it hasnt visited is the blank symbol. If the TM starts with input on the tape, this input is finite as well - it can be arbitrarily long but it is finite. (If you give the TM an infinite input, it is possible for the resulting machine to compute uncomputable functions. TM + infinite inputs has more power than regular TMs)

What does reachability in a vector space have to do with reachability of a line of code?

An excellent video, but I take issue when science communicators say things like "turned out to be more complex than anyone had imagined". People are pretty good at imagining things. Theoretical mathmeticians and computer scientists are _really_ good at imagining things, it being part of their job.

Increase abstraction, minimize function scope, and always throw errors on specific algorithms 😊

Incredibly interesting!

And, of course, computers do not follow the laws of arithmetic as they finite state machines and cannot represent all integers. Also, in floating point sums may depend on the order of operations violating associativity. Then there are hardware bugs and glitiches and the occasional high energy particle that causes an error

Haven't watched it yet but you should be able to branch through every possible state using negation operators to redefine conditions to a new output state for each possible error/condition.

@MrVontar

2 ай бұрын

If set of conditions then there exists a subset for the set such that each condition may be recalculated such that there exists a new subset related to the initial set. Then for each set to subset relation then we may categorically restrict each state rather than calculating each state such that if it does not meet the categorical state restrictions then there exists a calculation that will result in a successful runtime

@SwistakMiecio

Ай бұрын

The catch is that it might that take a very long time to find the correct path. There are instances where the shortest path to the solution is absurdly long. It is also not clear when you should stop your computation and say "I'm sure the target is not reachable" - doing that is a topic for 3 heavy lectures

it is amazing how clunky our compute is so far. we are still in the dark ages of compute. but the advancement we will see from now on will be astounding.

Unit testing. Each node is tested for all possible tests. Inputs take any input without blowing up. Number is expected and alpha is provided should re-ask. Etc. I was in a new group that went through 1,000,000 lines of code. It wasn't easy but was developed and improved quality. Languages pop stacks and if it jumps to an non-resolved address it jumps to garbage binary code and runs a junk program. Code has to be written with proper codes. All cases covered.

"Verification" is a bit of a backwater for academic computer scientists, most of whom are inept or terrible programmers - which is an open secret in the world of IT, where accomplished programmers code "mission-critical" apps/programs via a rigorous peer-review process that is impossible in academia. It comes into play though, in commercial apps such as "windows" which are released to the public with countless THOUSANDS of bugs - relying on customers to self-report.... In 5 decades in IT and, after coding millions of LOC myself, in teams, and solo, I can't remember a single instance of a "computer scientist" who was an accomplished programmer.

Nice video. Consider going into more depth.

So it's easier than the halting problem at least...

I don't understand how this video can discuss algorithm analysis at such depth without once mentioning the Turing Halting problem, if only to define how that issue differs -- assuming it does.

Looks to me like the reachability problem in the case of vector addition systems boils down to whether the target is a lattice point in the lattice defined by the transitions. And figuring out if a point is in a lattice is linear. So I'm missing something, I guess

@EmceeJoseph

2 ай бұрын

Lattice would be with only as many transitions as the dimensionality iinw but there can be many more transitions

@fastandfemme

2 ай бұрын

It appears a key difference is that a VAS doesn't allow the subtraction of transition vectors. Under this restriction, reachability is equivalent to subset sum when the transition vectors are one-dimensional, and thus NP-Hard.

@EmceeJoseph

2 ай бұрын

@@fastandfemme aha!

subtitles are wrong, vector addition systems is written as "vector edition system"

Ummm, how is this "simple"? It's literally EXACTLY as "difficult" as writing the original program to check whether that program has no logical flaws... if you can do one you can do the other... and who's going to check that program ALSO had no bugs. Algorithms regardless of provability REQUIRE implementation and then possibly an IMPERFECT translation into machine code... which will then be run on an IMPERFECT computer with IMPERFECT inputs storing its state in IMPERFECT memory. The laws of physics and information theory firmly state that this is a fools errand (see signal encoding in a noisy channel for classical constraints with Johnson and Shot noise setting your fundamental limits while quantum processes like tunneling and the no cloning theorem bound you from attacking it on semi classical or quantum architecture). We live in an IMPERFECT world. Programming and IMPERFECT encoding by human linguistic schemes is just another facet of the same problem.

@DemPilafian

2 ай бұрын

You can solve this problem with hashing. You hash your original program and compare its hash to the verification program's hash. If the hashes don't match you create the next verification program and check its hash against all previous hashes. Continue until you get a match. Store the hashes in a bucket that can handle the heat death of the universe.

@robmorgan1214

2 ай бұрын

@DemPilafian nice. Now we just need to figure out how to create 10^100 more protons without accidentally collapsing the universe into a black hole... don't worry, I'm pretty good at this kind of thing! It sounds like you got the bucket idea under control, so you take point on that part.

Optical illusion at 3:20 , try to spot the black vertex

@NathanY0ung

2 ай бұрын

It's everywhere and nowhere at the same time.

The most reliable code we can ever have is the one that develops itself from scratch, evolving into being as error free as possible.

"It is a very important milestone." Really? An algorithm that is merely exponential is unfeasible enough, and this problem was known to be much worse than exponential a long time ago. Any actual reliability determination has always had and will always have nothing to do with this theory

@SwistakMiecio

Ай бұрын

It is a very important _theoretical_ milestone. I admit it was known to be out of reach for real world applications, but that doesn't change the fact that it remained a fundamental theoretical question

How is complexity measured? I thought it was still a big open question in science?

Constraint the input to a fixed formulation.

So, does this also solve the Halting problem?

@Sebastian-_

2 ай бұрын

halting problem is proven to be unsolvable bruh at least on infinite memory computers

@sharmakefarah2064

2 ай бұрын

No, in the sense that if you have an oracle for the Vector Addition System problem, you don't get to solve the halting problem.

If error correction would be based on principles of self regulation and self ordering, than the question of reachability would lose its importance.

While I have never been involved in critical systems where lives are on the line (medical, military, space, energy, aviation, etc.), it is my experience that any "best practices" efforts to make software "perfect" ends up making it have more bugs and be less readable/maintainable. It's partly from the affect of non-technical people thinking they can "help" by enforcing draconian practices on competent people, and partly because there's a tendency to stop acting in good faith when your job is more about following protocols than thinking.

@rcnhsuailsnyfiue2

2 ай бұрын

The concepts in this video transcend any human opinions of best practices; Formal Verification is used at much lower levels of computation. It affects things like hardware circuitry, cryptography, and compiler design, which need to be mathematically-proven as accurate.

6:16 With my knowledge of the Halting Problen and Busy Beavers, I thought the Ackerman function was tiny, lol. Is this "Reachability Analysis" only concerned with programs whose Halting Problem is solvable? Because it's simply impossible to perform this analysis on arbitrary programs

Sure, but algorithmic correctness doesn't necessarily equate to program correctness. Errors can creep into implementation of correct algorithms. Moreover, compilers create machine code from source code. Different compilers create different machine code including applying different types of optimizations. Another concern is algorithm implementation in given program languages. One can violate program language rules, which results in programs that have undefined behavior.😢

@meh5647

2 ай бұрын

It's simple to verify that an algorithm is implemented correctly. The hard part is verifying that the algorithm does what is intended./

@bentationfunkiloglio

2 ай бұрын

@@meh5647 Perhaps if it's a simple algorithm. Otherwise, that's not true at all. Search for "crypto implementation attacks" if you want more info.

Reachability = Whether Jack Reacher can do something... or not Q.E.D

1:07 did this guy do the voice for Steven Hawking?

That's why we have ops and SRE 😂

A(4) = 4^4^4^4 ≈ 10^(8.07×10)^153 ...which is a 1 with 807,000 trillion trillion trillion trillion googol zeros after it. One trillion seconds is about 31,700 years.

Good video but felt shrt of content. 😅 Would appreciate to let us know more about it all.

W koncu jakies dobre wiesci z Polski!

Now sprinkle some AI and quantum computers on this problem.

based

After casual watching for computer engineers or software programmers like me who do not pay attention, it may "sound" like we are talking about an NP hard problem which reachability is NOT. Hope the video had made this clear when it said that the problem is hard. It's of Polynomial complexity. But as the internet nodes and networks become vast and mammoth in size the same polynomial complexity becomes exponential to the Ackerman size. Computationally that is a hard context to be in. Another thing the video missed is talking about the way to conquer this computational size. Is it still parallelism?

This video is misleading. We don't need to analyze worst-case programs. We need to analyze the programs that people actually write.

And why should that be odd that you cannot answer a complex question 100% correct ? Language is a subjective field. Objective reality cannot be represented by words that may have subjective meaning attached to them. All words have subjective meaning to them, thats why there is no such thing as a perfect program.

8:33

Annoying how it doesn't tell us what the lower or upper bounds were or anything about the algorithms.

Somehow, the fact that the Mathematician is using a chalkboard, warms my heart.

@100c0c

2 ай бұрын

Most of them still do I believe

@cf7571

2 ай бұрын

@@100c0c am mathematician, can confirm we basically only use blackboards. anything else is inferior

*_"Essentially solved."_* ...maybe for simplistic tic-tac-toe games and even then only if you ignore I/O and integration issues. The academic research is good to do, but let's be sensible in our descriptions of the real world.

I forgot the definition of basic

@timjohnson979

Ай бұрын

The programming language? Beginners All-purpose Symbolic Instruction Code.

This video is so misleading that I would say it spreads disinformation. I have greatly enjoyed similar videos from other fields, feeling I learn something. Now this is in my own field, and it is so blatantly wrong that I need to re-evaluate Quanta seriously. How could they put this up? The reachability problem of computer programs has been know to be undecidable for almost a century. Some three minutes into the video it is suddenly instead about vector addition systems. These have nothing to do with real-world programs. The connection with reachability in real programs is simply false. This is not to take away from the mathematical result which is beautiful in its own right.

Wait, why is ack(4) not infinity ?

From my point of view, there is no such thing as an irrefutable mathematical proof. If you wait long enough, some new information comes along, that can throw any mathematical proof into a tailspin.

Just don't divide by 0 and you're good.

p vs. np solution I hope. but that would lead to artificial superintelligence

@ccgarciab

2 ай бұрын

It's not like that

@teeesen

2 ай бұрын

If P=NP, this VAS reachability problem is still hard.

Congratulations! The video is even more useless than the paper it reports on. The paper is mathematics for the sake of mathematics. No useful result will ever come from this even though it is supposed to help in "solving" the reachability problem. The video is just a clickbaity bad explanation of a useless scientific paper.

@timjohnson979

Ай бұрын

This has been a holy grail of programming or computer science, if you will, since I started in the field as a software engineer in the early 70s. And the search goes on...

Raheelrehmat Pakistani

👎And here is the problem of this "research": Neither is this relevant for any task in real life of a e.g. Java developer or for the P-NP problem. Not for operations research nor for any field in economy, engineering or physics. In real life things must boil down to a JUnit test. Nobody needs a mathematician with strange symbols. - Write test cases. - Write a damn for loop if required. - Cover all lines and branches in the code. - Write clean code.

This result is completely practically useless. Not that it doesn't matter, but it is disingenuous to present it like it has something to do with actually making real world software more reliable.

I have a novel idea. How about we outsource all of our programming knowledge to a third world country like India? Because they'll be no consequences there right? Boeing?

super duuuuuuuuuuumb

duuuuuuuuuuuuuuuuuuuumb

Interesting how you gave examples of possible catastrophic consequences of software errors citing money loss for banks and massive loss of human life on the same level.

@flytape8490

2 ай бұрын

eyeroll

lol running out of content?