Two Paths to Better AI Reasoning: Test-Time Scaling and Formal Verification

Article

At the MSR India Summit, two researchers explored the core challenges facing modern AI reasoning from two distinct angles: system efficiency and reasoning trustworthiness. Hongxiong Fan, Assistant Professor at Imperial College London (also affiliated with the University of Cambridge and a recipient of the Microsoft Research Faculty Fellowship), focused on efficiency optimization through "test-time scaling," while a Principal Researcher at Microsoft Research India proposed a new paradigm called "verified reasoning." This article synthesizes the key insights from both talks and outlines two critical paths to more efficient and reliable AI reasoning.

The Cost Problem in AI Reasoning

Hongxiong Fan opened by highlighting a fundamental tension in AI development: the explosive growth of algorithmic complexity. Driven by Scaling Laws, model parameter counts and computational demands have skyrocketed since the ChatGPT era — with some recent open-source models reaching the trillion-parameter scale, placing enormous pressure on underlying compute infrastructure.

Scaling Laws, introduced by OpenAI researchers Kaplan et al. in 2020, describe a power-law relationship between model performance and three variables: parameter count, training data volume, and compute. The discovery that continuously scaling all three dimensions yields continuous capability improvements drove the creation of GPT-3 (175 billion parameters), GPT-4, and even larger models. But scaling laws come with a hidden cost: doubling performance often requires a ten-fold increase in compute resources, creating a positive feedback loop where "more capable" always means "more expensive."

At the same time, Moore's Law is running out of steam. Proposed by Intel co-founder Gordon Moore in 1965, it predicted that transistor counts on integrated circuits would double every 18–24 months. Since the mid-2010s, however, physical limits such as quantum tunneling and thermal bottlenecks have significantly slowed single-core performance gains. Citing data from a book by David Patterson (father of RISC architecture and Turing Award laureate), CPU performance improvements have been decelerating since 1980, and the natural dividends of hardware advancement are nearly exhausted. Future efficiency gains must increasingly rely on software algorithms and cross-layer co-design. Energy consumption is also a pressing concern: training a BERT model from scratch generates carbon emissions equivalent to the entire lifetime emissions of five cars, and the energy supply chain for U.S. data centers has become a bottleneck.

Beyond environmental costs, affordability has emerged as a critical issue in recent years. Leading labs invest enormous sums in training costs to stay ahead on benchmarks, and inference is far from free — some reports suggest AI usage costs can exceed the cost of human labor. As models continue to grow, this problem will only worsen. The fundamental question becomes: even if AI becomes extremely powerful, will everyone be able to afford it?

Test-Time Scaling: A Comeback for Small Models

What Is Test-Time Scaling

Faced with these challenges, Fan's team chose a "cross-stack co-design" research approach — optimizing across the algorithm, system, hardware, and chip layers simultaneously rather than tackling any single layer in isolation. Their NeurIPS paper is a prime example of algorithm-system co-design.

Test-Time Scaling is a concept from OpenAI's "Strawberry" project. The core idea: since so much GPU compute is already invested in training, why not allocate more compute during inference to boost model performance? The philosophy closely mirrors how humans solve hard problems — drafting, checking work, revising — trading inference-time compute for higher accuracy. It essentially searches more thoroughly through the output space to compensate for the limitations of smaller model sizes. Experiments show that accuracy continues to improve as more compute is allocated at test time — with proper test-time scaling, open-source edge models can even match the performance of closed-source cloud models.

But this is no free lunch. Text-based Long Chain-of-Thought (Long CoT) reasoning causes a "token explosion." Chain-of-Thought (CoT), introduced by Google researchers Wei et al. in 2022, demonstrated that prompting models to "think step by step" significantly improves complex reasoning accuracy. Long CoT extends this by allowing models to generate thousands or even tens of thousands of intermediate reasoning tokens, including self-reflection and error correction. However, models can fall into "overthinking," generating over 52× more tokens than necessary for certain tasks, driving up energy consumption and latency.

Finding the Optimal Verification Granularity

