Session on Reasoning

This session from the Microsoft Research India Academic Research Summit 2026 featured talks by Hongxiang Fan and Nagarajan Natarajan, focusing on enhancing the efficiency and reliability of AI reasoning, particularly for large language models (LLMs).

Hongxiang Fan: Cross-stack Co-design Pathway for Pushing Efficiency Frontier of AI Reasoning

Hongxiang Fan, an assistant professor at Imperial College London, introduced the critical need for a cross-stack co-design pathway to address the growing challenges in AI.

Motivation for Efficient AI

He highlighted several key issues driving this research:

• Increasing Algorithmic Complexity: Driven by the scaling law, models like Kim K 2.5 are reaching trillion parameters, placing immense strain on computing systems.
• End of Moore’s Law: CPU performance gains are slowing, and even GPUs face energy efficiency challenges. Training a BERT model, for instance, has a carbon footprint equivalent to five cars’ lifetime emissions.
• Affordability of AI: The high cost of training and inference, especially with ever-larger models, raises concerns about AI’s accessibility and long-term sustainability.

Fan’s core belief is that achieving sustainable and efficient AI requires optimization across the entire stack, encompassing algorithmic, system, hardware, and chip-level co-design, rather than focusing on isolated layers.

Test-Time Scaling (TTS) and its Challenges

The talk then delved into Test-Time Scaling (TTS), a technique where additional computation is allocated during inference to boost algorithmic performance. While TTS can enable smaller open-source models on edge devices to match the performance of larger cloud models, it comes with significant challenges:

• Output Token Explosion: Existing methods like Chain-of-Thought (CoT) can increase token generation by over 52 times, leading to higher energy consumption and latency.
• Typical TTS Approaches: Fan illustrated CoT (sequential steps), Best-of-N (parallel generation with final selection), and Beam Search (stepwise selection and expansion of promising paths).

Key Research Questions and Findings

Fan presented three research questions from their NuRIPS 25 paper:

1. Is the current verification granularity optimal?
   • An “Oracle approach” study, which explored the performance upper bound, revealed that current granularities (per-step or whole-response) are not optimal, suggesting a potential for 75x FLOPs reduction and 1.1x accuracy increase.
2. What is the system cost of verification?
   • GPU profiling demonstrated that verification incurs significant overhead, often dominating overall execution time, especially when fine-grained (G=1, every step) and with many samples (N > 64). System performance can be bounded by verification.
3. How should the optimal verification granularity be decided?
   • Empirical studies showed that stronger generators prefer sparse verification (larger granularity, smaller verifier models).
   • To address this, they proposed Variable Granularity Search (VGS), an adaptable and dynamic scheme that adjusts verification granularity based on task difficulty. VGS achieved a 3% accuracy improvement and 52% FLOPs reduction compared to prior methods like Beam Search and DVT.

Future Directions for Efficient AI Reasoning

Fan outlined crucial open questions for future research:

• Verifier Selection: What kind of verifier is most suitable (general LLM, process reward model, domain-specific tool, LLM with tool code, RL-enhanced reward models)?
• Verifier Triggering: When should verification be triggered (token-wise, step-wise, special token, or confidence-based)?
• Cost-Aware Verifier Design: How can verification costs be integrated into the training process?

System Optimization for Edge AI with Test-Time Scaling

In a related ASPLOS paper, Fan’s team tackled the challenge of deploying TTS-enabled small models on edge devices while maintaining performance and latency comparable to cloud models. They identified and addressed several inefficiencies in current VLM (Visual Language Model) backends:

1. Irregular Workloads: Varying token generation lengths across reasoning paths lead to idle time.
   • Solution: Speculative Beam Search / Reasoning Extension was proposed to “hack” the VLM engine, allowing speculative execution without waiting for slower paths, similar to branch prediction.
2. Inefficient Prefix Sharing: VLM engines don’t fully exploit prefix sharing, especially under memory constraints.
   • Solution: Dynamic Prefix-Aware Scheduling prioritizes execution order to reduce KV cache eviction.
3. Memory Constraints on Edge Devices: Deploying both a generator and a verifier on limited memory.
   • Solution: Off-line Model Guided Multi-model Memory Allocation uses an off-line model to intelligently allocate GPU memory between the verifier and generator based on their computational and memory characteristics.

These optimizations collectively enable edge devices with TTS to achieve accuracy close to cloud models with similar latency, though current evaluations are primarily in the math domain.

---

