主要证据
- MaLARea: a Metasystem for Automated Reasoning in Large TheoriesS1 · 主要研究来源 · 论文 · 2007-06-27
MaLARea 在大型理论上建立机器学习与定理证明反馈循环
系统反复从已有证明训练相关性模型，在筛选前提上调用自动证明器，并把新找到的证明纳入后续学习轮次。
发生了什么？
Josef Urban 的 MaLARea 论文于 2007 年 6 月 27 日随 ESARLT 2007 proceedings 发布，描述一个结合机器学习、自动定理证明与模型查找的大型理论元系统。
为什么重要？
“演绎—学习”反馈循环后来成为自我改进式定理证明系统的核心范式，并预示现代形式数学中的 search-and-learning agents。
重要性说明：MaLARea 将大型理论推理明确组织为迭代循环：机器学习选择有用知识，ATP 尝试证明，成功结果再反馈给学习器用于后续问题。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 自主主导
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 学习式前提选择模型与自动证明器在自主循环中协作，并从此前证明结果持续改进。
- 人类贡献
- Josef Urban 设计元系统、学习/推理循环、数据接口与实验。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-15
技术细节
- 系统
- malarea
- 机构
- charles-university
- 数学问题
- large-theory-theorem-proving
- 方法
- machine-learning, premise-selection, automated-theorem-proving, model-finding, feedback-loop
全部来源与工件
- MaLARea: a Metasystem for Automated Reasoning in Large TheoriesS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
验证历史
- 2007-06-27 · 论文已发布 · E2 · 研究记录
CEUR proceedings 确认 MaLARea 系统及其学习/推理架构。
更正
当前没有记录的更正。