= 27d567bc2d48d9f40e9ccc20ea370b15)
John_Maxwell_IV comments on AALWA: Ask any LessWronger anything - 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 (611)
I'm a Research Associate at MIRI. I became a supporter in late 2005, then contributed to research and publication in various ways. Please, AMA.
Opinions I express here and elsewhere are mine alone, not MIRI's.
To be clear, as an Associate, I am an outsider to the MIRI team (who collaborates with them in various ways).
I've talked to a former grad student (fiddlemath, AKA Matt Elder) who worked on formal verification, and he said current methods are not anywhere near up to the task of formally verifying an FAI. Does MIRI have a formal verification research program? Do they have any plans to build programming processes like this or this?
I don't know anything about MIRI research strategy than is publicly available, but if you look at what they are working on, it is all in the direction of formal verification.
After speaking to experts in formal verification of chips and of other systems, and they have confirmed what you learned from fiddlemath. Formal verification is limited in its capabilities: Often, you can only verify some very low-level or very specific assertions. And you have to be able to specify the assertion that you are verifying.
So, it seems that they are taking on a very difficult challenge.