Microsoft Research
Microsoft Research is Microsoft’s research organization, working across disciplines on scientific discovery and technology innovation, with a stated focus on challenges relevant to Microsoft and society.
Machine Learning Turns PDE Singularity Search Into Computer-Assisted Proof
Caltech applied math PhD candidate Yixuan Wang argues that high-precision computation can make singularity questions in nonlinear PDEs tractable only when it is tied to stability analysis and rigorous verification. In a Microsoft Research seminar on Navier-Stokes blowup and weak-solution nonuniqueness, Wang presents machine-learning tools such as PINNs, neural operators, and Kolmogorov–Arnold Networks as ways to discover candidate singular structures, not as substitutes for proof. His broader case is that numerics, analytical a posteriori estimates, and interval-certified computation must work together if singularities in systems such as Navier-Stokes are to be identified and verified.
Wavelet Score Models Show Local Interactions Drive Diffusion Denoising
Emma Finn argues that the memorization puzzle in diffusion models can be probed by replacing a black-box score network with an analytically solvable wavelet parameterization. In her Microsoft Research New England seminar, Finn presents the method as a way to isolate which data moments and dependency structures matter across noise scales. Her reported experiments on MNIST suggest that local same-scale wavelet interactions improve denoising more consistently than independent coefficient models or orientation-only coupling, while the larger question of whether the framework explains generative novelty remains unresolved.
Energy-Based Fine-Tuning Trains Language Models on Whole Responses
Microsoft Research’s presentation on energy-based fine-tuning argues that language-model post-training can be aimed at whole responses rather than next-token imitation. Carles Domingo-Enrich presents EBFT as a middle path between supervised fine-tuning and reinforcement learning: it samples model completions, compares them with ground-truth answers in a model-derived feature space, and turns that comparison into a policy-gradient update without a separate reward model or verifier. The reported results show gains over SFT on several coding and translation measures, with performance often comparable to RLVR while avoiding explicit correctness rewards.
AI’s Biggest Disruption Requires Rebuilding Markets Around Agents
David Rothschild argues that AI’s largest economic effects will come less from better models than from whether workflows and markets are rebuilt for agents rather than humans. In his Microsoft Research Forum talk and related work on agentic markets, he says the key question is architectural: open systems could reduce communication friction and spread welfare gains, while closed platforms could use the same capabilities to reinforce incumbency. The transition, in his account, depends on choices about delegation, monitoring, auditability, and market access that are being made before the full disruption is visible.
Interwhen Verifies AI Agent Actions Before They Become Irreversible
Microsoft Research’s Amit Sharma presents Interwhen as a framework for moving AI agents from post-hoc checking to verified execution while they are still acting. The open-source library uses LLMs to turn natural-language instructions, policies, and partial responses into smaller verifiable properties, then applies symbolic or model-based verifiers to tool calls and intermediate behavior. Sharma argues that this lets agents continue normally when checks pass but interrupts them when a verifier detects a violation, addressing risks that final-output review may catch too late.
GitHub Agentic Workflows Turn Actions Into AI-Run Development Processes
Microsoft Research’s Peli Halleux and Yash Lara present GitHub Agentic Workflows as a move from AI-assisted coding to repository-level process automation. Their argument is that agents should be embedded inside GitHub Actions to research, plan, assign, and open pull requests under human review, rather than operate as unconstrained swarms. The system’s promised scale depends on orchestration, sandboxing, limited permissions, and Microsoft-hosted models on Azure.
MagenticLite Brings Full Agent Workflows to Small Language Models
Microsoft Research is presenting MagenticLite as a full-stack agentic system designed to make small language models usable for multi-step work across a browser and local files. Weili Shi, Harkirat Behl and Hussein Mozannar argue that the capability comes from specializing the stack rather than relying on frontier-scale models: MagenticBrain handles planning, coding and delegation, while Fara 1.5 controls the browser. The release also emphasizes user oversight, with the agent pausing for credentials, approvals or other points where the user needs to take control.
Language-Agnostic Analysis Finds 15 Vulnerabilities in ZKP Projects
Arman Kolozyan of the Max Planck Institute for Security and Privacy argues that many zero-knowledge proof bugs arise from a mismatch between what a prover’s computation can produce and what a verifier’s constraints will accept. Presenting the paper “Language-Agnostic Detection of Bugs in Zero-Knowledge Proof Programs,” he describes a formal model, the Domain Consistency Model, and a static-analysis tool, CCC-Check, designed to detect those mismatches across ZKP languages. The work reports two-orders-of-magnitude speedups over SMT-based approaches on benchmarks and 15 previously unknown vulnerabilities in six ZKP projects, most of them outside the reach of existing models.