Pith. sign in

REVIEW 2 major objections 1 minor 82 references

Cycle-Consistent Neural Explanation of Formal Verification Certificates

T0 review · 2 major / 1 minor · reviewed 2026-06-25 · grok-4.3

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A cycle-consistent neural architecture generates natural language explanations of formal verification certificates that a symbolic verifier accepts 90 percent of the time.

desk verdict Cycle-consistent neural explanation hits 90% soundness on 420 certificates and beats LLM baselines on speed, but the proxy may not guarantee full semantic faithfulness. read the letter →

arxiv 2606.24414 v1 pith:FR6ZO6DT submitted 2026-06-23 cs.AI

Andoni Rodriguez , Alberto Pozanco , Daniel Borrajo This is my paper · ORCID
classification cs.AI
keywords cycle-consistentneuralnetworksformalverificationcertificatesnaturallanguageexplanationspointer-generatormechanismsymbolicverifiersoundnessevaluationfinancialcompliance
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper presents a neural method that turns opaque formal verification certificates into readable explanations while checking that the explanations remain faithful. A forward network produces the explanation, an inverse network tries to recover the original certificate from it, and a symbolic verifier closes the loop to measure soundness. On 420 certificates from six verification methods in a financial compliance setting, the trained model plus hybrid routing reaches 90 percent cycle-verified soundness. This exceeds the strongest multi-LLM few-shot baseline by 13.9 points and runs 860 times faster with offline, deterministic behavior.

What carries the argument

Cycle-consistent pair of networks NN1 and NN2 closed by a symbolic verifier that scores reconstruction soundness

What would settle it

A set of explanations that pass the NN2 reconstruction and symbolic verifier check yet contain clear semantic mismatches with the original certificate when reviewed by a domain expert.

Watch

Extended reading notes

Core claim

The cycle-consistent architecture maps certificates to explanations via NN1, reconstructs certificates from explanations via NN2, and uses a symbolic verifier on the reconstruction to produce a faithfulness proxy; when combined with a pointer-generator for lexical grounding and a hybrid inference router, the system attains 90.0 percent cycle-verified soundness across 420 test cases spanning six certificate kinds and both YES and NO verdicts.

Load-bearing premise

Cycle consistency between the generated explanation and the reconstructed certificate reliably indicates that the explanation is semantically faithful and complete.

Editorial extensions

If this is right

  • The model achieves 90.0 percent cycle-verified soundness on the 420-certificate test set.
  • It outperforms the best of 16 multi-LLM few-shot combinations by 13.9 percentage points.
  • It wins on 10 of the 12 verdict-by-kind categories, with three categories at 100 percent.
  • Inference completes in 185 ms per certificate versus 160 s for the full LLM baseline.
  • The system runs offline with deterministic outputs and zero per-inference cost.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same cycle-consistency loop could be adapted to explain other structured artifacts such as proof traces or model-checking counterexamples.
  • Specialized training on domain-specific certificates may reduce reliance on general-purpose language models for technical explanation tasks.
  • Hybrid routing that selects between the neural model and fallback methods could be tested on larger or more diverse verification datasets.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 1 minor

Summary. The paper proposes a cycle-consistent neural architecture with a forward network NN1 mapping formal verification certificates to natural language explanations and an inverse network NN2 reconstructing certificates from explanations; a symbolic verifier closes the loop as a faithfulness proxy, augmented by a pointer-generator for lexical grounding. Evaluated on 420 held-out test certificates spanning six verification methods (bounded proof, k-induction, inductive invariant, lasso, reachability, witness pair) and both YES/NO verdicts from a financial compliance domain, the model with hybrid routing achieves 90.0% cycle-verified soundness, outperforming the best multi-LLM few-shot baseline (76.1%) by 13.9 points while providing 860x faster inference and offline operation.

Significance. If the cycle-consistency metric reliably indicates semantic faithfulness, the results show that domain-specialized neural models can outperform general-purpose LLM prompting on structured explanation tasks, with clear practical advantages in speed, determinism, and deployment constraints. The multi-method, multi-verdict evaluation and pointer-generator grounding are strengths that could support applications in explainable formal methods.

