Aws Albarghouthi retweeted
Ah, another beautiful question in quantum complexity theory solved! This one is due to Scott Aaronson and @AAmbainis, about the necessity of structure in a problem for exponential quantum advantage. This question inspired a lot of research and we collectively learned a lot about quantum computing from it.
The problem seemed ripe; this year it felt like we were closing in on it. The most recent (human-written) papers on it had solved special cases showing that parallel quantum algorithms cannot achieve exponential speedups for unstructured problems.
What is the next beautiful question in quantum algorithms that will spur another generation of learning and understanding?
* Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, Quantum Speedups Require Structure or Depth (arxiv.org/abs/2608.19158)
* Qipeng Liu, Saachi Mutreja (my fantastic student!), Parallel Quantum Advantage with Limited Adaptivity Requires Structure (arxiv.org/abs/2608.20297)
The problem seemed ripe; this year it felt like we were closing in on it. The most recent (human-written) papers on it had solved special cases showing that parallel quantum algorithms cannot achieve exponential speedups for unstructured problems.
What is the next beautiful question in quantum algorithms that will spur another generation of learning and understanding?
* Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, Quantum Speedups Require Structure or Depth (arxiv.org/abs/2608.19158)
* Qipeng Liu, Saachi Mutreja (my fantastic student!), Parallel Quantum Advantage with Limited Adaptivity Requires Structure (arxiv.org/abs/2608.20297)
Today Physical Superintelligence PBC is announcing a proof of the Aaronson-Ambainis conjecture, one of the central open problems in quantum complexity, with major implications for quantum computing speedup.
psi.inc/research/aaron…
Thread 👇
6
41
181
21,465
Aws Albarghouthi retweeted
Happy to announce that our FV Job Board now has a RSS 2.0 feed! Now you can follow the newest job updates through your favorite RSS feed reader.
typetheoryforall.github.io/FVjobs/
As always, this is a community project and job updates and PRs are very welcome!
typetheoryforall.github.io/FVjobs/
As always, this is a community project and job updates and PRs are very welcome!
0
8
69
14,976
🔥
Just about to give a seminar at the University of Glasgow on Why The World of Formal Verification is On Fire! @GlasgowCS @UofGlasgow
0
0
5
406
Aws Albarghouthi retweeted
I'm thrilled to bring &Truth out of stealth as its co-founder and Chief Science Officer. With a team I'm proud to be part of, we're setting out to specify and prove all the world's software correct and secure.
If you geek out over code people can understand and trust, join us!
If you geek out over code people can understand and trust, join us!
We are out of stealth! As AI writes more code, we're building tools to prove programs meet precise requirements, with Lean proofs anyone can independently check. Let's make verified software the norm in every language and application.
Come take a look: andtruth.com
25
49
496
26,114
Aws Albarghouthi retweeted
An internal model at OpenAI has produced a claimed refutation of ETH! Russell Impagliazzo, Mohan Paturi, and I have been asked to help organize an open and independent examination of this claim. 1/4
304
792
7,419
3,760,396
Aws Albarghouthi retweeted
The bitter lesson of ML is that scale eats all. The bitter lesson of PL is that [efficient] brute force eats all.
The results from Anthropic + Theorem feel like a “bitter lesson” moment for formal verification. They just went for semantics-level proofs. No fancy program logics, proof techniques or algorithms. Just bare metal proofs with a vanilla Hoare logic over RISC-V.
4
17
111
6,787
The results from Anthropic + Theorem feel like a “bitter lesson” moment for formal verification. They just went for semantics-level proofs. No fancy program logics, proof techniques or algorithms. Just bare metal proofs with a vanilla Hoare logic over RISC-V.
25
5
218
23,197
Aws Albarghouthi retweeted
in 1948, Turing introduced "unorganized machines", machines that learn, which we now call neural nets.
in 1949, in "Checking a large routing", Turing introduced formal verification (Floyd-Hoare triples).
Today, neural nets do formal verification. Pretty wild.
in 1949, in "Checking a large routing", Turing introduced formal verification (Floyd-Hoare triples).
Today, neural nets do formal verification. Pretty wild.
0
2
30
1,726
Aws Albarghouthi retweeted
This seems like a good time to remind everyone that northeastern is hiring tenure track faculty in formal methods and ai. Apply!
0
2
3
268
The trajectory is clear
New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time).
With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks.
Read our research in full here: anthropic.com/research/forma…
6
17
112
6,542
Aws Albarghouthi retweeted
We should rebrand Formal Verification to Proof Against the Machine
1
7
59
2,064
Aws Albarghouthi retweeted
I've discovered that all popular quantum computing SDKs / compilers have serious bugs when it comes to handling angles -- floating point strikes again!
IBM's Qiskit, Google's Cirq, Rigetti's quilc, IQM's Qrisp, NVIDIA's CUDA-Q, Xanadu's PennyLane, qBraid's SDK, ...
🧵1/n
IBM's Qiskit, Google's Cirq, Rigetti's quilc, IQM's Qrisp, NVIDIA's CUDA-Q, Xanadu's PennyLane, qBraid's SDK, ...
🧵1/n
3
1
29
1,932
Aws Albarghouthi retweeted
Models are sycophantic, and when they do challenge faulty or incorrect inputs, they're ambiguous and ineffective.
In a new paper w/ multilingual co-authors, we find that people may view LM responses that push back, yet still end up believing false content is true.
In a new paper w/ multilingual co-authors, we find that people may view LM responses that push back, yet still end up believing false content is true.
4
21
99
5,238
Aws Albarghouthi retweeted
More cake to celebrate Francis Halzen’s well-deserved Nobel Prize @NobelPrize ! 🎂 Proud to be part of UW–Madison Physics @UWMadPhysics, where extraordinary science continues to happen. Here’s to more discoveries—and more milestones worth celebrating—in the years ahead!
0
3
22
710
I used to Claude to build some security tool. It built the thing. Then at some point it realized it’s debugging a security tool and the guardrails kicked in 😂
1
0
18
1,251
I've discovered that all popular quantum computing SDKs / compilers have serious bugs when it comes to handling angles -- floating point strikes again!
IBM's Qiskit, Google's Cirq, Rigetti's quilc, IQM's Qrisp, NVIDIA's CUDA-Q, Xanadu's PennyLane, qBraid's SDK, ...
🧵1/n
IBM's Qiskit, Google's Cirq, Rigetti's quilc, IQM's Qrisp, NVIDIA's CUDA-Q, Xanadu's PennyLane, qBraid's SDK, ...
🧵1/n
3
1
29
1,932
IMO, any future experimental claims should come with the entire software stack. Otherwise, take them with a grain of salt and a shot of Guadalajara's heaviest offerings.
5/n
5/n
1
0
2
161