Jiening Siow

Amy Xin, Jiening Siow, Junjie Wang et al.

LLM-based agents have shown increasing potential in automating scientific discovery. Given an optimizable metric and an execution environment, they can propose, validate, and iterate scientific solutions, and have produced results that outperform human-designed approaches. As model capabilities continue to improve, we argue that the bottleneck for autonomous scientific discovery is shifting from prescribing agent workflows to designing agent environments: the resources, constraints, and interfaces that shape agent behavior. We frame this as environment engineering: building environments that amplify productive behaviors, such as open-ended exploration, systematic artifact management, and inter-agent collaboration, while suppressing harmful behaviors, such as reward hacking and high-friction human oversight. We present EurekAgent, an environment-engineered agent system for metric-driven autonomous scientific discovery. EurekAgent engineers the environment along four dimensions: permissions engineering for bounded agent execution and isolated evaluation; artifact engineering for filesystem and Git-based collaboration; budget engineering for budget-aware exploration; and human-in-the-loop engineering for easy human supervision and intervention. EurekAgent sets new state-of-the-art results on multiple mathematics, kernel engineering, and machine learning tasks, including new state-of-the-art 26-circle packing results discovered with less than $11 in total API cost. We open-source our code and results, and call for environment engineering as a core research direction for developing reliable autonomous research agents.

Jiening Siow, Hanrui Zuo, Hanyun Jiang et al.

Program analyzers often issue batches of SMT queries that share a large symbolic context and differ only in a small predicate. We formalize this recurring pattern as \emph{Shared-Context Batched Satisfiability}: given a formula $φ$ and predicates $P$, determine whether $φ\land p$ is satisfiable for each $p \in P$. We study three theory-agnostic strategies for this problem: predicate-by-predicate checking, disjunctive over-approximation, and Core-Literal Filter (CLF), a new algorithm that learns literals inconsistent with $φ$ and uses them to reject later predicates. Our evaluation on symbolic abstraction and active property checking shows that no strategy dominates universally: over-approximation is fastest on solved symbolic-abstraction queries, while CLF increases the number of solved hard instances and is fastest on active property checking. We advocate treating shared-context batched satisfiability as a first-class primitive in design program analyzers and exploring the algorithmic design space more systematically.