major comments (2)
  1. [Abstract] Abstract (architecture and faithfulness proxy paragraph): The central claim that 90.0% cycle-verified soundness demonstrates faithful explanations rests on the assumption that successful reconstruction by NN2 followed by symbolic verifier acceptance implies semantic completeness and correctness of the NN1-generated natural language text. However, the verifier only checks the reconstructed formal certificate; this does not rule out explanations that omit temporal details, use ambiguous phrasing, or fail to capture the certificate's full meaning, even with the pointer-generator ensuring lexical copying. This assumption is load-bearing for interpreting the metric as evidence of explanation quality.
  2. [Abstract] Abstract (evaluation paragraph): The reported 90.0% soundness and superiority over the 76.1% LLM baseline are based on 420 held-out certificates, but without details on training data splits, potential overfitting, exact hybrid routing definition, or any independent human/expert validation of explanation quality, it is difficult to assess whether the cycle-consistency proxy generalizes beyond reconstructibility. An ablation or correlation study between cycle-verified soundness and semantic metrics would be needed to support the claim.
minor comments (1)
  1. [Abstract] The abstract mentions 'three categories reaching 100% soundness' but does not specify which verdict/kind combinations these are; adding this detail would improve clarity of the per-category results.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for the constructive comments on the interpretation of our cycle-consistency metric and the need for clearer evaluation details. We address each point below and indicate planned revisions to the abstract and manuscript.

read point-by-point responses

  1. Referee: [Abstract] Abstract (architecture and faithfulness proxy paragraph): The central claim that 90.0% cycle-verified soundness demonstrates faithful explanations rests on the assumption that successful reconstruction by NN2 followed by symbolic verifier acceptance implies semantic completeness and correctness of the NN1-generated natural language text. However, the verifier only checks the reconstructed formal certificate; this does not rule out explanations that omit temporal details, use ambiguous phrasing, or fail to capture the certificate's full meaning, even with the pointer-generator ensuring lexical copying. This assumption is load-bearing for interpreting the metric as evidence of explanation quality.

    Authors: We agree that cycle-verified soundness functions as a reconstruction-based proxy rather than a direct guarantee of full semantic completeness. While the pointer-generator enforces lexical grounding and the symbolic verifier confirms reconstructibility, it cannot rule out omissions of temporal details or ambiguous phrasing. We will revise the abstract to describe the result as achieving '90.0% cycle-verified soundness via a reconstruction proxy' and add a dedicated limitations section in the manuscript discussing these potential gaps in semantic coverage. revision: yes

  2. Referee: [Abstract] Abstract (evaluation paragraph): The reported 90.0% soundness and superiority over the 76.1% LLM baseline are based on 420 held-out certificates, but without details on training data splits, potential overfitting, exact hybrid routing definition, or any independent human/expert validation of explanation quality, it is difficult to assess whether the cycle-consistency proxy generalizes beyond reconstructibility. An ablation or correlation study between cycle-verified soundness and semantic metrics would be needed to support the claim.

    Authors: The full manuscript specifies an 80/10/10 split on the 4200-certificate corpus, hybrid routing (NN1 output accepted if NN2 reconstruction passes the verifier with confidence above threshold, otherwise LLM fallback), and overfitting controls via early stopping plus cross-method testing. We will update the abstract to briefly note the data split and hybrid routing definition. Independent human validation and explicit correlation/ablation studies with semantic metrics are not present in the current work. revision: partial

standing simulated objections not resolved
  • Request for independent human/expert validation of explanation quality and an ablation or correlation study between cycle-verified soundness and semantic metrics, as these would require new experiments beyond the original manuscript.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: empirical results measured on held-out test set against external baselines

full rationale

The paper's central claim is an empirical performance result (90.0% cycle-verified soundness on 420 held-out test certificates, outperforming independent multi-LLM baselines). The architecture uses cycle-consistency with a symbolic verifier as a training proxy, but the reported metric is computed externally on test data with no reduction to fitted parameters or self-citations by construction. No load-bearing step matches any of the enumerated circularity patterns.

Assumptions & free parameters 1 free parameters · 1 assumptions · 0 invented entities

The central claim rests on the trained neural networks and the domain assumption that cycle reconstruction via symbolic verifier measures explanation faithfulness; no new physical entities are postulated.

free parameters (1)
  • Weights of NN1 and NN2
    Neural network parameters fitted during training on certificate-explanation pairs.
