Jove
Visualize
联系我们
JoVE
x logofacebook logolinkedin logoyoutube logo
关于 JoVE
概览领导团队博客JoVE 帮助中心
作者
出版流程编辑委员会范围与政策同行评审常见问题投稿
图书馆员
用户评价订阅访问资源图书馆顾问委员会常见问题
研究
JoVE JournalMethods CollectionsJoVE Encyclopedia of Experiments存档
教育
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab Manual教师资源中心教师网站
使用条款与条件
隐私政策
政策

相关概念视频

Language and Cognition01:27

Language and Cognition

681
Language serves as a bridge between ideas and communication, influencing how individuals perceive and interact with the world. Psychologists have long debated whether language shapes thought or vice versa. This discussion gained grip with Edward Sapir and Benjamin Lee Whorf in the 1940s, who proposed that language determines thought, a concept known as linguistic determinism. They suggested that the vocabulary and structure of a language influence how its speakers think and perceive reality.
681
Language Development01:22

Language Development

801
Children master language quickly and with relative ease, supported by both biological predisposition and reinforcement. B. F. Skinner (1957) proposed that language is learned through reinforcement, while Noam Chomsky (1965) argued that language acquisition mechanisms are biologically determined.
The critical period for language acquisition suggests that the ability to acquire language is at its peak early in life. As people age, this proficiency decreases. Language development begins very...
801
Synthetic Biology02:55

Synthetic Biology

5.5K
Synthetic biology is an interdisciplinary science that involves using principles from disciplines such as engineering, molecular biology, cell biology, and systems biology. It involves remodeling existing organisms from nature or constructing completely new synthetic organisms for applications such as protein or enzyme production, bioremediation, value-added macromolecule production, and the addition of desirable traits to crops, to name a few.
Golden rice
Golden rice is a genetically modified...
5.5K
Improving Translational Accuracy02:07

Improving Translational Accuracy

3.5K
3.5K
Improving Translational Accuracy02:07

Improving Translational Accuracy

14.0K
Base complementarity between the three base pairs of mRNA codon and the tRNA anticodon is not a failsafe mechanism. Inaccuracies can range from a single mismatch to no correct base pairing at all. The free energy difference between the correct and nearly correct base pairs can be as small as 3 kcal/ mol. With complementarity being the only proofreading step, the estimated error frequency would be one wrong amino acid in every 100 amino acids incorporated. However, error frequencies observed in...
14.0K
Language01:16

Language

855
Language is a unique communication system that uses words and systematic rules to organize and transmit information. Unlike other forms of communication, which may involve postures, movements, odors, or vocalizations, language relies on symbols and grammar. This makes human communication distinct from that of other species, who also communicate but do not use language in the same way humans do.
Corballis and Suddendorf (2007) and Tomasello and Rakoczy (2003) highlight the role of language in...
855

您也可能阅读

相关文章

通过共同作者、期刊和引用图与本文相关的文章。

排序
Same author

Breakthrough mucormycosis after hematopoietic stem cell transplantation: a retrospective multiyear cohort study in Eastern China.

Annals of clinical microbiology and antimicrobials·2026
Same author

Fatty Acid-Binding Protein 4 and Major Adverse Cardiovascular Events: A Dose-Response Meta-Analysis of Prospective Cohort Studies.

European journal of preventive cardiology·2026
Same author

<i>Hex</i>-MASP for Mapping the Whole-tissue Spatial Proteome and the Intra-brain Distribution of Monoclonal Antibodies.

bioRxiv : the preprint server for biology·2026
Same author

Tetrandrine, a Major Alkaloid From <i>Stephaniae Tetrandrae Radix</i>, Ameliorates Non-Alcoholic Fatty Liver Disease in Zebrafish via the PI3K/AKT/STAT3 Pathway.

Food science & nutrition·2026
Same author

Social jet lag and visual acuity decline in junior high students: a retrospective cohort study.

Scientific reports·2026
Same author

Impact of intraoperative nonsteroidal anti-inflammatory drugs on acute kidney injury after major noncardiac surgery: a propensity score-matched analysis.

