SEVerA uses Formally Guarded Generative Models and a three-stage Search-Verification-Learning process to synthesize self-evolving agents that satisfy hard formal constraints while improving task performance.
Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
representative citing papers
A program synthesis system models collaborative physical activities from narrated demonstrations as editable programs, enabling users to teach, inspect, and correct them, with a study showing 70% success in refining soccer tactics programs.
CoCoMagic applies constrained cooperative co-evolution to metamorphic and differential testing to find up to 287% more distinct behavioral divergences in an end-to-end ADS than baseline search methods.
ClassInvGen co-generates class invariants and tests with LLMs to outperform pure LLM generation and Daikon on C++ data structures.
Weighted NetKAT extends NetKAT with semiring weights and weighted NetKAT automata to enable automatic verification of quantitative safety and reachability properties.
Replicates SPARK humanoid safety filters and stress-tests them under crowding, noise, and delays, showing trade-offs in goal tracking versus collision reduction.
citing papers explorer
-
SEVerA: Verified Synthesis of Self-Evolving Agents
SEVerA uses Formally Guarded Generative Models and a three-stage Search-Verification-Learning process to synthesize self-evolving agents that satisfy hard formal constraints while improving task performance.
-
Interactive Program Synthesis for Modeling Collaborative Physical Activities from Narrated Demonstrations
A program synthesis system models collaborative physical activities from narrated demonstrations as editable programs, enabling users to teach, inspect, and correct them, with a study showing 70% success in refining soccer tactics programs.
-
Constrained Co-evolutionary Metamorphic Differential Testing for Autonomous Systems with an Interpretability Approach
CoCoMagic applies constrained cooperative co-evolution to metamorphic and differential testing to find up to 287% more distinct behavioral divergences in an end-to-end ADS than baseline search methods.
-
ClassInvGen: Class Invariant Synthesis using Large Language Models
ClassInvGen co-generates class invariants and tests with LLMs to outperform pure LLM generation and Daikon on C++ data structures.
-
Weighted NetKAT: A Programming Language For Quantitative Network Verification
Weighted NetKAT extends NetKAT with semiring weights and weighted NetKAT automata to enable automatic verification of quantitative safety and reachability properties.
-
Adversarial Stress Testing of SPARK Humanoid Safety Filters
Replicates SPARK humanoid safety filters and stress-tests them under crowding, noise, and delays, showing trade-offs in goal tracking versus collision reduction.