7 papers
Exponential quantum advantage for learning signals with a single qubit
Ishaan Kannan, Sridhar Prabhu, Saeed A. Khan +7
Quantum technology has the potential to transform scientific discovery, but quantum advantages often require processing capabilities well beyond the reach of experimental platforms…
Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
Jialin Lu, Soonho Kong, Rodrigo Stehling +4
We present Lean Refactor, a plug-and-play retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs. LLM-generated proo…
Teaching LLMs Program Semantics via Symbolic Execution Traces
Jonas Bayer, Stefan Zetzsche, Olivier Bouissou +3
We introduce an evaluation framework of 500 C verification tasks across five property types (memory safety, overflow, termination, reachability, data races) built on SV-COMP 2025,…
s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
Balaji Rao, John Harrison, Soonho Kong +2
Neurosymbolic approaches leveraging Large Language Models (LLMs) with formal methods have recently achieved strong results on mathematics-oriented theorem-proving benchmarks. Howev…
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…
Learning Adaptive LLM Decoding
Chloe H. Su, Zhe Ye, Samuel Tenka +3
Decoding from large language models (LLMs) typically relies on fixed sampling hyperparameters (e.g., temperature, top-p), despite substantial variation in task difficulty and uncer…