The field of formal verification is all about using mathematically rigorous techniques and tools to prove properties about systems. The applications of formal verification vary widely. There are computer-checked correctness proofs for critical pieces of software such as compilers…
How do we allocate items among individuals with different preferences in a way that is both fair and efficient?
Striking this balance is a fundamental challenge in economics and game theory, with implications ranging from inheritance division and divorce settlements to resourc…
The content of this blog post is derived from the research paper Computing Game Symmetries and Equilibria That Respect Them, published at AAAI-25, and authored by Emanuel Tewolde, Brian Hu Zhang, Caspar Oesterheld, Tuomas Sandholm, and Vincent Conitzer.
TL;DR: We discuss the impl…
Modern AI excels at pattern recognition but suffers when faced with logical reasoning tasks. What happens when we ask a neural network to solve a Sudoku puzzle from an image, verify a mathematical proof, or diagnose a medical condition based on a set of symptoms and rules? These…
Key takeaway: When learning over discrete prompts used in modern vision-language models, classical PAC-Bayes bounds turn out to be remarkably tight — significantly tighter than prior PAC-Bayes results on deep networks.
If you have ever tinkered with a large vision-language model …
This post explains the key findings and algorithm of our 2023 SIGGRAPH paper “Winding Numbers on Discrete Surfaces”.
For a given point on a surface, we would like to know whether it is inside or outside a given curve.
For example, coloring points on this cow according to inside…
In this post, I’ll be discussing my part of my work on how to use compiler
analysis to aid in optimizing memory allocation.
I will begin with some background and motivation, and then introduce my
proposed workflow as well as some interesting
challenges that this work involves.
C…
I’ll start by introducing the main idea behind safe Pareto improvements with an example (without game-theoretic terminology).
I then give some very basic background on game theory, both to motivate safe (Pareto) improvements and to describe safe Pareto improvements more precise…
Large language models (LLMs) represent a promising but controversial assistant in the process of preparing and reviewing scientific papers. They may serve as useful analytical tools to scrutinize manuscripts and identify possible weaknesses or inaccuracies that need addressing. H…
The workload of state-vector quantum circuit simulation is massively parallel. Most quantum gates multiply one small matrix to many vectors, and the workload is balanced.
Challenge: the state vector is too large to be stored on one GPU, and the communication cost is very high. …
