Search for: All records

Automated planning is traditionally the domain of experts, utilized in fields like manufacturing and healthcare with the aid of expert planning tools. Recent advancements in LLMs have made planning more accessible to everyday users due to their potential to assist users with complex planning tasks. However, LLMs face several application challenges within end-user planning, including consistency, accuracy, and user trust issues. This paper introduces VeriPlan, a system that applies formal verification techniques, specifically model checking, to enhance the reliability and flexibility of LLMs for end-user planning. In addition to the LLM planner, VeriPlan includes three additional core features—a rule translator, flexibility sliders, and a model checker—that engage users in the verification process. Through a user study (𝑛 = 12), we evaluate VeriPlan, demonstrating improvements in the perceived quality, usability, and user satisfaction of LLMs. Our work shows the effective integration of formal verification and user-control features with LLMs for end-user planning tasks. 

In this paper, we consider how to provide fast estimates of flow-level tail latency performance for very large scale data center networks. Network tail latency is often a crucial metric for cloud application performance that can be affected by a wide variety of factors, including network load, inter-rack traffic skew, traffic burstiness, flow size distributions, oversubscription, and topology asymmetry. Network simulators such as ns-3 and OMNeT++ can provide accurate answers, but are very hard to parallelize, taking hours or days to answer what if questions for a single configuration at even moderate scale. Recent work with MimicNet has shown how to use machine learning to improve simulation performance, but at a cost of including a long training step per configuration, and with assumptions about workload and topology uniformity that typically do not hold in practice. We address this gap by developing a set of techniques to provide fast performance estimates for large scale networks with general traffic matrices and topologies. A key step is to decompose the problem into a large number of parallel independent single-link simulations; we carefully combine these link-level simulations to produce accurate estimates of end-to-end flow level performance distributions for the entire network. Like MimicNet, we exploit symmetry where possible to gain additional speedups, but without relying on machine learning, so there is no training delay. On a large-scale net- work where ns-3 takes 11 to 27 hours to simulate five seconds of network behavior, our techniques run in one to two minutes with accuracy within 9% for tail flow completion times. 

CRISPR-Cas–guided base editors convert A•T to G•C, or C•G to T•A, in cellular DNA for precision genome editing. To understand the molecular basis for DNA adenosine deamination by adenine base editors (ABEs), we determined a 3.2-angstrom resolution cryo–electron microscopy structure of ABE8e in a substrate-bound state in which the deaminase domain engages DNA exposed within the CRISPR-Cas9 R-loop complex. Kinetic and structural data suggest that ABE8e catalyzes DNA deamination up to ~1100-fold faster than earlier ABEs because of mutations that stabilize DNA substrates in a constrained, transfer RNA–like conformation. Furthermore, ABE8e’s accelerated DNA deamination suggests a previously unobserved transient DNA melting that may occur during double-stranded DNA surveillance by CRISPR-Cas9. These results explain ABE8e-mediated base-editing outcomes and inform the future design of base editors.