Showing cs.AIShow all
2 papers · 1 filter
cs.AI2026
P: Joint Program-and-Proof Planning for Verified Code Generation
Zenan Li, Ziran Yang, Peiyang Song +2
Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promi…
cs.AI2026
Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement
Jui-Hui Chung, Ziyang Cai, Zihao Li +14
We introduce Goedel-Architect, an agentic framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement. A blueprint is a dependency graph of defin…