arXiv subjects

Jim Portegies

Publications and source records attributed to Jim Portegies.

14 recordsLinked to original sources

arXiv2026

The Educational Proof Assistant Waterproof in an Introductory Proof Course: Proof Construction and Learning Processes

We study the use of an educational proof assistant in an introductory proof course through a quasi-experiment in a varied setting: multiple teachers, students with different study programs, and a mixed Dutch-English language environment. First-year university students are known to struggle with writing proofs. Waterproof is a proof assistant that is designed to support the transfer of skills to paper proofs by working with controlled natural language. We focus on the students' ability to construct valid mathematical proofs, and on their learning process. We study this through in-class observation, surveys, and analysis of student performance and proof structure. We present evidence that effects of using an educational proof assistant carry over to the pen-and-paper context,even when the assistant is English and the proof is given in Dutch. We also present evidence that suggests students in the Mathematics-Computer Science program achieve higher grades when using Waterproof. Our most important conclusion is that an educational proof assistant can help students be more explicit in their proofs. As students self-selected into using Waterproof rather than being randomly assigned, these results are suggestive rather than causal.

math.HO↗

arXiv2026

Waterproof Editor: an educational environment for proof assistants and programming languages

Waterproof Editor provides an educational environment specifically targeted to teaching with proof assistants or programming languages. It arose from Waterproof, educational software targeted at helping students acquire the skill of giving mathematical proofs. Its original features such as enabling rich formatting and providing clear input areas are now abstracted away in an npm package and can be used in different educational contexts. We invite interested parties to use this component in their educational software, and offer to assist with this.

math.HO↗

arXiv2025

A blueprint for the formalization of Carleson's theorem on convergence of Fourier series

This paper is the blueprint underlying the Lean formalization of the proof of Carleson's classical result asserting almost everywhere convergence of Fourier series of continuous functions. We break up the proof into two steps, a reduction of the classical result to a new theorem that appears in a sibling communication and a proof of this new theorem, which is also detailed as blueprint in this paper. An early version of this blueprint was used to initiate the Lean formalization. During the formalization, many contributors elaborated the blueprint with minor corrections, modifications and extensions. The final version is presented here as a guide through the accompanying Lean code.

math.CA↗

arXiv2024

Classification of Covering Spaces and Canonical Change of Basepoint

Using the language of homotopy type theory (HoTT), we 1) prove a synthetic version of the classification theorem for covering spaces, and 2) explore the existence of canonical change-of-basepoint isomorphisms between homotopy groups. There is some freedom in choosing how to translate concepts from classical algebraic topology into HoTT. The final translations we ended up with are easier to work with than the ones we started with. We discuss some earlier attempts to shed light on this translation process. The proofs are mechanized using the Coq proof assistant and closely follow classical treatments like those by Hatcher.

math.AT↗

arXiv2024

Waterproof: Educational Software for Learning How to Write Mathematical Proofs

In order to help students learn how to write mathematical proofs, we adapt the Coq proof assistant into an educational tool we call Waterproof. Like with other interactive theorem provers, students write out their proofs inside the software using a specific syntax, and the software provides feedback on the logical validity of each step. Waterproof consists of two components: a custom proof language that allows formal, machine-verified proofs to be written in a style that closely resembles handwritten proofs, and a custom editor that allows these proofs to be combined with formatted text to improve readability. The editor can be used for Coq documents in general, but also offers special features designed for use in education. Student input, for example, can be limited to specific parts of the document to prevent exercises from being accidentally deleted. Waterproof has been used to supplement teaching the Analysis 1 course at Eindhoven University of Technology (TU/e) for the last four years. Students started using the specific formulations of proof steps from the custom proof language in their handwritten proofs; the explicit phrasing of these sentences helped to clarify the logical structure of their arguments.

math.HO↗

arXiv2022

Feedforward Control in the Presence of Input Nonlinearities: A Learning-based Approach

