In March, 2024, researchers discovered a backdoor hidden in an update of open-source Linux tool XZ Utils – a vulnerability that appears likely to be the result of a multi-year, state-sponsored supply chain attack. This latest close call is only the most recent in a growing history of incidents underscoring the fragility of a modern […]
Read More
Growing up, Taisa Kushner loved math. There was a functional elegance to the way mathematical techniques could be used to unravel even the most complex problems, and how seemingly disparate systems were linked through simple equations. But she enjoyed the biological sciences too, and wanted to find a career where she could use her skills […]
Read More
Illegal, Unreported, and Unregulated (IUU) fishing represents a significant global threat to our shared natural resources, undermining the sustainability of fish stocks, damaging ocean ecosystems, and robbing nations of their natural heritage and economic foundation. Nowhere is this challenge more acute than in the Galapagos Marine Reserve (GMR), a biodiversity hotspot of extreme ecological significance. […]
Read More
At Galois, we have been experimenting with multiple Large Language Models (LLMs), including GPT-4. Part of the motivation for this is to continue increasing the accessibility and utility of our formal verification and software assurance tools. While these tools provide high assurance for critical software, they can require significant expertise or time to extract full […]
Read More
There has been a lot of chatter recently about large language models, including GPT-4 and LLaMa. At Galois, we have been experimenting with GPT-4, the most capable available large language model. One group of intriguing results that I am excited to present is in the creation of SAWScript memory safety proofs. Using a very simple […]
Read More
Organizations seeking to integrate digital-first practices into their engineering processes often rapidly discover a common roadblock: critical dependencies on the individual expertise of specific employees embedded in legacy workflows. Discovering this issue has prompted some to ask what role might generative technologies play in supporting digital engineering transformation efforts: “Can they help us reduce reliance […]
Read More
We’ve all seen it—a couple on a date, politicians, friends, or colleagues talking right past each other, trapped in a moment of profound misunderstanding over the meaning of a single word. For me, that moment came when my partner, a New Yorker through and through, told me, a Midwesterner, to take “the next left” while […]
Read More
Thus far in our ongoing series on artificial intelligence we’ve spoken in depth on questions of trust, human perception, and limitations of generative models. We have focused specifically on large language models (LLMs), due in part to their recent successes and media attention. We’ve explored questions of data, testing, and broad model implications. However, LLMs […]
Read More
In my ongoing efforts to deeply engage with research into large language models, I have continually wrestled with and confronted a persistent sense of dissatisfaction. Unfortunately, the source of my dissatisfaction has also been frustratingly difficult to articulate and to pin down. At times, I have wondered if I’m not dissatisfied but rather uneasy because […]
Read More
A broken 12-hour clock is correct for its assigned job – telling the time – twice a day. It is correct for an alternative job – being a paperweight – almost all the time. Then again, even as a paperweight, a broken clock might perform terribly if we use it to hold paper to a […]
Read More