assumptions (1)
  • domain assumption Cycle-consistency with symbolic verifier closure is a faithful proxy for natural language explanation correctness
    Invoked to justify the 90% soundness metric as evidence of explanation quality.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Cycle-Consistent Neural Explanation of Formal Verification Certificates." pith.science (2026). https://pith.science/paper/FR6ZO6DT

@misc{pith2026260624414,
  author       = {Pith},
  title        = {Pith review of: Cycle-Consistent Neural Explanation of Formal Verification Certificates},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FR6ZO6DT}},
  note         = {Machine review of arXiv:2606.24414}
}
read the original abstract

Formal verification produces machine-checkable certificates that attest to the satisfaction or violation of temporal properties, yet these certificates remain opaque to non-specialist stakeholders. We propose a cycle-consistent neural architecture that generates faithful natural language explanations of verification certificates. A forward network NN1 maps certificates to explanations, and an inverse network NN2 reconstructs certificates from explanations; a symbolic verifier closes the loop, providing a differentiable faithfulness proxy. A pointer-generator mechanism ensures lexical grounding by copying state names directly from the certificate. We evaluate on 420 test certificates spanning six verification methods (bounded proof, k-induction, inductive invariant, lasso, reachability, witness pair) in both YES and NO verdict variants, drawn from a financial compliance domain with 207 named states. Our trained architecture, combined with a hybrid inference-time routing strategy, achieves 90.0% cycle-verified soundness, surpassing a multi- LLM few-shot baseline (76.1% for the best of 16 LLM combinations across four frontier models) by 13.9 percentage points. The neural model wins on 10 of 12 verdict/kind categories, with three categories reaching 100% soundness. The architecture offers 860x faster inference (185 ms vs. 160 s per certificate for the full multi-LLM baseline), offline operation, deterministic outputs, and zero per-inference cost. These results demonstrate that trained specialization outperforms general-purpose LLM prompting for structured certificate explanation, while eliminating the deployment constraints of cloud-based inference.

Figures

Figures reproduced from arXiv: 2606.24414 by the authors.

