6 papers
Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny
Chuanhao Yan, Fengdi Che, Xuhan Huang +12
Existing informal language-based (e.g., human language) Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification proce…
OPD-Evolver: Cultivating Holistic Agent Evolver via On-Policy Distillation
Guibin Zhang, Xun Xu, Yanwei Yue +4
Memory has become a standard substrate for self-evolving agents, yet retaining experience is not the same as learning how to evolve through it. Existing memory agents can store tra…
VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
Lingfei Zeng, Fengdi Che, Xuhan Huang +4
Formal verification is the next frontier for ensuring the correctness of code generated by Large Language Models (LLMs). While methods that co-generate code and formal specificatio…
Aligning LLMs with Graph Neural Solvers for Combinatorial Optimization
Shaodi Feng, Zhuoyi Lin, Yaoxin Wu +4
Recent research has demonstrated the effectiveness of large language models (LLMs) in solving combinatorial optimization problems (COPs) by representing tasks and instances in natu…
AnalogAgent: Self-Improving Analog Circuit Design Automation with LLM Agents
Zhixuan Bao, Zhuoyi Lin, Jiageng Wang +5
Recent advances in large language models (LLMs) suggest strong potential for automating analog circuit design. Yet most LLM-based approaches rely on a single-model loop of generati…
Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
Xu Xu, Xin Li, Xingwei Qu +2
We introduce DafnyCOMP, a benchmark for evaluating large language models (LLMs) on compositional specification generation in Dafny. Unlike prior benchmarks that focus on single-fun…