3 ms·
First, who is saying "termination implies safety"? There need to be a citations for that, so we can know what specific claim is supposedly being refuted here.
by WCSTombs 8mo ago
First, who is saying "termination implies safety"? There need to be a citations for that, so we can know what specific claim is supposedly being refuted here.
Second, Rice's theorem states that no nontrivial property on the set of partial recursive functions is decidable. However, there are subsets of the set of all recursive functions that do have decidable properties, and it's pretty trivial to cook some of them up. Since some of these sub-languages also consist only of total functions, there are "total languages" for which the analogous statement of Rice's theorem is false. To fix this we would need to choose a specific total language. There could be some interesting ones for which the analogous statement of Rice's theorem still holds, but I'm not an expert on that.
- user1138 8mo agoWhile I do have a formal citations there is this https://venturebeat.com/ai/lean4-how-the-theorem-prover-works-and-why-its-the-new-competitive-edge-in https://venturebeat.com/ai/lean4-how-the-theorem-prover-work...
- WCSTombs 8mo agoNot only is this just a random article from the internet, as opposed to something peer-reviewed, but more importantly, nowhere does it even attempt to claim that the mere fact of a program terminating implies its suitability in a safety context.
- user1138 8mo agoHere's your citation — ARIA's Safeguarded AI program, £59M in UK government funding, explicitly claiming mathematical safety guarantees through restricted verifiable models — total languages by another name. The claim exists. It has a budget. Now, do you have a substantive response to the proof, or are we done here?" @techreport{ARIA2024, author = {{Advanced Research and Invention Agency}}, title = {Safeguarded AI: Constructing Guaranteed Safety}, institution = {ARIA}, year = {2024}, url = {https://www.aria.org.uk/programs/safeguarded-ai/ https://www.aria.org.uk/programs/safeguarded-ai/}, abstract = {Outlines a 'Safeguarded AI' program that seeks to build AI systems with 'mathematical guarantees.' It argues that by using restricted, verifiable models—effectively total languages—one can avoid the 'impossible' task of verifying general AI and instead produce 'quantitative safety guarantees.'} }
- user1138 8mo agoYou're correct on the citations though that will probably be very easy as we have many people claiming exactly that. As to your second point, yes, and the safety claims being made are not restricted to those decidable subsets. The moment you claim general safety guarantees for systems operating beyond those constrained subsets you're back in full Rice territory. If you can name a total language with an early termination guarantee, I'm all ears. You asked for my citations, now show me yours.