用大模型自动把政策文本转为可验证的逻辑形式，确保合规性。
A Neurosymbolic Approach to Natural Language Formalization and Verification
- 利用大模型+人工指导将自然语言政策转化为形式化逻辑
- 推理时多轮形式化并比对语义，准确率达99%以上，误报近乎为零
- 生成可审计结果，适合金融医疗等强监管领域使用
大型语言模型在自然语言理解和推理方面表现良好，但缺乏形式正确性保证，限制了其在金融、医疗等严格监管行业的应用。为此，我们推出了自动化推理检查（ARc）：一项公共服务，(1) 使用大模型结合可选的人工指导，将自然语言政策形式化，实现对形式化过程的细粒度控制；(2) 在推理时通过自动形式化验证自然语言陈述是否符合政策。ARc在推理时执行多次冗余形式化步骤，并检查形式化结果之间的语义等价性。基准测试显示，ARc的可靠性超过99%，识别逻辑有效性的误报率接近零。该方法生成可审计的产物，可佐证验证结果，并用于改进原始文本。ARc是主要云服务商首次将自动化推理集成到生成式AI安全护栏中的商业产品。
原文摘要 · Abstract (English)
Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries like finance and health-care that operate under strict policies. To address this limitation, we launched Automated Reasoning checks (ARc): a public service that (1) uses LLMs with optional human guidance to formalize natural language policies, allowing fine-grained control of the formalization process, and (2) uses inference-time autoformalization to validate logical correctness of natural language statements against those policies. ARc performs multiple redundant formalization steps at inference time, checking the formalizations for semantic equivalence. Our benchmarks show that ARc exceeds 99% soundness and achieves a near-zero false positive rate in identifying logical validity. Our approach produces auditable artifacts that substantiate the verification outcomes and can be used to improve the original text. ARc is the first commercial offering from a major cloud provider to integrate automated reasoning into a generative AI guardrail.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。