Leveraging LLM Reasoning with Dual Horn Programs
summary
Claims that Dual Horn programs produce constructive falsifications with actual variable bindings and that a compilation to Horn clauses preserves performance, enabling goal-directed forward and backward reasoning. Implements an embedded SymLP language and a DeepLM Streamlit pipeline that generates propositional Horn/Dual-Horn programs, compiles dual clauses into a module false, and computes the unique minimal model in linear time (P-complete propositional class). Demonstrations include recursive consequence exploration (Fed independence, nuclear escalation) and a stock example yielding cautious buy answers (QQQ, Apple, Met, Berkshire).
AI-written summary · about
chapters (18)
- 0:00LLM reasoning with dual horn programs
- 2:55Negation as failure harmful
- 6:31Constructive logic challenges
- 10:36Dual horn clauses and falsification
- 13:11Goal-directed forward reasoning
- 14:59Symmetric logic in Prologue
- 17:12Fed independence risks
- 18:58DLM for recursive knowledge extraction
- 21:33Abducible clauses in OWL semantics
- 22:16Default reasoning with dual horn
- 23:39Stock evaluation with positive/negative advice
- 26:19Positive and negative logic merits
- 26:39DLM for task decomposition
- 27:43Minimizing LLM inaccuracies
- 28:05Nuclear escalation risks
- 28:46Dual programs vs constructive negation
- 30:33Generative AI and logic synergy
- 31:07Q&A
related talks
22mTowards Verified Code Reasoning by LLMs
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better
53mSemantics-based program manipulation in the age of LLMs
01h 04mInvited Talk: Finding Good Programs by Avoiding Bad Ones
31mBeyond LLMs and Maturing RAG use cases
30mToward Programming Languages for Reasoning -- Humans, Symbolic Systems, and AI ...
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
19mLLM-Integrated Declarative Program Analysis