Proof-Carrying Neuro-Symbolic Code
This invited paper introduces the concept of "proof-carrying neuro-symbolic code" and explains its meaning and value, from both the "neural" and the "symbolic" perspectives. The talk outlines the first successes and challenges that this new area of research faces.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction
We propose ProofNet++, a neuro-symbolic framework that enhances automated theorem proving by combining large language models (LLMs) with formal proof verification and self-correction mechanisms. Current LLM-based systems…
Automated Theorem ProvingProving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
Large language models (LLMs) can prove mathematical theorems formally by generating proof steps (\textit{a.k.a.} tactics) within a proof system. However, the space of possible tactics is vast and complex, while the avail…
Mathematical ReasoningConstructing a Neuro-Symbolic Mathematician from First Principles
Large Language Models (LLMs) exhibit persistent logical failures in complex reasoning due to the lack of an internal axiomatic framework. We propose Mathesis, a neuro-symbolic architecture that encodes mathematical state…
A Semantic Framework for Neuro-Symbolic Computing
The field of neuro-symbolic AI aims to benefit from the combination of neural networks and symbolic systems. A cornerstone of the field is the translation or encoding of symbolic knowledge into neural networks. Although …
Lemmanaid: Neuro-Symbolic Lemma Conjecturing
Automatically conjecturing useful, interesting and novel lemmas would greatly improve automated reasoning tools and lower the bar for formalizing mathematics in proof assistants. It is however a very challenging task for…
LEMMA