4 papers
Reset Early, Reset Often, Eliminate Models
Martin S. Fixman, Fredrik Rømming, Sean B. Holden
Connection-tableau provers typically construct closed tableaux by backtracking search. This gives lightweight proof procedures, but their low-memory search state leaves little deri…
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…