8 papers
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…
LeAct: Learning to Reason from Expert Actions
Ziran Yang, Chengshuai Shi, Raj Ghugare +3
Modern reasoning models depend on reasoning data, today sourced from human annotations or distilled from stronger LLMs. However, a rich and largely untapped source of supervision l…
MLS-Bench: A Holistic and Rigorous Assessment of AI Systems on Building Better AI
Bohan Lyu, Yucheng Yang, Siqiao Huang +25
Modern AI progress has been driven by ML methods that are generalizable across settings and scalable to larger regimes. As large language models demonstrate advanced capabilities i…
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…
AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
Haoyu Zhao, Ziran Yang, Jiawei Li +6
Vericoding refers to the generation of formally verified code from rigorous specifications. Recent AI models show promise in vericoding, but a unified methodology for cross-paradig…
Odysseus: Scaling VLMs to 100+ Turn Decision-Making in Games via Reinforcement Learning
Chengshuai Shi, Wenzhe Li, Xinran Liang +10
Given the rapidly growing capabilities of vision-language models (VLMs), extending them to interactive decision-making tasks such as video games has emerged as a promising frontier…