29 citations · 73 across the 19 of their papers we have counts for
22 papers
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…
ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Mantas Baksys, Stefan Zetzsche, Olivier Bouissou +3
Large language models have become proficient at generating functional code, but ensuring the output truly matches the programmer's intent remains difficult. Testing improves trust,…
Certified Control: An Architecture for Verifiable Safety of Autonomous Vehicles
Daniel Jackson, Valerie Richmond, Mike Wang +6
Widespread adoption of autonomous cars will require greater confidence in their safety than is currently possible. Certified control is a new safety architecture whose goal is two-…
Better AI through Logical Scaffolding
Nikos Arechiga, Jonathan DeCastro, Soonho Kong +1
We describe the concept of logical scaffolds, which can be used to improve the quality of software that relies on AI components. We explain how some of the existing ideas on runtim…
Delta-Decision Procedures for Exists-Forall Problems over the Reals
Soonho Kong, Armando Solar-Lezama, Sicun Gao
Solving nonlinear SMT problems over real numbers has wide applications in robotics and AI. While significant progress is made in solving quantifier-free SMT formulas in the domain,…
REAS: Combining Numerical Optimization with SAT Solving
Jeevana Priya Inala, Sicun Gao, Soonho Kong +1
In this paper, we present ReaS, a technique that combines numerical optimization with SAT solving to synthesize unknowns in a program that involves discrete and floating point comp…
Elaboration in Dependent Type Theory
Leonardo de Moura, Jeremy Avigad, Soonho Kong +1
To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring inform…
Towards Personalized Prostate Cancer Therapy Using Delta-Reachability Analysis
Bing Liu, Soonho Kong, Sicun Gao +2
Recent clinical studies suggest that the efficacy of hormone therapy for prostate cancer depends on the characteristics of individual patients. In this paper, we develop a computat…
Proof Generation from Delta-Decisions
Sicun Gao, Soonho Kong, Edmund Clarke
We show how to generate and validate logical proofs of unsatisfiability from delta-complete decision procedures that rely on error-prone numerical algorithms. Solving this problem…
Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions
Bing Liu, Soonho Kong, Sicun Gao +2
A central problem in systems biology is to identify parameter values such that a biological model satisfies some behavioral constraints (\eg, time series). In this paper we focus o…
Delta-Complete Analysis for Bounded Reachability of Hybrid Systems
Sicun Gao, Soonho Kong, Wei Chen +1
We present the framework of delta-complete analysis for bounded reachability problems of general hybrid systems. We perform bounded reachability checking through solving delta-deci…
SReach: A Bounded Model Checker for Stochastic Hybrid Systems
Qinsi Wang, Paolo Zuliani, Soonho Kong +2
In this paper we describe a new tool, SReach, which solves probabilistic bounded reachability problems for two classes of stochastic hybrid systems. The first one is (nonlinear) hy…
Revisiting the Complexity of Stability of Continuous and Hybrid Systems
Sicun Gao, Soonho Kong, Edmund Clarke
We develop a framework to give upper bounds on the "practical" computational complexity of stability problems for a wide range of nonlinear continuous and hybrid systems. To do so,…
Satisfiability Modulo ODEs
Sicun Gao, Soonho Kong, Edmund Clarke
We study SMT problems over the reals containing ordinary differential equations. They are important for formal verification of realistic hybrid systems and embedded software. We de…