= 27d567bc2d48d9f40e9ccc20ea370b15)
loup-vaillant comments on Progress on automated mathematical theorem proving? - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (65)
The Prover company is working on the safety of train signalling software. Basically, they seek to prove that a given program is "safe" along a number of formal criteria. It involves the translation of the program in some (boolean based) standard form, which is then analysed.
The formal criteria are chosen manually, but the proofs are found completely automatically.
Despite the sizeable length of the proofs, combinatorial explosion is generally avoided, because programs written by humans (and therefore their standard form translation) tend to have shapes that lend them amenable to massive cuts in the search tree.
It doesn't always work: first, the criteria are simple and bounded. Second, combinatorial explosion sometimes does occur, in which case human-devised tweaks are needed.
Oh, and it's all proprietary. Maybe there's some related academic papers, though.
I don't think this is what Jonah is talking about. This is just one of thousands of examples of formal verification of safety-critical software.
The key part is that some of those formal verification processes involve automated proof generation. This is exactly what Jonah is talking about:
Those who make (semi-)automated proof for a living have a vested interest in making such things as useful as possible. Among other things, this means as automated as possible, and as general as possible. They're not there yet, but they're definitely working on it.