3 papers
cs.LG2025
ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
Alex Gu, Bartosz Piotrowski, Fabian Gloeckle +2
Neural theorem proving has advanced rapidly in the past year, reaching IMO gold-medalist capabilities and producing formal proofs that span thousands of lines. Although such proofs…
cs.AI2025
Lightweight Latent Verifiers for Efficient Meta-Generation Strategies
Bartosz Piotrowski, Witold Drzewakowski, Konrad Staniszewski +1
Verifiers are auxiliary models that assess the correctness of outputs generated by base large language models (LLMs). They play a crucial role in many strategies for solving reason…
cs.LG2024
Repurposing Language Models into Embedding Models: Finding the Compute-Optimal Recipe
Alicja Ziarko, Albert Q. Jiang, Bartosz Piotrowski +3
Text embeddings are essential for many tasks, such as document retrieval, clustering, and semantic similarity assessment. In this paper, we study how to contrastively train text em…