No Cover Image

Conference Paper/Proceeding/Abstract 806 views 86 downloads

A Computability Perspective on (Verified) Machine Learning

Tonicha Crook, Jay Paul Morgan Orcid Logo, Arno Pauly Orcid Logo, Markus Roggenbach Orcid Logo

Recent Trends in Algebraic Development Techniques, Volume: 13710, Pages: 63 - 80

Swansea University Authors: Tonicha Crook, Jay Paul Morgan Orcid Logo, Arno Pauly Orcid Logo, Markus Roggenbach Orcid Logo

Abstract

In Computer Science there is a strong consensus that it is highly desirable to combine the versatility of Machine Learning (ML) with the assurances formal verification can provide. However, it is unclearwhat such ‘verified ML’ should look like.This paper is the first to formalise the concepts of cla...

Full description

Published in: Recent Trends in Algebraic Development Techniques
ISBN: 9783031433443 9783031433450
ISSN: 0302-9743 1611-3349
Published: Cham Springer Nature Switzerland 2023
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa63849
first_indexed 2023-07-10T13:13:11Z
last_indexed 2024-11-25T14:12:58Z
id cronfa63849
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2024-11-06T15:54:56.3544249</datestamp><bib-version>v2</bib-version><id>63849</id><entry>2023-07-10</entry><title>A Computability Perspective on (Verified) Machine Learning</title><swanseaauthors><author><sid>f392e8826eef757ada89c294fbeeb2c2</sid><firstname>Tonicha</firstname><surname>Crook</surname><name>Tonicha Crook</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>df9a27bcf77b4769c2ebbb702b587491</sid><ORCID>0000-0003-3719-362X</ORCID><firstname>Jay Paul</firstname><surname>Morgan</surname><name>Jay Paul Morgan</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>17a56a78ec04e7fc47b7fe18394d7245</sid><ORCID>0000-0002-0173-3295</ORCID><firstname>Arno</firstname><surname>Pauly</surname><name>Arno Pauly</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>7733869ae501442da6926fac77cd155b</sid><ORCID>0000-0002-3819-2787</ORCID><firstname>Markus</firstname><surname>Roggenbach</surname><name>Markus Roggenbach</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2023-07-10</date><deptcode>MACS</deptcode><abstract>In Computer Science there is a strong consensus that it is highly desirable to combine the versatility of Machine Learning (ML) with the assurances formal verification can provide. However, it is unclearwhat such &#x2018;verified ML&#x2019; should look like.This paper is the first to formalise the concepts of classifiers and learners in ML in terms of computable analysis. It provides results about which properties of classifiers and learners are computable. By doing this we establish a bridge between the continuous mathematics underpinning ML and the discrete setting of most of computer science.We define the computational tasks underlying the newly suggested verified ML in a model-agnostic way, i.e., they work for all machine learning approaches including, e.g., random forests, support vector machines, and Neural Networks. We show that they are in principle computable.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Recent Trends in Algebraic Development Techniques</journal><volume>13710</volume><journalNumber/><paginationStart>63</paginationStart><paginationEnd>80</paginationEnd><publisher>Springer Nature Switzerland</publisher><placeOfPublication>Cham</placeOfPublication><isbnPrint>9783031433443</isbnPrint><isbnElectronic>9783031433450</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords>Machine Learning, adversarial examples, formal verification, computable analysis</keywords><publishedDay>22</publishedDay><publishedMonth>10</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-10-22</publishedDate><doi>10.1007/978-3-031-43345-0_3</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2024-11-06T15:54:56.3544249</lastEdited><Created>2023-07-10T13:54:49.9621427</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Tonicha</firstname><surname>Crook</surname><order>1</order></author><author><firstname>Jay Paul</firstname><surname>Morgan</surname><orcid>0000-0003-3719-362X</orcid><order>2</order></author><author><firstname>Arno</firstname><surname>Pauly</surname><orcid>0000-0002-0173-3295</orcid><order>3</order></author><author><firstname>Markus</firstname><surname>Roggenbach</surname><orcid>0000-0002-3819-2787</orcid><order>4</order></author></authors><documents><document><filename>63849__28068__64c1495d365444c788e0879f0012ac35.pdf</filename><originalFilename>63849.pdf</originalFilename><uploaded>2023-07-10T14:13:11.3408250</uploaded><type>Output</type><contentLength>489436</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2024-10-22T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2024-11-06T15:54:56.3544249 v2 63849 2023-07-10 A Computability Perspective on (Verified) Machine Learning f392e8826eef757ada89c294fbeeb2c2 Tonicha Crook Tonicha Crook true false df9a27bcf77b4769c2ebbb702b587491 0000-0003-3719-362X Jay Paul Morgan Jay Paul Morgan true false 17a56a78ec04e7fc47b7fe18394d7245 0000-0002-0173-3295 Arno Pauly Arno Pauly true false 7733869ae501442da6926fac77cd155b 0000-0002-3819-2787 Markus Roggenbach Markus Roggenbach true false 2023-07-10 MACS In Computer Science there is a strong consensus that it is highly desirable to combine the versatility of Machine Learning (ML) with the assurances formal verification can provide. However, it is unclearwhat such ‘verified ML’ should look like.This paper is the first to formalise the concepts of classifiers and learners in ML in terms of computable analysis. It provides results about which properties of classifiers and learners are computable. By doing this we establish a bridge between the continuous mathematics underpinning ML and the discrete setting of most of computer science.We define the computational tasks underlying the newly suggested verified ML in a model-agnostic way, i.e., they work for all machine learning approaches including, e.g., random forests, support vector machines, and Neural Networks. We show that they are in principle computable. Conference Paper/Proceeding/Abstract Recent Trends in Algebraic Development Techniques 13710 63 80 Springer Nature Switzerland Cham 9783031433443 9783031433450 0302-9743 1611-3349 Machine Learning, adversarial examples, formal verification, computable analysis 22 10 2023 2023-10-22 10.1007/978-3-031-43345-0_3 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2024-11-06T15:54:56.3544249 2023-07-10T13:54:49.9621427 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Tonicha Crook 1 Jay Paul Morgan 0000-0003-3719-362X 2 Arno Pauly 0000-0002-0173-3295 3 Markus Roggenbach 0000-0002-3819-2787 4 63849__28068__64c1495d365444c788e0879f0012ac35.pdf 63849.pdf 2023-07-10T14:13:11.3408250 Output 489436 application/pdf Accepted Manuscript true 2024-10-22T00:00:00.0000000 true eng
title A Computability Perspective on (Verified) Machine Learning
spellingShingle A Computability Perspective on (Verified) Machine Learning
Tonicha Crook
Jay Paul Morgan
Arno Pauly
Markus Roggenbach
title_short A Computability Perspective on (Verified) Machine Learning
title_full A Computability Perspective on (Verified) Machine Learning
title_fullStr A Computability Perspective on (Verified) Machine Learning
title_full_unstemmed A Computability Perspective on (Verified) Machine Learning
title_sort A Computability Perspective on (Verified) Machine Learning
author_id_str_mv f392e8826eef757ada89c294fbeeb2c2
df9a27bcf77b4769c2ebbb702b587491
17a56a78ec04e7fc47b7fe18394d7245
7733869ae501442da6926fac77cd155b
author_id_fullname_str_mv f392e8826eef757ada89c294fbeeb2c2_***_Tonicha Crook
df9a27bcf77b4769c2ebbb702b587491_***_Jay Paul Morgan
17a56a78ec04e7fc47b7fe18394d7245_***_Arno Pauly
7733869ae501442da6926fac77cd155b_***_Markus Roggenbach
author Tonicha Crook
Jay Paul Morgan
Arno Pauly
Markus Roggenbach
author2 Tonicha Crook
Jay Paul Morgan
Arno Pauly
Markus Roggenbach
format Conference Paper/Proceeding/Abstract
container_title Recent Trends in Algebraic Development Techniques
container_volume 13710
container_start_page 63
publishDate 2023
institution Swansea University
isbn 9783031433443
9783031433450
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-031-43345-0_3
publisher Springer Nature Switzerland
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description In Computer Science there is a strong consensus that it is highly desirable to combine the versatility of Machine Learning (ML) with the assurances formal verification can provide. However, it is unclearwhat such ‘verified ML’ should look like.This paper is the first to formalise the concepts of classifiers and learners in ML in terms of computable analysis. It provides results about which properties of classifiers and learners are computable. By doing this we establish a bridge between the continuous mathematics underpinning ML and the discrete setting of most of computer science.We define the computational tasks underlying the newly suggested verified ML in a model-agnostic way, i.e., they work for all machine learning approaches including, e.g., random forests, support vector machines, and Neural Networks. We show that they are in principle computable.
published_date 2023-10-22T05:12:39Z
_version_ 1851368678663127040
score 11.089572