Cyfrifiadureg Ddamcaniaethol
Mae Cyfrifiadureg Ddamcaniaethol yn defnyddio dulliau mathemategol a rhesymegol i ddeall natur cyfrifiadu a datrys problemau sylfaenol sy'n codi trwy ddefnydd ymarferol pob dydd o systemau cyfrifiadurol. Mae Cyfrifiadureg Ddamcaniaethol yn ddyledus iawn am ei llwyddiant i Alan Turing (1912-1954), y mae llawer yn ei ystyried yn dad Cyfrifiadureg Ddamcaniaethol, ac i Kurt Gödel (1906-1978), sylfaenydd rhesymeg fodern.
Rhoddodd Turing ddiffiniad manwl o'r syniad o gyfrifiadu trwy ei beiriannau Turing a dangosodd fod problemau cyfrifiadura yn bodoli na fydd unrhyw gyfrifiadur, pa mor bwerus bynnag, byth yn gallu eu datrys. Dangosodd Gödel y gellir ffurfioli a mecaneiddio rhesymu rhesymegol yn llawn, ond ar y llaw arall, mae llawer o briodweddau strwythurau data a systemau cyfrifiadura yn anbenderfynadwy yn eu hanfod, hynny yw, nid oes modd eu profi na'u gwrthbrofi.
Yn seiliedig ar fewnwelediadau sylfaenol Turing a Gödel, a ddangosodd bŵer a chyfyngiadau cyfrifiadu a rhesymeg, datblygodd Cyfrifiadureg Ddamcaniaethol amrywiaeth eang o ddulliau i brofi cywirdeb system gyfrifiadura a darganfod gwallau meddalwedd cyn iddynt arwain at fethiannau cyfrifiadurol trychinebus. Mae Cyfrifiadureg Ddamcaniaethol hefyd yn asesu anhawster cynhenid problemau cyfrifiadura, yn datblygu dulliau newydd effeithlon i ddatrys problemau cyfrifiadura caled ac yn darparu methodolegau pwerus ar gyfer datblygu meddalwedd gywir a dibynadwy.
Cyfrifiadureg Ddamcaniaethol yn Abertawe:
Dilysu
Mae gennym arbenigedd mewn sawl prawf theorem megis Agda, B-Method, Coq, Event-B, Isabelle/HOL, Minlog, a Maude. Rydym wedi datblygu llyfrgelloedd arbennig ar gyfer gwirio meddalwedd fel CSP-CASL, CSP-Prover, efelychydd CSP Timed, OnTrack, K-Android, Gwiriwr Cysondeb CASL, CSP-Agda, OOAgda. Mae gennym arbenigedd mewn algebrâu prosesau, yn enwedig CSP a CCS, ac mewn amrywiol resymegau moddol ac amserol. Rydym wedi bod yn gwirio systemau cydgloi rheilffyrdd gyda'n partner diwydiannol Siemens. Mae hyn yn cynnwys systemau traddodiadol sy'n seiliedig ar resymeg ysgol yn ogystal â'r ERTMS-ETCS newydd sy'n seiliedig ar reilffyrdd heb signalau a phrotocolau cyfathrebu dosbarthedig. Bu ffocws arbennig ar optimeiddio systemau cydgloi rheilffyrdd, er mwyn cynyddu capasiti rheilffyrdd, o bosibl gan ddefnyddio’r addasiadau ffisegol lleiaf posibl. Mae gennym ni arbenigedd hefyd mewn gwirio caledwedd gyfrifiadurol.
Theori Math
Defnyddir mathau mewn rhaglennu i gael rhaglenni sydd â gradd uwch o gywirdeb, a helpu'r crynhowyr i lunio rhaglenni'n fwy effeithlon. Ein prif ffocws mewn theori math yw theori math dibynnol, lle gellir paramedreiddio mathau (dibynnu) ar elfennau o fathau eraill. Mae hyn yn galluogi disgrifio cywirdeb gweithdrefnau trwy fynegi allbwn gweithdrefn yn ôl math sy'n cael ei baramedreiddio gan ei fewnbynnau. Er enghraifft, gellir mynegi bod allbwn ffwythiant didoli yn rhestr sydd wedi'i didoli ac sydd â'r un elfennau â'i mewnbynnau. Enghraifft arall yw'r briodwedd, ar ôl diweddaru system rhyng-gloi rheilffordd yn dibynnu ar geisiadau gan ddefnyddwyr, bod y system gyd-gloi newydd yn bodloni meini prawf diogelwch. Er enghraifft, gellir diffinio'r math o ryngwyneb defnyddiwr graffigol fel math sy'n dibynnu ar ryngwyneb y defnyddiwr ei hun. Yn Abertawe mae gennym arbenigedd arbennig mewn theori prawf Theori Math Martin Laf, profi theorem rhyngweithiol gan ddefnyddio profwyr theorem ddamcaniaethol math Agda a Coq, coalgebras a chyd-anwythiad. Mae gennym arbenigedd mewn rhaglennu teipio'n ddibynnol, gan gynnwys ysgrifennu rhyngwynebau defnyddiwr graffigol wedi'u gwirio, ffurfioli algebrâu prosesau mewn theori math, gwirio systemau gyd-gloi rheilffyrdd gan ddefnyddio profwyr theorem theori math.
Technoleg Blockchain
Mae blockchains, ac yn gyffredinol Dechnolegau Cyfriflyfr Dosbarthedig, yn darparu ffordd newydd o gytuno ar wybodaeth ddigidol ddibynadwy ymhlith partïon heb ymddiriedaeth. Y defnydd mwyaf adnabyddus o'r dechnoleg newydd hon yw cryptoarian digidol fel Bitcoin, sydd wedi'u datblygu i ddisodli'r system bresennol o storio cyfrifon banc ar weinydd canolog. Y broblem gyda'r gweinydd canolog yw ei fod yn ffurfio methiant pwynt sengl a gellir ei drin heb ganiatâd y defnyddwyr. Mewn cryptoarian, mae cyfrifon banc yn cael eu storio mewn cronfa ddata ddosbarthedig ac mae amrywiol fodelau consensws (y prif un yw mwyngloddio) wedi'u datblygu i benderfynu pa gofnodion cronfa ddata sy'n gywir. Y tu hwnt i gryptoarian , gellir defnyddio blockchain i storio unrhyw ddata a chreu ymddiriedaeth ymhlith defnyddwyr heb ymddiriedaeth ynghylch ei gywirdeb. Gellir defnyddio contractau clyfar i gyflawni trafodion yn awtomatig ar blockchain pan fodlonir rhai amodau. Gan fod y canlyniadau economaidd ac ariannol yn enfawr, mae gwirio protocolau sy'n gysylltiedig â blockchains, cryptoarian a chontractau clyfar yn bwysig iawn. Rydym wedi datblygu model o blockchain ac yn gweithio ar wirio contractau clyfar a phrotocolau eraill mewn profwyr theoremau. Rydym yn archwilio ffyrdd mwy cyffredinol o ddefnyddio technolegau blockchain fel olrhain y defnydd o asedau yn y gadwyn gyflenwi. Mae'r gwaith hwn hefyd yn rhan o http://www.swanseablockchainlab.com/.
Damcaniaeth Dadl
Wedi'i astudio'n wreiddiol mewn athroniaeth a'r gyfraith, mae ymdrafod wedi cael ei ymchwilio'n helaeth mewn Deallusrwydd Artiffisial a Chyfrifiadureg yn ystod y degawd diwethaf. Yn syml, mae damcaniaeth dadl yn canolbwyntio ar anghydfodau a dadleuon, lle mae partïon yn dadlau o blaid ac yn erbyn casgliadau. Mae damcaniaeth dadl yn darparu mecanwaith pwerus ar gyfer delio â gwybodaeth anghyson, anghyflawn gan ddefnyddio rhesymu y gellir ei ddirymu/heb fod yn fonotonig; mae'n cynnig modd ar gyfer cynrychioli a helpu i ddatrys gwrthdaro a gwahaniaethau barn ymhlith gwahanol bartïon. Gall y mecanweithiau drîn synnwyr cyffredin a phatrymau rhesymu dynol pob dydd yn ffurfiol. Fel gyda rhesymeg, gall damcaniaeth dadl gynhyrchu esboniadau (profion) ar gyfer casgliadau ynghyd â'r broses gyfrifiadu. Mae pŵer esboniadol damcaniaeth dadl wedi'i archwilio mewn gwneud penderfyniadau a chynllunio yn seiliedig ar ddadl mewn lleoliadau cyfreithiol a meddygol. Ym Mhrifysgol Abertawe, mae arbenigedd mewn damcaniaeth dadl, ymdrafod a phrosesu iaith naturiol, cynlluniau ymdrafod, a chynllunio. O ddiddordeb arbennig mae ymchwil ryngddisgyblaethol ar ymdrafod yn y gyfraith gyda rhyngweithiadau rhwng yr Adran Gyfrifiadureg ac Ysgol y Gyfraith.
Theori Gêm
Theori gêm yw'r ddamcaniaeth fathemategol o ryngweithiadau strategol rhwng asiantau. Ar y naill law, mae'n ffurfio'r sylfaen ddamcaniaethol ar gyfer gwirio, gan y gallwn weld senario gwirio fel gêm sy'n cael ei chwarae rhwng y system a'i hamgylchedd. Yn ogystal, mae Cyfrifiadureg Ddamcaniaethol yn hanfodol ar gyfer sylfeini theori gêm, gan ei bod yn caniatáu inni ystyried cymhlethdod algorithmig gwneud penderfyniadau ar gyfer theori gêm.
Rhesymeg a Chymhlethdod
Mae damcaniaeth cymhlethdod cyfrifiadol yn tarddu o resymeg. Nod sylfaenol y maes hwn yw deall terfynau cyfrifiadu effeithlon (hynny yw, deall y dosbarth o broblemau y gellir eu datrys yn gyflym ac ag adnoddau cyfyngedig) a ffynonellau anhydrinedd (dyna sy'n mynd â rhai problemau y tu hwnt i gyrraedd atebion mor effeithlon yn eu hanfod). Y broblem agored enwocaf yn y maes yw'r broblem P yn erbyn NP, a restrir ymhlith saith problem Gwobr Mileniwm Clay (gweler hefyd y pwnc 'Satisfiability Solving'). Mae rhesymeg yn darparu pecyn amrywiol o dechnegau i ddadansoddi cwestiynau fel hyn, ac mae rhai ohonynt yn addo darparu mewnwelediadau dwfn i natur a therfynau cyfrifiadu effeithlon. Mae'r Grŵp Damcaniaeth yn Abertawe yn canolbwyntio ar ddisgrifiadau rhesymegol o gymhlethdod, yn benodol cymhlethdod prawf gosodiadol a rhifyddeg gyfyngedig. Mewn rhifyddeg gyfyngedig, y broblem agored fawr yw profi canlyniadau annibyniaeth cryf a fyddai'n gwahanu ei lefelau. Mewn cymhlethdod prawf gosodiadol, y broblem agored fwyaf yw profi ffiniau is cryf ar gyfer systemau prawf gosodiadol mynegiannol.
Seiberddiogelwch
Mae seiberddiogelwch yn faes Cyfrifiadureg sy'n effeithio'n barhaus ar ein bywydau pob dydd. Mae'n faes sydd â chefndir eang, o hanfodion craidd (e.e. cryptograffeg) i faterion cymdeithasol sy'n gysylltiedig â pheirianneg gymdeithasol (e.e. ymosodiadau sy'n twyllo barn ddynol). Yma yn Abertawe, rydym yn mabwysiadu dull rhyngddisgyblaethol sy'n cwmpasu themâu ymchwil ym maes Cyfrifiadureg ac yn ymestyn i feysydd ehangach fel y Gyfraith. Mae'r Grŵp Damcaniaeth yn arbennig o awyddus i ddadansoddi diogelwch systemau'n drylwyr ac maent yn cyfrannu'n barhaus at y maes, e.e., drwy fodelu a gwirio cryptoarian, gweithio ar fodelau preifatrwydd, ystyried diogelwch cymwysiadau symudol a llunio dulliau i ddal seiberderfysgaeth.
Deallusrwydd Artiffisial a'r Gyfraith
Mae Deallusrwydd Artiffisial a'r Gyfraith yn faes ymchwil o fewn Deallusrwydd Artiffisial. Mae theori ac offer deallusrwydd artiffisial yn cael eu cymhwyso i wybodaeth gyfreithiol (e.e. deddfwriaeth, cyfraith achosion, a chontractau) a phrosesau (e.e. ymgynghoriadau, achosion llys, trafodaethau, ac olrhain cydymffurfiaeth). Mae gwybodaeth gyfreithiol yn herio theori ac offer deallusrwydd artiffisial i fynd i'r afael â materion cymhleth, heb eu datrys (e.e. dirymadwyedd, anghysondeb, amwysedd, dehongli, ymdrafod, modelu systemau, cymhlethdod ieithyddol, normau, a rhesymu yn seiliedig ar achosion). Fel y cydnabyddir gan sefydliadau ariannu ymchwil y Deyrnas Unedig, bydd datblygiadau mewn deallusrwydd artiffisial a'r Gyfraith yn cael effaith sylfaenol, eang a pharhaol ar bob lefel o gymdeithas. Ym Mhrifysgol Abertawe, mae cydweithrediad unigryw, rhyngddisgyblaethol rhwng yr Adran Gyfrifiadureg ac Ysgol y Gyfraith. Mewn cyfrifiadureg, mae arbenigedd mewn rhesymeg, cynrychioli gwybodaeth, dysgu peirianyddol, prosesu iaith naturiol, rhesymu yn seiliedig ar achosion, deialog/trafodaeth, sgwrsfotiaid, ac efelychu cymdeithasol. Yn y Gyfraith, mae arbenigedd mewn ymdrafod, cyfraith achosion, cyfraith gyhoeddus a throseddol, cyngor cyfreithiol, a phoblogaethau agored i niwed.
Prosesu Iaith Naturiol
Mae prosesu iaith naturiol (NLP) yn is-faes o AI sy'n canolbwyntio ar brosesu a dadansoddi iaith naturiol yn awtomataidd, e.e. dosrannu, semanteg eiriol, cynrychiolaeth semantig, disgwrs, a chynhyrchu. Dau brif ddull yw: dysgu peirianyddol, lle mae testunau'n cael eu dadansoddi a'u dosbarthu'n ystadegol o ran teimlad, barn, pwnc, a mathau eraill; cynrychiolaeth gwybodaeth a rhesymu, lle defnyddir rheolau a strwythurau gwybodaeth (rhesymegol) i brosesu, cysylltu, echdynnu, cynrychioli a rhesymu gyda'r wybodaeth fanwl sydd wedi'i hamgodio mewn iaith. Defnyddir deialog/trafodaeth a chynhyrchu iaith naturiol i ddatblygu sgwrsfotiaid. Ym Mhrifysgol Abertawe, mae arbenigedd mewn echdynnu gwybodaeth, ieithoedd naturiol rheoledig (geirfa a gramadeg gyfyngol i gyfieithu iaith naturiol yn iaith ffurfiol at ddiben casgliad), dadansoddi dadleuon yn awtomataidd mewn iaith naturiol, NLP gan ddefnyddio dysgu peirianyddol, sgwrsfotiaid, a delweddu gwybodaeth ieithyddol ar raddfa fawr. O ddiddordeb arbennig yw cymhwyso prosesu iaith naturiol (NLP) i destunau cyfreithiol. Mae prosesu iaith naturiol yn ymwneud â Theori Math (dulliau theori math ar gyfer cystrawen a semanteg), ymdrafod, rhesymeg a theori prawf, pynciau eraill mewn deallusrwydd artiffisial lle mae cefnogaeth i benderfyniadau a rhesymu wedi'u seilio ar iaith.
Theori Cydredeg
Mae theori cydredeg yn cynrychioli'r maes cyfrifiadureg ddamcaniaethol sy'n astudio priodweddau dadgyfansoddadwyedd rhaglen, algorithm, neu broblem yn rhannau y gellir eu gweithredu'n ddiogel (yn rhannol) allan o drefn. Gan ddechrau â gwaith arloesol Carl Adam Petri ar rwydi Petri yn gynnar yn y 1960au, mae amrywiaeth eang o ffurfioldebau wedi'u datblygu ar gyfer modelu a rhesymu ynghylch cydredeg. Ym Mhrifysgol Abertawe, ein ffocws yn bennaf yw calcwli prosesau, sef ffurfioldeb algebraidd ar gyfer mynegi systemau cydredol, ac yn benodol cysylltiadau â theori awtomata a rhesymeg moddol ac amserol, gan fynd i'r afael â materion sy'n ymwneud â mynegiant, penderfyniadadwyedd a chymhlethdod calcwli prosesau a'r rhesymeg ar gyfer rhesymu amdanynt.
Seiliau Addysgol, Hanesyddol ac Athronyddol Cyfrifiadureg
Mae dylanwad data, meddalwedd a chyfrifiannu ar y byd yn dwysáu. Mae ymddangosiad ystod syfrdanol o dechnolegau digidol wedi trawsnewid yn sylfaenol lawer o agweddau ar ein bywydau gwleidyddol, economaidd, cymdeithasol a phersonol. Mae cyfrifiadurwyr wrth wraidd y technolegau hyn a gallant gael mewnwelediadau dwfn i sut maen nhw'n effeithio ar y byd ac yn ei newid: o ddamcaniaeth, i bolisi ac ymarfer. Mae cyfrifiadurwyr Abertawe wedi gwneud, ac yn gwneud, cyfraniadau technegol sy'n sbarduno newid, ond maent hefyd yn mynd i'r afael â chwestiynau Addysgol, Hanesyddol ac Athronyddol. Addysg: Pa addysg ym maes cyfrifiadura dylem ni ei chynnig (i) i fyfyrwyr ac athrawon ysgol a phrifysgol; (ii) i bobl sy'n gweithio mewn busnesau, gwasanaethau cyhoeddus a'r proffesiynau, a (iii) i ddinasyddion? Hanes a Threftadaeth: Beth yw achosion y newidiadau? Beth yw'r dyfeisiadau a'r arloesiadau sy'n allweddol i'n technolegau, ein huchelgeisiau a'n pryderon presennol? Athroniaeth: Sut mae ein technolegau'n siarad â phroblemau athronyddol dynol clasurol o ran yr hyn y gallwn ei wybod, yr hyn y gallwn ei wneud, a phwy ydym ni? [Dolen i'r dudalen draws-doriadol yn y fersiwn ar-lein]
Theori Rhesymeg a Phrawf
Camgymeriad dynol yw'r prif achos dros ddamweiniau traffig angheuol. Felly, mae ceir heb yrwyr yn cael eu datblygu i wneud gyrru'n fwy diogel. Gweithgaredd hyd yn oed mwy peryglus na gyrru yw rhaglennu. Gan fod rhaglenni cyfrifiadurol yn rheoli awyrennau, gorsafoedd pŵer niwclear, dyfeisiau meddygol a systemau bancio, gall bygiau a gyflwynir gan raglenwyr achosi colled drychinebus o fywyd a bywoliaeth. Yn Abertawe rydym yn defnyddio dulliau o Theori Rhesymeg a Phrawf i gynhyrchu rhaglenni cyfrifiadurol yn awtomatig sy'n sicr o fod heb wallau. Mae gwreiddiau'r dulliau hyn yn argyfwng sylfaenol mathemateg a achoswyd gan baradocsau rhesymegol, er enghraifft, paradocs Russell, a Theorem Anghyflawnder Goedel, sydd, yn nhermau Cyfrifiadureg, yn nodi nad oes unrhyw resymeg a all brofi pob datganiad gwir am system gyfrifiadurol, yn waeth byth, ni all unrhyw resymeg brofi ohoni'i hun ei bod yn rhydd o wrthddywediad. Yn eu brwydr yn erbyn anghyflawnrwydd, mae rhesymegwyr a cyfrifiadurwyr yn datblygu rhesymeg a oedd wedyn yn hynod ddefnyddiol hefyd wrth wneud meddalwedd gyfrifiadurol - ac felly ein bywydau - yn fwy diogel.
Mae rhesymegwyr hefyd wedi troi at weithio gyda rhesymeg anfonotonig a dirymadwy er mwyn cysylltu'n well â rhesymu synnwyr cyffredin mewn cyd-destun deinamig. Mae creu cronfeydd gwybodaeth sy'n deillio o arbenigedd dynol yn gynyddol hanfodol. Yn y ffyrdd hyn, mae rhesymeg yn dod yn fwy rhyngddisgyblaethol, gan ymwneud â deallusrwydd artiffisial a'r Gyfraith, prosesu iaith naturiol, ac ymdrafod.
Damcaniaeth Cyfrifadwyedd (computability)
A oes terfynau i'r hyn y gallwn ei gyfrifiadura? A allai fod ffyrdd o gyfrifiadura sy'n fwy pwerus nag eraill? Cwestiynau sylfaenol o'r math hwn oedd yr hyn a sbardunodd y bwrlwm o weithgarwch yn y 1930au, a ystyrir yn gyffredinol fel dechrau cyfrifiadureg fodern ac a arweiniodd yn y pen draw at ddyfeisio cyfrifiaduron digidol ffisegol. Mae'r maes yn dal i ymwneud â chwestiynau sylfaenol am gyfrifiadau. Wrth i'r pwnc esblygu, mae llawer o gwestiynau cymhleth am gyfrifiadau wedi'u codi, ond mae materion sylfaenol yn parhau megis cyfrifiannu dros ddata parhaus (fel union rifau go iawn a ffrydiau anfeidraidd) yn hytrach na data arwahanol. Yn Abertawe rydym yn ymchwilio i'r sylfaen fathemategol ar gyfer cyfrifianu dros ddata parhaus ac yn datblygu meddalwedd wedi'i gwirio ar gyfer cyfrifiannu union rifau go iawn.
Datrys Bodlonadwyedd
Datrys Bodlonadwyedd (SAT) yw'r datrysiad algorithmig o system o hafaliadau rhesymegol (Boole). Mae wedi dod yn dechnoleg chwyldroadol yn y diwydiant caledwedd, gan ddarparu injan resymegol bwerus ar gyfer profi cywirdeb a gwirio. Mae Datrys Bodlonadwyedd hefyd yn fwyfwy ganolog ar gyfer profi theoremau awtomataidd (ATP). Stori lwyddiant ddiweddar oedd datrysiad Problem Triphlyg Pythagoras Boole, a gynhyrchodd y prawf mwyaf erioed gan ddefnyddio strategaethau ciwb-a-gorchfygu deallus. Ac mae llawer o feysydd cymhwysiad eraill, lle mae'n rhaid datrys "posau rhesymegol" mawr (meddyliwch am "Sudokus mawr") fel diogelwch rheilffyrdd, ymdrafod, deallusrwydd artiffisial yn gyffredinol, a rhesymeg a chymhlethdod. Ar ffurf y broblem P yn erbyn NP, mae cymhlethdod datrys bodlonadwyedd yn un o bynciau canolog cyfrifiadureg ddamcaniaethol. Yn Abertawe rydym yn ymdrin â'r maes cyfan, o'r sylfeini damcaniaethol trwy weithrediadau ffynhonnell agored i gymwysiadau mewn diwydiant a mathemateg.
