6 papers
OpenProver: Agentic and Interactive Theorem Proving with Lean 4
MatÄj Kripner, Milan Straka
In this system paper, we present OpenProver, an open-source system for LLM-driven automated theorem proving (ATP) with integrated Lean 4 formal verification. OpenProver integrates…
CorPipe at CRAC 2025: Evaluating Multilingual Encoders for Multilingual Coreference Resolution
Milan Straka
We present CorPipe 25, the winning entry to the CRAC 2025 Shared Task on Multilingual Coreference Resolution. This fourth iteration of the shared task introduces a new LLM track al…
Findings of the Fourth Shared Task on Multilingual Coreference Resolution: Can LLMs Dethrone Traditional Approaches?
Michal Novák, Miloslav KonopÃk, Anna Nedoluzhko +6
The paper presents an overview of the fourth edition of the Shared Task on Multilingual Coreference Resolution, organized as part of the CODI-CRAC 2025 workshop. As in the previous…
LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
MatÄj Kripner, Michal Å ustr, Milan Straka
Automated theorem proving (ATP) has been a classical problem in artificial intelligence since its inception, yet it remains challenging due to its vast state and action space. Larg…
Findings of the Third Shared Task on Multilingual Coreference Resolution
Michal Novák, Barbora Dohnalová, Miloslav KonopÃk +7
The paper presents an overview of the third edition of the shared task on multilingual coreference resolution, held as part of the CRAC 2024 workshop. Similarly to the previous two…
beeFormer: Bridging the Gap Between Semantic and Interaction Similarity in Recommender Systems
VojtÄch VanÄura, Pavel KordÃk, Milan Straka
Recommender systems often use text-side information to improve their predictions, especially in cold-start or zero-shot recommendation scenarios, where traditional collaborative fi…