Thomas Voice — accepted AI-conference papers

2026

Hilbert: Recursively Building Formal Proofs with Informal Reasoning

Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, Ke Ye

ICLR 2026poster

Large Language Models (LLMs) demonstrate impressive mathematical reasoning abilities, but their solutions frequently contain errors that cannot be automatically verified. Formal theorem proving systems such as Lean 4 offer automated verification with complete accuracy, motivating recent efforts to b…

Cited by 0 Source ↗Scholar ↗

2026

Reusing Pre-Training Data at Test Time is a Compute Multiplier

Alex Fang, Thomas Voice, Ruoming Pang, Ludwig Schmidt, Tom Gunter

ICLR 2026poster

Large language models learn from their vast pre-training corpora, gaining the ability to solve an ever increasing variety of tasks; yet although researchers work to improve these datasets, there is little effort to understand how efficient the pre-training apparatus is at extracting ideas and knowle…

Cited by 0 Source ↗Scholar ↗