29 citations · 73 across the 19 of their papers we have counts for
9 papers · 1 filter
Agentic Verified Optimization of Real-World Software
Zhe Ye, Udaya Ghai, Zhizhen Qin +2
Program optimization aims to improve performance while preserving behavior. Coding agents can already make programs faster by changing algorithms, data structures, and execution st…
TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science
Chutong Yang, Xiyuan Zhang, Yu Huang +7
Large language models perform strongly on competition mathematics, but their research-level reasoning remains difficult to evaluate systematically. Theoretical computer science (TC…
SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
Hojae Han, Jongyoon Kim, Sanghyeok Park +8
Autoformalization translates informal mathematical theorems into code for proof assistants such as Lean. A central challenge is that current evaluation metrics can accept type-corr…
Vero: Can AI Agents Build Formally Verified Software Repositories?
Zhe Ye, Hantao Lou, Yuechun Sun +8
AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an…
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,…
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…
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…