In June, our research group released MLCEngine,
a universal LLM deployment engine powered by machine learning compilation.
MLCEngine is a single engine to enable LLM deployment across both cloud and edge devices, with full support for OpenAI API.
Performance has been one of the k…
Automated reasoning (AR) is a branch of artificial intelligence that applies various reasoning techniques to solve problems from mathematics and logic.
AR engines use clever optimizations and heuristics to solve typically intractable (e.g., NP-hard) problems.
Before a problem …
This post describes a part of our work NodeMedic-FINE, an automated tool to find arbitrary command injection and arbitrary code execution vulnerabilities in Node.js packages. While I am the sole author of this blog post, the work it describes was done in collaboration with Darion…
Randomness is a fundamental component of numerous real-world protocols. It is used everywhere, from ensuring fairness in the green card lottery to its application in clinical trials, financial audits, and various blockchain technologies.
For these protocols, randomness must satis…
In 2006, Senator Ted Stevens infamously described the Internet as a “series of tubes’‘, where “filled tubes’’ delayed his email. While Senator Stevens was ridiculed at the time for his simplistic understanding of the Internet, his characterization was not entirely wrong:
“It’s …
It is nearly inevitable that bugs will appear in a codebase during software development. To catch these bugs before they lead to real-world consequences,
the formal verification community has developed a wide variety of tools for ensuring code correctness. These tools fall
into t…
Satisfiability Modulo Theories (SMT) solvers are powerful tools
that answer logical and mathematical questions.
As an example, let’s say I want to know whether there exists integers
\(a, b, c\) such that \(3a^{2} -2ab -b^2c = 7\).
To ask an SMT solver, I need to write an SMT quer…
\[
\gdef\lf{\left \lfloor}
\gdef\rf{\right \rfloor}
\]
Imagine using a popular messaging app that includes a contact discovery feature to find which of your phone contacts are already using the service and to get information on how to communicate with them. While convenient, this…
Truly Anonymous Service Providers can offer users confirmed privacy, but also allow inappropriate behavior 😳
Anonymous Blocklisting permits blocking ill-behaved users without denanonymizing them. Specifically, the service provider blocks individual posts, and the benign users u…
In 2008, a groundbreaking development in the world of finance occurred: the birth of Bitcoin, the first decentralized digital currency. This innovation, introduced by blockchain technology, enables value transfer between parties without the need for traditional intermediaries lik…
