Trosolwg o'r Grŵp
Mae Grŵp Damcaniaeth Abertawe yn adnabyddus yn rhyngwladol am ei ymchwil mewn Rhesymeg mewn Cyfrifiadureg. Y meysydd ymchwil gweithredol yw: Damcaniaeth Cyfrifadwyedd, Cymhlethdod Cyfrifiadol, Theori Prawf, Theori Math, Theori Gêm, Algorithmau, Dulliau Ffurfiol (Profi Theoremau Awtomataidd a Rhyngweithiol), Seiberddiogelwch, Technoleg Blockchain, Dilysu Systemau Rheoli Rheilffyrdd, Deallusrwydd Artiffisial (Datrys Bodlonrwydd, Systemau Aml-asiant, Damcaniaeth Dadl, Dysgu Peiriannau Dibynadwy, Deallusrwydd Artiffisial a'r Gyfraith).
Mae'r ymchwil i Systemau Rheoli Rheilffyrdd wedi arwain at sefydlu Grŵp Dilysu Rheilffyrdd Abertawe a gyflwynodd ddwy Astudiaeth Achos Effaith hefyd. Mae is-grŵp arall a sefydlwyd yn ddiweddar yn astudio Sylfaen Addysgol, Hanesyddol ac Athronyddol Cyfrifiadureg.
Newyddion a Digwyddiadau
Cyfrifadwyedd
Mae Grŵp Cyfrifadwyedd Abertawe'n ymchwilio i agweddau hanfodol cyfrifiadureg a'u cymhwyso mewn cyfrifiadureg a mathemateg.
Rydym yn grŵp blaenllaw mewn dadansoddi cyfrifiannu, sy'n ymwneud â damcaniaeth cyfrifiannu gyda gwrthrychau megis rhifau go iawn a swyddogaethau parhaus. Rydym yn archwilio sut mae theoremau cyfrifiannu o fathemateg, gan ddefnyddio cymhlethdod Weihrauch fel fframwaith yn bennaf.
Algorithmau a Cymhlethdod
Mae'r grŵp Algorithmau a Chymhlethdod yn ymchwilio i'r rhyngweithio rhwng rhesymeg ffurfiol a dylunio algorithmig drwy lens cymhlethdod cyfrifiadol, gan bontio safbwyntiau damcaniaethol a chymhwysol. Rydym yn dadansoddi cwestiynau sylfaenol am derfynau cyfrifiadol a fframweithiau dilysu, wrth archwilio cymwysiadau ymarferol megis algorithmau datrys ar gyfer posau cyfuniadol (e.e. Sudokus) a systemau profi theoremau awtomataidd. Mae gwaith damcaniaethol yn canolbwyntio ar ddeillio ffiniau uchaf/isaf ar gyfer problemau a nodweddu mynegiant system prawf, tra mae ymdrechion ymarferol yn datblygu datryswyr effeithlon ac offer dilysu. Drwy gyfuno manwl gywirdeb mathemategol â gweithredu meddalwedd, rydym yn gwella dealltwriaeth o sut mae strwythurau rhesymegol yn cyfyngu neu'n galluogi cyfrifiannu effeithlon, gan astudio profion fel gwrthrychau damcaniaethol (hyd, cymhlethdod) ac arteffactau ymarferol (cynhyrchu, dilysu). Mae'r ffocws deuol hwn yn cysylltu damcaniaeth gymhlethdod haniaethol â datrys problemau yn y byd go iawn.
Theori Prawf, Theori Math, Profi Theoremau Awtomataidd
Mae'r Grŵp Damcaniaeth Brawf a Damcaniaeth Fath yn Abertawe'n canolbwyntio ar y dadansoddiad trefnol o ddamcaniaethau mathemategol i fesur eu cryfder o safbwynt cysondeb. Maes ymchwil allweddol yw Damcaniaeth Fath Martin-Löf (MLTT) a'i hestyniadau, megis Bydysawd Mahlo, dychweliad anwythiad ac anwythiad-anwythiad.
Mae ein gwaith yn cynnwys echdynnu rhaglenni o brofion, gan gynnwys rhaglenni cytgroes a gorchmynnol yn ogystal â rhai ffwythiannol. Rydym yn datblygu estyniadau o MLTT sy’n gryf o safbwynt damcaniaeth brawf, sy'n cael eu cyfiawnhau'n honiadol fel rhan o raglen Hilbert ddiwygiedig. Rydym hefyd yn gwirio cywirdeb rhaglenni, gan gynnwys y rhai hynny ar gyfer pleidleisio electronig a chontractau clyfar, gan ddefnyddio profwyr theorem ryngweithiol megis Coq, Agda, Minlog, Lean, a Prawf.
Rydym yn archwilio rhaglennu sy’n ddibynnol ar fath, gan ganolbwyntio ar gyd-anwythiad, rhaglenni ar sail gwrthrychau a rhaglenni wedi’u gwirio â rhyngwyneb defnyddwyr graffig. Hefyd, rydym yn datblygu gwirwyr ar gyfer profi theoremau awtomataidd, megis datryswyr SAT/SMT, ac yn ymchwilio i sylfeini cyd-anwythiad er mwyn ffurfioli strwythurau anfeidraidd. Mae ein gwaith ymchwil hefyd yn archwilio semanteg prawf ddamcaniaeth a thrawsnewid profion. Yn ogystal, rydym yn defnyddio profwyr theorem i greu algorithmau cyfrif pleidleisiau a phrotocolau cryptograffig a'u profi nhw'n gywir.
Deallusrwydd Artiffisial Dibynadwy
Mae AI Dibynadwy'n cyfeirio’n aml at gysyniadau polisi generig: tegwch a chynwysoldeb, preifatrwydd a diogelwch, tryloywder, atebolrwydd, dibynadwyedd a diogelwch. Gall hefyd ymwneud ag ardystiad (gwirio a dilysu systemau). Mae'r cysyniadau hyn yn cyfeirio at faint o hyder sydd gan ddefnyddwyr mewn system gyfrifiadol i weithio’n gyson ac yn ddibynadwy yn ôl y bwriad ac ymddwyn o fewn ffiniau derbyniol.
Edrychir ar AI Dibynadwy'n aml o safbwynt cymhwyso'r Gyfraith i'r system gyfrifiadol; hynny yw, a all gweithiwr cyfreithiol proffesiynol ddadlau bod system wedi glynu wrth y gyfraith neu beidio ac os nad yw, pwy sy'n atebol. Er enghraifft, a yw system gyfrifiadol wedi torri diogelwch data unigolyn. Y cwestiwn yw a oes polisi wedi cael ei dorri wrth ddefnyddio'r system. Yr effaith bosib mewn Cyfrifiadureg yw y gallai'r datblygwyr neu'r rhai sy'n cynnal y system fod yn atebol am dorri polisïau, yn enwedig o ran gweithrediadau adrodd fel y gall gweithwyr cyfreithiol proffesiynol werthuso'r system.
Serch hynny, mae’n fwy perthnasol i ymchwil Cyfrifiadureg cynnwys y cysyniadau polisi yn y system gyfrifiadol. Hynny yw, mae'r system weithredu'n glynu wrth y cysyniadau polisi, neu mewn rhai achosion, yn eu torri nhw. Mae rhai cysyniadau'n cael eu datblygu e.e. diogeledd, preifatrwydd, tryloywder, dibynadwyedd, diogelwch ac ardystio. Gall cysyniadau eraill e.e. tegwch a chynwysoldeb, fod yn fwy perthnasol i ddata na'r system weithredu. Mae’n fwy o her ceisio mynd i'r afael ag ymddygiad a ddiffinnir gan y gyfraith yn benodol, sy'n sail i'r cysyniadau. Er enghraifft, mewn cerbydau awtonomaidd, beth mae’n ei olygu bod y cerbyd yn glynu wrth Reolau'r Ffordd Fawr, ac mewn rhai achosion, yn torri cyfreithiau penodol ac yn osgoi cosb oherwydd amgylchiadau lliniarol?
Ar gyfer hyn mae angen cynrychioliadau ffurfiol arnom o'r gyfraith y gellir eu gweithredu a rhesymu ar eu sail. Felly, mae'n tynnu ar achosion defnydd ar gyfer gwaith is-grwpiau damcaniaeth eraill ac yn eu darparu. Er enghraifft, gellir defnyddio cynrychiolaeth ffurfiol, dulliau ffurfiol (gwirio a dilysu), profi theorem, SAT, ac ymagweddau damcaniaethol eraill er mwyn gwella dibynadwyedd y system. Yn yr ystyr hwn, mae AI Dibynadwy'n cynnig maes cymhwyso ar gyfer gwaith damcaniaethol. Ar yr un pryd, gall AI Dibynadwy ganfod problemau nad ydynt wedi cael eu trafod mewn ymagweddau damcaniaethol eto e.e. aneglurder neu wead agored, diffyg monotonegedd, natur doradwy neu eraill.
Mae gwaith presennol yn archwilio'r canlynol:
- Modelu Rheolau Ffordd Fawr y DU yn Prolog a chysylltu'r model ag efelychydd gyrru aml-gyfrwng.
- Damcaniaethau ffurfiol i gynrychioli dewisiadau penodol iawn (gwerthoedd) a ddefnyddir i resymu am ddewisiadau gweithredu a'u blaenoriaethu mewn perthynas â’r gyfraith.
- Dulliau i echdynnu (ar sail rheolau neu gyda modelau iaith mawr) a chynrychioli (mewn ieithoedd gwe semantig megis LegalRuleML, OWL, SHACL-SPARQL, neu iaith anodiad arbenigol) gwybodaeth gyfreithiol o ddeddfwriaeth a rheoliadau mewn ieithoedd gwe semantig ().
