arXiv subjects

Moa Johansson

Publications and source records attributed to Moa Johansson.

24 records · Page 2Linked to original sources

arXiv2021

Conjectures, Tests and Proofs: An Overview of Theory Exploration

A key component of mathematical reasoning is the ability to formulate interesting conjectures about a problem domain at hand. In this paper, we give a brief overview of a theory exploration system called QuickSpec, which is able to automatically discover interesting conjectures about a given set of functions. QuickSpec works by interleaving term generation with random testing to form candidate conjectures. This is made tractable by starting from small sizes and ensuring that only terms that are irreducible with respect to already discovered conjectures are considered. QuickSpec has been successfully applied to generate lemmas for automated inductive theorem proving as well as to generate specifications of functional programs. We give an overview of typical use-cases of QuickSpec, as well as demonstrating how to easily connect it to a theorem prover of the user's choice.

cs.LO↗

arXiv2019

Identifying cross country skiing techniques using power meters in ski poles

Power meters are becoming a widely used tool for measuring training and racing effort in cycling, and are now spreading also to other sports. This means that increasing volumes of data can be collected from athletes, with the aim of helping coaches and athletes analyse and understanding training load, racing efforts, technique etc. In this project, we have collaborated with Skisens AB, a company producing handles for cross country ski poles equipped with power meters. We have conducted a pilot study in the use of machine learning techniques on data from Skisens poles to identify which "gear" a skier is using (double poling or gears 2-4 in skating), based only on the sensor data from the ski poles. The dataset for this pilot study contained labelled time-series data from three individual skiers using four different gears recorded in varied locations and varied terrain. We systematically evaluated a number of machine learning techniques based on neural networks with best results obtained by a LSTM network (accuracy of 95% correctly classified strokes), when a subset of data from all three skiers was used for training. As expected, accuracy dropped to 78% when the model was trained on data from only two skiers and tested on the third. To achieve better generalisation to individuals not appearing in the training set more data is required, which is ongoing work.

cs.LG↗

arXiv2018

Proving Type Class Laws for Haskell

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.

cs.PL↗

arXiv2018

Towards Machine Learning on data from Professional Cyclists

Professional sports are developing towards increasingly scientific training methods with increasing amounts of data being collected from laboratory tests, training sessions and competitions. In cycling, it is standard to equip bicycles with small computers recording data from sensors such as power-meters, in addition to heart-rate, speed, altitude etc. Recently, machine learning techniques have provided huge success in a wide variety of areas where large amounts of data (big data) is available. In this paper, we perform a pilot experiment on machine learning to model physical response in elite cyclists. As a first experiment, we show that it is possible to train a LSTM machine learning algorithm to predict the heart-rate response of a cyclist during a training session. This work is a promising first step towards developing more elaborate models based on big data and machine learning to capture performance aspects of athletes.

cs.LG↗

arXiv2014

Hipster: Integrating Theory Exploration in a Proof Assistant

This paper describes Hipster, a system integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering new interesting lemmas in a given theory development. Hipster can be used in two main modes. The first is exploratory mode, used for automatically generating basic lemmas about a given set of datatypes and functions in a new theory development. The second is proof mode, used in a particular proof attempt, trying to discover the missing lemmas which would allow the current goal to be proved. Hipster's proof mode complements and boosts existing proof automation techniques that rely on automatically selecting existing lemmas, by inventing new lemmas that need induction to be proved. We show example uses of both modes.

cs.LO↗

arXiv2013

Proof-Pattern Recognition and Lemma Discovery in ACL2

We present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery. The resulting tool, ACL2(ml), gathers proof statistics and uses statistical pattern-recognition to pre-processes data from libraries, and then suggests auxiliary lemmas in new proofs by analogy with already seen examples. This paper presents the implementation of ACL2(ml) alongside theoretical descriptions of the proof-pattern recognition and lemma discovery methods involved in it.

cs.LO↗