publications

2026

1. LeanPolish: A Kernel-Verified Dataset and Symbolic Compression Framework for Lean 4 Proofs

   Pauline Bourigault

   2026

   TL;DR Code Dataset Website

   TL;DR: A kernel-verified symbolic compression framework and dataset for Lean 4 proofs, including structured before/after pairs with quality-tier and gate annotations.

2. Coverage Cliffs in Learning from Logged World Feedback

   Pauline Bourigault

   In ICML Workshop on RL from World Feedback, 2026

   TL;DR PDF Code

   TL;DR: We study when logged world feedback can certify tail safety, giving a PAC-Bayes off-policy VaR certificate and identifying a quantile-specific coverage cliff caused by insufficient weighted CDF mass.

3. CovCal: Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning

   Pauline Bourigault, Xiaotong Ji, Matthieu Zimmer, Rasul Tutunov, and Haitham Bou-Ammar

   In ICML AI for Math Workshop, 2026

   TL;DR arXiv Code Website

   TL;DR: COVCAL shows when Lean proofs can be safely trusted as partial evidence for math-answer selection by calibrating coverage diagnostics and abstaining when formal evidence is insufficient.

2025

1. Information-Geometric Neural Granger Causality

   Pauline Bourigault and Danilo P. Mandic

   In ICML Workshop on High-dimensional Learning Dynamics, 2025

   TL;DR PDF

   TL;DR: We introduce Information-Geometric Neural Granger Causality (IG-NGC), a framework that provides a partial theoretical explanation for neural causality methods. Our key insight is that when assuming Gaussian output distributions and diagonal Fisher Information approximation, causality can be interpreted as directional information flow measured by a simplified Fisher metric on statistical manifolds.

2. FrEVL: Leveraging Frozen Pretrained Embeddings for Efficient Vision-Language Understanding

   Emmanuelle Bourigault and Pauline Bourigault

   In ICCV Workshop on Safe and Trustworthy Multimodal AI Systems, 2025

   Oral Presentation

   TL;DR arXiv Code

   TL;DR: FrEVL is a vision-language understanding by freezing pretrained CLIP embeddings and training only a lightweight fusion network. This approach delivers: 3× faster inference than ALBEF/BLIP, 70% lower deployment costs, 68.4M trainable parameters (vs 200M+ in SOTA models), 850 images/sec throughput on single V100, production-ready with <25ms p99 latency.

3. Kernel-Based Anomaly Detection Using Generalized Hyperbolic Processes

   Pauline Bourigault and Danilo P. Mandic

   In International Conference on Acoustics, Speech and Signal Processing (ICASSP), 2025

   TL;DR arXiv Code

   TL;DR: We present a novel approach to anomaly detection by integrating Generalized Hyperbolic (GH) processes into kernel-based methods. The GH distribution, known for its flexibility in modeling skewness, heavy tails, and kurtosis, helps to capture complex patterns in data that deviate from Gaussian assumptions. We propose a GH-based kernel function and utilize it within Kernel Density Estimation (KDE) and One-Class Support Vector Machines (OCSVM) to develop anomaly detection frameworks. Theoretical results confirmed the positive semi-definiteness and consistency of the GH-based kernel, ensuring its suitability for machine learning applications. Empirical evaluation on synthetic and real-world datasets showed that our method improves detection performance in scenarios involving heavy-tailed and asymmetric or imbalanced distributions.

4. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning

   Project Numina and Kimi (Moonshot AI) Teams

   arXiv preprint arXiv:2504.11354, 2025

   arXiv Code

2024

1. Multi-Modal Information Bottleneck Attribution with Cross-Attention Guidance

   Pauline Bourigault, Emmanuelle Bourigault, and Danilo P. Mandic

   In British Machine Vision Conference (BMVC), 2024

   TL;DR PDF

   TL;DR: A multi-modal attribution method that leverages the information bottleneck principle and cross-attention guidance to identify the most relevant features across different modalities.

2. MVDiff: Scalable and Flexible Multi-view Diffusion for 3D Object Reconstruction

   Emmanuelle Bourigault and Pauline Bourigault

   In CVPR Workshop on Generative Models for Computer Vision, 2024

   TL;DR PDF Code

   TL;DR: MVDiff is a diffusion model that generates consistent multi-view images from single-view inputs for high-quality 3D reconstruction.

3. Quaternion Recurrent Neural Network with Real-Time Learning and Maximum Correntropy

   Pauline Bourigault, Dongpo Xu, and Danilo P. Mandic

   In International Joint Conference on Neural Networks (IJCNN), 2024

   Oral Presentation

   TL;DR arXiv

   TL;DR: We develop a robust quaternion recurrent neural network (QRNN) for real-time processing of 3D and 4D data with outliers. This is achieved by combining the real-time recurrent learning (RTRL) algorithm and the maximum correntropy criterion (MCC) as a loss function. While both the mean square error and maximum correntropy criterion are viable cost functions, it is shown that the non-quadratic maximum correntropy loss function is less sensitive to outliers, making it suitable for applications with multidimensional noisy or uncertain data. Both algorithms are derived based on the novel generalised HR (GHR) calculus, which allows for the differentiation of real functions of quaternion variables and offers the product and chain rules, thus enabling elegant and compact derivations.

2023

1. Convex Quaternion Optimization for Signal Processing: Theory and Applications

   Shuli Sun, Qiankun Diao, Dongpo Xu, Pauline Bourigault, and Danilo P. Mandic

   IEEE Transactions on Signal Processing, 2023

   TL;DR PDF

   TL;DR: Convex optimization methods have been extensively used in communications and signal processing. However, the theory of quaternion optimization is currently not as fully developed and systematic as that of complex and real optimization. To this end, we establish the convex optimization theory in quaternion variables based on the generalized Hamilton-real (GHR) calculus. This is achieved in a way that conforms with traditional complex and real optimization theory. We present several discriminant theorems for convex quaternion functions analogous to their complex counterparts. We also provide several discriminant criteria for strongly convex functions by the theorems of convex quaternion functions. Furthermore, we prove that the quaternion Newton method can converge in one step for positive definite quadratic quaternion functions and provide two applications in quaternion signal processing. These results provide a solid theoretical foundation for convex quaternion optimization and open avenues for further developments in quaternion signal processing applications.

2. The HR-Calculus: Enabling Information Processing with Quaternion Algebra

   Danilo P. Mandic, Soroush Pourya Talebi, Clive Cheong Took, Yili Xia, Dongpo Xu, Min Xiang, and Pauline Bourigault

   arXiv preprint arXiv:2311.16771, 2023

   TL;DR arXiv

   TL;DR: In this work, the foundations of the HR-calculus are revised and the required tools for deriving adaptive learning techniques suitable for dealing with quaternion-valued signals, such as the gradient operator, chain and product derivative rules, and Taylor series expansion are presented. This serves to establish important applications of adaptive information processing in the quaternion domain for both single-node and multi-node formulations.

2022

1. Timing of Hypoxia PET/CT Imaging after 18F-Fluoromisonidazole Injection in NSCLC Patients

   Pauline Bourigault, Michael Skwarski, Ruth E Macpherson, Geoff S Higgins, and Daniel McGowan

   Nature Scientific Reports, 2022

   PDF

2021

1. Investigation of Atovaquone-Induced Spatial Changes in Tumour Hypoxia

   Pauline Bourigault, Michael Skwarski, Ruth E Macpherson, Geoff S Higgins, and Daniel McGowan

   EJNMMI Research, 2021

   PDF