Mantas Baksys — accepted AI-conference papers

2026

MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

Mantas Baksys, Sean B Holden, Olivier Bouissou, Stefan Zetzsche

ICML 2026poster

LLMs excel at reasoning, but validating their steps remains challenging. Formal verification offers a solution through mechanically checkable proofs. Interactive theorem provers (ITPs) dominate mathematical reasoning but require detailed low-level proof steps, while auto-active verifiers offer autom…

Cited by 0 Source ↗Scholar ↗

2023

Formal Mathematics Statement Curriculum Learning

Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, Ilya Sutskever

ICLR 2023top-25%

We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a…

Cited by 177 Source ↗PDF ↗code ↗Scholar ↗