Advanced feedforward control methods enable mechatronic systems to perform varying motion tasks with extreme accuracy and throughput. The aim of this paper is to develop a data-driven feedforward controller that addresses input nonlinearities, which are common in typical applications such as semiconductor back-end equipment. The developed method consists of parametric inverse-model feedforward that is optimized for tracking error reduction by exploiting ideas from iterative learning control. Results on a simulated set-up indicate improved performance over existing identification methods for systems with nonlinearities at the input.

eess.SY↗

arXiv2022

PDE-based Group Equivariant Convolutional Neural Networks

We present a PDE-based framework that generalizes Group equivariant Convolutional Neural Networks (G-CNNs). In this framework, a network layer is seen as a set of PDE-solvers where geometrically meaningful PDE-coefficients become the layer's trainable weights. Formulating our PDEs on homogeneous spaces allows these networks to be designed with built-in symmetries such as rotation in addition to the standard translation equivariance of CNNs. Having all the desired symmetries included in the design obviates the need to include them by means of costly techniques such as data augmentation. We will discuss our PDE-based G-CNNs (PDE-G-CNNs) in a general homogeneous space setting while also going into the specifics of our primary case of interest: roto-translation equivariance. We solve the PDE of interest by a combination of linear group convolutions and non-linear morphological group convolutions with analytic kernel approximations that we underpin with formal theorems. Our kernel approximations allow for fast GPU-implementation of the PDE-solvers, we release our implementation with this article in the form of the LieTorch extension to PyTorch, available at https://gitlab.com/bsmetsjr/lietorch . Just like for linear convolution a morphological convolution is specified by a kernel that we train in our PDE-G-CNNs. In PDE-G-CNNs we do not use non-linearities such as max/min-pooling and ReLUs as they are already subsumed by morphological convolutions. We present a set of experiments to demonstrate the strength of the proposed PDE-G-CNNs in increasing the performance of deep learning based imaging applications with far fewer parameters than traditional CNNs.

cs.LG↗

arXiv2022

Is Vanilla Policy Gradient Overlooked? Analyzing Deep Reinforcement Learning for Hanabi

In pursuit of enhanced multi-agent collaboration, we analyze several on-policy deep reinforcement learning algorithms in the recently published Hanabi benchmark. Our research suggests a perhaps counter-intuitive finding, where Proximal Policy Optimization (PPO) is outperformed by Vanilla Policy Gradient over multiple random seeds in a simplified environment of the multi-agent cooperative card game. In our analysis of this behavior we look into Hanabi-specific metrics and hypothesize a reason for PPO's plateau. In addition, we provide proofs for the maximum length of a perfect game (71 turns) and any game (89 turns). Our code can be found at: https://github.com/bramgrooten/DeepRL-for-Hanabi

cs.LG↗

arXiv2022

Gaussian Process Position-Dependent Feedforward: With Application to a Wire Bonder

Mechatronic systems have increasingly stringent performance requirements for motion control, leading to a situation where many factors, such as position-dependency, cannot be neglected in feedforward control. The aim of this paper is to compensate for position-dependent effects by modeling feedforward parameters as a function of position. A framework to model and identify feedforward parameters as a continuous function of position is developed by combining Gaussian processes and feedforward parameter learning techniques. The framework results in a fully data-driven approach, which can be readily implemented for industrial control applications. The framework is experimentally validated and shows a significant performance increase on a commercial wire bonder.

eess.SY↗

arXiv2022

Learning nonlinear feedforward: a Gaussian Process Approach Applied to a Printer with Friction

Feedforward control is essential to achieving good tracking performance in positioning systems. The aim of this paper is to develop an identification strategy for inverse models of systems with nonlinear dynamics of unknown structure using input-output data, which directly delivers feedforward signals for a-priori unknown tasks. To this end, inverse systems are regarded as noncausal nonlinear finite impulse response (NFIR) systems and modeled as a Gaussian Process with a stationary kernel function that imposes properties such as smoothness and periodicity. The approach is validated experimentally on a consumer printer with friction and shown to lead to improved tracking performance with respect to linear feedforward.

