The optimization of expensive black-box functions is ubiquitous in science and engineering. A common solution to this problem is Bayesian optimization (BO), which is generally comprised of two components: (i) a surrogate model and (ii) an acquisition function, which generally require expensive re-training and optimization steps at each iteration, respectively. Although recent work enabled in-context surrogate models that do not require re-training, virtually all existing BO methods still require acquisition function maximization to select the next observation, which introduces many knobs to tune, such as Monte Carlo samplers and multi-start optimizers. In this work, we propose a completely in-context, zero-shot solution for BO that does not require surrogate fitting or acquisition function optimization. This is done by using a pre-trained deep generative model to directly sample from the posterior over the optimum point. We show that this process is equivalent to Thompson sampling and demonstrate the capabilities and cost-effectiveness of our foundation model on a suite of real-world benchmarks. We achieve an efficiency gain of more than 35x in terms of wall-clock time when compared with Gaussian process-based BO, enabling efficient parallel and distributed BO, e.g., for high-throughput optimization.

Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present AutoVerus. AutoVerus uses LLM to automatically generate correctness proof for Rust code. AutoVerus is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. AutoVerus consists of a network of LLM agents that are crafted and orchestrated to mimic human experts' three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate AutoVerus and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that AutoVerus can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.

W3C Standards Work: FIBO is expressed in the standard W3C semantic modeling language, OWL, which is natively supported by the Anzo Smart Data Lake. Loading FIBO into Anzo was a simple import function. FIBO Works: There was an excellent match between the FIBO model and the data sources (Front Arena and Dun & Bradstreet). Mapping & Loading Data is Easy: The alignment between FIBO and the data sources made mapping fast and easy. Once mapped, data loading and transformation was automatic.

W3C Standards Work: FIBO is expressed in the standard W3C semantic modeling language, OWL, which is natively supported by the Anzo Smart Data Lake. Loading FIBO into Anzo was a simple import function. FIBO Works: There was an excellent match between the FIBO model and the data sources (Front Arena and Dun & Bradstreet). Mapping & Loading Data is Easy: The alignment between FIBO and the data sources made mapping fast and easy. Once mapped, data loading and transformation was automatic.