25 articles tagged with #formal-methods. AI-curated summaries with sentiment analysis and key takeaways from 50+ sources.
Researchers introduce VASO, a framework that combines formal verification with self-evolving language model skills for robot control, achieving 97.2% specification compliance on physical tasks. The approach bridges formal methods and foundation models by using counterexamples from model checking as optimization feedback for skill contracts rather than modifying underlying model weights.
Researchers introduce CHECKMATE, a tool that automatically generates optimization algorithms through code evolution, requiring only formal problem specifications and natural language descriptions rather than expert-designed heuristics. The evolved algorithms outperform state-of-the-art solvers on industrial configuration and scheduling problems, demonstrating formal methods can guide automated algorithm discovery for complex real-world optimization challenges.
Researchers present a hybrid neuro-symbolic architecture that combines formal logic with neural semantic analysis to verify LLM outputs in high-stakes domains like healthcare. The system achieves over 83% hallucination detection rates for structured data and 72% for semantic fabrications while reducing report creation time by 30%, demonstrating practical safeguards for deploying LLMs in data-sensitive applications.
Researchers propose a shift from deterministic to probabilistic safety verification for embodied AI systems, arguing that provable probabilistic guarantees offer a more practical path to large-scale deployment in safety-critical applications like autonomous vehicles and robotics than the infeasible goal of absolute safety across all scenarios.
Researchers prove a fundamental theoretical limit in AI safety verification using Kolmogorov complexity theory. They demonstrate that no finite formal verifier can certify all policy-compliant AI instances of arbitrarily high complexity, revealing intrinsic information-theoretic barriers beyond computational constraints.
SentinelAgent introduces a formal framework for securing multi-agent AI systems through verifiable delegation chains, achieving 100% accuracy in testing with zero false positives. The system uses seven verification properties and a non-LLM authority service to ensure secure delegation between AI agents in federal environments.
Researchers introduce Theory of Mind Utility (ToM-U), a formal computational framework for modeling how agents infer others' beliefs by tracking information access and credibility. The model uses directed graphs called Local Epistemic World Models to represent epistemic relationships and generates falsifiable predictions about mentalizing failures, advancing cognitive science theory beyond existing Bayesian and simulation-based approaches.
Researchers propose a runtime enforcement framework using Hybrid Automata to actively prevent safety violations in autonomous and cyber-physical systems by monitoring and modifying unsafe behaviors in real time. The approach combines discrete-event editing with continuous monitoring and is validated through an Adaptive Cruise Control case study, demonstrating effective safety compliance with minimal computational overhead.
Researchers have adapted GPU parallelism techniques to neural network verification, enabling formal safety proofs on larger models. Fully Sharded Data Parallelism (FSDP) reduces memory usage by 80-90% while maintaining identical verification results, though Tensor Parallelism trades some bound quality for memory efficiency.
Researchers introduce Spatio-Temporal Bound Propagation (STBP), a verification framework for neural networks processing video and volumetric data that provides formal robustness guarantees under realistic adversarial constraints. The method achieves 1.7x higher certified robust accuracy compared to existing approaches while maintaining computational scalability, addressing a critical gap in AI safety for applications like autonomous driving and medical imaging.
TOKI is a formal framework that types contradiction resolution in LLM-agent persistent memory systems as a write-time concurrency control problem. The research proves that four common heuristics used in production systems admit unspecified isolation levels and anomalies, and proposes a bitemporal operator algebra with audit-row provenance that excludes three critical write-time anomalies while maintaining language-model oversight.
Researchers introduce a novel shielding framework for reinforcement learning agents that guarantees safety without requiring prior knowledge of system dynamics. By combining robust MDPs with linear temporal logic specifications and PAC learning guarantees, the approach enables the creation of minimally restrictive safety shields for unknown environments while maintaining strong performance as data accumulates.
SEMBridge is a tagless-final framework that enables developers to write program semantics once and automatically generate multiple interpretations, including executable code, weakest-precondition verification conditions, and bounded-checking validators. The Python prototype demonstrates synchronization of formal verification artifacts with executable semantics across loop-free imperative programs, addressing the practical gap between formal methods and software engineering.
Researchers present a novel neural network verification method called partial multi-neuron relaxation that selectively applies computationally expensive multi-neuron bounds to strategically chosen neurons rather than all neurons. This approach balances the tightness-scalability tradeoff in formal verification, showing improved performance when integrated into the Marabou verifier.
Researchers introduce Hilbert-Geo, a neural-symbolic AI framework for solving solid geometry problems by combining formal language representation with theorem-based reasoning. The system achieves 77.3% accuracy on solid geometry tasks, significantly outperforming leading AI models like GPT-4 and Gemini-2.5-pro, demonstrating advances in multimodal geometric reasoning.
Researchers developed a hybrid system combining formal symbolic planning with large language models to improve capability-based planning in industrial automation. The system integrates natural-language interaction, explainability, and human-approved knowledge model adaptation, achieving high accuracy across planning and query tasks while maintaining formal correctness guarantees.
A new computability theory paper proves that finite internal self-modification in AI systems cannot exceed their existing computational layer, while qualitatively stronger capabilities require access to a higher computational level (the Turing jump). This formally separates recursive self-improvement narratives into within-layer iteration versus genuine capability ascent, constraining theoretical claims about AI recursive self-improvement.
Researchers present 2-ASP(Q)^w, a fragment of Answer Set Programming extended with quantifiers and weak constraints, proving its theoretical complexity bounds and introducing practical computation strategies using CEGAR techniques. The work bridges theoretical computer science with implementable solutions for optimization problems, offering both formal completeness results and experimental validation on real-world benchmarks.
Researchers propose a formal framework for describing knowledge graph affordances to agents, extending decades-old semantic web service standards to address modern KG discovery and composition challenges. The framework introduces the Agentic Affordance Profile (AAP), a metadata layer that enables principled selection and failure diagnosis by specifying what agents can prove from a knowledge graph and under what epistemic conditions.
Researchers demonstrate how functional stable model semantics enhances Answer Set Programming Modulo Theories (ASPMT), enabling integration of intensional functions that derive values from other predicates rather than pre-defined sources. The framework allows tight ASPMT programs to translate into SMT instances, extending the theoretical foundations of logic programming.
Cplus2ASP Version 2 is a new system that translates action language C+ into answer set programming, offering significant performance improvements over the Causal Calculator through modern ASP solving techniques. The tool supports incremental execution, external atoms via Lua integration, and extensible translations for other action languages, making it relevant for automated reasoning and planning applications.
Researchers introduce DPrivBench, a benchmark for evaluating how well large language models can reason about differential privacy algorithms and verify their correctness. Testing shows current LLMs handle basic DP mechanisms competently but fail significantly on advanced algorithms, exposing critical gaps in automated privacy reasoning capabilities.
Researchers introduce Text2Model and Text2Zinc, frameworks that use large language models to translate natural language descriptions into formal optimization and satisfaction models. The work represents the first unified approach combining both problem types with a solver-agnostic architecture, though experiments reveal LLMs remain imperfect at this task despite showing competitive performance.
SPEAR is a multi-agent AI framework designed to automate smart contract auditing through coordinated specialist agents that prioritize contracts, allocate tasks, and recover from failures autonomously. The research demonstrates how established multi-agent system patterns can improve security analysis workflows beyond centralized or pipeline-based approaches.
Researchers introduce FAME (Formal Abstract Minimal Explanations), a new method for explaining neural network decisions that scales to large networks while producing smaller explanations. The approach uses abstract interpretation and dedicated perturbation domains to eliminate irrelevant features and converge to minimal explanations more efficiently than existing methods.
