Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mastodon.gamedev.place is one of the many independent Mastodon servers you can use to participate in the fediverse.
Mastodon server focused on game development and related topics.

Administered by:

Server stats:

5.6K
active users

mastodon.gamedev.place: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.5

#smt

4 posts4 participants0 posts today
Public
Benjamin Carr, Ph.D. 👨🏻‍💻🧬

SMT Remains Very Advantageous For #Zen5 #AMD #EPYC Performance
#SMT typically was of measurable benefit to the 5th Gen AMD EPYC processor with the exception of some #HPC workloads that perform better with SMT disabled or otherwise limited by memory bandwidth. SMT also hurt the OpenVINO inference latency but by and large Simultaneous Multi-Threading remains an important and valuable feature for AMD processors.
phoronix.com/review/amd-epyc-z

www.phoronix.comSMT Remains Very Advantageous For 5th Gen AMD EPYC Performance Review
Public
José A. Alonso

NL2FOL: Translating natural language to first-order logic for logical fallacy detection. ~ Abhinav Lalwani et als. arxiv.org/abs/2405.02318 #LLMs #Logig #SMT

arXiv logo
arXiv.orgNL2FOL: Translating Natural Language to First-Order Logic for Logical Fallacy DetectionTranslating natural language into formal language such as First-Order Logic (FOL) is a foundational challenge in NLP with wide-ranging applications in automated reasoning, misinformation tracking, and knowledge validation. In this paper, we introduce Natural Language to First-Order Logic (NL2FOL), a framework to autoformalize natural language to FOL step by step using Large Language Models (LLMs). Our approach addresses key challenges in this translation process, including the integration of implicit background knowledge. By leveraging structured representations generated by NL2FOL, we use Satisfiability Modulo Theory (SMT) solvers to reason about the logical validity of natural language statements. We present logical fallacy detection as a case study to evaluate the efficacy of NL2FOL. Being neurosymbolic, our approach also provides interpretable insights into the reasoning process and demonstrates robustness without requiring model fine-tuning or labeled training data. Our framework achieves strong performance on multiple datasets. On the LOGIC dataset, NL2FOL achieves an F1-score of 78%, while generalizing effectively to the LOGICCLIMATE dataset with an F1-score of 80%.
Public
José A. Alonso

Logic.py: Bridging the gap between LLMs and constraint solvers. ~ Pascal Kesseli, Peter O'Hearn, Ricardo Silveira Cabral. arxiv.org/abs/2502.15776 #LLMs #Logic #SAT #SMT

arXiv.orgLogic.py: Bridging the Gap between LLMs and Constraint SolversWe present a novel approach to formalise and solve search-based problems using large language models, which significantly improves upon previous state-of-the-art results. We demonstrate the efficacy of this approach on the logic puzzles benchmark ZebraLogicBench. Instead of letting the LLM attempt to directly solve the puzzles, our method prompts the model to formalise the problem in a logic-focused domain-specific language (DSL) called Logic.py. This formalised representation is then solved using a constraint solver, leveraging the strengths of both the language model and the solver. Our approach achieves a remarkable 65% absolute improvement over the baseline performance of Llama 3.1 70B on ZebraLogicBench, setting a new state-of-the-art with an accuracy of over 90%. This significant advancement demonstrates the potential of combining language models with domain-specific languages and auxiliary tools on traditionally challenging tasks for LLMs.
Public
José A. Alonso

Instantiation-based formalization of logical reasoning tasks using language models and logical solvers. ~ Mohammad Raza, Natasa Milic-Frayling. arxiv.org/abs/2501.16961 #LLMs #Reasoning #SMT #Z3

arXiv.orgInstantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical SolversRobustness of reasoning remains a significant challenge for large language models, and addressing it is essential for the practical applicability of AI-driven reasoning systems. We introduce Semantic Self-Verification (SSV), a novel approach that addresses the key challenge in combining language models with the rigor of logical solvers: to accurately formulate the reasoning problem from natural language to the formal language of the solver. SSV uses a consistency-based approach to produce strong abstract formalizations of problems using concrete instantiations that are generated by the model and verified by the solver. In addition to significantly advancing the overall reasoning accuracy over the state-of-the-art, a key novelty that this approach presents is a feature of verification that has near-perfect precision over a significant coverage of cases, as we demonstrate on open reasoning benchmarks. We propose such *near-certain reasoning* as a new approach to reduce the need for manual verification in many cases, taking us closer to more dependable and autonomous AI reasoning systems.
Public
Jeremy

Just bought the original #Persona3 soundtrack! I was thinking about getting that of SMT5 or SMT4 instead since I beat those and never played through the original P3 but I find #Persona music more enjoyable to listen to on its own than #SMT music. The latter is a lot more atmospheric.

I want the P5R and P3P soundtracks too but I’m going to continue holding off on them until I beat their respective games.

Public
José A. Alonso

Evaluating SAT and SMT solvers on large-scale sudoku puzzles. ~ Liam Davis, Tairan Ji. arxiv.org/abs/2501.08569 #SAT #SMT

arXiv.orgEvaluating SAT and SMT Solvers on Large-Scale Sudoku PuzzlesModern SMT solvers have revolutionized the approach to constraint satisfaction problems by integrating advanced theory reasoning and encoding techniques. In this work, we evaluate the performance of modern SMT solvers in Z3, CVC5 and DPLL(T) against a standard SAT solver in DPLL. By benchmarking these solvers on novel, diverse 25x25 Sudoku puzzles of various difficulty levels created by our improved Sudoku generator, we examine the impact of advanced theory reasoning and encoding techniques. Our findings demonstrate that modern SMT solvers significantly outperform classical SAT solvers. This work highlights the evolution of logical solvers and exemplifies the utility of SMT solvers in addressing large-scale constraint satisfaction problems.
ExploreLive feeds
About