2 papers
cs.LG2026
VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving
Manish Acharya, Zhenyu Liao, Yueke Zhang +3
LLM-based formal provers often collapse rich verifier signals (syntax errors, type mismatches, partial goal progress) into a binary pass/fail bit. We present VERITAS, a zero-shot f…
cs.LG2026
Intent-aligned Formal Specification Synthesis via Traceable Refinement
Zhe Ye, Aidan Z. H. Yang, Huangyuan Su +6
Large language models are increasingly used to generate code from natural language, but ensuring correctness remains challenging. Formal verification offers a principled way to obt…