Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

We have proof automation now

imperialviolet.org

Post reply on HN
Print view View original

61–70 of 117 posts

Re: We have proof automation now

#61

Post by hobofan »

thomasahle wrote: post #59
hobofan wrote: post #55

Earlier quoted context omitted.

> I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time. I don't know. It seems to match the general futility of pedantry that exists in all professions. Yes, you can try to optimize for absolute 0 flaws in your code, but in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit s…

> in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit silly beyond a certain point CPUs are tested so so much more thoroughly than any software today. Including using formal proofs. If the chance of a CPU bug is something like 1/10^6 and each module in your software is 1/10, reducing that to 1/100 makes a bog difference.

> software is 1/10, reducing that to 1/100 makes a bog difference

I fully agree! I'm all for moving the needle towards moving the needle towards more formal verification, but what GP is suggesting is full verification of programs, which is more akin to trying to achieve a 1/10^6 bug rate.

Re: We have proof automation now

#62

Post by colechristensen »

I think people are overestimating the usefulness LLMs will bring us based on early examples of low hanging fruit being harvested.

LLMs have a VERY different set of things which are easy and which are hard and from software security to math proofs we're seeing very early impressive results but those will run out and new classes of what is difficult will show themselves.

The "this new tech will cause everything to be easy from now on!" feeling has happened many times before and always new limitations were found.

Industrialization was thought to be basically the end of the need for money or significant labor during the industrial revolution (this optimism is where communism came from) and that future never came.

The same will be here: rapid change but also new limitations which are still hard to imagine.

Re: We have proof automation now

#63

Post by let_rec »

momentoftop wrote: post #35

Theorem provers have always made extensive use of AI and automation. Formal logic is insanely laborious, and it took Russell a monumental effort to not get very far with his manual verifications in Principia Mathematica, working out all the details by hand. In 1956, Newell came up with the Logic Theorist which was able to prove a decent chunk of the Principia automatically. When Newell informed him, Russell conceded…

To someone completely outside the field: why is creating a formal verification of an existing proof so hard?

1. Convert the natural language proof steps into formal language

2. Pass it to the solver to verify the steps

Genuinely curious!

Re: We have proof automation now

#64

Post by singularity2001 »

trenchgun wrote: post #48
Buttons840 wrote: post #19

Earlier quoted context omitted.

Lean has dependant types. Wouldn't something like Haskell or Idris, that are trying to be general purpose dependantly typed languages--wouldn't they be a better start than versus? Versus appears to just be a formal verification tool. Perhaps I misunderstand? You want the formal verification built into the language because the tooling can start to get really crazy good. Agda is the dependantly typed language I've used…

Lean4 is a general purpose programming language.

Have you tried writing any programs in it?

Re: We have proof automation now

#65

Post by anilgulecha »

logicchains wrote: post #46
anilgulecha wrote: post #40

I'm convinced Math is the canary for what's going to happen to knowledge work. Coding was ahead in harnessing early LLM capability, but Math, given it's pure form, has aleady racing ahead. The dimensions to notice are: Research speedup, practitioner expertize, labour dynamics, junior entrants, world impact. In that sense it's a canary, whatever happens to Math, will in order flow to other sciences in-order of purity:…

Math is the opposite of a canary because it's possible to generate infinite amounts of synthetic training data for it, unlike almost every other kind of knowledge work where correctness depends on external input.

That's why it's a canary - because it has minimal external input, and most pure.

External inputs are bound get LLM friendlier with time, in the order I mentioned above.

Re: We have proof automation now

#66

Post by andai »

I had a funny experience recently, during a vibe coding bender. This was a few weeks ago when these very impressive new models came out, a whole new class of intelligence and autonomy! So I wanted to see how far I would get, letting the computer handle all the details.

Eventually I did take a look at all the new code, and found that one of the main features had been implemented completely backwards, in a way that was pointless and completely defeated the purpose.

(An LLM also pointed that out, so I guess it must have been a different one which implemented it? I'm trying to get them to sign their names in the commits...)

These new models are very thorough and responsible however, so of course it had written a copious number of tests, and of course all the tests passed! I found this very amusing. It had diligently proven the correctness of the incorrect functionality!*

I've been thinking about how cool it is the AI can assist with writing proofs now, and how we can use this new ability to boost the correctness of our code. It later occurred to me, however, that formal verification would not have helped in this case. It would have just formally verified that the wrong thing was correct!

--

*Yeah I know tests prove the presence of bugs but not their absence. Couldn't think of a better way to phrase that though.

Re: We have proof automation now

#67

Post by hajile »

m1el wrote: post #27

Self-insert time. I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost. We've seen how Mythos has found more vul…

You formally verify that your incorrect solution executes without a hitch, but you might just be formally verifying that any user can hit your API and download all your plaintext passwords.

Lots of security bugs are caused by incorrect specs from misunderstanding the problem and a formal verifier can’t fix these. Humans can’t think through every situation either (or the bugs wouldn’t exist) SMS that’s doubly true because NOBODY understands all the interactions of the system as a whole and how changes in the part they understand affect everything else.

I’m not saying formal verification is bad, but it’s not a panacea and I’d wager would only fix a small percentage of existing bugs.

Re: We have proof automation now

#68

Post by david-gpu »

andai wrote: post #66

I had a funny experience recently, during a vibe coding bender. This was a few weeks ago when these very impressive new models came out, a whole new class of intelligence and autonomy! So I wanted to see how far I would get, letting the computer handle all the details. Eventually I did take a look at all the new code, and found that one of the main features had been implemented completely backwards, in a way that was…

I had a college professor do the exact same thing in class: he made a fairly subtle mistake formalizing his specification, and thus his proof was perfect but did not solve the actual problem he was trying to address.

He was a mathematician and was convinced that formal methods were the future of software engineering. He also loved handwaving that due to Godel's incompleteness theorem, humans were necessary to introduce creative insights (new axioms) that computers would never be able to do.

I eventually obtained top marks both semesters and left convinced that formal methods are a waste of time in >99% of the cases.

Re: We have proof automation now

#69

Post by eru »

The article says that their zstd decoder is 10x slower than the 'normal' one. I would be interested in seeing if that can be driven down to (almost) parity, with a bit more LLM time and perhaps human effort.

Re: We have proof automation now

#70

Post by pjmlp »

> Aside: verified assembly

This isn't new, it is actually part of how Dafny came to be, another formal verification programming language.

"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System"

https://www.microsoft.com/en-us/research/publication/safe-to...

However so far hardly anyone in mainstram cared about verified assembly, maybe now with LLMs.

"Programming Language Design and Implementation in the Era of Machine Learning"

https://www.youtube.com/watch?v=Fc3cW0nqAQ0

Post reply on HN