Umeå University's logo

umu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Can proof assistants verify multi-agent systems?
Umeå University, Faculty of Science and Technology, Department of Computing Science.ORCID iD: 0000-0002-7383-0529
Umeå University, Faculty of Science and Technology, Department of Computing Science.ORCID iD: 0000-0002-6458-2252
2024 (English)Conference paper, Oral presentation only (Refereed)
Abstract [en]

This paper presents the Soda language for verifying multi-agent systems. Soda is a high-level functional and object-oriented language that supports the compilation of its code not only to Scala, a strongly statically typed high-level programming language, but also to Lean, a proof assistant and programming language. Given these capabilities, Soda can implement multi-agent systems, or parts thereof, that can then be integrated into a mainstream software ecosystem on the one hand and formally verified with state-of-the-art tools on the other hand.

We provide a brief and informal introduction to Soda and the aforementioned interoperability capabilities, as well as a simple demonstration of how interaction protocols can be designed and verified with Soda. In the course of the demonstration, we highlight challenges with respect to real-world applicability.

Place, publisher, year, edition, pages
2024.
Keywords [en]
Engineering Multi-Agent Systems, Formal Verification, Proof Automation
National Category
Computer Sciences Computer Engineering Computer Systems
Research subject
Computer Science; Computer Systems; Mathematical Logic
Identifiers
URN: urn:nbn:se:umu:diva-232383OAI: oai:DiVA.org:umu-232383DiVA, id: diva2:1916794
Conference
21st European Conference on Multi-Agent Systems, EUMAS 2024, Dublin, Ireland, August 26-28, 2024
Available from: 2024-11-28 Created: 2024-11-28 Last updated: 2025-02-04
In thesis
1. Making fairness actionable
Open this publication in new window or tab >>Making fairness actionable
2024 (English)Licentiate thesis, comprehensive summary (Other academic)
Alternative title[sv]
Att göra rättvisa handlingsbart
Abstract [en]

The opaque nature of machine learning systems has raised concerns about whether these systems can guarantee fairness. In addition, ensuring fair decision-making requires that multiple perspectives of fairness be considered.

Currently, there is no agreement on the definitions, the facilitation of shared interpretation is difficult, and there is a lack of a unified formal language to describe them. Current definitions are implicit in the operationalization of systems, making them difficult to compare.

In this thesis, we discuss how to make fairness actionable, providing concrete tools for that. We provide not only conceptual elements to model and abstract problems of fairness, but also a technical framework and a description language.

Abstract [sv]

Den opaka naturen hos maskininlärningssystem väcker oro kring om dessa system kan garantera rättvisa. Dessutom kräver rättvis beslutsfattande att flera perspektiv på rättvisa beaktas.

För närvarande finns det ingen enighet kring definitionerna, vilket försvårar delad tolkning, och det saknas ett enhetligt formellt språk för att beskriva dem. Nuvarande definitioner är inbyggda i hur systemen används, vilket gör dem svåra att jämföra.

I denna avhandling diskuterar vi hur rättvisa kan göras praktiskt tillämpbar och tillhandahåller konkreta verktyg för detta. Vi erbjuder både konceptuella element för att modellera och abstrahera rättviseproblem samt en teknisk ram och ett beskrivningsspråk.

Place, publisher, year, edition, pages
Umeå: Umeå University, 2024. p. 24
Series
Report / UMINF, ISSN 0348-0542 ; 24.12
Keywords
Algorithmic fairness, Ethics in artificial intelligence, Formal representation of fairness, Formal verification, Functional languages, Human-centered programming languages, Responsible artificial intelligence
National Category
Computer Sciences Software Engineering Ethics
Research subject
Computer Science; Computer Systems; Ethics
Identifiers
urn:nbn:se:umu:diva-232384 (URN)9789180705356 (ISBN)9789180705349 (ISBN)
Presentation
2024-12-13, MIT.A.121, MIT-huset, Campustorget 5, Umeå, Sweden, 13:00 (English)
Opponent
Supervisors
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Available from: 2024-12-03 Created: 2024-11-28 Last updated: 2024-12-03Bibliographically approved

Open Access in DiVA

fulltext(387 kB)70 downloads
File information
File name FULLTEXT01.pdfFile size 387 kBChecksum SHA-512
3e1221d6aaad20976b68d9bdf106b13551d6022b1a5a167053b98eedd275c4e7352dfcb5be41ed46a4fb871bd9cb3e8119afbc0443e3de0ced20ce882dfa5e69
Type fulltextMimetype application/pdf

Authority records

Mendez, Julian AlfredoKampik, Timotheus

Search in DiVA

By author/editor
Mendez, Julian AlfredoKampik, Timotheus
By organisation
Department of Computing Science
Computer SciencesComputer EngineeringComputer Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 70 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 278 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf