检索结果-内蒙古大学图书馆

Training and inference Time Efficiency Assessment Framework for machine learning algorithms: A case study for hyperspectral image classification

引用

International Journal of Applied Earth Observation and Geoinformation 2025年 141卷

作者： Xiaorou Zheng Jianxin Jia Shoubin Dong Yawei Wang Runuo Lu Yuwei Chen Yueming Wang Guangdong Provincial Key Laboratory of Multimodal Big Data Intelligent Analysis School of Computer Science and Engineering South China University of Technology Guangzhou 510006 China Department of Photogrammetry and Remote Sensing Finnish Geospatial Research Institute FI-02150 Espoo Finland Guangzhou Institute of Geography Guangdong Academy of Sciences Guangzhou 311100 Guangdong China Hangzhou Institute for Advanced Study University of Chinese Academy of Sciences Hangzhou 310024 Zhejiang China The Advanced Laser Technology Laboratory of Anhui Province Hefei 230037 China Key Laboratory of Space Active Opto-Electronics Technology Shanghai Institute of Technical Physics Chinese Academy of Sciences Shanghai 200083 China

The increasing complexity and scale of remote sensing datasets, coupled with the challenges of accurately estimating algorithmic time efficiency, often lead to significant resource waste or even failure when using machine learning algorithms in urgent or resource-constrained scenarios. Accurate time efficiency estimation is critical for deploying effective algorithms, yet it remains challenging due to the many factors influencing computational performance. Traditional methods of evaluating time efficiency often neglect the effects of core model parameters and complex data scales in spectral and temporal dimensions. In addition, inference time, an essential factor in real-world applications, is often overlooked. To address these limitations, we propose the Time Efficiency Assessment Framework (TEAF), a novel method for evaluating the time efficiency of machine learning algorithms. Through mathematical reasoning, TEAF models the training and inference time as functions ( ψ ) of complex data scales and core model parameters. The strong linear correlation between ψ and the actual runtime allows TEAF to accurately predict the time and cost of machine learning tasks with a low computational overhead before algorithm execution. To validate this framework, we derived TEAF formulations for five classical machine learning algorithms and tested them on state-of-the-art hyperspectral image datasets and Sentinel-2 multispectral datasets. The results demonstrated that TEAF could accurately predict both training and inference time for various algorithms, with a strong linear correlation between ψ and actual runtime ( R 2 > 0 . 942 ). This study offers a practical solution to the challenges posed by the increasing volume and complexity of data in remote sensing image processing. The code is available at https://***/SCUT-CCNL/TEAF .

关键词： Time efficiency Hyperspectral image Inference time algorithm derivation Time prediction Complexity data scale

来源：评论

学校读者我要写书评

暂无评论

Relationships between suspended mineral concentrations and red-waveband reflectances in moderately turbid shelf seas

引用

REMOTE SENSING OF ENVIRONMENT 2011年第12期115卷 3719-3730页

作者： Neil, Claire Cunningham, Alex McKee, David Univ Strathclyde Dept Phys Glasgow G4 0NG Lanark Scotland

This paper considers the uncertainties that arise in estimating the concentration of suspended minerals by optical remote sensing in waters which contain unknown concentrations of other optically significant constituents. Relationships between suspended mineral concentrations and remote sensing reflectance were calculated by radiative transfer modelling using representative specific inherent optical properties (SIOPs) for phytoplankton (CHL), suspended mineral particles of terrigenous origin (MSSter) and coloured dissolved organic matter (CDOM) that were derived from measurements at 173 stations in UK shelf seas. When only suspended minerals were present, remote sensing reflectance (R-rs) was related to MSSter, by a family of saturation curves whose shape depended strongly on wavelength. However the addition of CHL and CDOM made this relationship considerably more complex. Polynomial expressions were therefore derived for the maximum and minimum values of MMSter consistent with a given R(rs)667 in the presence of independently varying concentrations of CHL and CDOM. For CHL ranging from 0 to 10 mg m(-3) and CDOM from 0 to 1 m(-1), for example, an R(rs)667 observation 0.01 sr(-1) could corresponded to MSSter values between 7 and 12 g m(-3). The presence of biogenic minerals in the form of diatom frustules. MSSdia, had little influence on the accuracy of MSSter retrieval. The degree of variability in the relationship between MSSter and Rrs667 predicted by the model was confirmed by measurements of radiometric profiles and mineral concentrations at 110 Irish Sea stations. Uncertainties in the remote sensing of MSSter in coastal waters are more appropriately indicated by upper and lower limits set according to the likely ranges of other optically significant constituents than by percentage errors. Moreover, the influence of these constituents should be eliminated before variations in the relationship between MSSter and Rrs are attributed to qualitative changes in minera

