photo of the Redmond lab building entrance

Microsoft Research Lab – Redmond

News & features

In the news | Nature

Proof-assistant software handles an abstract concept at the cutting edge of research, revealing a bigger role for software in mathematics. Peter Scholze wants to rebuild much of modern mathematics, starting from one of its cornerstones. Now, he has received validation…

Diagram: The proposed SOLOIST model architecture and training objectives. Dialog history, Belief state, DB state, and Response make up the pipeline. Task 1, belief state prediction, corresponds with belief state. Task 2 and Task 3, grounded response generation and contrastive objective correspond with response. A user is shown thinking a goal, which points from the dialog history to the user (response), and then back to dialog history (input). Belief state points down to an image of a computer server (Belief state query) and then back to DB State (DB state results). The server points to readouts labeled “entity.”
Microsoft Research Blog

| Baolin Peng, Chunyuan Li, Jinchao Li, Lars Liden, and Jianfeng Gao

The increasing use of personal assistants and messaging applications has spurred interest in building task-oriented dialog systems (or task bots) that can communicate with users through natural language to accomplish a wide range of tasks, such as restaurant booking, weather…

A chart showing a GAN comparing fake images with real images, filtering them through a discriminator to produce a value indicating how fake the image is.
Microsoft Research Blog

| Zeyuan Allen-Zhu and Yuanzhi Li

A Generative adversarial network, or GAN, is one of the most powerful machine learning models proposed by Goodfellow et al. (opens in new tab) for learning to generate samples from complicated real-world distributions. GANs have sparked millions of applications, ranging…

Awards | A Taxonomy of Sounds in Virtual Reality

In the news | Microsoft Research Website

Dhruv “DJ” Jain, an intern alumni of the Microsoft Research Ability group, has been named a recipient of the 2021 Microsoft Research Dissertation Grant for his dissertation titled “Sound Sensing and Feedback Techniques for Deaf and Hard of Hearing Users”.…

A graphic depicting audio and video content items passing through an audio transformer layer and a video transformer layer, respectively, before being combined while passing through a multimodal transformer layer
Microsoft Research Blog

| Yale Song

Understanding video is one of the most challenging problems in AI, and an important underlying requirement is learning multimodal representations that capture information about objects, actions, sounds, and their long-range statistical dependencies from audio-visual signals. Recently, transformers have been successful in…

GamesBond VR Prototype
Microsoft Research Blog

| Michel Pahud, Mike Sinclair, and Andrea Bianchi

Editor’s Note: Bimanual controllers are frequently used to enhance the realism and immersion of virtual reality experiences such as games and simulations. Researchers have typically relied on mechanical linkages between the controllers to recreate the sensation of holding different objects…

Awards | Fast Company

Microsoft’s Premonition platform—a winner of Fast Company’s 2021 World Changing Ideas Awards—tracks, captures, and analyzes mosquitoes, to give health officials a sense of what pathogens are circulating in the area.

An animation showing an example of a high-level language message format specified by EverParse. From the message, two arrows labeled “EverParse” point to a rectangle labeled “formal specification” and a rectangle labeled “low-level implementation,” respectively, inside a larger rectangle labeled “F* code.” The figure represents EverParse’s ability to automatically generate safe, correct, and fast F* parsing code. “Correctness” is defined as “Correctness: ​parse (serialize msg) = msg​” and “valid msg ==> serialize (parse msg) = msg​.” The F* logo appears with the description that F* is a type theory–based programming language and proof assistant that can prove theorems about programs​. From the “F* code” rectangle, arrows point from the “low-level implementation” rectangle and a rectangle labeled “verified libraries for combinators” to a rectangle labeled “Safe high-performance C code.”
Microsoft Research Blog

| Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy

EverParse (opens in new tab) is a framework for generating provably secure parsers and formatters used to improve the security of critical code bases at Microsoft. EverParse is developed as part of Project Everest (opens in new tab), a collaboration…