QLL is a novel logic for neuro-symbolic learning that uses ML-native operations (sum, log-sum-exp) on logits to embed constraints, satisfying most linear logic properties and showing stronger correlation between empirical robustness and formal verification than prior approaches.
Johnson, and Haoze Wu
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
citation-role summary
background 2
citation-polarity summary
years
2026 5roles
background 1polarities
background 1representative citing papers
New verification connection from C-RASP to Lustre model checkers plus local search algorithm for synthesizing C-RASP programs from examples.
Viverra generates C code from text descriptions together with assertions that are verified by model checkers, and a user study with over 400 participants shows the verified assertions improve code comprehension.
Super-DeepG improves linear relaxation techniques and Lipschitz optimization for neural network robustness certification against geometric perturbations, with a GPU implementation that claims better precision and speed than prior work.
Luna delivers a C++ bound propagator supporting interval, DeepPoly/CROWN, and alpha-CROWN analyses that reports tighter bounds and higher speed than the leading Python alpha-CROWN implementation on VNN-COMP 2025 benchmarks.
citing papers explorer
-
Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
QLL is a novel logic for neuro-symbolic learning that uses ML-native operations (sum, log-sum-exp) on logits to embed constraints, satisfying most linear logic properties and showing stronger correlation between empirical robustness and formal verification than prior approaches.
-
Synthesis and Verification of Transformer Programs (Technical Report)
New verification connection from C-RASP to Lustre model checkers plus local search algorithm for synthesizing C-RASP programs from examples.
-
Viverra: Text-to-Code with Guarantees
Viverra generates C code from text descriptions together with assertions that are verified by model checkers, and a user study with over 400 participants shows the verified assertions improve code comprehension.
-
Certified geometric robustness -- Super-DeepG
Super-DeepG improves linear relaxation techniques and Lipschitz optimization for neural network robustness certification against geometric perturbations, with a GPU implementation that claims better precision and speed than prior work.
-
The Luna Bound Propagator for Formal Analysis of Neural Networks
Luna delivers a C++ bound propagator supporting interval, DeepPoly/CROWN, and alpha-CROWN analyses that reports tighter bounds and higher speed than the leading Python alpha-CROWN implementation on VNN-COMP 2025 benchmarks.