Conference Paper/Proceeding/Abstract 276 views
A Computability Perspective on (Verified) Machine Learning
Recent Trends in Algebraic Development Techniques, Volume: 13710, Pages: 63 - 80
Swansea University Authors: Jay Morgan , Tonicha Crook, Arno Pauly , Markus Roggenbach
DOI (Published version): 10.1007/978-3-031-43345-0_3
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...
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 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
first_indexed |
2023-07-10T13:13:11Z |
---|---|
last_indexed |
2023-07-10T13:13:11Z |
id |
cronfa63849 |
recordtype |
SURis |
fullrecord |
<?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><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>df9a27bcf77b4769c2ebbb702b587491</sid><ORCID>0000-0003-3719-362X</ORCID><firstname>Jay</firstname><surname>Morgan</surname><name>Jay Morgan</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>f392e8826eef757ada89c294fbeeb2c2</sid><firstname>Tonicha</firstname><surname>Crook</surname><name>Tonicha Crook</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 ‘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.</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-07-25T13:37:53.3387314</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>Jay</firstname><surname>Morgan</surname><orcid>0000-0003-3719-362X</orcid><order>1</order></author><author><firstname>Tonicha</firstname><surname>Crook</surname><order>2</order></author><author><firstname>Jay</firstname><surname>Morgan</surname><orcid>0000-0003-3719-362x</orcid><order>3</order></author><author><firstname>Arno</firstname><surname>Pauly</surname><orcid>0000-0002-0173-3295</orcid><order>4</order></author><author><firstname>Markus</firstname><surname>Roggenbach</surname><orcid>0000-0002-3819-2787</orcid><order>5</order></author></authors><documents><document><filename>Under embargo</filename><originalFilename>Under embargo</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 |
v2 63849 2023-07-10 A Computability Perspective on (Verified) Machine Learning df9a27bcf77b4769c2ebbb702b587491 0000-0003-3719-362X Jay Morgan Jay Morgan true false f392e8826eef757ada89c294fbeeb2c2 Tonicha Crook Tonicha Crook 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-07-25T13:37:53.3387314 2023-07-10T13:54:49.9621427 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Jay Morgan 0000-0003-3719-362X 1 Tonicha Crook 2 Jay Morgan 0000-0003-3719-362x 3 Arno Pauly 0000-0002-0173-3295 4 Markus Roggenbach 0000-0002-3819-2787 5 Under embargo Under embargo 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 Jay Morgan Tonicha Crook 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 |
df9a27bcf77b4769c2ebbb702b587491 f392e8826eef757ada89c294fbeeb2c2 17a56a78ec04e7fc47b7fe18394d7245 7733869ae501442da6926fac77cd155b |
author_id_fullname_str_mv |
df9a27bcf77b4769c2ebbb702b587491_***_Jay Morgan f392e8826eef757ada89c294fbeeb2c2_***_Tonicha Crook 17a56a78ec04e7fc47b7fe18394d7245_***_Arno Pauly 7733869ae501442da6926fac77cd155b_***_Markus Roggenbach |
author |
Jay Morgan Tonicha Crook Arno Pauly Markus Roggenbach |
author2 |
Jay Morgan Tonicha Crook Jay 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 |
0 |
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-22T13:37:52Z |
_version_ |
1805554625220182016 |
score |
11.028886 |