AMIT SHARMA:<\/strong> Hi, I\u2019m Amit Sharma, a Principal Researcher at Microsoft Research in India.<\/p>\n\n\n\nToday I\u2019m excited to introduce Interwhen, a framework we\u2019ve built for steering reasoning agents with real-time verification. This is joint work with my colleagues at MSR India, as well as Professor Subbarao Kambhampati from Arizona State University.<\/p>\n\n\n\n
AI systems today are moving from passive generators of text to agentic systems that can execute actions in the real world, either through tool calls or other means.<\/p>\n\n\n\n
For example, consider an agent that is operating your inbox, executing complex workflows in an organization, or even interacting in the physical world. These agents are equipped with tool calls that can make irreversible changes\u2014for example, sending an email on your behalf, writing to an organizational database, or even moving an actual robot next to you.<\/p>\n\n\n\n
So it is critical not just to verify their final output, but also their intermediate actions.<\/p>\n\n\n\n
A central question for us is: how do we go from agentic execution as it exists today to a future with verified agentic execution?<\/p>\n\n\n\n
Let\u2019s look at current verification systems and their limitations. Typically, a verifier has access to the model response at a given time, the task instruction, and possibly some domain policies.<\/p>\n\n\n\n
One approach uses an LLM as a judge, but this is a monolithic verifier and may miss nuanced errors, making it unreliable. Another approach uses formal verifiers, which are reliable but restricted to math and code.<\/p>\n\n\n\n
To address these challenges, we built Interwhen, a real-time framework for agent verification.<\/p>\n\n\n\n
Ideally, we want to use formal verifiers in general domains\u2014but how do we apply them in settings where there may be thousands of tokens and high ambiguity?<\/p>\n\n\n\n
The key innovation in Interwhen is an LLM-based projection step that automatically breaks outputs into a list of verifiable properties\u2014desirable conditions that any solution should satisfy.<\/p>\n\n\n\n
The framework can then automatically generate a formal specification and create a provable verifier in Python or Lean.<\/p>\n\n\n\n
Importantly, the system does not operate only after the agent is done. It can verify partial responses at any point in time, provide actionable feedback, and steer the reasoning model to avoid violations.<\/p>\n\n\n\n
We designed the system with two important principles. First, verification runs asynchronously so the system remains efficient. Second, it is plug-and-play, allowing practitioners to bring in their existing verifiers.<\/p>\n\n\n\n
Now let\u2019s look at how this works in a real-world setting.<\/p>\n\n\n\n
Interwhen achieves state-of-the-art results on agentic benchmarks such as Tau2 Bench, where even small models can rival the accuracy of frontier models.<\/p>\n\n\n\n
The first step is extracting verifiable properties\u2014structured, atomic conditions that any solution should satisfy.<\/p>\n\n\n\n
For example, in a retail scenario from Tau2 Bench, a policy expressed in natural language can be converted into properties such as \u201ca refund must go to the original payment method.\u201d From this, the system can automatically generate Python code that acts as a verifier.<\/p>\n\n\n\n
This is a one-time operation that can be reviewed and validated. The key value comes at runtime, when variables in the verifier are dynamically filled using the user\u2019s context and the model\u2019s current response.<\/p>\n\n\n\n
For instance, if an agent attempts to process a return using the wrong payment ID, the verifier detects the violation and produces feedback such as \u201cRefund to credit card not allowed.\u201d In the next step, the model uses this feedback to correct its mistake.<\/p>\n\n\n\n
Efficiency is a core design goal. Verification must not only ensure correctness but also be practical.<\/p>\n\n\n\n
To achieve this, we built a separate monitoring system that tracks the agent\u2019s output in real time and calls verifiers asynchronously for reversible tool calls. Execution is only stopped if an error is detected; otherwise, the process continues as normal.<\/p>\n\n\n\n
The framework is general and improves output quality across many tasks, including customer service, travel booking, logical reasoning, and ensuring safety in agent responses.<\/p>\n\n\n\n
It is fully plug-and-play, works with both proprietary and open-weight models, and enforces strict verification\u2014meaning the agent provides no answer if verification fails.<\/p>\n\n\n\n
I\u2019m excited to announce that we have open-sourced Interwhen on GitHub.<\/p>\n\n\n\n
At Microsoft Research, we believe in open collaboration. Our goal is to foster a community focused on AI verification and safety, where we can collectively build and test verifiers for real-world use cases and enable a future where all agentic execution is verified.<\/p>\n\n\n\n
If you\u2019d like to learn more about Interwhen, you can visit the link below.<\/p>\n\n\n\n
Thank you.<\/p>\n\n\t\t\t\t<\/span>\n\t\t\t<\/div>\n\t\t\t\n\t\t\t\tShow more\t\t\t<\/button>\n\t\t<\/div>\n\t<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"What if AI agents could check their work as they go? This verification method extracts verifiable properties from natural language and evaluates them using symbolic or model-based verifiers. Interwhen, a new open-source library, enables real-time verification of each step, helping agents act more safely and reliably in complex, real-world tasks.<\/p>\n","protected":false},"featured_media":1171931,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr_hide_image_in_river":0,"footnotes":""},"research-area":[13556],"msr-video-type":[268311],"msr-locale":[268875],"msr-post-option":[],"msr-session-type":[256174],"msr-impact-theme":[],"msr-pillar":[],"msr-episode":[270329],"msr-research-theme":[270112],"class_list":["post-1171596","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-research-area-artificial-intelligence","msr-video-type-microsoft-research-forum","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/s8vkG5czZtY","msr_secondary_video_url":"","msr_video_file":"http:\/\/0","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/1171596","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":4,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/1171596\/revisions"}],"predecessor-version":[{"id":1172010,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/1171596\/revisions\/1172010"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/1171931"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=1171596"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=1171596"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=1171596"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=1171596"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=1171596"},{"taxonomy":"msr-session-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-session-type?post=1171596"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=1171596"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=1171596"},{"taxonomy":"msr-episode","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-episode?post=1171596"},{"taxonomy":"msr-research-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-theme?post=1171596"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}