paper-with-me

Papers

SMLP: Symbolic Machine Learning Prover (User Manual)

2024-05-16 · Franz Brauße, Zurab Khasidashvili, Konstantin Korovin

SMLP: Symbolic Machine Learning Prover an open source tool for exploration and optimization of systems represented by machine learning models. SMLP uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint and NN solvers. In addition its exploration methods are guided by probabilistic and statistical methods. SMLP is a general purpose tool that requires only data suitable for ML modelling in the csv format (usually samples of the system's input/output). SMLP has been applied at Intel for analyzing and optimizing hardware designs at the analog level. Currently SMLP supports NNs, polynomial and tree models, and uses SMT solvers for reasoning and optimization at the backend, integration of specialized NN solvers is in progress.

📄 PDF Abstract BibTeX arXiv:2405.10215

Code (1)

fbrausse/smlp 공식 구현 tf

Similar Papers 제목 키워드 기반

SMLP: Symbolic Machine Learning Prover

2024-02-02 · Franz Brauße, Zurab Khasidashvili, Konstantin Korovin

Symbolic Machine Learning Prover (SMLP) is a tool and a library for system exploration based on data samples obtained by simulating or executing the system on a number of input vectors. SMLP aims at exploring the system …

Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs

2026-05-06 · Beibei Xiong, Hangyu Lv, Junqi Liu, Yisen Wang 외 arxiv

Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Symbolic methods such as the Wilf-Zeilberge…

UFAL-CUNI at SemEval-2026 Task 11: An Efficient Modular Neuro-symbolic Method for Syllogistic Reasoning

2026-05-06 · Ivan Kartáč, Kristýna Onderková, Jan Bronec, Zdeněk Kasner 외 arxiv

This paper describes our system submitted to SemEval-2026 Task 11: Disentangling Content and Formal Reasoning in Large Language Models. We present an efficient modular neuro-symbolic approach, combining a symbolic prover…

Machine Translation

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization

2026-05-21 · Riyaz Ahuja, Tate Rowney, Jeremy Avigad, Sean Welleck arxiv

Formal mathematics libraries are rapidly expanding, creating a growing need to refactor verified proofs for maintainability and to improve training data quality for neural provers. However, scalable proof optimization is…

A Closer Look at Logical Reasoning with LLMs: The Choice of Tool Matters

2024-06-01 · Long Hei Matthew Lam, Ramya Keerthy Thatikonda, Ehsan Shareghi

The emergence of Large Language Models (LLMs) has demonstrated promising progress in solving logical reasoning tasks effectively. Several recent approaches have proposed to change the role of the LLM from the reasoner in…

Logical ReasoningTranslation