Nagarajan Natarajan: Advancing Verified Reasoning

Nagarajan Natarajan, a principal researcher at Microsoft Research India, presented his work on Advancing Verified Reasoning, emphasizing the need for reliable agentic execution.

The Need for Verified Agentic Execution

Natarajan highlighted that modern AI agents execute complex, multi-step workflows. The core problem is ensuring these agents do exactly what they’re supposed to do and do not do what they’re not supposed to do, especially in high-stakes domains like retail customer service (e.g., refund policies) or patent law (e.g., drafting legal responses adhering to complex implicit and explicit policies). This demands determinism from powerful but often stochastic AI systems. The technical challenge lies in verifying long reasoning traces (thousands of tokens) against complex policies with minimal inference overhead.

Beyond Verification: The Role of Steering

Compliance alone is insufficient; if an agent errs, the system must steer it back onto the correct path. The goal is to guide the agent’s trajectory to be both:

• Compliant: Adhering to all implicit and explicit rules.
• Correct: Successfully solving the user’s task. This pursuit aims for significant improvements in both reasoning compliance and quality.

InterVent: A Paradigm for Verified Agentic Execution

Natarajan introduced InterVent, a platform and paradigm for verified agentic execution. It critiques current verification methods:

• LLM as a judge: Suffers from the same unreliability as the agent itself.
• Custom verifiers: Hard to scale due to expertise and time requirements.
• Efficiency: Both methods often require pausing agent execution, incurring latency.

InterVent proposes leveraging formal verification methods for general domains to achieve deterministic execution, while still utilizing LLMs for crucial semantic parsing. The process is divided into offline and runtime phases:

Offline Phase: Auto-formalization

• Input: Task descriptions and policies (typically ambiguous text).
• Process: Convert these informal descriptions into a common representation language. Formal verification techniques are then used to generate formal specifications and, subsequently, executable verifier code (e.g., Python scripts).
• Challenges: Auto-formalization beyond math and code is difficult due to subjective clauses, contradictions, and ambiguous text in real-world policies. The correctness of verifiers (especially completeness) is hard to guarantee, though soundness (never calling a correct trajectory wrong) is more achievable. Formal systems like Lean are explored for generating specifications and proofs. For properties that resist formalization (e.g., “grounded in the document”), atomic rubrics are created, designed for low-variance evaluation by even small LLMs.

Runtime Phase: Verification and Steering

• Mechanism: CPU-bound verifier code runs in the background. When the agent makes a tool call, relevant verifiers are invoked.
• LLM Role: A small LLM (e.g., 4B parameters) is used for extraction of necessary information (e.g., payment_ID) from the agent’s chain of thought or tool calls, rather than for reasoning.
• Efficiency: The process is typically fast due to CPU-bound verifiers and asynchronous execution. The system can speculatively continue agent execution, assuming correctness, and only roll back if a verifier signals a failure.
• Steering: If verification fails, crafted feedback is provided to the agent to redirect its actions. This feedback is “out-of-policy” text, which can be challenging for the model to integrate effectively.

Key Challenges and Future Research Directions

Natarajan outlined critical areas for future work:

• Auto-formalization: Improving the conversion of ambiguous text policies into sound and complete formal specifications and verified code.
• Steering Models by Feedback: Optimizing the granularity, content, and timing of feedback to maximize instruction following without derailing the model.
• Turning Verification Signals into Rewards: Using intermediate verification signals during training (rather than just outcome-based rewards) to help models explore better trajectories, learn from failures, and improve compliance. This connects to techniques like SFT, RL, self-distillation, and critic-based approaches.

Empirical Results

InterVent has shown significant promise:

• TaP Bench: A 30 billion-parameter model, when combined with InterVent’s verification and steering, achieved 87.7% accuracy, a substantial leap from a 32% baseline, and significantly outperforming vanilla GPT-3.5/4 (47.4%).
• Maze Dataset: Experiments on maze-solving tasks demonstrated that early feedback from verifiers leads to a huge lift in performance, with diminishing returns as the trajectory progresses.

The goal for InterVent is to span the complexity spectrum from toy problems to real-world policies and to be able to verify any agent, from open-source to proprietary large-scale models.

• Tags:
• AI Agents
• Feature
• Verification
• LLM Systems
• Edge AI
• Formal Verification
• AI Reasoning
• Efficient AI
• Cross-Stack Optimization
• Test-Time Scaling
• System Co-Design
• Computational Efficiency
• Model Steering