| 1. |
- Hagström, Lovisa, 1995, et al.
(författare)
-
The Effect of Scaling, Retrieval Augmentation and Form on the Factual Consistency of Language Models
- 2023
-
Ingår i: Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 5457–5476, Singapore. - : Association for Computational Linguistics.
-
Konferensbidrag (refereegranskat)abstract
- Large Language Models (LLMs) make natural interfaces to factual knowledge, but their usefulness is limited by their tendency to deliver inconsistent answers to semantically equivalent questions. For example, a model might supply the answer “Edinburgh” to “Anne Redpath passed away in X.” and “London” to “Anne Redpath’s life ended in X.” In this work, we identify potential causes of inconsistency and evaluate the effectiveness of two mitigation strategies: up-scaling and augmenting the LM with a passage retrieval database. Our results on the LLaMA and Atlas models show that both strategies reduce inconsistency but that retrieval augmentation is considerably more efficient. We further consider and disentangle the consistency contributions of different components of Atlas. For all LMs evaluated we find that syntactical form and task artifacts impact consistency. Taken together, our results provide a better understanding of the factors affecting the factual consistency of language models.
|
|
| 2. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
TriCo—Triple Co-piloting of Implementation, Specification and Tests
- 2022
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 13701 LNCS, s. 174-187, s. 174-187
-
Konferensbidrag (refereegranskat)abstract
- This white paper presents the vision of a novel methodology for developing safety-critical software, which is inspired by late developments in learning based co-piloting of implementations. The methodology, called TriCo, integrates formal methods with learning based approaches to co-pilot the agile, simultaneous development of three artefacts: implementation, specification, and tests. Whenever the user changes any of these, a TriCo empowered IDE would suggest changes to the other two artefacts in such a way that the three are kept consistent. The user has the final word on whether the changes are accepted, rejected, or modified. In the latter case, consistency will be checked again and re-established. We discuss the emerging trends which put the community in a good position to realise this vision, describe the methodology and workflow, as well as challenges and possible solutions for the realisation of TriCo.
|
|
| 3. |
- Alferes, José Júlio, et al.
(författare)
-
Preface
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 11372 LNCS, s. V-VI
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)
|
|
| 4. |
|
|
| 5. |
- Arvidsson, Andreas, et al.
(författare)
-
Proving Type Class Laws for Haskell
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 10447 LNCS, s. 61-74
-
Konferensbidrag (refereegranskat)abstract
- Type classes in Haskell are used to implement ad-hoc polymorphism, i.e. a way to ensure both to the programmer and the compiler that a set of functions are defined for a specific data type. All instances of such type classes are expected to behave in a certain way and satisfy laws associated with the respective class. These are however typically just stated in comments and as such, there is no real way to enforce that they hold. In this paper we describe a system which allows the user to write down type class laws which are then automatically instantiated and sent to an inductive theorem prover when declaring a new instance of a type class.
|
|
| 6. |
- Atterfors, Johan, 1998, et al.
(författare)
-
Machine Learning of Pacing Patterns for Half Marathon
- 2022
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- Every year over 40 000 runners participate in Gothenburg Half Marathon, one of the world’s largest half-marathons. Based on publicly available results data (423 496 entries) for ten years (2010 – 2019), we investigate machine learning models for two tasks: prediction of finishing times and identification of runners risking hitting the wall. Our models improve results over the current baseline on finish time prediction and manage to correctly identify many of the runners who later hit the wall, although it also misclassifies many who do not.
|
|
| 7. |
- Bonacina, M.P., et al.
(författare)
-
Interpolation Systems for Ground Proofs in Automated Deduction: a Survey
- 2015
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 54:4, s. 353-390
-
Tidskriftsartikel (refereegranskat)abstract
- Interpolation is a deductive technique applied in program analysis and verification: for example, it is used to compute over-approximations of images or refine abstractions. An interpolation system takes a refutation and extracts an interpolant by building it inductively from partial interpolants. We survey color-based interpolation systems for ground proofs produced by key inference engines of state-of-the-art solvers: DPLL for propositional logic, equality sharing for combination of convex theories, and DPLL((Formula presented.)) for SMT-solving. Since color-based interpolation systems use colors to track symbols in proofs, equality is problematic, because replacement of equals by equals mixes symbols and therefore colors. We analyze interpolation in the presence of equality, and we demonstrate the color-based approach by giving a complete interpolation system for ground proofs by superposition.
|
|
| 8. |
- Bonacina, M.P., et al.
(författare)
-
On Interpolation in Automated Theorem Proving
- 2015
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 54:1, s. 69-97
-
Tidskriftsartikel (refereegranskat)abstract
- Given two inconsistent formul', a (reverse) interpolant is a formula implied by one, inconsistent with the other, and only containing symbols they share. Interpolation finds application in program analysis, verification, and synthesis, for example, towards invariant generation. An interpolation system takes a refutation of the inconsistent formul' and extracts an interpolant by building it inductively from partial interpolants. Known interpolation systems for ground proofs use colors to track symbols. We show by examples that the color-based approach cannot handle non-ground refutations by resolution and paramodulation/superposition. We present a two-stage approach that works by tracking literals, computes a provisional interpolant, which may contain non-shared symbols, and applies lifting to replace non-shared constants by quantified variables. We obtain an interpolation system for non-ground refutations, and we prove that it is complete, if the only non-shared symbols in provisional interpolants are constants.
|
|
| 9. |
- Bonafilia, Brian, et al.
(författare)
-
Sudden Semantic Shifts in Swedish NATO Discourse
- 2023
-
Ingår i: Association for Computational Linguistics . Annual Meeting Conference Proceedings. - 0736-587X. ; 4, s. 184-193
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we investigate a type of semantic shift that occurs when a sudden event radically changes public opinion on a topic. Looking at Sweden's decision to apply for NATO membership in 2022, we use word embeddings to study how the associations users on Twitter have regarding NATO evolve. We identify several changes that we successfully validate against real-world events. However, the low engagement of the public with the issue often made it challenging to distinguish true signals from noise. We thus find that domain knowledge and data selection are of prime importance when using word embeddings to study semantic shifts.
|
|
| 10. |
- Bruinsma, Sebastianus Cornelis Jacobus, 1991, et al.
(författare)
-
Finding the structure of parliamentary motions in the Swedish Riksdag 1971–2015
- 2023
-
Ingår i: Quality and Quantity. - 1573-7845 .- 0033-5177. ; In press
-
Tidskriftsartikel (refereegranskat)abstract
- The current increase in the number of large, open sets of unstructured textual data has created both opportunities and challenges for social scientists. Here, we explore if and how we can use such data by looking at a dataset of over 144,000 documents used by parliamentary committees in Sweden. Of these, we aim to understand: (a) the topical content of these motions, (b) how these topics have changed over time, and (c) how these topics differ across political parties. To do so, we use a Structural Topic Model, which allows us to not only find the topics using the textual data itself, but also to include the documents’ metadata, such as authorship and date of publication. Doing so, we find 30 topics, which we combine into 9 broader themes. We find that these themes often rise and fall in popularity in line with historical events, and relate to the various political parties as we would expect. Throughout our analysis, we provide a step-by-step overview of how to use structural topic models in practice and also how to handle the type of dataset we use here.
|
|