Typical test-time scaling techniques fall into three categories: Long CoT (sequential generation), Best-of-N (parallel generation followed by selection), and Beam Search (retaining the most promising reasoning steps at each stage). Beam Search is a classic decoding algorithm in natural language generation, originating from speech recognition and machine translation. At each step, it keeps the top-K candidate sequences by score (K being the beam width), balancing search quality against compute cost through limited parallel exploration. Best-of-N represents the coarsest verification granularity; Beam Search represents the finest.

The team investigated three core questions:

• Is current verification granularity optimal? Experiments exploring the upper bound of performance found that existing granularity choices are suboptimal — under ideal conditions, FLOPs can be reduced by 75× while improving accuracy by 1.1%.

• What is the system cost of verification? GPU profiling revealed that when verification granularity is very fine (verifying at every step) and the number of samples is large (e.g., more than 64), verification cost dominates overall execution time — the finer the granularity and the more samples, the more system performance is bottlenecked by the verification step.

• How do we determine optimal verification granularity? The team proposed Variable Granularity Search, which dynamically adjusts verification granularity at runtime based on task difficulty: hard tasks use fine-grained step-by-step verification, while easy tasks only need Best-of-N. Compared to state-of-the-art methods like Beam Search and DVTS, this approach achieves approximately 3% higher accuracy while reducing compute by 52%.

Bringing Cloud-Level Performance to Small Models

In follow-up work published at ASPLOS, the team further demonstrated that a locally deployed 7B open-source model with test-time scaling can match closed-source cloud model accuracy on specific tasks. The challenge is latency — allocating too much compute causes execution time to far exceed cloud response times.

To address this, the team used NSight for GPU profiling, identified three key inefficiencies in the VLM engine, and proposed corresponding optimizations:

• Speculative Beam Search: Short reasoning paths don't need to wait for longer paths to complete — they can speculatively generate ahead. This draws inspiration from the branch prediction mechanism in CPUs — optimistically execute first, roll back if verification fails. The Speculative Decoding technique that emerged in 2023 follows the same logic: a small draft model rapidly generates candidate tokens, which are then verified in parallel by the large main model. Multiple tokens can be accepted in a single forward pass, breaking the serial bottleneck of autoregressive generation.

• Dynamic Prefix-Aware Scheduling: In memory-constrained scenarios, prioritize continuous-generation reasoning paths to reduce KV cache eviction. KV caching is a core acceleration technique for Transformer inference — it stores previously computed Key-Value matrices in GPU memory for O(1) incremental computation, at the cost of memory usage that grows linearly with sequence length. Multiple parallel reasoning paths share prefix KV caches, but when memory is insufficient the system is forced to evict cache data and recompute it, causing severe latency spikes.

• Roofline Model-Guided Multi-Model Memory Allocation: The Roofline Model is a standard GPU performance analysis tool that classifies compute tasks as either compute-bound or memory-bound and guides the selection of optimization strategies. The team used it to allocate GPU memory appropriately between the verifier and generator, ensuring both components operate near their respective performance ceilings.

With these combined optimizations, open-source models running on a local AI PC can achieve accuracy and response latency comparable to closed-source cloud models.

Verified Reasoning: From Execution to Trustworthy Execution

The second talk shifted to a different dimension — trustworthiness. The Microsoft Research India researcher noted that today's AI agents can execute complex multi-step workflows spanning high-value domains like patent law and retail customer service, involving dozens or even hundreds of steps.

The Dual Goals of Compliance and Correctness

The key question is: how do we ensure an agent "does what it should and doesn't do what it shouldn't"? Take a retail agent policy as an example: one rule states "refunds must be returned to the original payment method or as a gift card," and all of the model's tool calls and messages must comply with this policy. In complex scenarios like patent responses, policies are often implicit — legal standards that lawyers follow by default.

