让神经符号代码自带可验证证明，提升可信度与安全性。

Proof-Carrying Neuro-Symbolic Code

• 神经与符号计算融合，代码自带形式化证明。
• 首次实现可验证的神经符号程序运行。
• 适合对安全性和可解释性要求高的系统设计者。

本文提出「证明携带型神经符号代码」概念，从神经与符号两个视角阐述其意义与价值。该方法将形式化证明嵌入神经符号程序中，使代码在执行时可被自动验证。演讲回顾了该研究领域的首批成果与当前挑战，包括如何高效生成和验证证明、如何协调神经模块与符号推理的不确定性。该范式有望显著提升复杂智能系统的可靠性与可解释性，尤其适用于自动驾驶、医疗诊断等高风险场景。

原文摘要 · Abstract (English)

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.

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。