LLM News

Researchers have identified and solved a critical scaling problem in LLM-based theorem prediction called Structural Drift, where in-context learning performance collapses as reasoning depth increases. Using Theorem Precedence Graphs to encode topological dependencies, they achieved 89.29% accuracy on the FormalGeo7k benchmark—matching state-of-the-art supervised approaches without any gradient-based training.

Researchers introduce NeuroProlog, a neurosymbolic framework that compiles math word problems into executable Prolog programs with formal verification guarantees. A multi-task "Cocktail" training strategy achieves significant accuracy improvements on GSM8K: +5.23% on Qwen-32B, +3.43% on GPT-OSS-20B, and +5.54% on Llama-3B compared to single-task baselines.

Researchers have introduced VeriStruct, a framework that extends AI-assisted formal verification from individual functions to complete data structure modules in Verus. The system successfully verified 128 of 129 functions (99.2%) across eleven Rust data structure modules by using a planner module to generate abstractions, type invariants, and proof code, with automatic error correction for Verus syntax.