Renal failure·2026

相关实验视频

Updated: Jan 7, 2026

Evidence-based Knowledge Synthesis and Hypothesis Validation: Navigating Biomedical Knowledge Bases via Explainable AI and Agentic Systems
05:47

Evidence-based Knowledge Synthesis and Hypothesis Validation: Navigating Biomedical Knowledge Bases via Explainable AI and Agentic Systems

Published on: June 13, 2025

1.2K

KerSpecGen:与精细的知识图和大型语言模型共同驾驶正式的内核规范合成.

Zi Wang1, Xiaoyu Zhu2, Hongqiang Wang2

  • 1School of Cyber Science and Technology, Beihang University, Beijing, China.

PloS one
|December 31, 2025
PubMed
概括

本研究介绍了KerSpecGen,这是一个大型语言模型 (LLM) 框架,可以自动合成复杂的微内核的正式内核规范. KerSpecGen显著减少了正式验证所需的手工工作,提高了效率.

更多相关视频

Augmenting Large Language Models via Vector Embeddings to Improve Domain-Specific Responsiveness
03:14

Augmenting Large Language Models via Vector Embeddings to Improve Domain-Specific Responsiveness

Published on: December 6, 2024

983
Constructing and Visualizing Models using Mime-based Machine-learning Framework
06:19

Constructing and Visualizing Models using Mime-based Machine-learning Framework

Published on: July 22, 2025

2.2K

相关实验视频

Last Updated: Jan 7, 2026

Evidence-based Knowledge Synthesis and Hypothesis Validation: Navigating Biomedical Knowledge Bases via Explainable AI and Agentic Systems
05:47

Evidence-based Knowledge Synthesis and Hypothesis Validation: Navigating Biomedical Knowledge Bases via Explainable AI and Agentic Systems

Published on: June 13, 2025

1.2K
Augmenting Large Language Models via Vector Embeddings to Improve Domain-Specific Responsiveness
03:14

Augmenting Large Language Models via Vector Embeddings to Improve Domain-Specific Responsiveness

Published on: December 6, 2024

983
Constructing and Visualizing Models using Mime-based Machine-learning Framework
06:19

Constructing and Visualizing Models using Mime-based Machine-learning Framework

Published on: July 22, 2025

2.2K

科学领域:

  • 计算机科学 计算机科学
  • 软件工程 软件工程 软件工程
  • 正式方法 正式方法

背景情况:

  • 正式验证对于软件的正确性至关重要,但对于seL4等复杂的微内核来说,由于劳动密集的规范写作,这是一个挑战.
  • 现有的方法依赖于专业知识和有限,阻碍了正式方法在微核开发中的实际应用.

研究的目的:

  • 提出 KerSpecGen,一个使用大型语言模型 (LLM) 来自动化正式内核规范的合成的新框架.
  • 解决复杂微核的手动规范编写的局限性,从而提高正式验证的实用性.

主要方法:

  • 开发了KerSpecGen,这是一个基于LLM的框架,集成知识图来将要求描述与规范属性连接起来.
  • 构建了一个精细的知识图,其中包括除重复,属性判断和来源注释以确保准确性.
  • 创建了一个自定义数据集,用于微调模型以将规范属性转换为代码,并设计了面向LLM的模板来生成完整的规范.

主要成果:

  • 在 KerSpecProperty 基准指标上,KerSpecGen 在 Few-shot 方法中表现优越,在 BLEU-4 中平均高出 7.06 个百分点.
  • 该框架在使用Llama-3.1-405B模型时,在30个seL4功能模块中的23个中产生了更好的规范质量.
  • 生成的规范是高质量的参考文献,大大减少了手工规范写作的负担.

结论:

  • KerSpecGen代表了复杂微内核的正式规范生成自动化的重大进步.
  • 该框架有效地利用LLM和知识图表将要求描述和形式属性联系起来.
  • 虽然直接执行可能需要轻微的调整,但KerSpecGen大大降低了在微核系统中进行正式验证的进入障碍.