Cover Image

Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Bharti, Varun, Jha, Shashwat, Kumar, Dhruv, Jalote, Pankaj
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Machine Learning Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Automated Type Annotation in Python Using Large Language Models
by: Bharti, Varun, et al.
Published: (2025)

Neuro-Symbolic Compliance: Integrating LLMs and SMT Solvers for Automated Financial Legal Analysis
by: Hsia, Yung-Shen, et al.
Published: (2026)

An Encoding for CLP Problems in SMT-LIB
by: Amrollahi, Daneshvar, et al.
Published: (2024)

A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
by: King, Daragh, et al.
Published: (2025)

MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents
by: Anand, Ashwani, et al.
Published: (2026)

CIll: CTI-Guided Invariant Generation via LLMs for Model Checking
by: Su, Yuheng, et al.
Published: (2026)

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
by: Zilberstein, Noam, et al.
Published: (2024)

'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
by: Judson, Samuel, et al.
Published: (2023)

Lattice Annotated Temporal (LAT) Logic for Non-Markovian Reasoning
by: Mukherji, Kaustuv, et al.
Published: (2025)

Hybrid Models for Natural Language Reasoning: The Case of Syllogistic Logic
by: Guzmán, Manuel Vargas, et al.
Published: (2025)

Boosting Few-Pixel Robustness Verification via Covering Verification Designs
by: Shapira, Yuval, et al.
Published: (2024)

Smart Choices and the Selection Monad
by: Abadi, Martin, et al.
Published: (2020)

Mini-Batch Robustness Verification of Deep Neural Networks
by: Tzour-Shaday, Saar, et al.
Published: (2025)

Towards a Certified Proof Checker for Deep Neural Network Verification
by: Desmartin, Remi, et al.
Published: (2023)

Programmatic Reinforcement Learning: Navigating Gridworlds
by: Shabadi, Guruprerana, et al.
Published: (2024)

Floating-Point Neural Networks Are Provably Robust Universal Approximators
by: Hwang, Geonho, et al.
Published: (2025)

Neural Network Verification is a Programming Language Challenge
by: Cordeiro, Lucas C., et al.
Published: (2025)

Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
by: Ye, Kangfeng, et al.
Published: (2023)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
by: Viennot, Jules, et al.
Published: (2025)

ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
by: Vin, Eric, et al.
Published: (2025)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2025)

NLP Verification: Towards a General Methodology for Certifying Robustness
by: Casadio, Marco, et al.
Published: (2024)

RLSF: Fine-tuning LLMs via Symbolic Feedback
by: Jha, Piyush, et al.
Published: (2024)

From Symbolic Tasks to Code Generation: Diversification Yields Better Task Performers
by: Zhang, Dylan, et al.
Published: (2024)

PolyQEnt: A Polynomial Quantified Entailment Solver
by: Chatterjee, Krishnendu, et al.
Published: (2024)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
by: Rustenholz, Louis, et al.
Published: (2024)

Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning
by: Luo, Ziyan, et al.
Published: (2023)

SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas
by: Wei, Anjiang, et al.
Published: (2025)

Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving
by: Rajaee, Sara, et al.
Published: (2025)

MathConstraint: Automated Generation of Verified Combinatorial Reasoning Instances for LLMs
by: Pati, Viresh, et al.
Published: (2026)

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
by: Hader, Thomas, et al.
Published: (2024)

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
by: Tsoukalas, George, et al.
Published: (2024)

Meaningfulness and Genericity in a Subsuming Framework
by: Kesner, Delia, et al.
Published: (2024)

LLM2SMT: Building an SMT Solver with Zero Human-Written Code
by: Janota, Mikoláš, et al.
Published: (2026)

An In-Context Learning Agent for Formal Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2023)

Decidable By Construction: Design-Time Verification for Trustworthy AI
by: Haynes, Houston
Published: (2026)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
by: Li, Guchan, et al.
Published: (2026)

Verification Modulo Tested Library Contracts
by: Uppar, Abhishek, et al.
Published: (2026)

Structured Abductive-Deductive-Inductive Reasoning for LLMs via Algebraic Invariants
by: Gilda, Sankalp, et al.
Published: (2026)

VERINA: Benchmarking Verifiable Code Generation
by: Ye, Zhe, et al.
Published: (2025)