The research framework pursues two goals: compliance (following explicit or implicit rules) and correctness (ultimately solving the user's problem). The core platform, called "Interven," is designed to verify and steer agents during runtime execution.

Introducing Formal Verification

The dominant verification approach today is "LLM-as-judge" — handing a complete trajectory of thousands of tokens to an LLM and asking it to determine compliance. But this inherits the same unreliability as the model being tested. The research team's core insight is: bring the determinism of formal verification into real, messy domains.

Formal verification originated in the field of program correctness proofs in computer science, using mathematical methods (such as model checking and theorem proving) to rigorously guarantee that system behavior conforms to specifications. Typical applications include aerospace software, hardware chip design (Intel adopted it extensively after the Pentium floating-point bug), and security protocol verification. Its core advantage is determinism — it doesn't rely on probabilistic sampling; given an input, it always yields a consistent conclusion. The team's innovation was building an automated pipeline that converts "natural language policy → intermediate representation → executable verification code," bringing the determinism of formal verification into the inherently ambiguous domain of business rules.

The technical approach unfolds in two phases — offline and online:

• Offline phase: Decompose text policies into rules, map them to an intermediate representation language, and generate corresponding verification code (think of it as Python code that checks each rule). The code contains "holes" to be filled at runtime with context-specific values (such as payment IDs).

• Online phase: Most verifiers are CPU-bound code snippets. When an agent makes a tool call, the corresponding verifier is triggered, calling a small language model only for parameter extraction (a 4B model is sufficient for extraction tasks). Since most verification is CPU-bound, the entire process has bounded latency.

Interestingly, this design shares the same spirit as Fan's speculative approach: verification calls can be asynchronous, allowing the model to assume an operation is correct and proceed, rolling back the trajectory only if verification fails. However, for irreversible calls such as "write operations," the system must block and wait for the verification result.

Steering, Feedback, and Training

Verification is only one side of the coin. The real value lies in "steering" — providing immediate feedback when the model makes a mistake to bring it back onto a compliant and correct trajectory. Experiments on a maze dataset revealed an important pattern: the earlier verification feedback is provided, the more significant the performance improvement; as the trajectory advances and model confidence increases, the marginal benefit of feedback diminishes.

On the Tau-bench benchmark — Tau-bench (Tool-Agent-User benchmark) is designed to evaluate AI agent performance in real-world business workflows, simulating scenarios like retail customer service and airline booking while assessing both task completion rate and policy compliance rate, corresponding exactly to the "correctness" and "compliance" goals — with verification and steering, a 30B model jumps from a 32% baseline to 87 points, while the original GPT-4o-mini scores only 47.4; in a harder configuration, a 24-point baseline can be lifted to 55. All operations are black-box, requiring no access to model internals — only the model's text output.

Open Challenges and Future Directions

Both talks converged on a set of shared open questions:

• Automated formalization beyond math and code: Real-world policies are "an ocean of ambiguous text." Handling subjective clauses, informal language, and contradictions across pages is a massive challenge.
• Proving verifier correctness: A distinction must be drawn between "soundness" (never incorrectly flagging a correct trajectory) and "completeness" (never missing an incorrect trajectory). The research team found completeness harder to guarantee.
• Alignment across different reference frames: When a reasoning task is based on Indian law but the verifier is based on U.S. law, how do you ensure alignment? This is especially acute in compliance scenarios involving governments, enterprises, and customers.
• Turning verification signals into training signals: Intermediate feedback is more conducive to learning than pure outcome feedback, and value can even be extracted from failed trajectories. This has inspired a range of algorithmic explorations: SFT, outcome-based RL, self-distillation RL, and critic-based RL.

Regarding the prospects for small model deployment, Fan's assessment is cautiously optimistic: GPU infrastructure is largely ready, but at the algorithm level — which verifier to choose for different task types, and when to trigger verification — these remain open questions, with clear answers likely one to two years away. Encouraging results have already been demonstrated in specific domains like mathematics; the key challenge is improving generalization.

From the efficiency optimization of test-time scaling to the trustworthiness guarantees of formal verification, these two paths together sketch a technical roadmap for AI reasoning that is both accessible and reliable.

Key Takeaways