eess.SY↗

arXiv2022

Position-Dependent Snap Feedforward: A Gaussian Process Framework

Mechatronic systems have increasingly high performance requirements for motion control. The low-frequency contribution of the flexible dynamics, i.e. the compliance, should be compensated for by means of snap feedforward to achieve high accuracy. Position-dependent compliance, which often occurs in motion systems, requires the snap feedforward parameter to be modeled as a function of position. Position-dependent compliance is compensated for by using a Gaussian process to model the snap feedforward parameter as a continuous function of position. A simulation of a flexible beam shows that a significant performance increase is achieved when using the Gaussian process snap feedforward parameter to compensate for position-dependent compliance.

eess.SY↗

arXiv2020

On the Role of Models in Learning Control: Actor-Critic Iterative Learning Control

Learning from data of past tasks can substantially improve the accuracy of mechatronic systems. Often, for fast and safe learning a model of the system is required. The aim of this paper is to develop a model-free approach for fast and safe learning for mechatronic systems. The developed actor-critic iterative learning control (ACILC) framework uses a feedforward parameterization with basis functions. These basis functions encode implicit model knowledge and the actor-critic algorithm learns the feedforward parameters without explicitly using a model. Experimental results on a printer setup demonstrate that the developed ACILC framework is capable of achieving the same feedforward signal as preexisting model-based methods without using explicit model knowledge.

eess.SY↗

arXiv2019

Total Variation and Mean Curvature PDEs on $\mathbb{R}^d \rtimes S^{d-1}$

Total variation regularization and total variation flows (TVF) have been widely applied for image enhancement and denoising. To include a generic preservation of crossing curvilinear structures in TVF we lift images to the homogeneous space $M = \mathbb{R}^d \rtimes S^{d-1}$ of positions and orientations as a Lie group quotient in SE(d). For d = 2 this is called 'total roto-translation variation' by Chambolle & Pock. We extend this to d = 3, by a PDE-approach with a limiting procedure for which we prove convergence. We also include a Mean Curvature Flow (MCF) in our PDE model on M. This was first proposed for d = 2 by Citti et al. and we extend this to d = 3. Furthermore, for d = 2 we take advantage of locally optimal differential frames in invertible orientation scores (OS). We apply our TVF and MCF in the denoising/enhancement of crossing fiber bundles in DW-MRI. In comparison to data-driven diffusions, we see a better preservation of bundle boundaries and angular sharpness in fiber orientation densities at crossings. We support this by error comparisons on a noisy DW-MRI phantom. We also apply our TVF and MCF in enhancement of crossing elongated structures in 2D images via OS, and compare the results to nonlinear diffusions (CED-OS) via OS.

math.AP↗

arXiv2018

SciSports: Learning football kinematics through two-dimensional tracking data

SciSports is a Dutch startup company specializing in football analytics. This paper describes a joint research effort with SciSports, during the Study Group Mathematics with Industry 2018 at Eindhoven, the Netherlands. The main challenge that we addressed was to automatically process empirical football players' trajectories, in order to extract useful information from them. The data provided to us was two-dimensional positional data during entire matches. We developed methods based on Newtonian mechanics and the Kalman filter, Generative Adversarial Nets and Variational Autoencoders. In addition, we trained a discriminator network to recognize and discern different movement patterns of players. The Kalman-filter approach yields an interpretable model, in which a small number of player-dependent parameters can be fit; in theory this could be used to distinguish among players. The Generative-Adversarial-Nets approach appears promising in theory, and some initial tests showed an improvement with respect to the baseline, but the limits in time and computational power meant that we could not fully explore it. We also trained a Discriminator network to distinguish between two players based on their trajectories; after training, the network managed to distinguish between some pairs of players, but not between others. After training, the Variational Autoencoders generated trajectories that are difficult to distinguish, visually, from the data. These experiments provide an indication that deep generative models can learn the underlying structure and statistics of football players' trajectories. This can serve as a starting point for determining player qualities based on such trajectory data.

cs.LG↗