Our projects

Pythagoras-Prover

A compute-efficient family of Lean theorem provers that combines autoregressive and diffusion-based models with curriculum learning and synthetic data generation. Augmented Lean Formalisation expands proof corpora without recompilation, achieving competitive results at small (4B parameter) scale.

PiShield

PiShield is the first package ever allowing for the integration of the requirements into the neural networks' topology, guaranteeing compliance with these requirements, regardless of input.

ROAD-R

ROAD-R is the first autonomous driving dataset annotated with logical requirements. Extending the ROAD dataset, it contains a set of 243 requirements over 41 labels grouped into agents, actions and locations.