Viktor Kun{\v{c}}ak

2 accepted papers

2025

RLMEval: Evaluating Research-Level Neural Theorem Proving

Auguste Poiroux, Antoine Bosselut, Viktor Kun{\v{c}}ak

EMNLP 2025

Despite impressive results on curated benchmarks, the practical impact of large language models (LLMs) on research-level neural theorem proving and proof autoformalization is still limited. We introduce RLMEval, an evaluation suite for these tasks, focusing on research-level mathematics from real-wo

Cited by 0 Source ↗PDF ↗Scholar ↗

2025

Reliable Evaluation and Benchmarks for Statement Autoformalization

Auguste Poiroux, Gail Weiss, Viktor Kun{\v{c}}ak, Antoine Bosselut

EMNLP 2025

Evaluating statement autoformalization, translating natural language mathematics into formal languages like Lean 4, remains a significant challenge, with few metrics, datasets, and standards to robustly measure progress. In this work, we present a comprehensive approach combining improved metrics, r

Cited by 0 Source ↗PDF ↗code ↗Scholar ↗