Research
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar
Neural Information Processing Systems (NeurIPS)
Oral Presentation
We release LeanDojo: an open-source playground consisting of toolkits, benchmarks, and models for LLMs to prove formal theorems in the Lean proof assistant. LeanDojo contains 1) tools for data extraction and interaction with Lean, 2) fine-grained annotations of where lemmas are used and defined, 3) a new benchmark of 97K human-written theorems from mathlib, and 4) a retrieval-augmented theorem prover using retrieval for relevant premise selection.
Spectrum Safety: Compatibility of NTS-3 Signals with GNSS Signals.
Rahul Chalamala, Joanna Hinks
Proceedings of the ION 2022 Joint Navigation Conference
Oral Presentation
We have analyzed the potential interference of Navigation Technology Satellite-3 (NTS-3) with existing GNSS signals using 1) a Python framework to calculate Spectral Separation Coefficients, 2) a methodology set by the ITU-R, 3) preliminary findings of negligible interference, and 4) exploration of strategies to mitigate any future risk.