Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification
Program verification establishes software correctness through machine-checkable proofs constructed in theorem provers. It's a guarantee especially valuable for code generated by large language models (LLMs), which is fluent but carries no assurance of correctness. Almost all existing provers, however, pursue pass rates...
Shuang-Jie Yao, Nikolaus Holzer, Mark Santolucito et al.
· 0 citations