该论文表明，通过使用现有的证明助理，可以以与建立证明助理自身的信任和可审计性原则相一致的方式，构建对自然语言表达的规范的支持。我们在 Lean 证明助理内实现了一种方式，以可扩展的正式英语子集提供规范，并自动将其翻译成正式的命题。我们的方法是可扩展的（对语法结构没有永久限制），模块化的（允许在库中分发有关新词的信息），并且生成解释了每个词的解释方式以及如何使用句子结构来计算含义的证明证书。我们将原型应用于从一本流行教材中翻译各种正式规范的英文描述；在仅需进行小幅修改的情况下，借助一个适度的词汇表，所有规范都能被正确翻译。

Oct, 2023

介绍了一种概率类型的自然推导演算法，能够推导出概率计算过程的可信性，并通过对频率和预期概率之间的距离进行假设检验来形式化信任。该演算法在验证自动分类算法方面有潜在应用。

Jun, 2022

本研究旨在通过引入 TrustGPT，评价 LLMs 在毒性、偏见和价值对齐三个关键领域，以促进更具伦理和社会责任感的语言模型的发展。

Jun, 2023

基于预定义的领域知识图谱，本文提出了一种系统的方法来衡量大型语言模型的可信度，其过程中人类参与验证和优化系统，该方法对于在卫生保健、国防、金融等关键环境中运营的实体以及所有大型语言模型用户十分重要。

Mar, 2024

提出了第一个全面的阿拉伯语语言模型信任度基准 ——AraTrust，其中包含了多个方面的真实性、伦理、安全性、身体健康、心理健康、不公正、非法活动、隐私和冒犯性语言的 516 道人工多项选择题。通过引入 AraTrust，旨在促进共同努力，为阿拉伯用户创造更安全、更值得信赖的语言模型，其中 GPT-4 在阿拉伯语方面表现出最高的可信度。

Mar, 2024

Laurel 是一种使用大型语言模型（LLMs）自动生成 Dafny 程序的辅助断言的工具，通过两种领域特定的提示技术，能够提高 LLMs 在此任务中的成功率，从而使 LLMs 成为进一步自动化实际程序验证的可用且经济实惠的工具。

May, 2024

介绍了 TrustLLM，这是一个关于 LLM（大型语言模型）信任度的综合研究，包括不同维度的信任度原则、建立的基准、评估和分析主流 LLM 的信任度，以及对开放挑战和未来方向的讨论。

Jan, 2024

该论文介绍了一种名为 LogicGuide 的工具，通过设置有状态和增量约束来指导语言模型的理性推理，即模型在这个指导下生成的内容是合理的。经过测试，LogicGuide 工具有效地提高了 GPT-3、GPT-3.5 Turbo 和 LLaMA 等模型的性能。

Jun, 2023

通过在交互证明助理中引入自然语言规范支持，可以在验证软件正确性的同时保证规范翻译的正确性和可审计性。

May, 2022

本文介绍了两款新的工具 ——Proof Tree Automaton 和 Proof Tree Graph—— 来帮助我们使用图论和自动机理论的方法处理大型演算，本文探讨了 PTA 和 PTG 之间的相关性，并展示了我们如何将 PTA 分解为从一个演算到传统树自动机的部分映射。最后，本文将我们的框架与证明网和字符串图进行了比较。

Jun, 2022