关键词： Shelf seas Suspended mineral particles algorithm derivation

来源：评论

学校读者我要写书评

暂无评论

Provably correct derivation of algorithms using FermaT

引用

FORMAL ASPECTS OF COMPUTING 2014年第5期26卷 993-1031页

作者： Ward, Martin Zedan, Hussein De Montfort Univ Software Technol Res Lab Leicester LE1 9BH Leics England

The transformational programming method of algorithm derivation starts with a formal specification of the result to be achieved, plus some informal ideas as to what techniques will be used in the implementation. The formal specification is then transformed into an implementation, by means of correctness-preserving refinement and transformation steps, guided by the informal ideas. The transformation process will typically include the following stages: (1) Formal specification (2) Elaboration of the specification, (3) Divide and conquer to handle the general case (4) Recursion introduction, (5) Recursion removal, if an iterative solution is desired, (6) Optimisation, if required. At any stage in the process, sub-specifications can be extracted and transformed separately. The main difference between this approach and the invariant based programming approach (and similar stepwise refinement methods) is that loops can be introduced and manipulated while maintaining program correctness and with no need to derive loop invariants. Another difference is that at every stage in the process we are working with a correct program: there is never any need for a separate "verification" step. These factors help to ensure that the method is capable of scaling up to the development of large and complex software systems. The method is applied to the derivation of a complex linked list algorithm and produces code which is over twice as fast as the code written by Donald Knuth to solve the same problem.

关键词： Transformational programming Formal methods Software development algorithm derivation FermaT WSL

来源：评论

学校读者我要写书评

暂无评论

A new efficient retiming algorithm derived by formal manipulation

引用

ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS 2008年第1期13卷 7-1-7-19页

作者： Zhou, Hai Northwestern Univ Dept Elect Engn & Comp Sci Evanston IL 60208 USA

A new efficient algorithm is derived for the minimal period retiming by formal manipulation. Contrary to all previous algorithms, which used fixed period feasibility checking to binary-search a candidate range, the derived algorithm checks the optimality of a feasible period directly. It is much simpler and more efficient than previous algorithms. Experimental results showed that it is even faster than ASTRA, an efficient heuristic algorithm. Since the derived algorithm is incremental by nature, it also opens the opportunity to be combined with other optimization techniques.

关键词： algorithm design clockperiod minimization retiming algorithm derivation

来源：评论

学校读者我要写书评

暂无评论

Deriving a Slicing algorithm via FermaT Transformations

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 2011年第1期37卷 24-47页

作者： Ward, Martin P. Zedan, Hussein De Montfort Univ Durham DH1 2TZ England De Montfort Univ Software Technol Res Lab Leicester LE1 9BH Leics England

In this paper, we present a case study in deriving an algorithm from a formal specification via FermaT transformations. The general method (which is presented in a separate paper) is extended to a method for deriving an implementation of a program transformation from a specification of the program transformation. We use program slicing as an example transformation since this is of interest outside the program transformation community. We develop a formal specification for program slicing in the form of a WSL specification statement which is refined into a simple slicing algorithm by applying a sequence of general purpose program transformations and refinements. Finally, we show how the same methods can be used to derive an algorithm for semantic slicing. The main novel contributions of this paper are: 1) developing a formal specification for slicing, 2) expressing the definition of slicing in terms of a WSL specification statement, and 3) by applying correctness preserving transformations to the specification, we can derive a simple slicing algorithm.

关键词： Program slicing program transformations formal methods algorithm derivation

来源：评论

学校读者我要写书评

暂无评论

Experience with correctness-by-construction

引用

SCIENCE OF COMPUTER PROGRAMMING 2015年第Part1期97卷 55-58页

作者： Watson, B. W. Kourie, D. G. Cleophas, L. Univ Stellenbosch Fastar Res Grp ZA-7600 Stellenbosch South Africa Univ Pretoria Fastar Res Grp ZA-0002 Pretoria South Africa

We discuss the correctness-by-construction approach to software development, and our experience with this approach in various small to large scale algorithmic settings. We argue that although it is not realistic to apply the approach in developing every line of code of a software system, its pragmatic application to the algorithmically complex parts of such a system is worthwhile. (C) 2013 Elsevier B.V. All rights reserved.

关键词： Correctness-by-construction Refinement calculus algorithm derivation

来源：评论

学校读者我要写书评

暂无评论

On Euclid's algorithm and elementary number theory

引用

SCIENCE OF COMPUTER PROGRAMMING 2011年第3期76卷 160-180页

作者： Backhouse, Roland Ferreira, Joao F. Univ Nottingham Sch Comp Sci Nottingham NG8 1BB England

