24 citations · 26 across the 8 of their papers we have counts for
8 papers
Imitation Learning for Connection-Tableau Construction
Fredrik Rømming, Mantas Bakšys, Martin S. Fixman +1
An automated theorem prover builds a proof step by step, choosing at each point what to add and what to remove. We cast this construction as a policy acting in a transition system…
WybeCoder: Verified Imperative Code Generation
Fabian Gloeckle, Mantas Baksys, Darius Feher +5
Recent progress in large language models (LLMs) has substantially advanced automatic code generation and formal theorem proving, yet software verification has not seen comparable g…
MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
Mantas Baksys, Stefan Zetzsche, Olivier Bouissou +1
LLMs excel at reasoning, but validating their steps remains challenging. Formal verification offers a solution through mechanically checkable proofs. Interactive theorem provers (I…
ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Mantas Baksys, Stefan Zetzsche, Olivier Bouissou +3
Large language models have become proficient at generating functional code, but ensuring the output truly matches the programmer's intent remains difficult. Testing improves trust,…
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
Haiming Wang, Mert Unsal, Xiaohan Lin +37
We introduce Kimina-Prover Preview, a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving, as showcased in this preview rele…
Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
Marco Dos Santos, Hugues de Saxcé, Haiming Wang +6
We introduce the Kimina Lean Server, an open-source project designed as a high-performance verifier for reinforcement learning pipelines. Built on top of the Lean REPL (Read-Eval-P…
Formal Mathematics Statement Curriculum Learning
Stanislas Polu, Jesse Michael Han, Kunhao Zheng +3
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 pr…
On number of different sized induced subgraphs of Bipartite-Ramsey graphs
Mantas Baksys, Xuanang Chen
In this paper, we investigate the set of sizes of induced subgraphs of bipartite graphs. We introduce the definition of -- graphs, which is closely related to…