arXiv subjects

Timothy Zhou

Publications and source records attributed to Timothy Zhou.

7 recordsLinked to original sources

arXiv2026

Language-Based Agent Control

This paper introduces language-based agent control (LBAC), a new programming model for agentic applications that brings techniques from programming languages and language-based security to the problem of agent control. In conventional programming, combinations of static typing and runtime enforcement have long been used to guarantee that well-typed programs satisfy user-specified policies, including policies for access control, information flow, data provenance, and more. The key idea behind LBAC is to extend these guarantees to agentic applications by requiring agents to generate programs that are themselves well typed in the context of the surrounding scaffolding code. Unsafe programs are rejected by the type-checker before execution, allowing policies to apply uniformly across the entire application, including both agent-generated behavior and developer-written scaffolding. At the same time, LBAC preserves substantial expressiveness: agents may perform arbitrary side-effect-free computation and recursively invoke subagents, which retain full tool access subject to the same -- or potentially more restrictive -- policies. We demonstrate LBAC with three case studies: I/O sandboxing via filesystem capabilities, data provenance, and information-flow control.

cs.PL↗

arXiv2025

ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models

Language models (LMs) can generate code but cannot guarantee its correctness$\unicode{x2014}$often producing outputs that violate type safety, program invariants, or other semantic properties. Constrained decoding offers a solution by restricting generation to only produce programs that satisfy user-defined properties. However, existing methods are either limited to syntactic constraints or rely on brittle, ad hoc encodings of semantic properties over token sequences rather than program structure. We present ChopChop, the first programmable framework for constraining the output of LMs with respect to semantic properties. ChopChop introduces a principled way to construct constrained decoders based on analyzing the space of programs a prefix represents. It formulates this analysis as a realizability problem which is solved via coinduction, connecting token-level generation with structural reasoning over programs. We demonstrate ChopChop's generality by using it to enforce (1) equivalence to a reference program and (2) type safety. Across a range of models and tasks, ChopChop improves success rates while maintaining practical decoding latency.

cs.PL↗

arXiv2025

Flexible and Efficient Grammar-Constrained Decoding

Large Language Models (LLMs) are often asked to generate structured outputs that obey precise syntactic rules, such as code snippets or formatted data. Grammar-constrained decoding (GCD) can guarantee that LLM outputs matches such rules by masking out tokens that will provably lead to outputs that do not belong to a specified context-free grammar (CFG). To guarantee soundness, GCD algorithms have to compute how a given LLM subword tokenizer can align with the tokens used by a given context-free grammar and compute token masks based on this information. Doing so efficiently is challenging and existing GCD algorithms require tens of minutes to preprocess common grammars. We present a new GCD algorithm together with an implementation that offers 17.71x faster offline preprocessing than existing approaches while preserving state-of-the-art efficiency in online mask computation.

cs.CL↗

arXiv2022

Passport: Improving Automated Formal Verification Using Identifiers

Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification, by learning from proof corpora to suggest proofs, have just begun to show their promise. These tools are effective because of the richness of the data the proof corpora contain. This richness comes from the stylistic conventions followed by communities of proof developers, together with the logical systems beneath proof assistants. However, this richness remains underexploited, with most work thus far focusing on architecture rather than making the most of the proof data. In this paper, we develop Passport, a fully-automated proof-synthesis tool that systematically explores how to most effectively exploit one aspect of that proof data: identifiers. Passport enriches a predictive Coq model with three new encoding mechanisms for identifiers: category vocabulary indexing, subword sequence modeling, and path elaboration. We compare Passport to three existing base tools which Passport can enhance: ASTactic, Tac, and Tok. In head-to-head comparisons, Passport automatically proves 29% more theorems than the best-performing of these base tools. Combining the three Passport-enhanced tools automatically proves 38% more theorems than the three base tools together, without Passport's enhancements. Finally, together, these base tools and Passport-enhanced tools prove 45% more theorems than the combined base tools without Passport's enhancements. Overall, our findings suggest that modeling identifiers can play a significant role in improving proof synthesis, leading to higher-quality software.

cs.PL↗

arXiv2021

How Packed Is It, Really?

The congestion of a curve is a measure of how much it zigzags around locally. More precisely, a curve $\pi$ is $c$-packed if the length of the curve lying inside any ball is at most $c$ times the radius of the ball, and its congestion is the minimum $c$ for which $\pi$ is $c$-packed. This paper presents a randomized $42$-approximation algorithm for computing the congestion of a curve (or any set of segments in the plane). It runs in $O( n \log^2 n)$ time and succeeds with high probability. Although the approximation factor is large, the running time improves over the previous fastest constant approximation algorithm, which took $\widetilde{O}(n^{4/3})$ time. We carefully combine new ideas with known techniques to obtain our new near-linear time algorithm.

cs.CG↗

arXiv2020

Improved Approximation Algorithms for Tverberg Partitions

$\newcommand{\floor}[1]{\left\lfloor {#1} \right\rfloor} \renewcommand{\Re}{\mathbb{R}}$ Tverberg's theorem states that a set of $n$ points in $\Re^d$ can be partitioned into $\floor{n/(d+1)}$ sets with a common intersection. A point in this intersection (aka Tverberg point) is a centerpoint of the input point set, and the Tverberg partition provides a compact proof of this, which is algorithmically useful. Unfortunately, computing a Tverberg point exactly requires $n^{O(d^2)}$ time. We provide several new approximation algorithms for this problem, which improve either the running time or quality of approximation, or both. In particular, we provide the first strongly polynomial (in both $n$ and $d$) approximation algorithm for finding a Tverberg point.

cs.CG↗

arXiv2019

Improved algorithms for Correlation Clustering with local objectives

Correlation Clustering is a powerful graph partitioning model that aims to cluster items based on the notion of similarity between items. An instance of the Correlation Clustering problem consists of a graph $G$ (not necessarily complete) whose edges are labeled by a binary classifier as ``similar'' and ``dissimilar''. An objective which has received a lot of attention in literature is that of minimizing the number of disagreements: an edge is in disagreement if it is a ``similar'' edge and is present across clusters or if it is a ``dissimilar'' edge and is present within a cluster. Define the disagreements vector to be an $n$ dimensional vector indexed by the vertices, where the $v$-th index is the number of disagreements at vertex $v$. Recently, Puleo and Milenkovic (ICML '16) initiated the study of the Correlation Clustering framework in which the objectives were more general functions of the disagreements vector. In this paper, we study algorithms for minimizing $\ell_q$ norms $(q \geq 1)$ of the disagreements vector for both arbitrary and complete graphs. We present the first known algorithm for minimizing the $\ell_q$ norm of the disagreements vector on arbitrary graphs and also provide an improved algorithm for minimizing the $\ell_q$ norm $(q \geq 1)$ of the disagreements vector on complete graphs. We also study an alternate cluster-wise local objective introduced by Ahmadi, Khuller and Saha (IPCO '19), which aims to minimize the maximum number of disagreements associated with a cluster. We also present an improved ($2 + \varepsilon$) approximation algorithm for this objective. Finally, we compliment our algorithmic results for minimizing the $\ell_q$ norm of the disagreements vector with some hardness results.

cs.DS↗