algorithms can be used to prove and to discover new theorems. This paper shows how algorithmic skills in general, and the notion of invariance in particular, can be used to derive many results from Euclid's algorithm. We illustrate how to use the algorithm as a verification interface (i.e., how to verify theorems) and as a construction interface (i.e., how to investigate and derive new theorems). The theorems that we verify are well-known and most of them are included in standard number-theory books. The new results concern distributivity properties of the greatest common divisor and a new algorithm for efficiently enumerating the positive rationals in two different ways. One way is known and is due to Moshe Newman. The second is new and corresponds to a deforestation of the Stern-Brocot tree of rationals. We show that both enumerations stem from the same simple algorithm. In this way, we construct a Stern-Brocot enumeration algorithm with the same time and space complexity as Newman's algorithm. A short review of the original papers by Stern and Brocot is also included. Crown Copyright (C) 2010 Published by Elsevier B.V. All rights reserved.

关键词： Number theory Calculational method Greatest common divisor Euclid's algorithm Invariant Eisenstein array Eisenstein-Stern tree (aka Calkin-Wilf tree) Stern-Brocot tree algorithm derivation Enumeration algorithm Rational number

来源：评论

学校读者我要写书评

暂无评论

The algorithmics of solitaire-like games

引用

SCIENCE OF COMPUTER PROGRAMMING 2013年第11期78卷 2029-2046页

作者： Backhouse, Roland Chen, Wei Ferreira, Joao F. Univ Nottingham Sch Comp Sci Nottingham NG8 1BB England

One-person solitaire-like games are explored with a view to using them in teaching algorithmic problem solving. The key to understanding solutions to such games is the identification of invariant properties of polynomial arithmetic. We demonstrate this via three case studies: solitaire itself, tiling problems and a novel class of one-person games. The known classification of states of the game of (peg) solitaire into 16 equivalence classes is used to introduce the relevance of polynomial arithmetic. Then we give a novel algebraic formulation of the solution to a class of tiling problems. Finally, we introduce an infinite class of challenging one-person games, which we call "replacement-set games", inspired by earlier work by Chen and Backhouse on the relation between cyclotomic polynomials and generalisations of the seven-trees-in-one type isomorphism. We present an algorithm to solve arbitrary instances of replacement-set games and we show various ways of constructing infinite (solvable) classes of replacement-set games. (C) 2012 Elsevier B.V. All rights reserved.

关键词： Solitaire Tiling problems Cyclotomic polynomials Cyclotomic game Replacement-set game Seven-trees-in-one algorithm derivation Invariants Type isomorphism

来源：评论

学校读者我要写书评

暂无评论

Logic Training through algorithmic Problem Solving

引用

3rd International Congress on Tools for Teaching Logic (TICTTL)

作者： Ferreira, Joao F. Mendes, Alexandra Cunha, Alcino Baquero, Carlos Silva, Paulo Barbosa, L. S. Oliveira, J. N. Univ Nottingham Sch Comp Sci Nottingham NG7 2RD England Univ Minho CCTC & Dep Informat Braga Portugal

ISBN: (纸本)9783642213496;9783642213502

Although much of mathematics is algorithmic in nature, the skills needed to formulate and solve algorithmic problems do not form an integral part of mathematics education. In particular, logic, which is central to algorithm development, is rarely taught explicitly at pre-university level, under the justification that it is implicit in mathematics and therefore does not need to be taught as an independent topic. This paper argues in the opposite direction, describing a one-week workshop done at the University of Minho, in Portugal, whose goal was to introduce to high-school students calculational principles and techniques of algorithmic problem solving supported by calculational logic. The workshop resorted to recreational problems to convey the principles and to software tools, the Alloy Analyzer and Netlogo, to animate models.

关键词： equational logic calculational method problem solving algorithm derivation

来源：评论

学校读者我要写书评

暂无评论

Toward Interactive Statistical Modeling

Toward Interactive Statistical Modeling

引用

International Conference on Computational Science (ICCS)

作者： Bhat, Sooraj Agarwal, Ashish Gray, Alexander Vuduc, Richard Georgia Inst Technol Coll Comp Atlanta GA 30332 USA Yale Univ Dept Comp Sci New Haven CT USA

When solving machine learning problems, there is currently little automated support for easily experimenting with alternative statistical models or solution strategies. This is because this activity often requires expertise from several different fields (e. g., statistics, optimization, linear algebra), and the level of formalism required for automation is much higher than for a human solving problems on paper. We present a system toward addressing these issues, which we achieve by (1) formalizing a type theory for probability and optimization, and (2) providing an interactive rewrite system for applying problem reformulation theorems. Automating solution strategies this way enables not only manual experimentation but also higher-level, automated activities, such as autotuning. (C) 2010 Published by Elsevier Ltd.

关键词： machine learning algorithm derivation interactive modeling type theory

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：