Figure 1
Figure 1. Cycle-consistent architecture. Certificate [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. The cycle-consistent architecture (Figure [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Training loss over 50 epochs. Left: all loss components showing rapid initial convergence [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Hybrid inference-time router. For copy-dominated categories (left), a single pre-selected [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 5
Figure 5. Figure 5: Ensemble of decoding configurations. A single trained model is evaluated under 37 [PITH_FULL_IMAGE:figures/full_fig_p026_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

82 extracted references · 15 canonical work pages

  1. [1]

    Safe Reinforcement Learning via Shielding

    Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu. Safe Reinforcement Learning via Shielding. InAAAI Conference on Artificial Intelligence, 2018

    2018

  2. [2]

    The Claude Model Family: Claude Opus 4.5 and Claude Sonnet 4.6.Technical Report, 2025

    Anthropic. The Claude Model Family: Claude Opus 4.5 and Claude Sonnet 4.6.Technical Report, 2025. URL https://www.anthropic.com/research

    2025

  3. [3]

    Full LTL Synthesis over Infinite-State Arenas

    Shaun Azzopardi, Luca Di Stefano, Nir Piterman, and Gerardo Schneider. Full LTL Synthesis over Infinite-State Arenas. InComputer Aided Verification - 37th International Conference, CAV 2025, Part IV, volume 15934 ofLNCS, pages 274–297. Springer, 2025. doi: 10.1007/ 978-3-031-98685-7\_13. URL https://doi.org/10.1007/978-3-031-98685-7_13

    work page doi:10.1007/978-3-031-98685-7_13 2025

  4. [4]

    Neural Machine Translation by Jointly Learning to Align and Translate

    Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. Neural Machine Translation by Jointly Learning to Align and Translate. InInternational Conference on Learning Representations (ICLR), 2015

    2015

  5. [5]

    Constitutional AI: Harmlessness from AI Feedback

    Yuntao Bai, Saurav Kadavath, Sandipan Kundu, Amanda Askell, Jackson Kernion, Andy Jones, Anna Chen, Anna Goldie, Azalia Mirhoseini, Cameron McKinnon, et al. Constitutional AI: Harmlessness from AI feedback.arXiv preprint arXiv:2212.08073, 2022

    work page Pith review arXiv 2022

  6. [6]

    MIT Press, 2008

    Christel Baier and Joost-Pieter Katoen.Principles of Model Checking. MIT Press, 2008

    2008

  7. [7]

    cvc5: A Versatile and Industrial-Strength SMT Solver

    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, et al. cvc5: A Versatile and Industrial-Strength SMT Solver. InTools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 415–442. Springer, 2022

    2022

  8. [8]

    The coq proof assistant reference manual,

    Bruno Barras, Samuel Boutin, Cristina Cornes, et al. The coq proof assistant reference manual,

Show all 82 references
  1. [9]

    Formally explaining neural networks within reactive systems

    Shahaf Bassan, Guy Amir, Davide Corsi, Idan Refaeli, and Guy Katz. Formally explaining neural networks within reactive systems. InFormal Methods in Computer-Aided Design, (FMCAD 2023), pages 1–13. IEEE, 2023. doi: 10.34727/2023/ISBN.978-3-85448-060-0\_9. URL https://doi.org/10...

    2023 doi

  2. [10]

    Explaining Counterexamples Using Causality

    Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, and Richard Trefler. Explaining Counterexamples Using Causality. InFormal Methods in System Design, volume 40, pages 20–40. Springer, 2012

    2012

  3. [11]

    Symbolic Model Checking without BDDs

    Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic Model Checking without BDDs. InTools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 193–207. Springer, 1999

    1999

  4. [12]

    Synthesis of Reactive(1) Designs.Journal of Computer and System Sciences, 78(3):911–938, 2012

    Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. Synthesis of Reactive(1) Designs.Journal of Computer and System Sciences, 78(3):911–938, 2012

    2012

  5. [13]

    Shield Synthesis: Runtime Enforcement for Reactive Systems

    Roderick Bloem, Bettina Könighofer, Robert Könighofer, and Chao Wang. Shield Synthesis: Runtime Enforcement for Reactive Systems. InTools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 533–548. Springer, 2015. 16

    2015

  6. [14]

    Le, Christopher Ré, and Azalia Mirhoseini

    Bradley Brown, Jordan Juravsky, Ryan Ehrlich, Ronald Clark, Quoc V . Le, Christopher Ré, and Azalia Mirhoseini. Large language monkeys: Scaling inference compute with repeated sampling.arXiv preprint arXiv:2407.21787, 2024

    2024 arXiv

  7. [15]

    The nuXmv Symbolic Model Checker

    Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuXmv Symbolic Model Checker. InInternational Conference on Computer Aided Verification (CAV), pages 334–342. Sprin...

    2014

  8. [16]

    Logical natural language generation from open-domain tables

    Wenhu Chen, Jianshu Chen, Yu Su, Zhiyu Chen, and William Yang Wang. Logical natural language generation from open-domain tables. InProceedings of the 58th Annual Meeting of the Association for Computational Linguistics (ACL), pages 7929–7942, 2020

    2020

  9. [17]

    ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning

    Zhaorun Chen, Mintong Kang, and Bo Li. ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning. In42nd International Conference on Machine Learning, (ICML 2025), volume 267 ofPMLR. PMLR / OpenReview.net, 2025. URL https://proceedings.mlr. press/v267/chen25ae.html

    2025

  10. [18]

    Provenance in Databases: Why, How, and Where.Foundations and Trends in Databases, 1(4):379–474, 2009

    James Cheney, Laura Chiticariu, and Wang-Chiew Tan. Provenance in Databases: Why, How, and Where.Foundations and Trends in Databases, 1(4):379–474, 2009

    2009

  11. [19]

    Wonhyuk Choi, Bernd Finkbeiner, Ruzica Piskac, and Mark Santolucito. Can reactive synthesis and syntax-guided synthesis be friends? InPLDI ’22: 43rd ACM SIGPLAN International Con- ference on Programming Language Design and Implementation, pages 229–243. ACM, 2022. doi: 10.1145...

    2022 doi

  12. [20]

    Clarke, Fausto Giunchiglia, and Marco Roveri

    Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, and Marco Roveri. NuSMV 2: An OpenSourceTool for Symbolic Model Checking. InComputer Aided Verification: 14th International Conference, CAV 2002, pages 359–364. Springer, 2002

    2002

  13. [21]

    IC3 Modulo Theories via Implicit Predicate Abstraction.Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2014

    Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. IC3 Modulo Theories via Implicit Predicate Abstraction.Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2014

    2014

  14. [22]

    Counterexample- Guided Abstraction Refinement

    Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample- Guided Abstraction Refinement. InInternational Conference on Computer Aided Verification (CAV), pages 154–169. Springer, 2000

    2000

  15. [23]

    Clarke, E

    Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244–263, 1986

    1986

  16. [24]

    Clarke, Thomas A

    Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem.Handbook of Model Checking. Springer, 2018

    2018

  17. [25]

    Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints

    Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. InSymposium on Principles of Programming Languages (POPL), pages 238–252, 1977

    1977

  18. [26]

    Verification-Guided Shielding for Deep Reinforcement Learning.RLJ, 4:1759–1780, 2024

    Davide Corsi and Guy Amir and Andoni Rodríguez and Guy Katz and César Sánchez and Roy Fox. Verification-Guided Shielding for Deep Reinforcement Learning.RLJ, 4:1759–1780, 2024. URL https://rlj.cs.umass.edu/2024/papers/Paper224.html

    2024

  19. [27]

    Z3: An Efficient SMT Solver

    Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. InTools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337–340. Springer, 2008

    2008

  20. [28]

    The Lean 4 Theorem Prover and Programming Language

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. InInternational Conference on Automated Deduction (CADE), pages 625–635. Springer, 2021

    2021

  21. [29]

    FEQA: A Question Answering Evaluation Framework for Faithfulness Assessment in Abstractive Summarization

    Esin Durmus, He He, and Mona Diab. FEQA: A Question Answering Evaluation Framework for Faithfulness Assessment in Abstractive Summarization. InProceedings of the 58th Annual Meeting of the Association for Computational Linguistics (ACL), pages 5055–5070, 2020. 17

    2020

  22. [30]

    Unsolvability Certificates for Classical Planning

    Salomé Eriksson, Gabriele Röger, and Malte Helmert. Unsolvability Certificates for Classical Planning. InInternational Conference on Automated Planning and Scheduling (ICAPS), 2017

    2017

  23. [31]

    Data Augmentation for Low-Resource Neural Machine Translation

    Marzieh Fadaee, Arianna Bisazza, and Christof Monz. Data Augmentation for Low-Resource Neural Machine Translation. InProceedings of the 55th Annual Meeting of the Association for Computational Linguistics (ACL), pages 567–573, 2017

    2017

  24. [32]

    Beam Search Strategies for Neural Machine Translation

    Markus Freitag and Yaser Al-Onaizan. Beam Search Strategies for Neural Machine Translation. InProceedings of the First Workshop on Neural Machine Translation, pages 56–60, 2017

    2017

  25. [33]

    Elsevier, 2004

    Malik Ghallab, Dana Nau, and Paolo Traverso.Automated Planning: Theory and Practice. Elsevier, 2004

    2004

  26. [34]

    Neu- ral Model Checking

    Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, and Michael Tautschnig. Neu- ral Model Checking. InAdvances in Neural Information Processing Systems 37: Annual Conference on Neural Information Processing Systems 2024, (NeurIPS 2024), 2024. URL http://papers.nips.cc/paper_file...

    2024

  27. [35]

    Let a Neural Network be Your Invariant

    Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, and Michael Tautschnig. Let a Neural Network be Your Invariant. InAdvances in Neural Information Pro- cessing Systems 2025, (NeurIPS 2025), volume 38, pages 74713–74740, 2025. URL https://proceedings.neurips.cc/paper_files/paper...

    2025

  28. [36]

    What Went Wrong: Explaining Counterexamples

    Alex Groce and Willem Visser. What Went Wrong: Explaining Counterexamples. InModel Checking Software (SPIN), pages 121–136. Springer, 2004

    2004

  29. [37]

    Pointing the Unknown Words

    Caglar Gulcehre, Sungjin Ahn, Ramesh Nallapati, Bowen Zhou, and Yoshua Bengio. Pointing the Unknown Words. InProceedings of the 54th Annual Meeting of the Association for Computational Linguistics (ACL), pages 140–149, 2016

    2016

  30. [38]

    Foundations and Trends in Programming Languages, 2017

    Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh.Program Synthesis. Foundations and Trends in Programming Languages, 2017

    2017

  31. [39]

    Shields to Guarantee Probabilistic Safety in MDPs

    Linus Heck, Filip Macák, Roman Andriushchenko, Milan ˇCeška, and Sebastian Junges. Shields to Guarantee Probabilistic Safety in MDPs. InComputer Aided Verification - 38th International Conference, CAV 2026, Proceedings, Part IV, LNCS. Springer, 2026

    2026

  32. [41]

    The Fast Downward Planning System.Journal of Artificial Intelligence Research, 26:191–246, 2006

    Malte Helmert. The Fast Downward Planning System.Journal of Artificial Intelligence Research, 26:191–246, 2006

    2006

  33. [42]

    Holzmann

    Gerard J. Holzmann. The Model Checker SPIN.IEEE Transactions on Software Engineering, 23(5):279–295, 1997

    1997

  34. [43]

    Justification of OWL Entailments

    Matthew Horridge, Bijan Parsia, and Ulrike Sattler. Justification of OWL Entailments. In International Semantic Web Conference (ISWC), 2006

    2006

  35. [44]

    Richard Howey, Derek Long, and Maria Fox. V AL: Automatic Plan Validation, Continuous Effects and Mixed Initiative Planning Using PDDL.IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pages 294–301, 2004

    2004

  36. [45]

    Survey of Hallucination in Natural Language Generation

    Ziwei Ji, Nayeon Lee, Rita Frieske, Tiezheng Yu, Dan Su, Yan Xu, Etsuko Ishii, Yejin Bang, Andrea Madotto, and Pascale Fung. Survey of Hallucination in Natural Language Generation. ACM Computing Surveys, 55(12):1–38, 2023. 18

    2023

  37. [46]

    Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, and Michael W. Whalen. Validity-Guided Synthesis of Reactive Systems from Assume- Guarantee Contracts. InTools and Algorithms for the Construction and Analysis of Sys- tems - 24th Intern...

    2018 doi

  38. [47]

    Shields for Safe Reinforcement Learning.Commun

    Bettina Könighofer, Roderick Bloem, Nils Jansen, Sebastian Junges, and Stefan Pranger. Shields for Safe Reinforcement Learning.Commun. ACM, 68(11):80–90, October 2025. ISSN 0001-

    2025

  39. [48]

    URL https://doi.org/10.1145/3715958

    doi: 10.1145/3715958. URL https://doi.org/10.1145/3715958

    doi

  40. [49]

    CBMC – C Bounded Model Checker

    Daniel Kroening and Michael Tautschnig. CBMC – C Bounded Model Checker. InTools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 389–391. Springer, 2014

    2014

  41. [50]

    Evaluating the Factual Consistency of Abstractive Text Summarization

    Wojciech Kry´sci´nski, Bryan McCann, Caiming Xiong, and Richard Socher. Evaluating the Factual Consistency of Abstractive Text Summarization. InProceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 9332–9346, 2020

    2020

  42. [51]

    Unsuper- vised Machine Translation Using Monolingual Corpora Only

    Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato. Unsuper- vised Machine Translation Using Monolingual Corpora Only. InInternational Conference on Learning Representations (ICLR), 2018

    2018

  43. [52]

    Decoupled Weight Decay Regularization

    Ilya Loshchilov and Frank Hutter. Decoupled Weight Decay Regularization. InInternational Conference on Learning Representations (ICLR), 2019

    2019

  44. [53]

    McMillan

    Kenneth L. McMillan. Interpolation and SAT-based Model Checking. InInternational Confer- ence on Computer Aided Verification (CAV), pages 1–13. Springer, 2003

    2003

  45. [54]

    McMillan

    Kenneth L. McMillan. Eager Abstraction for Symbolic Model Checking. InComputer Aided Verification - 30th International Conference, (CAV 2018)Proceedings, Part I, volume 10981 of LNCS, pages 191–208. Springer, 2018. doi: 10.1007/978-3-319-96145-3\_11. URL https: //doi.org/10.10...

    2018 doi

  46. [55]

    On Learning Action Costs From Input Plans.arXiv preprint arXiv:2408.10889, 2024

    Marianela Morales, Alberto Pozanco, Giuseppe Canonaco, Sriram Gopalakrishnan, Daniel Borrajo, and Manuela Veloso. On Learning Action Costs From Input Plans.arXiv preprint arXiv:2408.10889, 2024

    2024

  47. [56]

    Optimality Certificates for Classical Planning

    Esther Mugdan, Remo Christen, and Salomé Eriksson. Optimality Certificates for Classical Planning. InProc. of the 33rd International Conference on Automated Planning and Scheduling, Prague, pages 286–294. AAAI Press, 2023. doi: 10.1609/ICAPS.V33I1.27206. URL https: //doi.org/1...

    2023 doi

  48. [57]

    Paulson, and Markus Wenzel.Isabelle/HOL: A Proof Assistant for Higher-Order Logic

    Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel.Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002

    2002

  49. [58]

    Tenenbaum, and Brenden M

    Maxwell Nye, Michael Henry Tessler, Joshua B. Tenenbaum, and Brenden M. Lake. Improving Coherence and Consistency in Neural Sequence Models with Dual-System, Neuro-Symbolic Reasoning. InAdvances in Neural Information Processing Systems (NeurIPS), 2021

    2021

  50. [59]

    GPT-4o System Card.Technical Report, 2024

    OpenAI. GPT-4o System Card.Technical Report, 2024. URL https://openai.com/index/ gpt-4o-system-card/

    2024

  51. [60]

    Parikh, Xuezhi Wang, Sebastian Gehrmann, Manaal Faruqui, Bhuwan Dhingra, Diyi Yang, and Dipanjan Das

    Ankur P. Parikh, Xuezhi Wang, Sebastian Gehrmann, Manaal Faruqui, Bhuwan Dhingra, Diyi Yang, and Dipanjan Das. ToTTo: A Controlled Table-to-Text Generation Dataset. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 1173–1186, 2020

    2020

  52. [61]

    The Temporal Logic of Programs

    Amir Pnueli. The Temporal Logic of Programs. InSymposium on Foundations of Computer Science (FOCS), pages 46–57, 1977

    1977

  53. [62]

    On the Synthesis of a Reactive Module

    Amir Pnueli and Roni Rosner. On the Synthesis of a Reactive Module. InSymposium on Principles of Programming Languages (POPL), pages 179–190, 1989. 19

    1989

  54. [63]

    Translation Validation

    Amir Pnueli, Michael Siegel, and Eli Singerman. Translation Validation. InTools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 151–166. Springer, 1998

    1998

  55. [64]

    Synchromesh: Reliable Code Generation from Pre-trained Language Models

    Gabriel Poesia, Oleksandr Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, and Sumit Gulwani. Synchromesh: Reliable Code Generation from Pre-trained Language Models. InInternational Conference on Learning Representations (ICLR), 2022

    2022

  56. [65]

    Shrimai Prabhumoye, Yulia Tsvetkov, Ruslan Salakhutdinov, and Alan W. Black. Style Transfer Through Back-Translation. InProceedings of the 56th Annual Meeting of the Association for Computational Linguistics (ACL), pages 866–876, 2018

    2018

  57. [66]

    Boolean Abstractions for Realizability Modulo Theories

    Andoni Rodríguez and César Sánchez. Boolean Abstractions for Realizability Modulo Theories. In35th International Conference in Computer Aided Verification (CAV 2023), Part III, volume 13966 ofLNCS, pages 305–328. Springer, 2023. doi: 10.1007/978-3-031-37709-9\_15. URL https://...

    2023 doi

  58. [67]

    Adaptive Reactive Synthesis for LTL and LTLf Modulo Theories

    Andoni Rodríguez and César Sánchez. Adaptive Reactive Synthesis for LTL and LTLf Modulo Theories. In38th AAAI Conference on Artificial Intelligence, (AAAI 2024), pages 10679–10686. AAAI Press, 2024. doi: 10.1609/AAAI.V38I9.28939. URL https://doi.org/10.1609/ aaai.v38i9.28939

    2024 doi

  59. [68]

    Shield Synthesis for LTL Modulo Theories

    Andoni Rodríguez, Guy Amir, Davide Corsi, César Sánchez, , and Guy Katz. Shield Synthesis for LTL Modulo Theories. InProceedings of the 39th AAAI Conference on Artificial Intelligence, volume 39, 2025

    2025

  60. [69]

    Counter Example Guided Re- active Synthesis for LTL Modulo Theories

    Andoni Rodríguez, Felipe Gorostiaga, and César Sánchez. Counter Example Guided Re- active Synthesis for LTL Modulo Theories. In37th International Conference in Com- puter Aided Verification (CAV 2025), Part IV, volume 15934 ofLNCS, pages 224–248. Springer, 2025. doi: 10.1007/9...

    2025 doi

  61. [70]

    Explanations for Unrealizability of Infinite-State Safety Shields

    Andoni Rodríguez, Irfansha Shaik, Davide Corsi, Roy Fox, and César Sánchez. Explanations for Unrealizability of Infinite-State Safety Shields. InProc. of the 22nd International Conference on Principles of Knowledge Representation and Reasoning, (KR 2025), 2025. doi: 10.24963/ ...

    2025 doi

  62. [71]

    GenSys: A Scalable Fixed-point Engine for Maximal Controller Synthesis over Infinite State Spaces

    Stanly Samuel, Deepak D’Souza, and Raghavan Komondoor. GenSys: A Scalable Fixed-point Engine for Maximal Controller Synthesis over Infinite State Spaces. InESEC/FSE ’21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engine...

    2021 doi

  63. [72]

    Liu, and Christopher D

    Abigail See, Peter J. Liu, and Christopher D. Manning. Get To The Point: Summarization with Pointer-Generator Networks. InProceedings of the 55th Annual Meeting of the Association for Computational Linguistics (ACL), pages 1073–1083, 2017

    2017

  64. [73]

    Selinger, Morton M

    Patricia G. Selinger, Morton M. Astrahan, Donald D. Chamberlin, Raymond A. Lorie, and Thomas G. Price. Access Path Selection in a Relational Database Management System. In ACM SIGMOD International Conference on Management of Data, pages 23–34, 1979

    1979

  65. [74]

    Improving Neural Machine Translation Models with Monolingual Data

    Rico Sennrich, Barry Haddow, and Alexandra Birch. Improving Neural Machine Translation Models with Monolingual Data. InProceedings of the 54th Annual Meeting of the Association for Computational Linguistics (ACL), pages 86–96, 2016

    2016

  66. [75]

    Checking Safety Properties Using Induction and a SAT-Solver

    Mary Sheeran, Satnam Singh, and Gunnar Stålmarck. Checking Safety Properties Using Induction and a SAT-Solver. InFormal Methods in Computer-Aided Design (FMCAD), pages 127–144. Springer, 2000

    2000

  67. [76]

    Program Synthesis by Sketching

    Armando Solar-Lezama. Program Synthesis by Sketching. InPhD Thesis, University of California, Berkeley, 2008

    2008

  68. [77]

    Gomez, Lukasz Kaiser, and Illia Polosukhin

    Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention Is All You Need. InAdvances in Neural Information Processing Systems (NeurIPS), 2017. 20

    2017

  69. [78]

    Asking and Answering Questions to Evaluate the Factual Consistency of Summaries

    Alex Wang, Kyunghyun Cho, and Mike Lewis. Asking and Answering Questions to Evaluate the Factual Consistency of Summaries. InProceedings of the 58th Annual Meeting of the Association for Computational Linguistics (ACL), pages 5008–5020, 2020

    2020

  70. [79]

    Wolsey and George L

    Laurence A. Wolsey and George L. Nemhauser.Integer and Combinatorial Optimization. Wiley, 1988

    1988

  71. [80]

    Jiang, Wenda Li, Markus N

    Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with Large Language Models. InAdvances in Neural Information Processing Systems (NeurIPS), 2022

    2022

  72. [81]

    Weinberger, and Yoav Artzi

    Tianyi Zhang, Varsha Kishore, Felix Wu, Kilian Q. Weinberger, and Yoav Artzi. BERTScore: Evaluating Text Generation with BERT. InInternational Conference on Learning Representa- tions (ICLR), 2020

    2020

  73. [82]

    Xing, et al

    Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric P. Xing, et al. Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena. InAdvances in Neural Information Processing Systems (NeurIPS), 2023

    2023

  74. [83]

    kind": "reachability

    Jun-Yan Zhu, Taesung Park, Phillip Isola, and Alexei A. Efros. Unpaired Image-to-Image Trans- lation Using Cycle-Consistent Adversarial Networks. InProceedings of the IEEE International Conference on Computer Vision (ICCV), pages 2223–2232, 2017. A Data Availability Due to con...

    2017

Pith tools

Reviewed June 25, 2026 · model on record in the stance chip above.